:: SCPINVAR semantic presentation

theorem Th1: :: SCPINVAR:1

for b₁, b₂, b₃ being Nat st b₁ divides b₂ & b₁ divides b₃ holds
b₁ divides b₂ - b₃

proof end;

theorem Th2: :: SCPINVAR:2

for b₁, b₂ being Nat holds
( b₁ divides b₂ iff b₁ divides b₂ )

proof end;

theorem Th3: :: SCPINVAR:3

for b₁, b₂ being Nat holds b₁ hcf b₂ = b₁ hcf (abs (b₂ - b₁))

proof end;

theorem Th4: :: SCPINVAR:4

for b₁, b₂ being Integer st b₁ >= 0 & b₂ >= 0 holds
b₁ gcd b₂ = b₁ gcd (b₂ - b₁)

proof end;

theorem Th5: :: SCPINVAR:5

for b₁, b₂ being Instruction of SCMPDS
for b₃ being Program-block holds
( ((b₁ ';' b₂) ';' b₃) . (inspos 0) = b₁ & ((b₁ ';' b₂) ';' b₃) . (inspos 1) = b₂ )

proof end;

theorem Th6: :: SCPINVAR:6

for b₁, b₂ being Int_position ex b₃ being Function of product the Object-Kind of SCMPDS , NAT st
for b₄ being State of SCMPDS holds
( ( b₄ . b₁ = b₄ . b₂ implies b₃ . b₄ = 0 ) & ( b₄ . b₁ <> b₄ . b₂ implies b₃ . b₄ = max (abs (b₄ . b₁)),(abs (b₄ . b₂)) ) )

proof end;

theorem Th7: :: SCPINVAR:7

for b₁ being Int_position ex b₂ being Function of product the Object-Kind of SCMPDS , NAT st
for b₃ being State of SCMPDS holds
( ( b₃ . b₁ >= 0 implies b₂ . b₃ = 0 ) & ( b₃ . b₁ < 0 implies b₂ . b₃ = - (b₃ . b₁) ) )

proof end;

set c₁ = the Instruction-Locations of SCMPDS ;

set c₂ = SCM-Data-Loc ;

scheme :: SCPINVAR:sch 1
s1{ F₁( State of SCMPDS ) -> Nat, F₂() -> State of SCMPDS , F₃() -> shiftable No-StopCode Program-block, 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

E8: card F₃() > 0 and
E9: for b₁ being State of SCMPDS st P₁[ Dstate b₁] holds
( F₁((Dstate b₁)) = 0 iff b₁ . (DataLoc (F₂() . F₄()),F₅()) >= 0 ) and
E10: P₁[ Dstate F₂()] and
E11: for b₁ being State of SCMPDS st P₁[ Dstate b₁] & b₁ . F₄() = F₂() . F₄() & b₁ . (DataLoc (F₂() . F₄()),F₅()) < 0 holds
( (IExec F₃(),b₁) . F₄() = b₁ . F₄() & F₃() is_closed_on b₁ & F₃() is_halting_on b₁ & F₁((Dstate (IExec F₃(),b₁))) < F₁((Dstate b₁)) & P₁[ Dstate (IExec F₃(),b₁)] )

proof end;

set c₃ = intpos 1;

set c₄ = intpos 2;

set c₅ = intpos 3;

definition

let c₆, c₇ be Nat;
func sum c₁,c₂ -> Program-block equals :: SCPINVAR:def 1
((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- a₁))) ';' ((intpos 3) := (a₂ + 1))) ';' (while<0 GBP ,2,(((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)));
coherence ;

end;

:: deftheorem Def1 defines sum SCPINVAR:def 1 :

theorem Th8: :: SCPINVAR:8

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃, b₄, b₅ being Int_position
for b₆, b₇, b₈ being Nat
for b₉ being FinSequence of INT st card b₂ > 0 & b₉ is_FinSequence_on b₁,b₈ & len b₉ = b₆ & b₁ . b₄ = 0 & b₁ . b₃ = 0 & b₁ . (intpos b₇) = - b₆ & b₁ . b₅ = b₈ + 1 & ( for b₁₀ being State of SCMPDS st ex b₁₁ being FinSequence of INT st
( b₁₁ is_FinSequence_on b₁,b₈ & len b₁₁ = (b₁₀ . (intpos b₇)) + b₆ & b₁₀ . b₄ = Sum b₁₁ & b₁₀ . b₅ = (b₈ + 1) + (len b₁₁) ) & b₁₀ . b₃ = 0 & b₁₀ . (intpos b₇) < 0 & ( for b₁₁ being Nat st b₁₁ > b₈ holds
b₁₀ . (intpos b₁₁) = b₁ . (intpos b₁₁) ) holds
( (IExec b₂,b₁₀) . b₃ = 0 & b₂ is_closed_on b₁₀ & b₂ is_halting_on b₁₀ & (IExec b₂,b₁₀) . (intpos b₇) = (b₁₀ . (intpos b₇)) + 1 & ex b₁₁ being FinSequence of INT st
( b₁₁ is_FinSequence_on b₁,b₈ & len b₁₁ = ((b₁₀ . (intpos b₇)) + b₆) + 1 & (IExec b₂,b₁₀) . b₅ = (b₈ + 1) + (len b₁₁) & (IExec b₂,b₁₀) . b₄ = Sum b₁₁ ) & ( for b₁₁ being Nat st b₁₁ > b₈ holds
(IExec b₂,b₁₀) . (intpos b₁₁) = b₁ . (intpos b₁₁) ) ) ) holds
( (IExec (while<0 b₃,b₇,b₂),b₁) . b₄ = Sum b₉ & while<0 b₃,b₇,b₂ is_closed_on b₁ & while<0 b₃,b₇,b₂ is_halting_on b₁ )

proof end;

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

set c₇ = AddTo GBP ,2,1;

set c₈ = AddTo GBP ,3,1;

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

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

Lemma9: for b₁ being State of SCMPDS
for b₂ being Nat st b₁ . GBP = 0 & b₁ . (intpos 3) = b₂ holds
( (IExec (((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),b₁) . GBP = 0 & (IExec (((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),b₁) . (intpos 1) = (b₁ . (intpos 1)) + (b₁ . (intpos b₂)) & (IExec (((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),b₁) . (intpos 2) = (b₁ . (intpos 2)) + 1 & (IExec (((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),b₁) . (intpos 3) = b₂ + 1 & ( for b₃ being Nat st b₃ > 3 holds
(IExec (((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),b₁) . (intpos b₃) = b₁ . (intpos b₃) ) )

proof end;

Lemma10: card (((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)) = 3

proof end;

Lemma11: for b₁ being State of SCMPDS
for b₂, b₃ being Nat
for b₄ being FinSequence of INT st b₃ >= 3 & b₄ is_FinSequence_on b₁,b₃ & len b₄ = b₂ & b₁ . (intpos 1) = 0 & b₁ . GBP = 0 & b₁ . (intpos 2) = - b₂ & b₁ . (intpos 3) = b₃ + 1 holds
( (IExec (while<0 GBP ,2,(((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1))),b₁) . (intpos 1) = Sum b₄ & while<0 GBP ,2,(((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)) is_closed_on b₁ & while<0 GBP ,2,(((AddTo GBP ,1,(intpos 3),0) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)) is_halting_on b₁ )

proof end;

Lemma12: for b₁ being State of SCMPDS
for b₂, b₃ being Nat
for b₄ being FinSequence of INT st b₃ >= 3 & b₄ is_FinSequence_on b₁,b₃ & len b₄ = b₂ holds
( (IExec (sum b₂,b₃),b₁) . (intpos 1) = Sum b₄ & sum b₂,b₃ is_halting_on b₁ )

proof end;

theorem Th9: :: SCPINVAR:9

for b₁ being State of SCMPDS
for b₂, b₃ being Nat
for b₄ being FinSequence of INT st b₃ >= 3 & b₄ is_FinSequence_on b₁,b₃ & len b₄ = b₂ holds
( (IExec (sum b₂,b₃),b₁) . (intpos 1) = Sum b₄ & sum b₂,b₃ is parahalting )

proof end;

scheme :: SCPINVAR:sch 2
s2{ F₁( State of SCMPDS ) -> Nat, F₂() -> State of SCMPDS , F₃() -> shiftable No-StopCode Program-block, 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

E13: card F₃() > 0 and
E14: for b₁ being State of SCMPDS st P₁[ Dstate b₁] holds
( F₁((Dstate b₁)) = 0 iff b₁ . (DataLoc (F₂() . F₄()),F₅()) <= 0 ) and
E15: P₁[ Dstate F₂()] and
E16: for b₁ being State of SCMPDS st P₁[ Dstate b₁] & b₁ . F₄() = F₂() . F₄() & b₁ . (DataLoc (F₂() . F₄()),F₅()) > 0 holds
( (IExec F₃(),b₁) . F₄() = b₁ . F₄() & F₃() is_closed_on b₁ & F₃() is_halting_on b₁ & F₁((Dstate (IExec F₃(),b₁))) < F₁((Dstate b₁)) & P₁[ Dstate (IExec F₃(),b₁)] )

proof end;

definition

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

end;

:: deftheorem Def2 defines Fib-macro SCPINVAR:def 2 :

theorem Th10: :: SCPINVAR:10

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃, b₄, b₅ being Int_position
for b₆, b₇ being Nat st card b₂ > 0 & b₁ . b₃ = 0 & b₁ . b₄ = 0 & b₁ . b₅ = 1 & b₁ . (intpos b₇) = b₆ & ( for b₈ being State of SCMPDS
for b₉ being Nat st b₆ = (b₈ . (intpos b₇)) + b₉ & b₈ . b₄ = Fib b₉ & b₈ . b₅ = Fib (b₉ + 1) & b₈ . b₃ = 0 & b₈ . (intpos b₇) > 0 holds
( (IExec b₂,b₈) . b₃ = 0 & b₂ is_closed_on b₈ & b₂ is_halting_on b₈ & (IExec b₂,b₈) . (intpos b₇) = (b₈ . (intpos b₇)) - 1 & (IExec b₂,b₈) . b₄ = Fib (b₉ + 1) & (IExec b₂,b₈) . b₅ = Fib ((b₉ + 1) + 1) ) ) holds
( (IExec (while>0 b₃,b₇,b₂),b₁) . b₄ = Fib b₆ & (IExec (while>0 b₃,b₇,b₂),b₁) . b₅ = Fib (b₆ + 1) & while>0 b₃,b₇,b₂ is_closed_on b₁ & while>0 b₃,b₇,b₂ is_halting_on b₁ )

proof end;

set c₁₁ = GBP ,4 := GBP ,2;

set c₁₂ = AddTo GBP ,2,GBP ,1;

set c₁₃ = GBP ,1 := GBP ,4;

set c₁₄ = AddTo GBP ,3,(- 1);

set c₁₅ = (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1));

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

Lemma14: for b₁ being State of SCMPDS st b₁ . GBP = 0 holds
( (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),b₁) . GBP = 0 & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),b₁) . (intpos 1) = b₁ . (intpos 2) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),b₁) . (intpos 2) = (b₁ . (intpos 1)) + (b₁ . (intpos 2)) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),b₁) . (intpos 3) = (b₁ . (intpos 3)) - 1 )

proof end;

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

proof end;

Lemma16: for b₁ being State of SCMPDS
for b₂ being Nat st b₁ . GBP = 0 & b₁ . (intpos 1) = 0 & b₁ . (intpos 2) = 1 & b₁ . (intpos 3) = b₂ holds
( (IExec (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))),b₁) . (intpos 1) = Fib b₂ & (IExec (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))),b₁) . (intpos 2) = Fib (b₂ + 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 b₁ & while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))) is_halting_on b₁ )

proof end;

Lemma17: for b₁ being State of SCMPDS
for b₂ being Nat holds
( (IExec (Fib-macro b₂),b₁) . (intpos 1) = Fib b₂ & (IExec (Fib-macro b₂),b₁) . (intpos 2) = Fib (b₂ + 1) & Fib-macro b₂ is_halting_on b₁ )

proof end;

theorem Th11: :: SCPINVAR:11

for b₁ being State of SCMPDS
for b₂ being Nat holds
( (IExec (Fib-macro b₂),b₁) . (intpos 1) = Fib b₂ & (IExec (Fib-macro b₂),b₁) . (intpos 2) = Fib (b₂ + 1) & Fib-macro b₂ is parahalting )

proof end;

definition

let c₁₇ be Int_position ;
let c₁₈ be Integer;
let c₁₉ be Program-block;
func while<>0 c₁,c₂,c₃ -> Program-block equals :: SCPINVAR:def 3
(((a₁,a₂ <>0_goto 2) ';' (goto ((card a₃) + 2))) ';' a₃) ';' (goto (- ((card a₃) + 2)));
coherence ;

end;

:: deftheorem Def3 defines while<>0 SCPINVAR:def 3 :

theorem Th12: :: SCPINVAR:12

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds card (while<>0 b₁,b₂,b₃) = (card b₃) + 3

proof end;

Lemma19: for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds card (stop (while<>0 b₁,b₂,b₃)) = (card b₃) + 4

proof end;

theorem Th13: :: SCPINVAR:13

for b₁ being Int_position
for b₂ being Integer
for b₃ being Nat
for b₄ being Program-block holds
( b₃ < (card b₄) + 3 iff inspos b₃ in dom (while<>0 b₁,b₂,b₄) )

proof end;

theorem Th14: :: SCPINVAR:14

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds
( inspos 0 in dom (while<>0 b₁,b₂,b₃) & inspos 1 in dom (while<>0 b₁,b₂,b₃) )

proof end;

theorem Th15: :: SCPINVAR:15

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds
( (while<>0 b₁,b₂,b₃) . (inspos 0) = b₁,b₂ <>0_goto 2 & (while<>0 b₁,b₂,b₃) . (inspos 1) = goto ((card b₃) + 2) & (while<>0 b₁,b₂,b₃) . (inspos ((card b₃) + 2)) = goto (- ((card b₃) + 2)) )

proof end;

Lemma23: for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds while<>0 b₁,b₂,b₃ = (b₁,b₂ <>0_goto 2) ';' (((goto ((card b₃) + 2)) ';' b₃) ';' (goto (- ((card b₃) + 2))))

proof end;

theorem Th16: :: SCPINVAR:16

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being Int_position
for b₄ being Integer st b₁ . (DataLoc (b₁ . b₃),b₄) = 0 holds
( while<>0 b₃,b₄,b₂ is_closed_on b₁ & while<>0 b₃,b₄,b₂ is_halting_on b₁ )

proof end;

theorem Th17: :: SCPINVAR:17

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃, b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₃),b₅) = 0 holds
IExec (while<>0 b₃,b₅,b₂),b₁ = b₁ +* (Start-At (inspos ((card b₂) + 3)))

proof end;

theorem Th18: :: SCPINVAR:18

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being Int_position
for b₄ being Integer st b₁ . (DataLoc (b₁ . b₃),b₄) = 0 holds
IC (IExec (while<>0 b₃,b₄,b₂),b₁) = inspos ((card b₂) + 3)

proof end;

theorem Th19: :: SCPINVAR:19

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃, b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₃),b₅) = 0 holds
(IExec (while<>0 b₃,b₅,b₂),b₁) . b₄ = b₁ . b₄

proof end;

Lemma27: for b₁ being Program-block
for b₂ being Int_position
for b₃ being Integer holds Shift b₁,2 c= while<>0 b₂,b₃,b₁

proof end;

registration

let c₁₇ be shiftable Program-block;
let c₁₈ be Int_position ;
let c₁₉ be Integer;
cluster while<>0 a₂,a₃,a₁ -> shiftable ;
correctness

proof end;

end;

registration

let c₁₇ be No-StopCode Program-block;
let c₁₈ be Int_position ;
let c₁₉ be Integer;
cluster while<>0 a₂,a₃,a₁ -> No-StopCode ;
correctness

proof end;

end;

scheme :: SCPINVAR:sch 3
s3{ F₁( State of SCMPDS ) -> Nat, F₂() -> State of SCMPDS , F₃() -> shiftable No-StopCode Program-block, 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

E28: card F₃() > 0 and
E29: for b₁ being State of SCMPDS st P₁[ Dstate b₁] & F₁((Dstate b₁)) = 0 holds
b₁ . (DataLoc (F₂() . F₄()),F₅()) = 0 and
E30: P₁[ Dstate F₂()] and
E31: for b₁ being State of SCMPDS st P₁[ Dstate b₁] & b₁ . F₄() = F₂() . F₄() & b₁ . (DataLoc (F₂() . F₄()),F₅()) <> 0 holds
( (IExec F₃(),b₁) . F₄() = b₁ . F₄() & F₃() is_closed_on b₁ & F₃() is_halting_on b₁ & F₁((Dstate (IExec F₃(),b₁))) < F₁((Dstate b₁)) & P₁[ Dstate (IExec F₃(),b₁)] )

proof end;

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

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

provided

E28: card F₃() > 0 and
E29: F₂() . (DataLoc (F₂() . F₄()),F₅()) <> 0 and
E30: for b₁ being State of SCMPDS st P₁[ Dstate b₁] & F₁((Dstate b₁)) = 0 holds
b₁ . (DataLoc (F₂() . F₄()),F₅()) = 0 and
E31: P₁[ Dstate F₂()] and
E32: for b₁ being State of SCMPDS st P₁[ Dstate b₁] & b₁ . F₄() = F₂() . F₄() & b₁ . (DataLoc (F₂() . F₄()),F₅()) <> 0 holds
( (IExec F₃(),b₁) . F₄() = b₁ . F₄() & F₃() is_closed_on b₁ & F₃() is_halting_on b₁ & F₁((Dstate (IExec F₃(),b₁))) < F₁((Dstate b₁)) & P₁[ Dstate (IExec F₃(),b₁)] )

proof end;

scheme :: SCPINVAR:sch 5
s5{ F₁( State of SCMPDS ) -> Nat, F₂() -> State of SCMPDS , F₃() -> shiftable No-StopCode Program-block, 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

E28: card F₃() > 0 and
E29: for b₁ being State of SCMPDS st P₁[ Dstate b₁] holds
( F₁((Dstate b₁)) = 0 iff b₁ . (DataLoc (F₂() . F₄()),F₅()) = 0 ) and
E30: P₁[ Dstate F₂()] and
E31: for b₁ being State of SCMPDS st P₁[ Dstate b₁] & b₁ . F₄() = F₂() . F₄() & b₁ . (DataLoc (F₂() . F₄()),F₅()) <> 0 holds
( (IExec F₃(),b₁) . F₄() = b₁ . F₄() & F₃() is_closed_on b₁ & F₃() is_halting_on b₁ & F₁((Dstate (IExec F₃(),b₁))) < F₁((Dstate b₁)) & P₁[ Dstate (IExec F₃(),b₁)] )

proof end;

theorem Th20: :: SCPINVAR:20

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃, b₄, b₅ being Int_position
for b₆, b₇ being Integer st card b₂ > 0 & b₁ . b₃ = b₇ & b₁ . b₄ > 0 & b₁ . b₅ > 0 & b₁ . (DataLoc b₇,b₆) = (b₁ . b₄) - (b₁ . b₅) & ( for b₈ being State of SCMPDS st b₈ . b₄ > 0 & b₈ . b₅ > 0 & b₈ . b₃ = b₇ & b₈ . (DataLoc b₇,b₆) = (b₈ . b₄) - (b₈ . b₅) & b₈ . b₄ <> b₈ . b₅ holds
( (IExec b₂,b₈) . b₃ = b₇ & b₂ is_closed_on b₈ & b₂ is_halting_on b₈ & ( b₈ . b₄ > b₈ . b₅ implies ( (IExec b₂,b₈) . b₄ = (b₈ . b₄) - (b₈ . b₅) & (IExec b₂,b₈) . b₅ = b₈ . b₅ ) ) & ( b₈ . b₄ <= b₈ . b₅ implies ( (IExec b₂,b₈) . b₅ = (b₈ . b₅) - (b₈ . b₄) & (IExec b₂,b₈) . b₄ = b₈ . b₄ ) ) & (IExec b₂,b₈) . (DataLoc b₇,b₆) = ((IExec b₂,b₈) . b₄) - ((IExec b₂,b₈) . b₅) ) ) holds
( while<>0 b₃,b₆,b₂ is_closed_on b₁ & while<>0 b₃,b₆,b₂ is_halting_on b₁ & ( b₁ . (DataLoc (b₁ . b₃),b₆) <> 0 implies IExec (while<>0 b₃,b₆,b₂),b₁ = IExec (while<>0 b₃,b₆,b₂),(IExec b₂,b₁) ) )

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 ;

end;

:: deftheorem Def4 defines GCD-Algorithm SCPINVAR:def 4 :

theorem Th21: :: SCPINVAR:21

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃, b₄, b₅ being Int_position
for b₆, b₇ being Integer st card b₂ > 0 & b₁ . b₃ = b₇ & b₁ . b₄ > 0 & b₁ . b₅ > 0 & b₁ . (DataLoc b₇,b₆) = (b₁ . b₄) - (b₁ . b₅) & ( for b₈ being State of SCMPDS st b₈ . b₄ > 0 & b₈ . b₅ > 0 & b₈ . b₃ = b₇ & b₈ . (DataLoc b₇,b₆) = (b₈ . b₄) - (b₈ . b₅) & b₈ . b₄ <> b₈ . b₅ holds
( (IExec b₂,b₈) . b₃ = b₇ & b₂ is_closed_on b₈ & b₂ is_halting_on b₈ & ( b₈ . b₄ > b₈ . b₅ implies ( (IExec b₂,b₈) . b₄ = (b₈ . b₄) - (b₈ . b₅) & (IExec b₂,b₈) . b₅ = b₈ . b₅ ) ) & ( b₈ . b₄ <= b₈ . b₅ implies ( (IExec b₂,b₈) . b₅ = (b₈ . b₅) - (b₈ . b₄) & (IExec b₂,b₈) . b₄ = b₈ . b₄ ) ) & (IExec b₂,b₈) . (DataLoc b₇,b₆) = ((IExec b₂,b₈) . b₄) - ((IExec b₂,b₈) . b₅) ) ) holds
( (IExec (while<>0 b₃,b₆,b₂),b₁) . b₄ = (b₁ . b₄) gcd (b₁ . b₅) & (IExec (while<>0 b₃,b₆,b₂),b₁) . b₅ = (b₁ . b₄) gcd (b₁ . b₅) )

proof end;

set c₁₇ = GBP := 0;

set c₁₈ = GBP ,3 := GBP ,1;

set c₁₉ = SubFrom GBP ,3,GBP ,2;

set c₂₀ = Load (SubFrom GBP ,1,GBP ,2);

set c₂₁ = Load (SubFrom GBP ,2,GBP ,1);

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

set c₂₃ = GBP ,3 := GBP ,1;

set c₂₄ = SubFrom GBP ,3,GBP ,2;

set c₂₅ = ((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 c₂₆ = 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));

Lemma30: 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;

Lemma31: 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 Th22: :: SCPINVAR:22

card GCD-Algorithm = 12

proof end;

Lemma32: for b₁ being State of SCMPDS st b₁ . GBP = 0 holds
( ( b₁ . (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)),b₁) . (intpos 1) = (b₁ . (intpos 1)) - (b₁ . (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)),b₁) . (intpos 2) = b₁ . (intpos 2) ) ) & ( b₁ . (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)),b₁) . (intpos 2) = (b₁ . (intpos 2)) - (b₁ . (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)),b₁) . (intpos 1) = b₁ . (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)),b₁) . 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)),b₁) . (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)),b₁) . (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)),b₁) . (intpos 2)) )

proof end;

Lemma33: for b₁ being State of SCMPDS st b₁ . GBP = 0 & b₁ . (intpos 1) > 0 & b₁ . (intpos 2) > 0 & b₁ . (intpos 3) = (b₁ . (intpos 1)) - (b₁ . (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))),b₁) . (intpos 1) = (b₁ . (intpos 1)) gcd (b₁ . (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))),b₁) . (intpos 2) = (b₁ . (intpos 1)) gcd (b₁ . (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 b₁ & 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 b₁ )

proof end;

set c₂₇ = (((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)));

Lemma34: for b₁ being State of SCMPDS st b₁ . (intpos 1) > 0 & b₁ . (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)))),b₁) . (intpos 1) = (b₁ . (intpos 1)) gcd (b₁ . (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)))),b₁) . (intpos 2) = (b₁ . (intpos 1)) gcd (b₁ . (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 b₁ & (((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 b₁ )

proof end;

theorem Th23: :: SCPINVAR:23

for b₁ being State of SCMPDS
for b₂, b₃ being Integer st b₁ . (intpos 1) = b₂ & b₁ . (intpos 2) = b₃ & b₂ > 0 & b₃ > 0 holds
( (IExec GCD-Algorithm ,b₁) . (intpos 1) = b₂ gcd b₃ & (IExec GCD-Algorithm ,b₁) . (intpos 2) = b₂ gcd b₃ & GCD-Algorithm is_closed_on b₁ & GCD-Algorithm is_halting_on b₁ ) by Lemma34;