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 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