:: SCMP_GCD semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: SCMP_GCD:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat st m > 0 holds
n hcf m = m hcf (n mod m)
proof end;

theorem Th2: :: SCMP_GCD:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Integer st i >= 0 & j > 0 holds
i gcd j = j gcd (i mod j)
proof end;

theorem Th3: :: SCMP_GCD:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for j being Integer st inspos m = j holds
inspos (m + 2) = (2 * ((abs j) div 2)) + 4
proof end;

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

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

theorem Th4: :: SCMP_GCD:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2 being Nat st n1 <> n2 holds
intpos n1 <> intpos n2 by AMI_3:52;

theorem Th5: :: SCMP_GCD:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2 being Nat holds DataLoc n1,n2 = intpos (n1 + n2)
proof end;

theorem Th6: :: SCMP_GCD:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for m1, m2 being Nat st IC s = inspos (m1 + m2) holds
ICplusConst s,(- m2) = inspos m1
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 defines GBP SCMP_GCD:def 2 :
GBP = intpos 0;

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

theorem Th7: :: SCMP_GCD:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
GBP <> SBP by Th4;

theorem Th8: :: SCMP_GCD:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCMPDS
for I being Program-block holds card (I ';' i) = (card I) + 1
proof end;

theorem Th9: :: SCMP_GCD:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Instruction of SCMPDS holds card (i ';' j) = 2
proof end;

theorem Th10: :: SCMP_GCD:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCMPDS
for I being Program-block holds
( (I ';' i) . (inspos (card I)) = i & inspos (card I) in dom (I ';' i) )
proof end;

theorem Th11: :: SCMP_GCD:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCMPDS
for I, J being Program-block holds ((I ';' i) ';' J) . (inspos (card I)) = i
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 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 ;

theorem Th12: :: SCMP_GCD:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
card GCD-Algorithm = 15
proof end;

theorem :: SCMP_GCD:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds
( n < 15 iff inspos n in dom GCD-Algorithm ) by Th12, SCMPDS_4:1;

theorem Th14: :: SCMP_GCD:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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;

Lm1: for s being State of SCMPDS 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 )
proof end;

theorem Th15: :: SCMP_GCD:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS st Initialized GCD-Algorithm c= s holds
( IC ((Computation s) . 4) = inspos 5 & ((Computation s) . 4) . GBP = 0 & ((Computation s) . 4) . SBP = 7 & ((Computation s) . 4) . (intpos (7 + RetIC )) = inspos 2 & ((Computation s) . 4) . (intpos 9) = s . (intpos 9) & ((Computation s) . 4) . (intpos 10) = s . (intpos 10) )
proof end;

Lm2: for n, m being Nat st n > 0 holds
GBP <> intpos (m + n)
proof end;

Lm3: for n, m being Nat st n > 1 holds
SBP <> intpos (m + n)
proof end;

Lm4: for n being Nat
for s being State of SCMPDS 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 )
proof end;

Lm5: for n, m being Nat
for s being State of SCMPDS 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)
proof end;

theorem Th16: :: SCMP_GCD:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS 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 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 Nat st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = ((Computation s) . n) . (intpos j) ) )
proof end;

theorem Th17: :: SCMP_GCD:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS 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) >= 0 holds
ex n being 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 Nat st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = ((Computation s) . n) . (intpos j) ) )
proof end;

theorem :: SCMP_GCD:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS st Initialized GCD-Algorithm c= s holds
for x, y being Integer st s . (intpos 9) = x & s . (intpos 10) = y & x >= 0 & y >= 0 holds
(Result s) . (intpos 9) = x gcd y
proof end;

Lm6: for n being Nat
for s1, s2 being State of SCMPDS 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 )
proof end;

Lm7: for n being Nat
for s1, s2 being State of SCMPDS 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 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 )
proof end;

Lm8: for s1, s2 being State of SCMPDS 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 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 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 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 ) ) )
proof end;

Lm9: for s1, s2 being State of SCMPDS
for a being Int_position
for k being 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 )
proof end;

theorem :: SCMP_GCD:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinPartState of SCMPDS
for x, y being Integer st y >= 0 & x >= y & p = (intpos 9),(intpos 10) --> x,y holds
(Initialized GCD-Algorithm ) +* p is autonomic
proof end;