:: Justifying the Correctness of Fibonacci Sequence and Euclide Algorithm by Loop Invariant
:: by JingChao Chen
::
:: Received June 14, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

theorem Th5: :: SCPINVAR:1
for i, j being Instruction of SCMPDS
for I being Program of SCMPDS holds
( ((i ';' j) ';' I) . 0 = i & ((i ';' j) ';' I) . 1 = j )
proof end;

theorem Th6: :: SCPINVAR:2
for a, b being Int_position ex f being Function of (product (the_Values_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:3
for a being Int_position ex f being Function of (product (the_Values_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 = NAT ;

set D = SCM-Data-Loc ;

begin

scheme :: SCPINVAR:sch 1
WhileLEnd{ F1( State of SCMPDS) -> Element of NAT , F2() -> 0 -started State of SCMPDS, F3() -> Instruction-Sequence of SCMPDS, F4() -> halt-free shiftable Program of SCMPDS, F5() -> Int_position, F6() -> Integer, P1[ set ] } :
( F1((Initialize (IExec ((while<0 (F5(),F6(),F4())),F3(),F2())))) = 0 & P1[ Initialize (IExec ((while<0 (F5(),F6(),F4())),F3(),F2()))] )
provided
A2: for t being 0 -started State of SCMPDS st P1[t] holds
( F1(t) = 0 iff t . (DataLoc ((F2() . F5()),F6())) >= 0 ) and
A3: P1[F2()] and
A4: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = F2() . F5() & t . (DataLoc ((F2() . F5()),F6())) < 0 holds
( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & F1((Initialize (IExec (F4(),Q,t)))) < F1(t) & P1[ Initialize (IExec (F4(),Q,t))] )
proof end;

set a1 = intpos 1;

set a2 = intpos 2;

set a3 = intpos 3;

begin

:: sum=Sum=x1+x2+...+xn
definition
let n, p0 be Element of NAT ;
func sum (n,p0) -> Program of SCMPDS 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 of SCMPDS ;
end;

:: deftheorem defines sum SCPINVAR:def 1 :
for n, p0 being Element of 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)))));

definition
let ff be Function of (product (the_Values_of SCMPDS)),NAT;
let s be State of SCMPDS;
:: original: .
redefine func ff . s -> Element of NAT ;
coherence
ff . s is Element of NAT by ORDINAL1:def 12;
end;

theorem Th8: :: SCPINVAR:4
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a, b, c being Int_position
for n, i, p0 being Element of NAT
for f being FinSequence of INT st 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 0 -started State of SCMPDS
for Q being Instruction-Sequence 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 Element of NAT st i > p0 holds
t . (intpos i) = s . (intpos i) ) holds
( (IExec (I,Q,t)) . a = 0 & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,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,Q,t)) . c = (p0 + 1) + (len g) & (IExec (I,Q,t)) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds
(IExec (I,Q,t)) . (intpos i) = s . (intpos i) ) ) ) holds
( (IExec ((while<0 (a,i,I)),P,s)) . b = Sum f & while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )
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 P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for m being Element of 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))),P,(Initialize s))) . GBP = 0 & (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 1) = (s . (intpos 1)) + (s . (intpos m)) & (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 2) = (s . (intpos 2)) + 1 & (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3) = m + 1 & ( for i being Element of NAT st i > 3 holds
(IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i) ) )
proof end;

Lm3: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for n, p0 being Element of 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))))),P,(Initialize 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,P & while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)))) is_halting_on s,P )
proof end;

Lm4: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for n, p0 being Element of NAT
for f being FinSequence of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f = n holds
( (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f & sum (n,p0) is_halting_on s,P )
proof end;

theorem :: SCPINVAR:5
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for n, p0 being Element of NAT
for f being FinSequence of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f = n holds
( (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f & sum (n,p0) is parahalting )
proof end;

begin

scheme :: SCPINVAR:sch 2
WhileGEnd{ F1( State of SCMPDS) -> Element of NAT , F2() -> 0 -started State of SCMPDS, F3() -> Instruction-Sequence of SCMPDS, F4() -> halt-free shiftable Program of SCMPDS, F5() -> Int_position, F6() -> Integer, P1[ set ] } :
( F1((Initialize (IExec ((while>0 (F5(),F6(),F4())),F3(),F2())))) = 0 & P1[ Initialize (IExec ((while>0 (F5(),F6(),F4())),F3(),F2()))] )
provided
A2: for t being 0 -started State of SCMPDS st P1[t] holds
( F1(t) = 0 iff t . (DataLoc ((F2() . F5()),F6())) <= 0 ) and
A3: P1[F2()] and
A4: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = F2() . F5() & t . (DataLoc ((F2() . F5()),F6())) > 0 holds
( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & F1((Initialize (IExec (F4(),Q,t)))) < F1(t) & P1[ Initialize (IExec (F4(),Q,t))] )
proof end;

begin

definition
let n be Element of NAT ;
func Fib-macro n -> Program of SCMPDS 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 of SCMPDS ;
end;

:: deftheorem defines Fib-macro SCPINVAR:def 2 :
for n being Element of 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:6
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a, f0, f1 being Int_position
for n, i being Element of NAT st s . a = 0 & s . f0 = 0 & s . f1 = 1 & s . (intpos i) = n & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for k being Element of 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,Q,t)) . a = 0 & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (intpos i) = (t . (intpos i)) - 1 & (IExec (I,Q,t)) . f0 = Fib (k + 1) & (IExec (I,Q,t)) . f1 = Fib ((k + 1) + 1) ) ) holds
( (IExec ((while>0 (a,i,I)),P,s)) . f0 = Fib n & (IExec ((while>0 (a,i,I)),P,s)) . f1 = Fib (n + 1) & while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P )
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 P being Instruction-Sequence of SCMPDS
for s being 0 -started 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)))),P,s)) . GBP = 0 & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s)) . (intpos 1) = s . (intpos 2) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,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)))),P,s)) . (intpos 3) = (s . (intpos 3)) - 1 )
proof end;

Lm7: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for n being Element of 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)))))),P,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)))))),P,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,P & 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,P )
proof end;

Lm8: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for n being Element of NAT holds
( (IExec ((Fib-macro n),P,s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),P,s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is_halting_on s,P )
proof end;

theorem :: SCPINVAR:7
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for n being Element of NAT holds
( (IExec ((Fib-macro n),P,s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),P,s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is parahalting )
proof end;

begin

:: while (a,i)<>0 do I
definition
let a be Int_position;
let i be Integer;
let I be Program of SCMPDS;
func while<>0 (a,i,I) -> Program of SCMPDS 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 of SCMPDS ;
end;

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

begin

theorem Th12: :: SCPINVAR:8
for a being Int_position
for i being Integer
for I being Program of SCMPDS 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 of SCMPDS holds card (stop (while<>0 (a,i,I))) = (card I) + 4
proof end;

theorem Th13: :: SCPINVAR:9
for a being Int_position
for i being Integer
for m being Element of NAT
for I being Program of SCMPDS holds
( m < (card I) + 3 iff m in dom (while<>0 (a,i,I)) )
proof end;

theorem Th14: :: SCPINVAR:10
for a being Int_position
for i being Integer
for I being Program of SCMPDS holds
( 0 in dom (while<>0 (a,i,I)) & 1 in dom (while<>0 (a,i,I)) )
proof end;

theorem Th15: :: SCPINVAR:11
for a being Int_position
for i being Integer
for I being Program of SCMPDS holds
( (while<>0 (a,i,I)) . 0 = (a,i) <>0_goto 2 & (while<>0 (a,i,I)) . 1 = goto ((card I) + 2) & (while<>0 (a,i,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
proof end;

Lm10: for a being Int_position
for i being Integer
for I being Program of SCMPDS 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:12
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS
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,P & while<>0 (a,i,I) is_halting_on s,P )
proof end;

theorem Th17: :: SCPINVAR:13
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS
for a, c being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) = 0 holds
IExec ((while<>0 (a,i,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 3),SCMPDS))
proof end;

theorem :: SCPINVAR:14
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS
for a being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) = 0 holds
IC (IExec ((while<>0 (a,i,I)),P,(Initialize s))) = (card I) + 3
proof end;

theorem Th19: :: SCPINVAR:15
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS
for a, b being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) = 0 holds
(IExec ((while<>0 (a,i,I)),P,(Initialize s))) . b = s . b
proof end;

Lm11: for I being Program of SCMPDS
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 of SCMPDS;
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 halt-free Program of SCMPDS;
let a be Int_position;
let i be Integer;
cluster while<>0 (a,i,I) -> halt-free ;
correctness
coherence
while<>0 (a,i,I) is halt-free ;
proof end;
end;

begin

scheme :: SCPINVAR:sch 3
WhileNHalt{ F1( State of SCMPDS) -> Element of NAT , F2() -> 0 -started State of SCMPDS, F3() -> Instruction-Sequence of SCMPDS, F4() -> halt-free shiftable Program of SCMPDS, F5() -> Int_position, F6() -> Integer, P1[ set ] } :
( while<>0 (F5(),F6(),F4()) is_closed_on F2(),F3() & while<>0 (F5(),F6(),F4()) is_halting_on F2(),F3() )
provided
A2: for t being 0 -started State of SCMPDS st P1[t] & F1(t) = 0 holds
t . (DataLoc ((F2() . F5()),F6())) = 0 and
A3: P1[F2()] and
A4: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = F2() . F5() & t . (DataLoc ((F2() . F5()),F6())) <> 0 holds
( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & F1((Initialize (IExec (F4(),Q,t)))) < F1(t) & P1[ Initialize (IExec (F4(),Q,t))] )
proof end;

scheme :: SCPINVAR:sch 4
WhileNExec{ F1( State of SCMPDS) -> Element of NAT , F2() -> 0 -started State of SCMPDS, F3() -> Instruction-Sequence of SCMPDS, F4() -> halt-free shiftable Program of SCMPDS, F5() -> Int_position, F6() -> Integer, P1[ set ] } :
IExec ((while<>0 (F5(),F6(),F4())),F3(),F2()) = IExec ((while<>0 (F5(),F6(),F4())),F3(),(Initialize (IExec (F4(),F3(),F2()))))
provided
A2: F2() . (DataLoc ((F2() . F5()),F6())) <> 0 and
A3: for t being 0 -started State of SCMPDS st P1[t] & F1(t) = 0 holds
t . (DataLoc ((F2() . F5()),F6())) = 0 and
A4: P1[F2()] and
A5: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = F2() . F5() & t . (DataLoc ((F2() . F5()),F6())) <> 0 holds
( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & F1((Initialize (IExec (F4(),Q,t)))) < F1(t) & P1[ Initialize (IExec (F4(),Q,t))] )
proof end;

scheme :: SCPINVAR:sch 5
WhileNEnd{ F1( State of SCMPDS) -> Element of NAT , F2() -> 0 -started State of SCMPDS, F3() -> Instruction-Sequence of SCMPDS, F4() -> halt-free shiftable Program of SCMPDS, F5() -> Int_position, F6() -> Integer, P1[ set ] } :
( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),F3(),F2())))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),F3(),F2()))] )
provided
A2: for t being 0 -started State of SCMPDS st P1[t] holds
( F1(t) = 0 iff t . (DataLoc ((F2() . F5()),F6())) = 0 ) and
A3: P1[F2()] and
A4: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = F2() . F5() & t . (DataLoc ((F2() . F5()),F6())) <> 0 holds
( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & F1((Initialize (IExec (F4(),Q,t)))) < F1(t) & P1[ Initialize (IExec (F4(),Q,t))] )
proof end;

theorem Th20: :: SCPINVAR:16
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
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 0 -started State of SCMPDS
for Q being Instruction-Sequence 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,Q,t)) . a = d & I is_closed_on t,Q & I is_halting_on t,Q & ( t . b > t . c implies ( (IExec (I,Q,t)) . b = (t . b) - (t . c) & (IExec (I,Q,t)) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec (I,Q,t)) . c = (t . c) - (t . b) & (IExec (I,Q,t)) . b = t . b ) ) & (IExec (I,Q,t)) . (DataLoc (d,i)) = ((IExec (I,Q,t)) . b) - ((IExec (I,Q,t)) . c) ) ) holds
( while<>0 (a,i,I) is_closed_on s,P & while<>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) <> 0 implies IExec ((while<>0 (a,i,I)),P,s) = IExec ((while<>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )
proof end;

begin

:: by loop-invariant
:: gcd(x,y) < x=(GBP,1) y=(GBP,2),(GBP,3)=x-y >
:: while x<>y do
:: if x>y then x=x-y else y=y-x
definition
func GCD-Algorithm -> Program of SCMPDS 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 of SCMPDS ;
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:17
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a, b, c being Int_position
for i, d being Integer st s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc (d,i)) = (s . b) - (s . c) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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,Q,t)) . a = d & I is_closed_on t,Q & I is_halting_on t,Q & ( t . b > t . c implies ( (IExec (I,Q,t)) . b = (t . b) - (t . c) & (IExec (I,Q,t)) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec (I,Q,t)) . c = (t . c) - (t . b) & (IExec (I,Q,t)) . b = t . b ) ) & (IExec (I,Q,t)) . (DataLoc (d,i)) = ((IExec (I,Q,t)) . b) - ((IExec (I,Q,t)) . c) ) ) holds
( (IExec ((while<>0 (a,i,I)),P,s)) . b = (s . b) gcd (s . c) & (IExec ((while<>0 (a,i,I)),P,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:18
card GCD-Algorithm = 12
proof end;

Lm14: for P being Instruction-Sequence of SCMPDS
for s being 0 -started 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))),P,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))),P,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))),P,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))),P,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))),P,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))),P,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))),P,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))),P,s)) . (intpos 2)) )
proof end;

Lm15: for P being Instruction-Sequence of SCMPDS
for s being 0 -started 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))))),P,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))))),P,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,P & 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,P )
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 P being Instruction-Sequence of SCMPDS
for s being 0 -started 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)))))),P,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)))))),P,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,P & (((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,P )
proof end;

theorem :: SCPINVAR:19
for P being Instruction-Sequence of SCMPDS
for s being 0 -started 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,P,s)) . (intpos 1) = x gcd y & (IExec (GCD-Algorithm,P,s)) . (intpos 2) = x gcd y & GCD-Algorithm is_closed_on s,P & GCD-Algorithm is_halting_on s,P ) by Lm16;