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

begin

theorem :: SCPINVAR:1

canceled;

theorem :: SCPINVAR:2

canceled;

theorem :: SCPINVAR:3

canceled;

theorem :: SCPINVAR:4

canceled;

theorem Th5: :: SCPINVAR:5

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:6

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

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 = NAT ;

set D = SCM-Data-Loc ;

begin

scheme :: SCPINVAR:sch 1
WhileLEnd{ F₁( State of SCMPDS) -> Element of NAT , F₂() -> State of SCMPDS, F₃() -> the Instructions of SCMPDS -valued ManySortedSet of NAT , F₄() -> halt-free shiftable Program of SCMPDS, F₅() -> Int_position , F₆() -> Integer, P₁[ set ] } :

( F₁((Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),F₃(),F₂())))) = 0 & P₁[ Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),F₃(),F₂()))] )

provided

A2: for t being State of SCMPDS st P₁[ Dstate t] holds
( F₁((Dstate t)) = 0 iff t . (DataLoc ((F₂() . F₅()),F₆())) >= 0 ) and
A3: P₁[ Dstate F₂()] and
A4: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st P₁[ Dstate t] & t . F₅() = F₂() . F₅() & t . (DataLoc ((F₂() . F₅()),F₆())) < 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & F₁((Dstate (IExec (F₄(),Q,t)))) < F₁((Dstate t)) & P₁[ Dstate (IExec (F₄(),Q,t))] )

proof end;

set a1 = intpos 1;

set a2 = intpos 2;

set a3 = intpos 3;

begin

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 Object-Kind 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 13;

end;

theorem Th8: :: SCPINVAR:8

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 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
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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 the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . GBP = 0 & (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),P,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,s)) . (intpos 2) = (s . (intpos 2)) + 1 & (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),P,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,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 P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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 the Instructions of SCMPDS -valued ManySortedSet of NAT
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:9

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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{ F₁( State of SCMPDS) -> Element of NAT , F₂() -> State of SCMPDS, F₃() -> the Instructions of SCMPDS -valued ManySortedSet of NAT , F₄() -> halt-free shiftable Program of SCMPDS, F₅() -> Int_position , F₆() -> Integer, P₁[ set ] } :

( F₁((Dstate (IExec ((while>0 (F₅(),F₆(),F₄())),F₃(),F₂())))) = 0 & P₁[ Dstate (IExec ((while>0 (F₅(),F₆(),F₄())),F₃(),F₂()))] )

provided

A2: for t being State of SCMPDS st P₁[ Dstate t] holds
( F₁((Dstate t)) = 0 iff t . (DataLoc ((F₂() . F₅()),F₆())) <= 0 ) and
A3: P₁[ Dstate F₂()] and
A4: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st P₁[ Dstate t] & t . F₅() = F₂() . F₅() & t . (DataLoc ((F₂() . F₅()),F₆())) > 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & F₁((Dstate (IExec (F₄(),Q,t)))) < F₁((Dstate t)) & P₁[ Dstate (IExec (F₄(),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:10

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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 card I > 0 & s . a = 0 & s . f0 = 0 & s . f1 = 1 & s . (intpos i) = n & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 the Instructions of SCMPDS -valued ManySortedSet of NAT
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)))),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;

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

proof end;

Lm7: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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 the Instructions of SCMPDS -valued ManySortedSet of NAT
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:11

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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

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:12

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:13

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:14

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:15

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:16

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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:17

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s) = s +* (Start-At (((card I) + 3),SCMPDS))

proof end;

theorem :: SCPINVAR:18

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) = (card I) + 3

proof end;

theorem Th19: :: SCPINVAR:19

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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{ F₁( State of SCMPDS) -> Element of NAT , F₂() -> State of SCMPDS, F₃() -> the Instructions of SCMPDS -valued ManySortedSet of NAT , F₄() -> halt-free shiftable Program of SCMPDS, F₅() -> Int_position , F₆() -> Integer, P₁[ set ] } :

( while<>0 (F₅(),F₆(),F₄()) is_closed_on F₂(),F₃() & while<>0 (F₅(),F₆(),F₄()) is_halting_on F₂(),F₃() )

provided

A1: card F₄() > 0 and
A2: for t being State of SCMPDS st P₁[ Dstate t] & F₁((Dstate t)) = 0 holds
t . (DataLoc ((F₂() . F₅()),F₆())) = 0 and
A3: P₁[ Dstate F₂()] and
A4: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st P₁[ Dstate t] & t . F₅() = F₂() . F₅() & t . (DataLoc ((F₂() . F₅()),F₆())) <> 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & F₁((Dstate (IExec (F₄(),Q,t)))) < F₁((Dstate t)) & P₁[ Dstate (IExec (F₄(),Q,t))] )

proof end;

scheme :: SCPINVAR:sch 4
WhileNExec{ F₁( State of SCMPDS) -> Element of NAT , F₂() -> State of SCMPDS, F₃() -> the Instructions of SCMPDS -valued ManySortedSet of NAT , F₄() -> halt-free shiftable Program of SCMPDS, F₅() -> Int_position , F₆() -> Integer, P₁[ set ] } :

IExec ((while<>0 (F₅(),F₆(),F₄())),F₃(),F₂()) = IExec ((while<>0 (F₅(),F₆(),F₄())),F₃(),(IExec (F₄(),F₃(),F₂())))

provided

A1: card F₄() > 0 and
A2: F₂() . (DataLoc ((F₂() . F₅()),F₆())) <> 0 and
A3: for t being State of SCMPDS st P₁[ Dstate t] & F₁((Dstate t)) = 0 holds
t . (DataLoc ((F₂() . F₅()),F₆())) = 0 and
A4: P₁[ Dstate F₂()] and
A5: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st P₁[ Dstate t] & t . F₅() = F₂() . F₅() & t . (DataLoc ((F₂() . F₅()),F₆())) <> 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & F₁((Dstate (IExec (F₄(),Q,t)))) < F₁((Dstate t)) & P₁[ Dstate (IExec (F₄(),Q,t))] )

proof end;

scheme :: SCPINVAR:sch 5
WhileNEnd{ F₁( State of SCMPDS) -> Element of NAT , F₂() -> State of SCMPDS, F₃() -> the Instructions of SCMPDS -valued ManySortedSet of NAT , F₄() -> halt-free shiftable Program of SCMPDS, F₅() -> Int_position , F₆() -> Integer, P₁[ set ] } :

( F₁((Dstate (IExec ((while<>0 (F₅(),F₆(),F₄())),F₃(),F₂())))) = 0 & P₁[ Dstate (IExec ((while<>0 (F₅(),F₆(),F₄())),F₃(),F₂()))] )

provided

A1: card F₄() > 0 and
A2: for t being State of SCMPDS st P₁[ Dstate t] holds
( F₁((Dstate t)) = 0 iff t . (DataLoc ((F₂() . F₅()),F₆())) = 0 ) and
A3: P₁[ Dstate F₂()] and
A4: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st P₁[ Dstate t] & t . F₅() = F₂() . F₅() & t . (DataLoc ((F₂() . F₅()),F₆())) <> 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & F₁((Dstate (IExec (F₄(),Q,t)))) < F₁((Dstate t)) & P₁[ Dstate (IExec (F₄(),Q,t))] )

proof end;

theorem Th20: :: SCPINVAR:20

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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 State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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,(IExec (I,P,s))) ) )

proof end;

begin

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:21

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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 State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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:22

card GCD-Algorithm = 12

proof end;

Lm14: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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))),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 the Instructions of SCMPDS -valued ManySortedSet of NAT
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))))),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 the Instructions of SCMPDS -valued ManySortedSet of NAT
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)))))),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:23

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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;