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; :: thesis: for md, p0 being Element of NAT st s . GBP = 0 & s . (intpos 2) = md & md >= p0 + 1 & p0 >= 7 holds
( Partition is_closed_on s & Partition is_halting_on s )
let md, n0 be Element of NAT ; :: thesis: ( s . GBP = 0 & s . (intpos 2) = md & md >= n0 + 1 & n0 >= 7 implies ( Partition is_closed_on s & Partition is_halting_on s ) )
set s2 = IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),s);
set a = GBP ;
assume that
A1: s . GBP = 0 and
A2: s . (intpos 2) = md and
A3: md >= n0 + 1 and
A4: n0 >= 7 ; :: thesis: ( Partition is_closed_on s & Partition is_halting_on s )
A5: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),s)) . (intpos 2) = s . (intpos 2) by A1, Lm28;
set m3 = md;
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),s)) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) by A1, Lm28;
then A6: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),s)) . (intpos 4) = md + ((IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),s)) . (intpos 5)) by A1, A2, Lm28;
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),s)) . (intpos 3) = (s . (intpos 2)) + 1 by A1, Lm28;
then A7: s . (intpos 2) = ((IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),s)) . (intpos 3)) - 1 ;
A8: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),s)) . GBP = 0 by A1, Lm28;
then A9: 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))),s) by A2, A3, A4, A5, A7, A6, Lm27;
A10: 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))),s) by A2, A3, A4, A8, A5, A7, A6, Lm27;
then A11: (((((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 by A9, SCPISORT:10;
A12: (((((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 by A10, A9, SCPISORT:10;
then A13: ((((((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 by A11, SCPISORT:11;
A14: ((((((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 by A11, A12, SCPISORT:11;
then A15: (((((((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 by A13, SCPISORT:11;
(((((((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 by A13, A14, SCPISORT:11;
hence ( Partition is_closed_on s & Partition is_halting_on s ) by A15, SCPISORT:11; :: thesis: verum