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

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) . (inspos 0 ) = i & ((i ';' j) ';' I) . (inspos 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 ;

scheme :: SCPINVAR:sch 1
WhileLEnd{ F₁( State of SCMPDS ) -> Element of NAT , F₂() -> State of SCMPDS , F₃() -> shiftable No-StopCode Program of SCMPDS , F₄() -> Int_position , F₅() -> Integer, P₁[ set ] } :

( F₁((Dstate (IExec (while<0 F₄(),F₅(),F₃()),F₂()))) = 0 & P₁[ Dstate (IExec (while<0 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 st P₁[ Dstate t] & t . F₄() = F₂() . F₄() & t . (DataLoc (F₂() . F₄()),F₅()) < 0 holds
( (IExec F₃(),t) . F₄() = t . F₄() & F₃() is_closed_on t & F₃() is_halting_on t & F₁((Dstate (IExec F₃(),t))) < F₁((Dstate t)) & P₁[ Dstate (IExec F₃(),t)] )

proof end;

set a1 = intpos 1;

set a2 = intpos 2;

set a3 = intpos 3;

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)));

theorem Th8: :: SCPINVAR:8

for s being State of SCMPDS
for I being shiftable No-StopCode 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 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,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 Element of 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 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)),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 Element of 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 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))),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 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),s) . (intpos 1) = Sum f & sum n,p0 is_halting_on s )

proof end;

theorem :: SCPINVAR:9

for s being 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),s) . (intpos 1) = Sum f & sum n,p0 is parahalting )

proof end;

scheme :: SCPINVAR:sch 2
WhileGEnd{ F₁( State of SCMPDS ) -> Element of NAT , F₂() -> State of SCMPDS , F₃() -> shiftable No-StopCode Program of SCMPDS , F₄() -> Int_position , F₅() -> Integer, P₁[ set ] } :

( F₁((Dstate (IExec (while>0 F₄(),F₅(),F₃()),F₂()))) = 0 & P₁[ Dstate (IExec (while>0 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 st P₁[ Dstate t] & t . F₄() = F₂() . F₄() & t . (DataLoc (F₂() . F₄()),F₅()) > 0 holds
( (IExec F₃(),t) . F₄() = t . F₄() & F₃() is_closed_on t & F₃() is_halting_on t & F₁((Dstate (IExec F₃(),t))) < F₁((Dstate t)) & P₁[ Dstate (IExec F₃(),t)] )

proof end;

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 s being State of SCMPDS
for I being shiftable No-StopCode 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 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,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 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)))),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 Element of 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

for s being State of SCMPDS
for n being Element of 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 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)));

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 inspos 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
( inspos 0 in dom (while<>0 a,i,I) & inspos 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) . (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 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 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 & while<>0 a,i,I is_halting_on s )

proof end;

theorem Th17: :: SCPINVAR:17

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),s = s +* (Start-At (inspos ((card I) + 3)))

proof end;

theorem :: SCPINVAR:18

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),s) = inspos ((card I) + 3)

proof end;

theorem Th19: :: SCPINVAR:19

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),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 No-StopCode Program of SCMPDS ;
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{ F₁( State of SCMPDS ) -> Element of NAT , F₂() -> State of SCMPDS , F₃() -> shiftable No-StopCode Program of SCMPDS , F₄() -> Int_position , F₅() -> Integer, P₁[ set ] } :

( while<>0 F₄(),F₅(),F₃() is_closed_on F₂() & while<>0 F₄(),F₅(),F₃() is_halting_on 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 st P₁[ Dstate t] & t . F₄() = F₂() . F₄() & t . (DataLoc (F₂() . F₄()),F₅()) <> 0 holds
( (IExec F₃(),t) . F₄() = t . F₄() & F₃() is_closed_on t & F₃() is_halting_on t & F₁((Dstate (IExec F₃(),t))) < F₁((Dstate t)) & P₁[ Dstate (IExec F₃(),t)] )

proof end;

scheme :: SCPINVAR:sch 4
WhileNExec{ F₁( State of SCMPDS ) -> Element of NAT , F₂() -> State of SCMPDS , F₃() -> shiftable No-StopCode Program of SCMPDS , F₄() -> Int_position , F₅() -> Integer, P₁[ set ] } :

IExec (while<>0 F₄(),F₅(),F₃()),F₂() = IExec (while<>0 F₄(),F₅(),F₃()),(IExec 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 st P₁[ Dstate t] & t . F₄() = F₂() . F₄() & t . (DataLoc (F₂() . F₄()),F₅()) <> 0 holds
( (IExec F₃(),t) . F₄() = t . F₄() & F₃() is_closed_on t & F₃() is_halting_on t & F₁((Dstate (IExec F₃(),t))) < F₁((Dstate t)) & P₁[ Dstate (IExec F₃(),t)] )

proof end;

scheme :: SCPINVAR:sch 5
WhileNEnd{ F₁( State of SCMPDS ) -> Element of NAT , F₂() -> State of SCMPDS , F₃() -> shiftable No-StopCode Program of SCMPDS , F₄() -> Int_position , F₅() -> Integer, P₁[ set ] } :

( F₁((Dstate (IExec (while<>0 F₄(),F₅(),F₃()),F₂()))) = 0 & P₁[ Dstate (IExec (while<>0 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 st P₁[ Dstate t] & t . F₄() = F₂() . F₄() & t . (DataLoc (F₂() . F₄()),F₅()) <> 0 holds
( (IExec F₃(),t) . F₄() = t . F₄() & F₃() is_closed_on t & F₃() is_halting_on t & F₁((Dstate (IExec F₃(),t))) < F₁((Dstate t)) & P₁[ Dstate (IExec F₃(),t)] )

proof end;

theorem Th20: :: SCPINVAR:20

for s being State of SCMPDS
for I being shiftable No-StopCode 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 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 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 s being State of SCMPDS
for I being shiftable No-StopCode 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 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

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

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;