annex_1

(Annex №1 of Pham language 0.9

1/ PROOF OF PHAM UNDETERMINISTIC SELECTION THEOREM

PROOF OF FORMULA №0 ( SIMPLE CASE )

Describe initial condition : Given element aa as (a1 .. ak-1 (ak or ak+1) ak+2 .. an) .

Cite the equation : (((a1 .. ak-1 (ak or ak+1) ak+2 .. an) = ((((ak or ak+1) -> ak) and (a1 .. ak-1 ak ak+2 .. an)) or (((ak or ak+1) -> ak+1) and (a1 .. ak-1 ak+1 ak+2 .. an)))))

Declare intention : Need prove (left hand side) and (right hand side) of equation be equal .

Use (Pham axiom) to transform :

Step 1 : ((left hand side) = (a1 .. ak-1 (ak or ak+1) ak+2 .. an))

Step 2 : Apply (TRUE with (AND)) Pham generalized Boolean axiom .

((left hand side) = (TRUE and (a1 .. ak-1 (ak or ak+1) ak+2 .. an)))

Step 3 : Apply (Pham Completeness of Selection Axiom ) . Substitute TRUE by (((ak or ak+1) -> ak) or ((ak or ak+1) -> ak+1)) . 

 ((left hand side) = (((((ak or ak+1) -> ak) or ((ak or ak+1) -> ak+1))) and (a1 .. ak-1 (ak or ak+1) ak+2 .. an)))

Step 4 : Apply (Distributive property of Pham generalized Boolean axiom) to distribute AND over OR .

 ((left hand side) = (((((ak or ak+1) -> ak) and (a1 .. ak-1 (ak or ak+1) ak+2 .. an)) or (((ak or ak+1) -> ak+1) and (a1 .. ak-1 (ak or ak+1) ak+2 .. an)))))

Step 5 : Apply (Pham Concrete Selection Axiom) . Inside first branch , choice (ak or ak+1) become strict ak . Inside second branch , choice (ak or ak+1) become strict ak+1 . 

 ((left hand side) = (((((ak or ak+1) -> ak) and (a1 .. ak-1 ak ak+2 .. an)) or (((ak or ak+1) -> ak+1) and (a1 .. ak-1 ak+1 ak+2 .. an)))))

Step 6 : Final result confirm ((left hand side) = (right hand side)) . Proof complete .

________________________________________

PROOF OF FORMULA №1 (SYNCHRONIZED VARIABLE CASE)

Describe initial condition :

Given (f x) is pham language element value function of variable (pham language element x) .

Given (g x) is pham language element value function of variable (pham language element x) .

Cite the equation : (((f (g (a or b))) = ((((a or b) -> a) and (f (g a))) or (((a or b) -> b) and (f (g b))))))

Declare intention : Need prove (left hand side) and (right hand side) of equation be equal .

Use (Pham axiom) to transform :

Step 1 : ((left hand side) = (f (g (a or b))))

Step 2 : Apply (TRUE with (AND ) ) Pham generalized Boolean axiom .

((left hand side) = (TRUE and (f (g (a or b)))))

Step 3 : Apply (Pham Completeness of Selection Axiom ) .

Substitute TRUE by (((a or b) -> a) or ((a or b) -> b)) . 

((left hand side) = (((((a or b) -> a) or ((a or b) -> b))) and (f (g (a or b)))))

Step 4 : Apply ( Distributive property of Pham generalized Boolean axiom ) .

((left hand side) = (((((a or b) -> a) and (f (g (a or b)))) or (((a or b) -> b) and (f (g (a or b)))))))

Step 5 : Apply (Pham Concrete Selection Axiom ) .

Substitute target choice by concrete element in each respective branch .

((left hand side) = (((((a or b) -> a) and (f (g a))) or (((a or b) -> b) and (f (g b))))))

Step 6 : Final result confirm ((left hand side) = (right hand side)) . Proof complete .

________________________________________

PROOF OF FORMULA №2 (SYNCHRONIZED VARIABLE CASE INNER EXPANSION )

Given (f x) is pham language element value function of variable (pham language element x) .

Given (g x) is pham language element value function of variable (pham language element x) .

Describe initial condition : Given element (f (g (a or b))) .

Cite the equation : (((f (g (a or b))) = (f (((((a or b) -> a) and (g a)) or (((a or b) -> b) and (g b))))) ))

Declare intention : Need prove (left hand side) and (right hand side) of equation be equal .

Use (Pham axiom) to transform :

Step 1 : Target inner element (g (a or b)) inside (left hand side) .

Step 2 : Apply (TRUE with (AND) ) Pham generalized Boolean axiom on inner element .

 (((g (a or b)) = (TRUE and (g (a or b)))))

Step 3 : Apply (Pham Completeness of Selection Axiom ) .

 ((g (a or b)) = (((((a or b) -> a) or ((a or b) -> b))) and (g (a or b))))

Step 4 : Apply (Distributive property of Pham generalized Boolean axiom ) .

 ((g (a or b)) = (((((a or b) -> a) and (g (a or b))) or (((a or b) -> b) and (g (a or b))))))

Step 5 : Apply (Pham Concrete Selection Axiom) on target choice . ((g (a or b)) = (((((a or b) -> a) and (g a)) or (((a or b) -> b) and (g b)))))

Step 6 : Substitute expanded inner element back into f . ((left hand side) = (f (((((a or b) -> a) and (g a)) or (((a or b) -> b) and (g b))))))

Step 7 : Final result confirm ((left hand side) = (right hand side)) . Proof complete .

___________________________________________

PROOF OF FORMULA №3 (ASYNCHRONIZED VARIABLE CASE)

Describe initial condition :

Given (f x y z) is pham language element value function f of 3 variable ((pham language element x) (pham language element y) (pham language element z))

Given (g x y z) is pham language element value function g of 3 variable ((pham language element x) (pham language element y) (pham language element z))

Given element (f (g (a or b) a b) a b) .

Cite the equation :

((f (g (a or b) a b) a b) = ((((a or b) -> a) and (f (g a a b) a b)) or (((a or b) -> b) and (f (g b a b) a b))) )

Declare intention : Need to prove (left hand side) and (right hand side) of equation be equal .

Use (Pham axiom) to transform :

Step 1 : ((left hand side) = (f (g (a or b) a b) a b))

Step 2 : Apply (TRUE with (AND) ) Pham generalized Boolean axiom .

((left hand side) = (TRUE and (f (g (a or b) a b) a b)))

Step 3 : Apply (Pham Completeness of Selection Axiom ) .

 ((left hand side) = (((((a or b) -> a) or ((a or b) -> b))) and (f (g (a or b) a b) a b)))

Step 4 : Apply (Distributive property of Pham generalized Boolean axiom) .

 ((left hand side) = (((((a or b) -> a) and (f (g (a or b) a b) a b)) or (((a or b) -> b) and (f (g (a or b) a b) a b)))))

Step 5 : Apply (Pham Concrete Selection Axiom) . Fixed context a and b remain untouched . Only target choice (a or b) become concrete element .

 ((left hand side) = (((((a or b) -> a) and (f (g a a b) a b)) or (((a or b) -> b) and (f (g b a b) a b)))))

Step 6 : Final result confirm ((left hand side) = (right hand side)) . Proof complete .

_________________________________________

PROOF OF FORMULA №4 (ASYNCHRONIZED VARIABLE CASE INNER EXPANSION )

Describe initial condition :

Given (f x y z) is pham language element value function f of 3 variable ((pham language element x) (pham language element y) (pham language element z))

Given (g x y z) is pham language element value function g of 3 variable ((pham language element x) (pham language element y) (pham language element z))

Given element (f (g (a or b) a b) a b) .

Cite the equation : ((f (g (a or b) a b) a b) = (f (((((a or b) -> a) and (g a a b)) or (((a or b) -> b) and (g b a b))) a b)))

Declare intention : Need to prove (left hand side) and (right hand side) of equation be equal .

Use (Pham axiom) to transform :

Step 1 : Target inner element (g (a or b) a b) inside (left hand side) .

Step 2 : Apply (TRUE with (AND)) Pham generalized Boolean axiom on inner element .

 ((g (a or b) a b) = (TRUE and (g (a or b) a b)))

Step 3 : Apply (Pham Completeness of Selection Axiom ) .

 ((g (a or b) a b) = (((((a or b) -> a) or ((a or b) -> b))) and (g (a or b) a b)))

Step 4 : Apply (Distributive property of Pham generalized Boolean axiom) .

 ((g (a or b) a b) = (((((a or b) -> a) and (g (a or b) a b)) or (((a or b) -> b) and (g (a or b) a b)))))

Step 5 : Apply (Pham Concrete Selection Axiom) on target choice .

 ((g (a or b) a b) = (((((a or b) -> a) and (g a a b)) or (((a or b) -> b) and (g b a b)))))

Step 6 : Substitute expanded inner element back into f . Keep fixed context a and b outside g untouched .

 ((left hand side) = (f (((((a or b) -> a) and (g a a b)) or (((a or b) -> b) and (g b a b)))) a b))

Step 7 : Final result confirm ((left hand side) = (right hand side)) . Proof complete .

)

(

2. PROOF OF COMMUTATION FEATURE of (Pham undeterministic selection theorem) ( GENERAL CASE )

Describe initial condition :

Given arbitrary Pham language element value function f of 6 variable .

Initial element :

( (initial element) = (f (a or b) a b (c or d) c d) )

Cite the equation : ( (Path 1) = (Path 2) )

( Where (Path 1) be execution that apply theorem on (a or b) firstly , and (Path 2) be execution that apply theorem on (c or d) firstly ) .

Declare intention : Need prove (Path 1) and (Path 2) of equation be absolute equal by use Pham generalized Boolean axiom and Pham undeterministic selection theorem for asynchronized variable case to transform .

TRANSFORMATION OF PATH 1 :

( Expand (a or b) firstly )

Step 1.1 : ( (Path 1) = (f (a or b) a b (c or d) c d) )

Step 1.2 : Apply ( Pham undeterministic selection theorem for asynchronized variable case ) on choice (a or b) .

( (Path 1) =

(

( (((a or b) -> a) and (f a a b (c or d) c d)) )

or

( (((a or b) -> b) and (f b a b (c or d) c d)) )

)

)

Step 1.3 : Apply ( Pham undeterministic selection theorem for asynchronized variable case ) on choice (c or d) inside every branch .

( (Path 1) =

(

( (((a or b) -> a) and ( ((((c or d) -> c) and (f a a b c c d))) or ((((c or d) -> d) and (f a a b d c d))) ) ) )

or

( (((a or b) -> b) and ( ((((c or d) -> c) and (f b a b c c d))) or ((((c or d) -> d) and (f b a b d c d))) ) ) )

)

)

Step 1.4 : Apply Boolean distribution to distribute AND over OR .

( (Path 1) =

(

( (((a or b) -> a) and (((c or d) -> c) and (f a a b c c d))) )

or

( (((a or b) -> a) and (((c or d) -> d) and (f a a b d c d))) )

or

( (((a or b) -> b) and (((c or d) -> c) and (f b a b c c d))) )

or

( (((a or b) -> b) and (((c or d) -> d) and (f b a b d c d))) )

)

)

TRANSFORMATION OF PATH 2 ( Expand (c or d) firstly )

Step 2.1 : ( (Path 2) = (f (a or b) a b (c or d) c d) )

Step 2.2 : Apply ( Pham undeterministic selection theorem for asynchronized variable case ) on choice (c or d) .

( (Path 2) =

(

( (((c or d) -> c) and (f (a or b) a b c c d)) )

or

( (((c or d) -> d) and (f (a or b) a b d c d)) )

)

)

Step 2.3 : Apply ( Pham undeterministic selection theorem for asynchronized variable case ) on choice (a or b) inside every branch .

( (Path 2) =

(

( (((c or d) -> c) and ( ((((a or b) -> a) and (f a a b c c d))) or ((((a or b) -> b) and (f b a b c c d))) ) ) )

or

( (((c or d) -> d) and ( ((((a or b) -> a) and (f a a b d c d))) or ((((a or b) -> b) and (f b a b d c d))) ) ) )

)

)

Step 2.4 : Apply Boolean distribution to distribute AND over OR .

( (Path 2) =

(

( (((c or d) -> c) and (((a or b) -> a) and (f a a b c c d))) )

or

( (((c or d) -> c) and (((a or b) -> b) and (f b a b c c d))) )

or

( (((c or d) -> d) and (((a or b) -> a) and (f a a b d c d))) )

or

( (((c or d) -> d) and (((a or b) -> b) and (f b a b d c d))) )

)

)

PROOF OF EQUALITY

Step 3.1 : Compare term inside (Path 1) and (Path 2) .

Take 1 specific term from (Path 2) :

( (target branch) = ((((c or d) -> c) and (((a or b) -> a) and (f a a b c c d)))) )

Step 3.2 : Apply ( Commutation of AND ) axiom : ((a and b) = (b and a)) on this term .

( (target branch) = ((((a or b) -> a) and (((c or d) -> c) and (f a a b c c d)))) )

Step 3.3 : Apply ( Commutation of AND ) axiom on every 4 term of (Path 2) .

( (Path 2) =

(

( (((a or b) -> a) and (((c or d) -> c) and (f a a b c c d))) )

or

( (((a or b) -> b) and (((c or d) -> c) and (f b a b c c d))) )

or

( (((a or b) -> a) and (((c or d) -> d) and (f a a b d c d))) )

or

( (((a or b) -> b) and (((c or d) -> d) and (f b a b d c d))) )

)

)

Step 3.4 : Rearrange sequence of parallel branch to match (Path 1) .

( (Path 2) =

(

( (((a or b) -> a) and (((c or d) -> c) and (f a a b c c d))) )

or

( (((a or b) -> a) and (((c or d) -> d) and (f a a b d c d))) )

or

( (((a or b) -> b) and (((c or d) -> c) and (f b a b c c d))) )

or

( (((a or b) -> b) and (((c or d) -> d) and (f b a b d c d))) )

)

)

Final Conclusion : ( (Path 1) = (Path 2) )

The Commutation feature of Pham undeterministic selection theorem be absolute proven for the true general case of 6 variable .

)