begin
theorem
canceled;
theorem
canceled;
theorem Th3:
:: deftheorem defines intpos SCMP_GCD:def 1 :
theorem
canceled;
theorem Th5:
theorem Th6:
:: deftheorem defines GBP SCMP_GCD:def 2 :
:: deftheorem defines SBP SCMP_GCD:def 3 :
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
begin
definition
func GCD-Algorithm -> Program of
equals
((((((((((((((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 of
;
end;
:: deftheorem 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 i00 = GBP := 0 ;
set i01 = SBP := 7;
set i02 = saveIC SBP ,RetIC ;
set i03 = goto 2;
set i04 = halt SCMPDS ;
set i05 = SBP ,3 <=0_goto 9;
set i06 = SBP ,6 := SBP ,3;
set i07 = Divide SBP ,2,SBP ,3;
set i08 = SBP ,7 := SBP ,3;
set i09 = SBP ,(4 + RetSP ) := GBP ,1;
set i10 = AddTo GBP ,1,4;
set i11 = saveIC SBP ,RetIC ;
set i12 = goto (- 7);
set i13 = SBP ,2 := SBP ,6;
set i14 = return SBP ;
begin
theorem Th12:
theorem
theorem Th14:
(
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 )
Lm1:
for s being State of st GCD-Algorithm c= s holds
( s . (inspos 0 ) = GBP := 0 & s . (inspos 1) = SBP := 7 & s . (inspos 2) = saveIC SBP ,RetIC & s . (inspos 3) = goto 2 & s . (inspos 4) = halt SCMPDS & s . (inspos 5) = SBP ,3 <=0_goto 9 & s . (inspos 6) = SBP ,6 := SBP ,3 & s . (inspos 7) = Divide SBP ,2,SBP ,3 & s . (inspos 8) = SBP ,7 := SBP ,3 & s . (inspos 9) = SBP ,(4 + RetSP ) := GBP ,1 & s . (inspos 10) = AddTo GBP ,1,4 & s . (inspos 11) = saveIC SBP ,RetIC & s . (inspos 12) = goto (- 7) & s . (inspos 13) = SBP ,2 := SBP ,6 & s . (inspos 14) = return SBP )
theorem Th15:
Lm2:
for n, m being Element of NAT st n > 0 holds
GBP <> intpos (m + n)
Lm3:
for n, m being Element of NAT st n > 1 holds
SBP <> intpos (m + n)
Lm4:
for n being Element of NAT
for s being State of st GCD-Algorithm c= s & IC s = inspos 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc (s . SBP ),3) > 0 holds
( IC (Computation s,7) = inspos (5 + 7) & Computation s,8 = Exec (goto (- 7)),(Computation s,7) & (Computation s,7) . SBP = n + 4 & (Computation s,7) . GBP = 0 & (Computation s,7) . (intpos (n + 7)) = (s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)) & (Computation s,7) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) & (Computation s,7) . (intpos (n + 4)) = n & (Computation s,7) . (intpos (n + 5)) = inspos 11 )
Lm5:
for n, m being Element of NAT
for s being State of st GCD-Algorithm c= s & IC s = inspos 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc (s . SBP ),3) > 0 & 1 < m & m <= n + 1 holds
(Computation s,7) . (intpos m) = s . (intpos m)
theorem Th16:
for
s being
State of st
GCD-Algorithm c= s &
IC s = inspos 5 &
s . SBP > 0 &
s . GBP = 0 &
s . (DataLoc (s . SBP ),3) >= 0 &
s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) holds
ex
n being
Element of
NAT st
(
CurInstr (Computation s,n) = return SBP &
s . SBP = (Computation s,n) . SBP &
(Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for
j being
Element of
NAT st 1
< j &
j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )
theorem Th17:
begin
theorem
Lm6:
for n being Element of NAT
for s1, s2 being State of st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = inspos 5 & n = s1 . SBP & s1 . GBP = 0 & s1 . (DataLoc (s1 . SBP ),3) > 0 & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) holds
( IC (Computation s1,7) = inspos (5 + 7) & Computation s1,8 = Exec (goto (- 7)),(Computation s1,7) & (Computation s1,7) . SBP = n + 4 & (Computation s1,7) . GBP = 0 & (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 )
Lm7:
for n being Element of NAT
for s1, s2 being State of st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = inspos 5 & n = s1 . SBP & s1 . GBP = 0 & s1 . (DataLoc (s1 . SBP ),3) > 0 & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) holds
for k being Element of NAT
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )
Lm8:
for s1, s2 being State of st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = inspos 5 & s1 . SBP > 0 & s1 . GBP = 0 & s1 . (DataLoc (s1 . SBP ),3) >= 0 & s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) holds
ex n being Element of NAT st
( CurInstr (Computation s1,n) = return SBP & s1 . SBP = (Computation s1,n) . SBP & CurInstr (Computation s2,n) = return SBP & s2 . SBP = (Computation s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Computation s1,n) . (intpos j) & s2 . (intpos j) = (Computation s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) ) )
Lm9:
for s1, s2 being State of
for a being Int_position
for k being Element of NAT st Initialized GCD-Algorithm c= s1 & Initialized GCD-Algorithm c= s2 & s1 . a = s2 . a & k <= 4 holds
( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )
begin
theorem