let P be 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 )
let s be 0 -started State of SCMPDS; ( s . (intpos 1) > 0 & s . (intpos 2) > 0 implies ( (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 ) )
I:
Initialize s = s
by MEMSTR_0:44;
assume A1:
( s . (intpos 1) > 0 & s . (intpos 2) > 0 )
; ( (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 )
set t0 = s;
set Q0 = P;
set t1 = IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s);
set t2 = IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s);
set Q1 = P;
set t3 = Exec ((GBP := 0),s);
set a = GBP ;
A5: (Exec ((GBP := 0),s)) . (intpos 1) =
s . (intpos 1)
by AMI_3:10, SCMPDS_2:45
.=
s . (intpos 1)
;
A6:
(Exec ((GBP := 0),s)) . GBP = 0
by SCMPDS_2:45;
then A7:
DataLoc (((Exec ((GBP := 0),s)) . GBP),3) = intpos (0 + 3)
by SCMP_GCD:1;
1 <> abs (((Exec ((GBP := 0),s)) . GBP) + 3)
by A6, ABSVALUE:def 1;
then A8:
intpos 1 <> DataLoc (((Exec ((GBP := 0),s)) . GBP),3)
by ZFMISC_1:27;
A9: (IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . (intpos 1) =
(Exec (((GBP,3) := (GBP,1)),(Exec ((GBP := 0),s)))) . (intpos 1)
by SCMPDS_5:42
.=
s . (intpos 1)
by A5, A8, SCMPDS_2:47
;
A10: (Exec ((GBP := 0),s)) . (intpos 2) =
s . (intpos 2)
by AMI_3:10, SCMPDS_2:45
.=
s . (intpos 2)
;
A11: (IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . (intpos 3) =
(Exec (((GBP,3) := (GBP,1)),(Exec ((GBP := 0),s)))) . (intpos 3)
by SCMPDS_5:42
.=
(Exec ((GBP := 0),s)) . (DataLoc (((Exec ((GBP := 0),s)) . GBP),1))
by A7, SCMPDS_2:47
.=
s . (intpos 1)
by A6, A5, SCMP_GCD:1
;
2 <> abs (((Exec ((GBP := 0),s)) . GBP) + 3)
by A6, ABSVALUE:def 1;
then A12:
intpos 2 <> DataLoc (((Exec ((GBP := 0),s)) . GBP),3)
by ZFMISC_1:27;
A13: (IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . (intpos 2) =
(Exec (((GBP,3) := (GBP,1)),(Exec ((GBP := 0),s)))) . (intpos 2)
by SCMPDS_5:42
.=
s . (intpos 2)
by A10, A12, SCMPDS_2:47
;
0 <> abs (((Exec ((GBP := 0),s)) . GBP) + 3)
by A6, ABSVALUE:def 1;
then A14:
GBP <> DataLoc (((Exec ((GBP := 0),s)) . GBP),3)
by ZFMISC_1:27;
A15: (IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP =
(Exec (((GBP,3) := (GBP,1)),(Exec ((GBP := 0),s)))) . GBP
by SCMPDS_5:42
.=
0
by A6, A14, SCMPDS_2:47
;
then A16:
DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP),3) = intpos (0 + 3)
by SCMP_GCD:1;
0 <> abs (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP) + 3)
by A15, ABSVALUE:def 1;
then A17:
GBP <> DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP),3)
by ZFMISC_1:27;
A18: (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . GBP =
(Exec ((SubFrom (GBP,3,GBP,2)),(IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)))) . GBP
by SCMPDS_5:41
.=
0
by A15, A17, SCMPDS_2:50
;
1 <> abs (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP) + 3)
by A15, ABSVALUE:def 1;
then A19:
intpos 1 <> DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP),3)
by ZFMISC_1:27;
A20: (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 1) =
(Exec ((SubFrom (GBP,3,GBP,2)),(IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)))) . (intpos 1)
by SCMPDS_5:41
.=
s . (intpos 1)
by A9, A19, SCMPDS_2:50
;
2 <> abs (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP) + 3)
by A15, ABSVALUE:def 1;
then A21:
intpos 2 <> DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP),3)
by ZFMISC_1:27;
A22: (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 2) =
(Exec ((SubFrom (GBP,3,GBP,2)),(IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)))) . (intpos 2)
by SCMPDS_5:41
.=
s . (intpos 2)
by A13, A21, SCMPDS_2:50
;
X1:
(Initialize (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s))) . (intpos 1) = (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 1)
by SCMPDS_5:15;
X2:
(Initialize (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s))) . (intpos 2) = (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 2)
by SCMPDS_5:15;
A23: (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 3) =
(Exec ((SubFrom (GBP,3,GBP,2)),(IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)))) . (intpos 3)
by SCMPDS_5:41
.=
((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . (intpos 3)) - ((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . (DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP),2)))
by A16, SCMPDS_2:50
.=
((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 1)) - ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 2))
by A15, A13, A11, A20, A22, SCMP_GCD:1
;
X0:
(Initialize (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s))) . GBP = (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . GBP
by SCMPDS_5:15;
X3:
(Initialize (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s))) . (intpos 3) = (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 3)
by SCMPDS_5:15;
B25:
( 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 Initialize (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,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 Initialize (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)),P )
by A1, A18, A20, A22, Lm15, X1, X2, A23, X0, X3;
A24:
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 IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s),P
proof
for
k being
Element of
NAT holds
IC (Comput ((P +* (stop (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))))))),(Initialize (Initialize (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)))),k)) in dom (stop (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))))))
by B25, SCMPDS_6:def 2;
hence
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 IExec (
(((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),
P,
s),
P
by SCMPDS_6:def 2;
verum
end;
A25:
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 IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s),P
proof
P +* (stop (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)))))) halts_on Initialize (Initialize (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)))
by B25, SCMPDS_6:def 3;
hence
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 IExec (
(((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),
P,
s),
P
by SCMPDS_6:def 3;
verum
end;
(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,(Initialize (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s))))) . (intpos 1) = ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 1)) gcd ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 2))
by A1, A18, A20, A22, A23, Lm15, X1, X2, X3, X0;
hence
(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))
by A20, A22, A24, A25, SCPISORT:7; ( (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 )
(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,(Initialize (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s))))) . (intpos 2) = ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 1)) gcd ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 2))
by A1, A18, A20, A22, A23, Lm15, X1, X2, X3, X0;
hence
(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))
by A20, A22, A24, A25, SCPISORT:7; ( (((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 )
thus
( (((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 )
by A24, I, A25, SCPISORT:9; verum