:: AMI_4 semantic presentation

theorem Th1: :: AMI_4:1
for b1, b2 being Integer st b1 >= 0 & b2 >= 0 holds
b1 div b2 >= 0
proof end;

theorem Th2: :: AMI_4:2
for b1, b2 being Integer st b1 >= 0 & b2 >= 0 holds
( (abs b1) mod (abs b2) = b1 mod b2 & (abs b1) div (abs b2) = b1 div b2 )
proof end;

scheme :: AMI_4:sch 1
s1{ F1( Nat) -> Nat, F2( Nat) -> Nat, F3() -> Nat, F4() -> Nat } :
ex b1 being Nat st
( F1(b1) = F3() hcf F4() & F2(b1) = 0 )
provided
E3: 0 < F4() and
E4: F4() < F3() and
E5: F1(0) = F3() and
E6: F2(0) = F4() and
E7: for b1 being Nat st F2(b1) > 0 holds
( F1((b1 + 1)) = F2(b1) & F2((b1 + 1)) = F1(b1) mod F2(b1) )
proof end;

set c1 = dl. 0;

set c2 = dl. 1;

set c3 = dl. 2;

definition
func Euclide-Algorithm -> programmed FinPartState of SCM equals :: AMI_4:def 1
((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))));
coherence
((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))))) is programmed FinPartState of SCM
proof end;
correctness
;
end;

:: deftheorem Def1 defines Euclide-Algorithm AMI_4:def 1 :
Euclide-Algorithm = ((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))));

defpred S1[ State of SCM ] means ( a1 . (il. 0) = (dl. 2) := (dl. 1) & a1 . (il. 1) = Divide (dl. 0),(dl. 1) & a1 . (il. 2) = (dl. 0) := (dl. 2) & a1 . (il. 3) = (dl. 1) >0_goto (il. 0) & a1 halts_at il. 4 );

set c4 = (il. 0) .--> ((dl. 2) := (dl. 1));

set c5 = (il. 1) .--> (Divide (dl. 0),(dl. 1));

set c6 = (il. 2) .--> ((dl. 0) := (dl. 2));

set c7 = (il. 3) .--> ((dl. 1) >0_goto (il. 0));

set c8 = (il. 4) .--> (halt SCM );

set c9 = ((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ));

set c10 = ((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )));

set c11 = ((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))));

set c12 = ((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))));

theorem Th3: :: AMI_4:3
canceled;

theorem Th4: :: AMI_4:4
dom Euclide-Algorithm = {(il. 0),(il. 1),(il. 2),(il. 3),(il. 4)}
proof end;

Lemma4: for b1 being State of SCM st Euclide-Algorithm c= b1 holds
S1[b1]
proof end;

theorem Th5: :: AMI_4:5
for b1 being State of SCM st Euclide-Algorithm c= b1 holds
for b2 being Nat st IC ((Computation b1) . b2) = il. 0 holds
( IC ((Computation b1) . (b2 + 1)) = il. 1 & ((Computation b1) . (b2 + 1)) . (dl. 0) = ((Computation b1) . b2) . (dl. 0) & ((Computation b1) . (b2 + 1)) . (dl. 1) = ((Computation b1) . b2) . (dl. 1) & ((Computation b1) . (b2 + 1)) . (dl. 2) = ((Computation b1) . b2) . (dl. 1) )
proof end;

theorem Th6: :: AMI_4:6
for b1 being State of SCM st Euclide-Algorithm c= b1 holds
for b2 being Nat st IC ((Computation b1) . b2) = il. 1 holds
( IC ((Computation b1) . (b2 + 1)) = il. 2 & ((Computation b1) . (b2 + 1)) . (dl. 0) = (((Computation b1) . b2) . (dl. 0)) div (((Computation b1) . b2) . (dl. 1)) & ((Computation b1) . (b2 + 1)) . (dl. 1) = (((Computation b1) . b2) . (dl. 0)) mod (((Computation b1) . b2) . (dl. 1)) & ((Computation b1) . (b2 + 1)) . (dl. 2) = ((Computation b1) . b2) . (dl. 2) )
proof end;

theorem Th7: :: AMI_4:7
for b1 being State of SCM st Euclide-Algorithm c= b1 holds
for b2 being Nat st IC ((Computation b1) . b2) = il. 2 holds
( IC ((Computation b1) . (b2 + 1)) = il. 3 & ((Computation b1) . (b2 + 1)) . (dl. 0) = ((Computation b1) . b2) . (dl. 2) & ((Computation b1) . (b2 + 1)) . (dl. 1) = ((Computation b1) . b2) . (dl. 1) & ((Computation b1) . (b2 + 1)) . (dl. 2) = ((Computation b1) . b2) . (dl. 2) )
proof end;

theorem Th8: :: AMI_4:8
for b1 being State of SCM st Euclide-Algorithm c= b1 holds
for b2 being Nat st IC ((Computation b1) . b2) = il. 3 holds
( ( ((Computation b1) . b2) . (dl. 1) > 0 implies IC ((Computation b1) . (b2 + 1)) = il. 0 ) & ( ((Computation b1) . b2) . (dl. 1) <= 0 implies IC ((Computation b1) . (b2 + 1)) = il. 4 ) & ((Computation b1) . (b2 + 1)) . (dl. 0) = ((Computation b1) . b2) . (dl. 0) & ((Computation b1) . (b2 + 1)) . (dl. 1) = ((Computation b1) . b2) . (dl. 1) )
proof end;

theorem Th9: :: AMI_4:9
for b1 being State of SCM st Euclide-Algorithm c= b1 holds
for b2, b3 being Nat st IC ((Computation b1) . b2) = il. 4 holds
(Computation b1) . (b2 + b3) = (Computation b1) . b2
proof end;

Lemma10: for b1 being Nat
for b2 being State of SCM st b2 starts_at il. 0 & Euclide-Algorithm c= b2 & b2 . (dl. 0) > 0 & b2 . (dl. 1) > 0 holds
( ((Computation b2) . (4 * b1)) . (dl. 0) > 0 & ( ( ((Computation b2) . (4 * b1)) . (dl. 1) > 0 & IC ((Computation b2) . (4 * b1)) = il. 0 ) or ( ((Computation b2) . (4 * b1)) . (dl. 1) = 0 & IC ((Computation b2) . (4 * b1)) = il. 4 ) ) )
proof end;

Lemma11: for b1 being Nat
for b2 being State of SCM st b2 starts_at il. 0 & Euclide-Algorithm c= b2 & b2 . (dl. 0) > 0 & b2 . (dl. 1) > 0 & ((Computation b2) . (4 * b1)) . (dl. 1) > 0 holds
( ((Computation b2) . (4 * (b1 + 1))) . (dl. 0) = ((Computation b2) . (4 * b1)) . (dl. 1) & ((Computation b2) . (4 * (b1 + 1))) . (dl. 1) = (((Computation b2) . (4 * b1)) . (dl. 0)) mod (((Computation b2) . (4 * b1)) . (dl. 1)) )
proof end;

Lemma12: for b1 being State of SCM st b1 starts_at il. 0 & Euclide-Algorithm c= b1 holds
for b2, b3 being Integer st b1 . (dl. 0) = b2 & b1 . (dl. 1) = b3 & b2 > b3 & b3 > 0 holds
( (Result b1) . (dl. 0) = b2 gcd b3 & ex b4 being Nat st b1 halts_at IC ((Computation b1) . b4) )
proof end;

theorem Th10: :: AMI_4:10
for b1 being State of SCM st b1 starts_at il. 0 & Euclide-Algorithm c= b1 holds
for b2, b3 being Integer st b1 . (dl. 0) = b2 & b1 . (dl. 1) = b3 & b2 > 0 & b3 > 0 holds
(Result b1) . (dl. 0) = b2 gcd b3
proof end;

definition
func Euclide-Function -> PartFunc of FinPartSt SCM , FinPartSt SCM means :Def2: :: AMI_4:def 2
for b1, b2 being FinPartState of SCM holds
( [b1,b2] in a1 iff ex b3, b4 being Integer st
( b3 > 0 & b4 > 0 & b1 = (dl. 0),(dl. 1) --> b3,b4 & b2 = (dl. 0) .--> (b3 gcd b4) ) );
existence
ex b1 being PartFunc of FinPartSt SCM , FinPartSt SCM st
for b2, b3 being FinPartState of SCM holds
( [b2,b3] in b1 iff ex b4, b5 being Integer st
( b4 > 0 & b5 > 0 & b2 = (dl. 0),(dl. 1) --> b4,b5 & b3 = (dl. 0) .--> (b4 gcd b5) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of FinPartSt SCM , FinPartSt SCM st ( for b3, b4 being FinPartState of SCM holds
( [b3,b4] in b1 iff ex b5, b6 being Integer st
( b5 > 0 & b6 > 0 & b3 = (dl. 0),(dl. 1) --> b5,b6 & b4 = (dl. 0) .--> (b5 gcd b6) ) ) ) & ( for b3, b4 being FinPartState of SCM holds
( [b3,b4] in b2 iff ex b5, b6 being Integer st
( b5 > 0 & b6 > 0 & b3 = (dl. 0),(dl. 1) --> b5,b6 & b4 = (dl. 0) .--> (b5 gcd b6) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Euclide-Function AMI_4:def 2 :
for b1 being PartFunc of FinPartSt SCM , FinPartSt SCM holds
( b1 = Euclide-Function iff for b2, b3 being FinPartState of SCM holds
( [b2,b3] in b1 iff ex b4, b5 being Integer st
( b4 > 0 & b5 > 0 & b2 = (dl. 0),(dl. 1) --> b4,b5 & b3 = (dl. 0) .--> (b4 gcd b5) ) ) );

theorem Th11: :: AMI_4:11
for b1 being set holds
( b1 in dom Euclide-Function iff ex b2, b3 being Integer st
( b2 > 0 & b3 > 0 & b1 = (dl. 0),(dl. 1) --> b2,b3 ) )
proof end;

theorem Th12: :: AMI_4:12
for b1, b2 being Integer st b1 > 0 & b2 > 0 holds
Euclide-Function . ((dl. 0),(dl. 1) --> b1,b2) = (dl. 0) .--> (b1 gcd b2)
proof end;

theorem Th13: :: AMI_4:13
(Start-At (il. 0)) +* Euclide-Algorithm computes Euclide-Function
proof end;