:: SCMP_GCD semantic presentation

theorem Th1: :: SCMP_GCD:1
for b1, b2 being Nat st b1 > 0 holds
b2 hcf b1 = b1 hcf (b2 mod b1)
proof end;

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

theorem Th3: :: SCMP_GCD:3
for b1 being Nat
for b2 being Integer st inspos b1 = b2 holds
inspos (b1 + 2) = (2 * ((abs b2) div 2)) + 4
proof end;

definition
let c1 be Nat;
func intpos c1 -> Int_position equals :: SCMP_GCD:def 1
 dl. a1;
coherence
dl. c1 is Int_position
proof end;
end;

:: deftheorem Def1 defines intpos SCMP_GCD:def 1 :
for b1 being Nat holds intpos b1 = dl. b1;

theorem Th4: :: SCMP_GCD:4
for b1, b2 being Nat st b1 <> b2 holds
intpos b1 <> intpos b2 by AMI_3:52;

theorem Th5: :: SCMP_GCD:5
for b1, b2 being Nat holds DataLoc b1,b2 = intpos (b1 + b2)
proof end;

theorem Th6: :: SCMP_GCD:6
for b1 being State of SCMPDS
for b2, b3 being Nat st IC b1 = inspos (b2 + b3) holds
ICplusConst b1,(- b3) = inspos b2
proof end;

definition
func GBP -> Int_position equals :: SCMP_GCD:def 2
 intpos 0;
coherence
intpos 0 is Int_position ;
func SBP -> Int_position equals :: SCMP_GCD:def 3
 intpos 1;
coherence
intpos 1 is Int_position ;
end;

:: deftheorem Def2 defines GBP SCMP_GCD:def 2 :
GBP = intpos 0;

:: deftheorem Def3 defines SBP SCMP_GCD:def 3 :
SBP = intpos 1;

theorem Th7: :: SCMP_GCD:7
GBP <> SBP by Th4;

theorem Th8: :: SCMP_GCD:8
for b1 being Instruction of SCMPDS
for b2 being Program-block holds card (b2 ';' b1) = (card b2) + 1
proof end;

theorem Th9: :: SCMP_GCD:9
for b1, b2 being Instruction of SCMPDS holds card (b1 ';' b2) = 2
proof end;

theorem Th10: :: SCMP_GCD:10
for b1 being Instruction of SCMPDS
for b2 being Program-block holds
( (b2 ';' b1) . (inspos (card b2)) = b1 & inspos (card b2) in dom (b2 ';' b1) )
proof end;

theorem Th11: :: SCMP_GCD:11
for b1 being Instruction of SCMPDS
for b2, b3 being Program-block holds ((b2 ';' b1) ';' b3) . (inspos (card b2)) = b1
proof end;

definition
func GCD-Algorithm -> Program-block equals :: SCMP_GCD:def 4
((((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC SBP ,RetIC )) ';' (goto 2)) ';' (halt SCMPDS )) ';' (SBP ,3 <=0_goto 9)) ';' (SBP ,6 := SBP ,3)) ';' (Divide SBP ,2,SBP ,3)) ';' (SBP ,7 := SBP ,3)) ';' (SBP ,(4 + RetSP ) := GBP ,1)) ';' (AddTo GBP ,1,4)) ';' (saveIC SBP ,RetIC )) ';' (goto (- 7))) ';' (SBP ,2 := SBP ,6)) ';' (return SBP );
coherence
((((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC SBP ,RetIC )) ';' (goto 2)) ';' (halt SCMPDS )) ';' (SBP ,3 <=0_goto 9)) ';' (SBP ,6 := SBP ,3)) ';' (Divide SBP ,2,SBP ,3)) ';' (SBP ,7 := SBP ,3)) ';' (SBP ,(4 + RetSP ) := GBP ,1)) ';' (AddTo GBP ,1,4)) ';' (saveIC SBP ,RetIC )) ';' (goto (- 7))) ';' (SBP ,2 := SBP ,6)) ';' (return SBP ) is Program-block ;
end;

:: deftheorem Def4 defines GCD-Algorithm SCMP_GCD:def 4 :
GCD-Algorithm = ((((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC SBP ,RetIC )) ';' (goto 2)) ';' (halt SCMPDS )) ';' (SBP ,3 <=0_goto 9)) ';' (SBP ,6 := SBP ,3)) ';' (Divide SBP ,2,SBP ,3)) ';' (SBP ,7 := SBP ,3)) ';' (SBP ,(4 + RetSP ) := GBP ,1)) ';' (AddTo GBP ,1,4)) ';' (saveIC SBP ,RetIC )) ';' (goto (- 7))) ';' (SBP ,2 := SBP ,6)) ';' (return SBP );

set c1 = GBP := 0;

set c2 = SBP := 7;

set c3 = saveIC SBP ,RetIC ;

set c4 = goto 2;

set c5 = halt SCMPDS ;

set c6 = SBP ,3 <=0_goto 9;

set c7 = SBP ,6 := SBP ,3;

set c8 = Divide SBP ,2,SBP ,3;

set c9 = SBP ,7 := SBP ,3;

set c10 = SBP ,(4 + RetSP ) := GBP ,1;

set c11 = AddTo GBP ,1,4;

set c12 = saveIC SBP ,RetIC ;

set c13 = goto (- 7);

set c14 = SBP ,2 := SBP ,6;

set c15 = return SBP ;

theorem Th12: :: SCMP_GCD:12
card GCD-Algorithm = 15
proof end;

theorem Th13: :: SCMP_GCD:13
for b1 being Nat holds
( b1 < 15 iff inspos b1 in dom GCD-Algorithm ) by Th12, SCMPDS_4:1;

theorem Th14: :: SCMP_GCD:14
( GCD-Algorithm . (inspos 0) = GBP := 0 & GCD-Algorithm . (inspos 1) = SBP := 7 & GCD-Algorithm . (inspos 2) = saveIC SBP ,RetIC & GCD-Algorithm . (inspos 3) = goto 2 & GCD-Algorithm . (inspos 4) = halt SCMPDS & GCD-Algorithm . (inspos 5) = SBP ,3 <=0_goto 9 & GCD-Algorithm . (inspos 6) = SBP ,6 := SBP ,3 & GCD-Algorithm . (inspos 7) = Divide SBP ,2,SBP ,3 & GCD-Algorithm . (inspos 8) = SBP ,7 := SBP ,3 & GCD-Algorithm . (inspos 9) = SBP ,(4 + RetSP ) := GBP ,1 & GCD-Algorithm . (inspos 10) = AddTo GBP ,1,4 & GCD-Algorithm . (inspos 11) = saveIC SBP ,RetIC & GCD-Algorithm . (inspos 12) = goto (- 7) & GCD-Algorithm . (inspos 13) = SBP ,2 := SBP ,6 & GCD-Algorithm . (inspos 14) = return SBP )
proof end;

Lemma14: for b1 being State of SCMPDS st GCD-Algorithm c= b1 holds
( b1 . (inspos 0) = GBP := 0 & b1 . (inspos 1) = SBP := 7 & b1 . (inspos 2) = saveIC SBP ,RetIC & b1 . (inspos 3) = goto 2 & b1 . (inspos 4) = halt SCMPDS & b1 . (inspos 5) = SBP ,3 <=0_goto 9 & b1 . (inspos 6) = SBP ,6 := SBP ,3 & b1 . (inspos 7) = Divide SBP ,2,SBP ,3 & b1 . (inspos 8) = SBP ,7 := SBP ,3 & b1 . (inspos 9) = SBP ,(4 + RetSP ) := GBP ,1 & b1 . (inspos 10) = AddTo GBP ,1,4 & b1 . (inspos 11) = saveIC SBP ,RetIC & b1 . (inspos 12) = goto (- 7) & b1 . (inspos 13) = SBP ,2 := SBP ,6 & b1 . (inspos 14) = return SBP )
proof end;

theorem Th15: :: SCMP_GCD:15
for b1 being State of SCMPDS st Initialized GCD-Algorithm c= b1 holds
( IC ((Computation b1) . 4) = inspos 5 & ((Computation b1) . 4) . GBP = 0 & ((Computation b1) . 4) . SBP = 7 & ((Computation b1) . 4) . (intpos (7 + RetIC )) = inspos 2 & ((Computation b1) . 4) . (intpos 9) = b1 . (intpos 9) & ((Computation b1) . 4) . (intpos 10) = b1 . (intpos 10) )
proof end;

Lemma16: for b1, b2 being Nat st b1 > 0 holds
GBP <> intpos (b2 + b1)
proof end;

Lemma17: for b1, b2 being Nat st b1 > 1 holds
SBP <> intpos (b2 + b1)
proof end;

Lemma18: for b1 being Nat
for b2 being State of SCMPDS st GCD-Algorithm c= b2 & IC b2 = inspos 5 & b1 = b2 . SBP & b2 . GBP = 0 & b2 . (DataLoc (b2 . SBP ),3) > 0 holds
( IC ((Computation b2) . 7) = inspos (5 + 7) & (Computation b2) . 8 = Exec (goto (- 7)),((Computation b2) . 7) & ((Computation b2) . 7) . SBP = b1 + 4 & ((Computation b2) . 7) . GBP = 0 & ((Computation b2) . 7) . (intpos (b1 + 7)) = (b2 . (DataLoc (b2 . SBP ),2)) mod (b2 . (DataLoc (b2 . SBP ),3)) & ((Computation b2) . 7) . (intpos (b1 + 6)) = b2 . (DataLoc (b2 . SBP ),3) & ((Computation b2) . 7) . (intpos (b1 + 4)) = b1 & ((Computation b2) . 7) . (intpos (b1 + 5)) = inspos 11 )
proof end;

Lemma19: for b1, b2 being Nat
for b3 being State of SCMPDS st GCD-Algorithm c= b3 & IC b3 = inspos 5 & b1 = b3 . SBP & b3 . GBP = 0 & b3 . (DataLoc (b3 . SBP ),3) > 0 & 1 < b2 & b2 <= b1 + 1 holds
((Computation b3) . 7) . (intpos b2) = b3 . (intpos b2)
proof end;

theorem Th16: :: SCMP_GCD:16
for b1 being State of SCMPDS st GCD-Algorithm c= b1 & IC b1 = inspos 5 & b1 . SBP > 0 & b1 . GBP = 0 & b1 . (DataLoc (b1 . SBP ),3) >= 0 & b1 . (DataLoc (b1 . SBP ),2) >= b1 . (DataLoc (b1 . SBP ),3) holds
ex b2 being Nat st
( CurInstr ((Computation b1) . b2) = return SBP & b1 . SBP = ((Computation b1) . b2) . SBP & ((Computation b1) . b2) . (DataLoc (b1 . SBP ),2) = (b1 . (DataLoc (b1 . SBP ),2)) gcd (b1 . (DataLoc (b1 . SBP ),3)) & ( for b3 being Nat st 1 < b3 & b3 <= (b1 . SBP ) + 1 holds
b1 . (intpos b3) = ((Computation b1) . b2) . (intpos b3) ) )
proof end;

theorem Th17: :: SCMP_GCD:17
for b1 being State of SCMPDS st GCD-Algorithm c= b1 & IC b1 = inspos 5 & b1 . SBP > 0 & b1 . GBP = 0 & b1 . (DataLoc (b1 . SBP ),3) >= 0 & b1 . (DataLoc (b1 . SBP ),2) >= 0 holds
ex b2 being Nat st
( CurInstr ((Computation b1) . b2) = return SBP & b1 . SBP = ((Computation b1) . b2) . SBP & ((Computation b1) . b2) . (DataLoc (b1 . SBP ),2) = (b1 . (DataLoc (b1 . SBP ),2)) gcd (b1 . (DataLoc (b1 . SBP ),3)) & ( for b3 being Nat st 1 < b3 & b3 <= (b1 . SBP ) + 1 holds
b1 . (intpos b3) = ((Computation b1) . b2) . (intpos b3) ) )
proof end;

theorem Th18: :: SCMP_GCD:18
for b1 being State of SCMPDS st Initialized GCD-Algorithm c= b1 holds
for b2, b3 being Integer st b1 . (intpos 9) = b2 & b1 . (intpos 10) = b3 & b2 >= 0 & b3 >= 0 holds
(Result b1) . (intpos 9) = b2 gcd b3
proof end;

Lemma22: for b1 being Nat
for b2, b3 being State of SCMPDS st GCD-Algorithm c= b2 & GCD-Algorithm c= b3 & IC b2 = inspos 5 & b1 = b2 . SBP & b2 . GBP = 0 & b2 . (DataLoc (b2 . SBP ),3) > 0 & IC b3 = IC b2 & b3 . SBP = b2 . SBP & b3 . GBP = 0 & b3 . (DataLoc (b2 . SBP ),2) = b2 . (DataLoc (b2 . SBP ),2) & b3 . (DataLoc (b2 . SBP ),3) = b2 . (DataLoc (b2 . SBP ),3) holds
( IC ((Computation b2) . 7) = inspos (5 + 7) & (Computation b2) . 8 = Exec (goto (- 7)),((Computation b2) . 7) & ((Computation b2) . 7) . SBP = b1 + 4 & ((Computation b2) . 7) . GBP = 0 & ((Computation b2) . 7) . (intpos (b1 + 7)) = (b2 . (intpos (b1 + 2))) mod (b2 . (intpos (b1 + 3))) & ((Computation b2) . 7) . (intpos (b1 + 6)) = b2 . (intpos (b1 + 3)) & IC ((Computation b3) . 7) = inspos (5 + 7) & (Computation b3) . 8 = Exec (goto (- 7)),((Computation b3) . 7) & ((Computation b3) . 7) . SBP = b1 + 4 & ((Computation b3) . 7) . GBP = 0 & ((Computation b3) . 7) . (intpos (b1 + 7)) = (b2 . (intpos (b1 + 2))) mod (b2 . (intpos (b1 + 3))) & ((Computation b3) . 7) . (intpos (b1 + 6)) = b2 . (intpos (b1 + 3)) & ((Computation b2) . 7) . (intpos (b1 + 4)) = b1 & ((Computation b2) . 7) . (intpos (b1 + 5)) = inspos 11 & ((Computation b3) . 7) . (intpos (b1 + 4)) = b1 & ((Computation b3) . 7) . (intpos (b1 + 5)) = inspos 11 )
proof end;

Lemma23: for b1 being Nat
for b2, b3 being State of SCMPDS st GCD-Algorithm c= b2 & GCD-Algorithm c= b3 & IC b2 = inspos 5 & b1 = b2 . SBP & b2 . GBP = 0 & b2 . (DataLoc (b2 . SBP ),3) > 0 & IC b3 = IC b2 & b3 . SBP = b2 . SBP & b3 . GBP = 0 & b3 . (DataLoc (b2 . SBP ),2) = b2 . (DataLoc (b2 . SBP ),2) & b3 . (DataLoc (b2 . SBP ),3) = b2 . (DataLoc (b2 . SBP ),3) holds
for b4 being Nat
for b5 being Int_position st b4 <= 7 & b2 . b5 = b3 . b5 holds
( IC ((Computation b2) . b4) = IC ((Computation b3) . b4) & ((Computation b2) . b4) . b5 = ((Computation b3) . b4) . b5 )
proof end;

Lemma24: for b1, b2 being State of SCMPDS st GCD-Algorithm c= b1 & GCD-Algorithm c= b2 & IC b1 = inspos 5 & b1 . SBP > 0 & b1 . GBP = 0 & b1 . (DataLoc (b1 . SBP ),3) >= 0 & b1 . (DataLoc (b1 . SBP ),2) >= b1 . (DataLoc (b1 . SBP ),3) & IC b2 = IC b1 & b2 . SBP = b1 . SBP & b2 . GBP = 0 & b2 . (DataLoc (b1 . SBP ),2) = b1 . (DataLoc (b1 . SBP ),2) & b2 . (DataLoc (b1 . SBP ),3) = b1 . (DataLoc (b1 . SBP ),3) holds
ex b3 being Nat st
( CurInstr ((Computation b1) . b3) = return SBP & b1 . SBP = ((Computation b1) . b3) . SBP & CurInstr ((Computation b2) . b3) = return SBP & b2 . SBP = ((Computation b2) . b3) . SBP & ( for b4 being Nat st 1 < b4 & b4 <= (b1 . SBP ) + 1 holds
( b1 . (intpos b4) = ((Computation b1) . b3) . (intpos b4) & b2 . (intpos b4) = ((Computation b2) . b3) . (intpos b4) ) ) & ( for b4 being Nat
for b5 being Int_position st b4 <= b3 & b1 . b5 = b2 . b5 holds
( IC ((Computation b1) . b4) = IC ((Computation b2) . b4) & ((Computation b1) . b4) . b5 = ((Computation b2) . b4) . b5 ) ) )
proof end;

Lemma25: for b1, b2 being State of SCMPDS
for b3 being Int_position
for b4 being Nat st Initialized GCD-Algorithm c= b1 & Initialized GCD-Algorithm c= b2 & b1 . b3 = b2 . b3 & b4 <= 4 holds
( IC ((Computation b1) . b4) = IC ((Computation b2) . b4) & ((Computation b1) . b4) . b3 = ((Computation b2) . b4) . b3 )
proof end;

theorem Th19: :: SCMP_GCD:19
for b1 being FinPartState of SCMPDS
for b2, b3 being Integer st b3 >= 0 & b2 >= b3 & b1 = (intpos 9),(intpos 10) --> b2,b3 holds
(Initialized GCD-Algorithm ) +* b1 is autonomic
proof end;