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
SCMPDS 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 SCMPDS
;
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 . 0 = GBP := 0 &
GCD-Algorithm . 1
= SBP := 7 &
GCD-Algorithm . 2
= saveIC SBP ,
RetIC &
GCD-Algorithm . 3
= goto 2 &
GCD-Algorithm . 4
= halt SCMPDS &
GCD-Algorithm . 5
= SBP ,3
<=0_goto 9 &
GCD-Algorithm . 6
= SBP ,6
:= SBP ,3 &
GCD-Algorithm . 7
= Divide SBP ,2,
SBP ,3 &
GCD-Algorithm . 8
= SBP ,7
:= SBP ,3 &
GCD-Algorithm . 9
= SBP ,
(4 + RetSP ) := GBP ,1 &
GCD-Algorithm . 10
= AddTo GBP ,1,4 &
GCD-Algorithm . 11
= saveIC SBP ,
RetIC &
GCD-Algorithm . 12
= goto (- 7) &
GCD-Algorithm . 13
= SBP ,2
:= SBP ,6 &
GCD-Algorithm . 14
= return SBP )
Lm1:
for s being State of SCMPDS st GCD-Algorithm c= s holds
( s . 0 = GBP := 0 & s . 1 = SBP := 7 & s . 2 = saveIC SBP ,RetIC & s . 3 = goto 2 & s . 4 = halt SCMPDS & s . 5 = SBP ,3 <=0_goto 9 & s . 6 = SBP ,6 := SBP ,3 & s . 7 = Divide SBP ,2,SBP ,3 & s . 8 = SBP ,7 := SBP ,3 & s . 9 = SBP ,(4 + RetSP ) := GBP ,1 & s . 10 = AddTo GBP ,1,4 & s . 11 = saveIC SBP ,RetIC & s . 12 = goto (- 7) & s . 13 = SBP ,2 := SBP ,6 & s . 14 = return SBP )
theorem Th15:
for
s being
State of
SCMPDS st
Initialized GCD-Algorithm c= s holds
(
IC (Comput (ProgramPart s),s,4) = 5 &
(Comput (ProgramPart s),s,4) . GBP = 0 &
(Comput (ProgramPart s),s,4) . SBP = 7 &
(Comput (ProgramPart s),s,4) . (intpos (7 + RetIC )) = 2 &
(Comput (ProgramPart s),s,4) . (intpos 9) = s . (intpos 9) &
(Comput (ProgramPart s),s,4) . (intpos 10) = s . (intpos 10) )
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 SCMPDS st GCD-Algorithm c= s & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc (s . SBP ),3) > 0 holds
( IC (Comput (ProgramPart s),s,7) = 5 + 7 & Comput (ProgramPart s),s,8 = Exec (goto (- 7)),(Comput (ProgramPart s),s,7) & (Comput (ProgramPart s),s,7) . SBP = n + 4 & (Comput (ProgramPart s),s,7) . GBP = 0 & (Comput (ProgramPart s),s,7) . (intpos (n + 7)) = (s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)) & (Comput (ProgramPart s),s,7) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) & (Comput (ProgramPart s),s,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s),s,7) . (intpos (n + 5)) = 11 )
Lm5:
for n, m being Element of NAT
for s being State of SCMPDS st GCD-Algorithm c= s & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc (s . SBP ),3) > 0 & 1 < m & m <= n + 1 holds
(Comput (ProgramPart s),s,7) . (intpos m) = s . (intpos m)
theorem Th16:
for
s being
State of
SCMPDS st
GCD-Algorithm c= s &
IC s = 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 (ProgramPart (Comput (ProgramPart s),s,n)),
(Comput (ProgramPart s),s,n) = return SBP &
s . SBP = (Comput (ProgramPart s),s,n) . SBP &
(Comput (ProgramPart s),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) = (Comput (ProgramPart s),s,n) . (intpos j) ) )
theorem Th17:
for
s being
State of
SCMPDS st
GCD-Algorithm c= s &
IC s = 5 &
s . SBP > 0 &
s . GBP = 0 &
s . (DataLoc (s . SBP ),3) >= 0 &
s . (DataLoc (s . SBP ),2) >= 0 holds
ex
n being
Element of
NAT st
(
CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),
(Comput (ProgramPart s),s,n) = return SBP &
s . SBP = (Comput (ProgramPart s),s,n) . SBP &
(Comput (ProgramPart s),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) = (Comput (ProgramPart s),s,n) . (intpos j) ) )
begin
theorem
Lm6:
for n being Element of NAT
for s1, s2 being State of SCMPDS st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = 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 (Comput (ProgramPart s1),s1,7) = 5 + 7 & Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) & (Comput (ProgramPart s1),s1,7) . SBP = n + 4 & (Comput (ProgramPart s1),s1,7) . GBP = 0 & (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 )
Lm7:
for n being Element of NAT
for s1, s2 being State of SCMPDS st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = 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 (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a )
Lm8:
for s1, s2 being State of SCMPDS st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = 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 (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) )
Lm9:
for s1, s2 being State of SCMPDS
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 (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a )
begin
theorem