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

theorem Th1: :: SCPINVAR:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m, l being Nat st n divides m & n divides l holds
n divides m - l
proof end;

theorem Th2: :: SCPINVAR:2  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 holds
( m divides n iff m divides n )
proof end;

theorem Th3: :: SCPINVAR:3  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 holds m hcf n = m hcf (abs (n - m))
proof end;

theorem Th4: :: SCPINVAR:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Integer st a >= 0 & b >= 0 holds
a gcd b = a gcd (b - a)
proof end;

theorem Th5: :: SCPINVAR:5  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
for I being Program-block holds
( ((i ';' j) ';' I) . (inspos 0) = i & ((i ';' j) ';' I) . (inspos 1) = j )
proof end;

theorem Th6: :: SCPINVAR:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Int_position ex f being Function of product the Object-Kind of SCMPDS , NAT st
for s being State of SCMPDS holds
( ( s . a = s . b implies f . s = 0 ) & ( s . a <> s . b implies f . s = max (abs (s . a)),(abs (s . b)) ) )
proof end;

theorem Th7: :: SCPINVAR:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position ex f being Function of product the Object-Kind of SCMPDS , NAT st
for s being State of SCMPDS holds
( ( s . a >= 0 implies f . s = 0 ) & ( s . a < 0 implies f . s = - (s . a) ) )
proof end;

set A = the Instruction-Locations of SCMPDS ;

set D = SCM-Data-Loc ;

scheme :: SCPINVAR:sch 1
WhileLEnd{ F1( State of SCMPDS ) -> Nat, F2() -> State of SCMPDS , F3() -> shiftable No-StopCode Program-block, F4() -> Int_position , F5() -> Integer, P1[ set ] } :
( F1((Dstate (IExec (while<0 F4(),F5(),F3()),F2()))) = 0 & P1[ Dstate (IExec (while<0 F4(),F5(),F3()),F2())] )
provided
A1: card F3() > 0 and
A2: for t being State of SCMPDS st P1[ Dstate t] holds
( F1((Dstate t)) = 0 iff t . (DataLoc (F2() . F4()),F5()) >= 0 ) and
A3: P1[ Dstate F2()] and
A4: for t being State of SCMPDS st P1[ Dstate t] & t . F4() = F2() . F4() & t . (DataLoc (F2() . F4()),F5()) < 0 holds
( (IExec F3(),t) . F4() = t . F4() & F3() is_closed_on t & F3() is_halting_on t & F1((Dstate (IExec F3(),t))) < F1((Dstate t)) & P1[ Dstate (IExec F3(),t)] )
proof end;

set a1 = intpos 1;

set a2 = intpos 2;

set a3 = intpos 3;

definition
let n, p0 be Nat;
func sum n,p0 -> Program-block equals :: SCPINVAR:def 1
((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))) ';' (while<0 GBP ,2,(((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)));
coherence
((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))) ';' (while<0 GBP ,2,(((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1))) is Program-block ;
end;

:: deftheorem defines sum SCPINVAR:def 1 :
for n, p0 being Nat holds sum n,p0 = ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))) ';' (while<0 GBP ,2,(((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)));

theorem Th8: :: SCPINVAR:8  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 I being shiftable No-StopCode Program-block
for a, b, c being Int_position
for n, i, p0 being Nat
for f being FinSequence of INT st card I > 0 & f is_FinSequence_on s,p0 & len f = n & s . b = 0 & s . a = 0 & s . (intpos i) = - n & s . c = p0 + 1 & ( for t being State of SCMPDS st ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = (t . (intpos i)) + n & t . b = Sum g & t . c = (p0 + 1) + (len g) ) & t . a = 0 & t . (intpos i) < 0 & ( for i being Nat st i > p0 holds
t . (intpos i) = s . (intpos i) ) holds
( (IExec I,t) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec I,t) . (intpos i) = (t . (intpos i)) + 1 & ex g being FinSequence of INT st
( g is_FinSequence_on s,p0 & len g = ((t . (intpos i)) + n) + 1 & (IExec I,t) . c = (p0 + 1) + (len g) & (IExec I,t) . b = Sum g ) & ( for i being Nat st i > p0 holds
(IExec I,t) . (intpos i) = s . (intpos i) ) ) ) holds
( (IExec (while<0 a,i,I),s) . b = Sum f & while<0 a,i,I is_closed_on s & while<0 a,i,I is_halting_on s )
proof end;

set j1 = AddTo GBP ,1,(intpos 3),0;

set j2 = AddTo GBP ,2,1;

set j3 = AddTo GBP ,3,1;

set WB = ((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1);

set WH = while<0 GBP ,2,(((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1));

Lm1: for s being State of SCMPDS
for m being Nat st s . GBP = 0 & s . (intpos 3) = m holds
( (IExec (((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . GBP = 0 & (IExec (((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 1) = (s . (intpos 1)) + (s . (intpos m)) & (IExec (((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = (s . (intpos 2)) + 1 & (IExec (((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = m + 1 & ( for i being Nat st i > 3 holds
(IExec (((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
proof end;

Lm2: card (((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)) = 3
proof end;

Lm3: for s being State of SCMPDS
for n, p0 being Nat
for f being FinSequence of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f = n & s . (intpos 1) = 0 & s . GBP = 0 & s . (intpos 2) = - n & s . (intpos 3) = p0 + 1 holds
( (IExec (while<0 GBP ,2,(((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1))),s) . (intpos 1) = Sum f & while<0 GBP ,2,(((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)) is_closed_on s & while<0 GBP ,2,(((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)) is_halting_on s )
proof end;

Lm4: for s being State of SCMPDS
for n, p0 being Nat
for f being FinSequence of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f = n holds
( (IExec (sum n,p0),s) . (intpos 1) = Sum f & sum n,p0 is_halting_on s )
proof end;

theorem :: SCPINVAR:9  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 n, p0 being Nat
for f being FinSequence of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f = n holds
( (IExec (sum n,p0),s) . (intpos 1) = Sum f & sum n,p0 is parahalting )
proof end;

scheme :: SCPINVAR:sch 2
WhileGEnd{ F1( State of SCMPDS ) -> Nat, F2() -> State of SCMPDS , F3() -> shiftable No-StopCode Program-block, F4() -> Int_position , F5() -> Integer, P1[ set ] } :
( F1((Dstate (IExec (while>0 F4(),F5(),F3()),F2()))) = 0 & P1[ Dstate (IExec (while>0 F4(),F5(),F3()),F2())] )
provided
A1: card F3() > 0 and
A2: for t being State of SCMPDS st P1[ Dstate t] holds
( F1((Dstate t)) = 0 iff t . (DataLoc (F2() . F4()),F5()) <= 0 ) and
A3: P1[ Dstate F2()] and
A4: for t being State of SCMPDS st P1[ Dstate t] & t . F4() = F2() . F4() & t . (DataLoc (F2() . F4()),F5()) > 0 holds
( (IExec F3(),t) . F4() = t . F4() & F3() is_closed_on t & F3() is_halting_on t & F1((Dstate (IExec F3(),t))) < F1((Dstate t)) & P1[ Dstate (IExec F3(),t)] )
proof end;

definition
let n be Nat;
func Fib-macro n -> Program-block equals :: SCPINVAR:def 2
((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)) ';' (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))));
coherence
((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)) ';' (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))) is Program-block ;
end;

:: deftheorem defines Fib-macro SCPINVAR:def 2 :
for n being Nat holds Fib-macro n = ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)) ';' (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))));

theorem Th10: :: SCPINVAR:10  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 I being shiftable No-StopCode Program-block
for a, f0, f1 being Int_position
for n, i being Nat st card I > 0 & s . a = 0 & s . f0 = 0 & s . f1 = 1 & s . (intpos i) = n & ( for t being State of SCMPDS
for k being Nat st n = (t . (intpos i)) + k & t . f0 = Fib k & t . f1 = Fib (k + 1) & t . a = 0 & t . (intpos i) > 0 holds
( (IExec I,t) . a = 0 & I is_closed_on t & I is_halting_on t & (IExec I,t) . (intpos i) = (t . (intpos i)) - 1 & (IExec I,t) . f0 = Fib (k + 1) & (IExec I,t) . f1 = Fib ((k + 1) + 1) ) ) holds
( (IExec (while>0 a,i,I),s) . f0 = Fib n & (IExec (while>0 a,i,I),s) . f1 = Fib (n + 1) & while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s )
proof end;

set j1 = GBP ,4 := GBP ,2;

set j2 = AddTo GBP ,2,GBP ,1;

set j3 = GBP ,1 := GBP ,4;

set j4 = AddTo GBP ,3,(- 1);

set WB = (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1));

set WH = while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)));

Lm5: for s being State of SCMPDS st s . GBP = 0 holds
( (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . GBP = 0 & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 1) = s . (intpos 2) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 2) = (s . (intpos 1)) + (s . (intpos 2)) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 3) = (s . (intpos 3)) - 1 )
proof end;

Lm6: card ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))) = 4
proof end;

Lm7: for s being State of SCMPDS
for n being Nat st s . GBP = 0 & s . (intpos 1) = 0 & s . (intpos 2) = 1 & s . (intpos 3) = n holds
( (IExec (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))),s) . (intpos 1) = Fib n & (IExec (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))),s) . (intpos 2) = Fib (n + 1) & while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))) is_closed_on s & while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))) is_halting_on s )
proof end;

Lm8: for s being State of SCMPDS
for n being Nat holds
( (IExec (Fib-macro n),s) . (intpos 1) = Fib n & (IExec (Fib-macro n),s) . (intpos 2) = Fib (n + 1) & Fib-macro n is_halting_on s )
proof end;

theorem :: SCPINVAR:11  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 n being Nat holds
( (IExec (Fib-macro n),s) . (intpos 1) = Fib n & (IExec (Fib-macro n),s) . (intpos 2) = Fib (n + 1) & Fib-macro n is parahalting )
proof end;

definition
let a be Int_position ;
let i be Integer;
let I be Program-block;
func while<>0 a,i,I -> Program-block equals :: SCPINVAR:def 3
(((a,i <>0_goto 2) ';' (goto ((card I) + 2))) ';' I) ';' (goto (- ((card I) + 2)));
coherence
(((a,i <>0_goto 2) ';' (goto ((card I) + 2))) ';' I) ';' (goto (- ((card I) + 2))) is Program-block ;
end;

:: deftheorem defines while<>0 SCPINVAR:def 3 :
for a being Int_position
for i being Integer
for I being Program-block holds while<>0 a,i,I = (((a,i <>0_goto 2) ';' (goto ((card I) + 2))) ';' I) ';' (goto (- ((card I) + 2)));

theorem Th12: :: SCPINVAR:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position
for i being Integer
for I being Program-block holds card (while<>0 a,i,I) = (card I) + 3
proof end;

Lm9: for a being Int_position
for i being Integer
for I being Program-block holds card (stop (while<>0 a,i,I)) = (card I) + 4
proof end;

theorem Th13: :: SCPINVAR:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position
for i being Integer
for m being Nat
for I being Program-block holds
( m < (card I) + 3 iff inspos m in dom (while<>0 a,i,I) )
proof end;

theorem Th14: :: SCPINVAR:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position
for i being Integer
for I being Program-block holds
( inspos 0 in dom (while<>0 a,i,I) & inspos 1 in dom (while<>0 a,i,I) )
proof end;

theorem Th15: :: SCPINVAR:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position
for i being Integer
for I being Program-block holds
( (while<>0 a,i,I) . (inspos 0) = a,i <>0_goto 2 & (while<>0 a,i,I) . (inspos 1) = goto ((card I) + 2) & (while<>0 a,i,I) . (inspos ((card I) + 2)) = goto (- ((card I) + 2)) )
proof end;

Lm10: for a being Int_position
for i being Integer
for I being Program-block holds while<>0 a,i,I = (a,i <>0_goto 2) ';' (((goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 2))))
proof end;

theorem Th16: :: SCPINVAR: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
for I being Program-block
for a being Int_position
for i being Integer st s . (DataLoc (s . a),i) = 0 holds
( while<>0 a,i,I is_closed_on s & while<>0 a,i,I is_halting_on s )
proof end;

theorem Th17: :: SCPINVAR: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
for I being Program-block
for a, c being Int_position
for i being Integer st s . (DataLoc (s . a),i) = 0 holds
IExec (while<>0 a,i,I),s = s +* (Start-At (inspos ((card I) + 3)))
proof end;

theorem :: SCPINVAR: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
for I being Program-block
for a being Int_position
for i being Integer st s . (DataLoc (s . a),i) = 0 holds
IC (IExec (while<>0 a,i,I),s) = inspos ((card I) + 3)
proof end;

theorem Th19: :: SCPINVAR:19  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 I being Program-block
for a, b being Int_position
for i being Integer st s . (DataLoc (s . a),i) = 0 holds
(IExec (while<>0 a,i,I),s) . b = s . b
proof end;

Lm11: for I being Program-block
for a being Int_position
for i being Integer holds Shift I,2 c= while<>0 a,i,I
proof end;

registration
let I be shiftable Program-block;
let a be Int_position ;
let i be Integer;
cluster while<>0 a,i,I -> shiftable ;
correctness
coherence
while<>0 a,i,I is shiftable;
proof end;
end;

registration
let I be No-StopCode Program-block;
let a be Int_position ;
let i be Integer;
cluster while<>0 a,i,I -> No-StopCode ;
correctness
coherence
while<>0 a,i,I is No-StopCode;
proof end;
end;

scheme :: SCPINVAR:sch 3
WhileNHalt{ F1( State of SCMPDS ) -> Nat, F2() -> State of SCMPDS , F3() -> shiftable No-StopCode Program-block, F4() -> Int_position , F5() -> Integer, P1[ set ] } :
( while<>0 F4(),F5(),F3() is_closed_on F2() & while<>0 F4(),F5(),F3() is_halting_on F2() )
provided
A1: card F3() > 0 and
A2: for t being State of SCMPDS st P1[ Dstate t] & F1((Dstate t)) = 0 holds
t . (DataLoc (F2() . F4()),F5()) = 0 and
A3: P1[ Dstate F2()] and
A4: for t being State of SCMPDS st P1[ Dstate t] & t . F4() = F2() . F4() & t . (DataLoc (F2() . F4()),F5()) <> 0 holds
( (IExec F3(),t) . F4() = t . F4() & F3() is_closed_on t & F3() is_halting_on t & F1((Dstate (IExec F3(),t))) < F1((Dstate t)) & P1[ Dstate (IExec F3(),t)] )
proof end;

scheme :: SCPINVAR:sch 4
WhileNExec{ F1( State of SCMPDS ) -> Nat, F2() -> State of SCMPDS , F3() -> shiftable No-StopCode Program-block, F4() -> Int_position , F5() -> Integer, P1[ set ] } :
IExec (while<>0 F4(),F5(),F3()),F2() = IExec (while<>0 F4(),F5(),F3()),(IExec F3(),F2())
provided
A1: card F3() > 0 and
A2: F2() . (DataLoc (F2() . F4()),F5()) <> 0 and
A3: for t being State of SCMPDS st P1[ Dstate t] & F1((Dstate t)) = 0 holds
t . (DataLoc (F2() . F4()),F5()) = 0 and
A4: P1[ Dstate F2()] and
A5: for t being State of SCMPDS st P1[ Dstate t] & t . F4() = F2() . F4() & t . (DataLoc (F2() . F4()),F5()) <> 0 holds
( (IExec F3(),t) . F4() = t . F4() & F3() is_closed_on t & F3() is_halting_on t & F1((Dstate (IExec F3(),t))) < F1((Dstate t)) & P1[ Dstate (IExec F3(),t)] )
proof end;

scheme :: SCPINVAR:sch 5
WhileNEnd{ F1( State of SCMPDS ) -> Nat, F2() -> State of SCMPDS , F3() -> shiftable No-StopCode Program-block, F4() -> Int_position , F5() -> Integer, P1[ set ] } :
( F1((Dstate (IExec (while<>0 F4(),F5(),F3()),F2()))) = 0 & P1[ Dstate (IExec (while<>0 F4(),F5(),F3()),F2())] )
provided
A1: card F3() > 0 and
A2: for t being State of SCMPDS st P1[ Dstate t] holds
( F1((Dstate t)) = 0 iff t . (DataLoc (F2() . F4()),F5()) = 0 ) and
A3: P1[ Dstate F2()] and
A4: for t being State of SCMPDS st P1[ Dstate t] & t . F4() = F2() . F4() & t . (DataLoc (F2() . F4()),F5()) <> 0 holds
( (IExec F3(),t) . F4() = t . F4() & F3() is_closed_on t & F3() is_halting_on t & F1((Dstate (IExec F3(),t))) < F1((Dstate t)) & P1[ Dstate (IExec F3(),t)] )
proof end;

theorem Th20: :: SCPINVAR:20  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 I being shiftable No-StopCode Program-block
for a, b, c being Int_position
for i, d being Integer st card I > 0 & s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc d,i) = (s . b) - (s . c) & ( for t being State of SCMPDS st t . b > 0 & t . c > 0 & t . a = d & t . (DataLoc d,i) = (t . b) - (t . c) & t . b <> t . c holds
( (IExec I,t) . a = d & I is_closed_on t & I is_halting_on t & ( t . b > t . c implies ( (IExec I,t) . b = (t . b) - (t . c) & (IExec I,t) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec I,t) . c = (t . c) - (t . b) & (IExec I,t) . b = t . b ) ) & (IExec I,t) . (DataLoc d,i) = ((IExec I,t) . b) - ((IExec I,t) . c) ) ) holds
( while<>0 a,i,I is_closed_on s & while<>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) <> 0 implies IExec (while<>0 a,i,I),s = IExec (while<>0 a,i,I),(IExec I,s) ) )
proof end;

definition
func GCD-Algorithm -> Program-block equals :: SCPINVAR:def 4
(((GBP := 0) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)));
coherence
(((GBP := 0) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is Program-block ;
end;

:: deftheorem defines GCD-Algorithm SCPINVAR:def 4 :
GCD-Algorithm = (((GBP := 0) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)));

theorem Th21: :: SCPINVAR:21  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 I being shiftable No-StopCode Program-block
for a, b, c being Int_position
for i, d being Integer st card I > 0 & s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc d,i) = (s . b) - (s . c) & ( for t being State of SCMPDS st t . b > 0 & t . c > 0 & t . a = d & t . (DataLoc d,i) = (t . b) - (t . c) & t . b <> t . c holds
( (IExec I,t) . a = d & I is_closed_on t & I is_halting_on t & ( t . b > t . c implies ( (IExec I,t) . b = (t . b) - (t . c) & (IExec I,t) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec I,t) . c = (t . c) - (t . b) & (IExec I,t) . b = t . b ) ) & (IExec I,t) . (DataLoc d,i) = ((IExec I,t) . b) - ((IExec I,t) . c) ) ) holds
( (IExec (while<>0 a,i,I),s) . b = (s . b) gcd (s . c) & (IExec (while<>0 a,i,I),s) . c = (s . b) gcd (s . c) )
proof end;

set i1 = GBP := 0;

set i2 = GBP ,3 := GBP ,1;

set i3 = SubFrom GBP ,3,GBP ,2;

set j1 = Load (SubFrom GBP ,1,GBP ,2);

set j2 = Load (SubFrom GBP ,2,GBP ,1);

set IF = if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1));

set k1 = GBP ,3 := GBP ,1;

set k2 = SubFrom GBP ,3,GBP ,2;

set WB = ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2);

set WH = while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2));

Lm12: card (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) = 6
proof end;

Lm13: card (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) = 9
proof end;

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

Lm14: for s being State of SCMPDS st s . GBP = 0 holds
( ( s . (intpos 3) > 0 implies ( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) = (s . (intpos 1)) - (s . (intpos 2)) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) = s . (intpos 2) ) ) & ( s . (intpos 3) <= 0 implies ( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) = (s . (intpos 2)) - (s . (intpos 1)) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) = s . (intpos 1) ) ) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . GBP = 0 & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 3) = ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) - ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2)) )
proof end;

Lm15: for s being State of SCMPDS st s . GBP = 0 & s . (intpos 1) > 0 & s . (intpos 2) > 0 & s . (intpos 3) = (s . (intpos 1)) - (s . (intpos 2)) holds
( (IExec (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))),s) . (intpos 1) = (s . (intpos 1)) gcd (s . (intpos 2)) & (IExec (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))),s) . (intpos 2) = (s . (intpos 1)) gcd (s . (intpos 2)) & while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) is_closed_on s & while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) is_halting_on s )
proof end;

set GA = (((GBP := 0) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)));

Lm16: for s being State of SCMPDS st s . (intpos 1) > 0 & s . (intpos 2) > 0 holds
( (IExec ((((GBP := 0) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)))),s) . (intpos 1) = (s . (intpos 1)) gcd (s . (intpos 2)) & (IExec ((((GBP := 0) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)))),s) . (intpos 2) = (s . (intpos 1)) gcd (s . (intpos 2)) & (((GBP := 0) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is_closed_on s & (((GBP := 0) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is_halting_on s )
proof end;

theorem :: SCPINVAR:23  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 x, y being Integer st s . (intpos 1) = x & s . (intpos 2) = y & x > 0 & y > 0 holds
( (IExec GCD-Algorithm ,s) . (intpos 1) = x gcd y & (IExec GCD-Algorithm ,s) . (intpos 2) = x gcd y & GCD-Algorithm is_closed_on s & GCD-Algorithm is_halting_on s ) by Lm16;