begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem Th6:
theorem Th7:
set A = NAT ;
set D = SCM-Data-Loc ;
begin
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
((((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:
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 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 )
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 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))),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) ) )
Lm2:
card (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))) = 3
Lm3:
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))))),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 )
Lm4:
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)),s)) . (intpos 1) = Sum f & sum (n,p0) is_halting_on s )
theorem
begin
begin
definition
let n be
Element of
NAT ;
func Fib-macro n -> Program of
SCMPDS equals
((((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:
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
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 )
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 )
Lm6:
card (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))) = 4
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 )
Lm8:
for s being 0 -started 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 )
theorem
begin
:: 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:
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
theorem Th13:
theorem Th14:
theorem Th15:
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))))
theorem Th16:
theorem Th17:
theorem
theorem Th19:
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)
begin
theorem Th20:
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 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))) ) )
begin
definition
func GCD-Algorithm -> Program of
SCMPDS equals
(((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:
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 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) )
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
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
theorem
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)) )
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 )
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 )
theorem