let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for md, p0 being Nat st s . GBP = 0 & s . (intpos 2) = md & md >= p0 + 1 & p0 >= 7 holds
( Partition is_closed_on s,P & Partition is_halting_on s,P )
set KW = (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))));
let s be 0 -started State of SCMPDS; for md, p0 being Nat st s . GBP = 0 & s . (intpos 2) = md & md >= p0 + 1 & p0 >= 7 holds
( Partition is_closed_on s,P & Partition is_halting_on s,P )
let md, n0 be Nat; ( s . GBP = 0 & s . (intpos 2) = md & md >= n0 + 1 & n0 >= 7 implies ( Partition is_closed_on s,P & Partition is_halting_on s,P ) )
set s2 = IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s));
set a = GBP ;
set P2 = P;
assume that
A1:
s . GBP = 0
and
A2:
s . (intpos 2) = md
and
A3:
md >= n0 + 1
and
A4:
n0 >= 7
; ( Partition is_closed_on s,P & Partition is_halting_on s,P )
A5:
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 2) = s . (intpos 2)
by A1, Lm27;
set m3 = md;
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2))
by A1, Lm27;
then A6:
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4) = md + ((IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5))
by A1, A2, Lm27;
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3) = (s . (intpos 2)) + 1
by A1, Lm27;
then A7:
s . (intpos 2) = ((IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3)) - 1
;
A8:
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP = 0
by A1, Lm27;
A9:
(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s)))) . GBP = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP
by SCMPDS_5:15;
A10:
(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s)))) . (intpos 2) = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 2)
by SCMPDS_5:15;
A11:
(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s)))) . (intpos 3) = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3)
by SCMPDS_5:15;
A12:
(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s)))) . (intpos 4) = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4)
by SCMPDS_5:15;
A13:
(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s)))) . (intpos 5) = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5)
by SCMPDS_5:15;
A14:
while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))) is_halting_on Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))),P
by A2, A3, A4, A5, A7, A6, Lm26, A8, A9, A10, A11, A12, A13;
A15:
while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))) is_halting_on IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s)),P
proof
P +* (stop (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) halts_on Initialize (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))))
by A14, SCMPDS_6:def 3;
hence
while>0 (
GBP,5,
(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))
is_halting_on IExec (
(((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),
P,
(Initialize s)),
P
by SCMPDS_6:def 3;
verum
end;
A16:
while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))) is_closed_on Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))),P
by A2, A3, A4, A8, A5, A7, A6, Lm26, A9, A10, A11, A12, A13;
A17:
while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))) is_closed_on IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s)),P
proof
for
k being
Nat holds
IC (Comput ((P +* (stop (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))))),(Initialize (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))))),k)) in dom (stop (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))))
by A16, SCMPDS_6:def 2;
hence
while>0 (
GBP,5,
(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))
is_closed_on IExec (
(((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),
P,
(Initialize s)),
P
by SCMPDS_6:def 2;
verum
end;
then A18:
(((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))) is_closed_on s,P
by A15, SCPISORT:9;
A19:
(((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))) is_halting_on s,P
by A17, A15, SCPISORT:9;
then A20:
((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0)) is_closed_on s,P
by A18, SCPISORT:10;
A21:
((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0)) is_halting_on s,P
by A18, A19, SCPISORT:10;
then A22:
(((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0)) is_halting_on s,P
by A20, SCPISORT:10;
(((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0)) is_closed_on s,P
by A20, A21, SCPISORT:10;
hence
( Partition is_closed_on s,P & Partition is_halting_on s,P )
by A22, SCPISORT:10; verum