set a = GBP ;
let s be State of SCMPDS ; :: thesis:
let m3, md be Element of NAT ; :: thesis:
assume that
A1: s . GBP = 0 and
A2: s . (intpos 7) > 0 and
A3: (s . (intpos 3)) + (s . (intpos 7)) = m3 and
A4: s . (intpos 3) >= 8 and
A5: s . (intpos 2) = md and
A6: md >= 8 ; :: thesis:
s . (intpos 7) >= 1 + 0 by A2, INT_1:20;
then reconsider m7 = (s . (intpos 7)) - 1 as Element of NAT by INT_1:16, XREAL_1:50;
A7: s . (intpos 7) = m7 + 1 ;
defpred S₁[ Element of NAT ] means for t being State of SCMPDS st t . GBP = 0 & t . (intpos 7) = $1 + 1 & (t . (intpos 3)) + (t . (intpos 7)) = m3 & t . (intpos 3) >= 8 & t . (intpos 2) = md holds
( (IExec (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 ))))),t) . GBP = 0 & (IExec (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 ))))),t) . (intpos 1) = t . (intpos 1) & (IExec (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 ))))),t) . (intpos 7) = 0 & (IExec (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 ))))),t) . (intpos 2) = t . (intpos 2) & (IExec (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 ))))),t) . (intpos 4) = t . (intpos 4) & ( for i being Element of NAT st i >= 8 holds
(IExec (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 ))))),t) . (intpos i) = t . (intpos i) ) & ex m5, mE3 being Element of NAT st
( m5 = (IExec (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 ))))),t) . (intpos 5) & (IExec (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 ))))),t) . (intpos 3) = mE3 & mE3 + m5 = m3 & m5 <= t . (intpos 7) & ( for i being Element of NAT st t . (intpos 3) <= i & i < mE3 holds
(IExec (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 ))))),t) . (intpos md) > (IExec (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 ))))),t) . (intpos i) ) & ( m5 = 0 or (IExec (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 ))))),t) . (intpos md) <= (IExec (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 ))))),t) . (intpos mE3) ) ) );

A8: now

let k be Element of NAT ; :: thesis:
assume A9: S₁[k] ; :: thesis:

now

let t be State of SCMPDS ; :: thesis:
set b = DataLoc (t . GBP ),7;
assume that
A10: t . GBP = 0 and
A11: t . (intpos 7) = (k + 1) + 1 and
A12: (t . (intpos 3)) + (t . (intpos 7)) = m3 and
A13: t . (intpos 3) >= 8 and
A14: t . (intpos 2) = md ; :: thesis:
reconsider me = t . (intpos 3) as Element of NAT by A13, INT_1:16;
set It = IExec (((((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 )))),t;
A15: ( t . (intpos md) > t . (intpos me) implies ( (IExec (((((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 )))),t) . (intpos 7) = (t . (intpos 7)) - 1 & (IExec (((((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 )))),t) . (intpos 3) = (t . (intpos 3)) + 1 & (IExec (((((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 )))),t) . (intpos 5) = (t . (intpos 7)) - 1 ) ) by A6, A10, A13, A14, Lm14;
A16: DataLoc (t . GBP ),7 = intpos (0 + 7) by A10, SCMP_GCD:5;

A17: now

let v be State of SCMPDS ; :: thesis:
assume that
A18: v . (intpos 3) >= 8 and
A19: v . (intpos 2) = t . (intpos 2) and
A20: v . GBP = t . GBP and
A21: v . (DataLoc (t . GBP ),7) > 0 ; :: thesis:
reconsider ME = v . (intpos 3) as Element of NAT by A18, INT_1:16;
A22: ME = v . (intpos 3) ;
hence (IExec (((((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 )))),v) . GBP = v . GBP by A6, A10, A14, A18, A19, A20, Lm14; :: thesis:
thus ( ((((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 ))) is_closed_on v & ((((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 ))) is_halting_on v ) by SCMPDS_6:34, SCMPDS_6:35; :: thesis:
A23: ( v . (intpos md) > v . (intpos ME) implies ( (IExec (((((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 )))),v) . (intpos 7) = (v . (intpos 7)) - 1 & (IExec (((((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 )))),v) . (intpos 3) = (v . (intpos 3)) + 1 & (IExec (((((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 )))),v) . (intpos 5) = (v . (intpos 7)) - 1 ) ) by A6, A10, A14, A18, A19, A20, Lm14;

hereby :: thesis:

per cases ;

suppose A24: v . (intpos md) > v . (intpos ME) ; :: thesis:

hence (IExec (((((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 )))),v) . (DataLoc (t . GBP ),7) < v . (DataLoc (t . GBP ),7) by A16, A23, XREAL_1:148; :: thesis:
A25: (v . (intpos 3)) + 1 > v . (intpos 3) by XREAL_1:31;
(IExec (((((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 )))),v) . (intpos 3) = (v . (intpos 3)) + 1 by A6, A10, A14, A18, A19, A20, A24, Lm14;
hence (IExec (((((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 )))),v) . (intpos 3) >= 8 by A18, A25, XXREAL_0:2; :: thesis:

end;

suppose A26: v . (intpos md) <= v . (intpos ME) ; :: thesis:

end;

thus (IExec (((((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 )))),v) . (intpos 2) = v . (intpos 2) by A6, A10, A14, A18, A19, A20, A22, Lm14; :: thesis:

end;

A27: ( t . (intpos md) <= t . (intpos me) implies ( (IExec (((((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 )))),t) . (intpos 7) = 0 & (IExec (((((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 )))),t) . (intpos 3) = t . (intpos 3) & (IExec (((((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 )))),t) . (intpos 5) = t . (intpos 7) ) ) by A6, A10, A13, A14, Lm14;
A28: me = t . (intpos 3) ;
then A29: (IExec (((((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 )))),t) . GBP = 0 by A6, A10, A13, A14, Lm14;
then A30: DataLoc ((IExec (((((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 )))),t) . GBP ),7 = intpos (0 + 7) by SCMP_GCD:5;
A31: (IExec (((((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 )))),t) . (intpos 1) = t . (intpos 1) by A6, A10, A13, A14, A28, Lm14;
A32: (IExec (((((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 )))),t) . (intpos 4) = t . (intpos 4) by A6, A10, A13, A14, A28, Lm14;
A33: (IExec (((((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 )))),t) . (intpos 2) = t . (intpos 2) by A6, A10, A13, A14, A28, Lm14;

per cases ;

suppose A34: t . (intpos md) > t . (intpos me) ; :: thesis:

then t . (intpos 3) < (IExec (((((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 )))),t) . (intpos 3) by A15, XREAL_1:31;
then A35: (IExec (((((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 )))),t) . (intpos 3) >= 8 by A13, XXREAL_0:2;
A36: ((IExec (((((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 )))),t) . (intpos 3)) + ((IExec (((((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 )))),t) . (intpos 7)) = m3 by A12, A15, A34;
then consider m5, mE3 being Element of NAT such that
A37: m5 = (IExec (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 ))))),(IExec (((((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 )))),t)) . (intpos 5) and
A38: (IExec (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 ))))),(IExec (((((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 )))),t)) . (intpos 3) = mE3 and
A39: mE3 + m5 = m3 and
A40: m5 <= (IExec (((((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 )))),t) . (intpos 7) and
A41: for i being Element of NAT st (IExec (((((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 )))),t) . (intpos 3) <= i & i < mE3 holds
(IExec (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 ))))),(IExec (((((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 )))),t)) . (intpos md) > (IExec (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 ))))),(IExec (((((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 )))),t)) . (intpos i) and
A42: ( m5 = 0 or (IExec (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 ))))),(IExec (((((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 )))),t)) . (intpos md) <= (IExec (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 ))))),(IExec (((((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 )))),t)) . (intpos mE3) ) by A9, A11, A12, A14, A29, A33, A15, A27, A35;
A43: IExec (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 ))))),t = IExec (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 ))))),(IExec (((((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 )))),t) by A11, A13, A16, A17, Lm12, Th6;
hence (IExec (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 ))))),t) . GBP = 0 by A9, A11, A12, A14, A29, A33, A15, A27, A35, A36; :: thesis:
thus (IExec (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 ))))),t) . (intpos 1) = t . (intpos 1) by A9, A11, A12, A14, A29, A31, A33, A15, A27, A35, A36, A43; :: thesis:
thus (IExec (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 ))))),t) . (intpos 7) = 0 by A9, A11, A12, A14, A29, A33, A15, A27, A35, A36, A43; :: thesis:
thus (IExec (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 ))))),t) . (intpos 2) = t . (intpos 2) by A9, A11, A12, A14, A29, A33, A15, A27, A35, A36, A43; :: thesis:
thus (IExec (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 ))))),t) . (intpos 4) = t . (intpos 4) by A9, A11, A12, A14, A29, A33, A32, A15, A27, A35, A36, A43; :: thesis:

A44: now

let i be Element of NAT ; :: thesis:
assume A45: i >= 8 ; :: thesis:
hence (IExec (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 ))))),t) . (intpos i) = (IExec (((((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 )))),t) . (intpos i) by A9, A11, A12, A14, A29, A33, A15, A27, A35, A36, A43
.= t . (intpos i) by A6, A10, A13, A14, A28, A45, Lm14 ;
:: thesis:

end;

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume that
A47: t . (intpos 3) <= i and
A48: i < mE3 ; :: thesis:

per cases ;

suppose A49: i = t . (intpos 3) ; :: thesis:

(IExec (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 ))))),t) . (intpos me) = t . (intpos me) by A13, A44;
hence (IExec (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 ))))),t) . (intpos md) > (IExec (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 ))))),t) . (intpos i) by A6, A34, A44, A49; :: thesis:

end;

suppose i <> t . (intpos 3) ; :: thesis:

then t . (intpos 3) < i by A47, XXREAL_0:1;
then (IExec (((((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 )))),t) . (intpos 3) <= i by A46, INT_1:20;
hence (IExec (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 ))))),t) . (intpos md) > (IExec (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 ))))),t) . (intpos i) by A43, A41, A48; :: thesis:

end;

thus ( m5 = 0 or (IExec (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 ))))),t) . (intpos md) <= (IExec (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 ))))),t) . (intpos mE3) ) by A43, A42; :: thesis:

end;

suppose A50: t . (intpos md) <= t . (intpos me) ; :: thesis:

A51: now

let x be Int_position ; :: thesis:
thus (IExec (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 ))))),t) . x = (IExec (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 ))))),(IExec (((((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 )))),t)) . x by A11, A13, A16, A17, Lm12, Th6
.= (IExec (((((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 )))),t) . x by A27, A30, A50, SCMPDS_8:23 ; :: thesis:

end;

A52: now

let i be Element of NAT ; :: thesis:
assume A53: i >= 8 ; :: thesis:
thus (IExec (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 ))))),t) . (intpos i) = (IExec (((((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 )))),t) . (intpos i) by A51
.= t . (intpos i) by A6, A10, A13, A14, A28, A53, Lm14 ; :: thesis:

end;

hence for i being Element of NAT st i >= 8 holds
(IExec (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 ))))),t) . (intpos i) = t . (intpos i) ; :: thesis:
take m5 = (k + 1) + 1; :: thesis:
take mE3 = me; :: thesis:
thus (IExec (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 ))))),t) . (intpos 5) = m5 by A11, A27, A50, A51; :: thesis:
thus (IExec (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 ))))),t) . (intpos 3) = mE3 by A27, A50, A51; :: thesis:
thus mE3 + m5 = m3 by A11, A12; :: thesis:
thus m5 <= t . (intpos 7) by A11; :: thesis:
thus for i being Element of NAT st t . (intpos 3) <= i & i < mE3 holds
(IExec (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 ))))),t) . (intpos md) > (IExec (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 ))))),t) . (intpos i) ; :: thesis:
(IExec (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 ))))),t) . (intpos me) = t . (intpos me) by A13, A52;
hence ( m5 = 0 or (IExec (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 ))))),t) . (intpos md) <= (IExec (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 ))))),t) . (intpos mE3) ) by A6, A50, A52; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

now

let t be State of SCMPDS ; :: thesis:
set b = DataLoc (t . GBP ),7;
assume that
A54: t . GBP = 0 and
A55: t . (intpos 7) = 0 + 1 and
A56: (t . (intpos 3)) + (t . (intpos 7)) = m3 and
A57: t . (intpos 3) >= 8 and
A58: t . (intpos 2) = md ; :: thesis:
reconsider me = t . (intpos 3) as Element of NAT by A57, INT_1:16;
set It = IExec (((((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 )))),t;
A59: ( t . (intpos md) > t . (intpos me) implies ( (IExec (((((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 )))),t) . (intpos 7) = (t . (intpos 7)) - 1 & (IExec (((((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 )))),t) . (intpos 3) = (t . (intpos 3)) + 1 & (IExec (((((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 )))),t) . (intpos 5) = (t . (intpos 7)) - 1 ) ) by A6, A54, A57, A58, Lm14;
A60: DataLoc (t . GBP ),7 = intpos (0 + 7) by A54, SCMP_GCD:5;

A61: now

let v be State of SCMPDS ; :: thesis:
assume that
A62: v . (intpos 3) >= 8 and
A63: v . (intpos 2) = t . (intpos 2) and
A64: v . GBP = t . GBP and
A65: v . (DataLoc (t . GBP ),7) > 0 ; :: thesis:
reconsider ME = v . (intpos 3) as Element of NAT by A62, INT_1:16;
A66: ME = v . (intpos 3) ;
hence (IExec (((((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 )))),v) . GBP = v . GBP by A6, A54, A58, A62, A63, A64, Lm14; :: thesis:
thus ( ((((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 ))) is_closed_on v & ((((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 ))) is_halting_on v ) by SCMPDS_6:34, SCMPDS_6:35; :: thesis:
A67: ( v . (intpos md) > v . (intpos ME) implies ( (IExec (((((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 )))),v) . (intpos 7) = (v . (intpos 7)) - 1 & (IExec (((((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 )))),v) . (intpos 3) = (v . (intpos 3)) + 1 & (IExec (((((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 )))),v) . (intpos 5) = (v . (intpos 7)) - 1 ) ) by A6, A54, A58, A62, A63, A64, Lm14;

hereby :: thesis:

per cases ;

suppose A68: v . (intpos md) > v . (intpos ME) ; :: thesis:

hence (IExec (((((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 )))),v) . (DataLoc (t . GBP ),7) < v . (DataLoc (t . GBP ),7) by A60, A67, XREAL_1:148; :: thesis:
A69: (v . (intpos 3)) + 1 > v . (intpos 3) by XREAL_1:31;
(IExec (((((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 )))),v) . (intpos 3) = (v . (intpos 3)) + 1 by A6, A54, A58, A62, A63, A64, A68, Lm14;
hence (IExec (((((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 )))),v) . (intpos 3) >= 8 by A62, A69, XXREAL_0:2; :: thesis:

end;

suppose A70: v . (intpos md) <= v . (intpos ME) ; :: thesis:

end;

A71: ( t . (intpos md) <= t . (intpos me) implies ( (IExec (((((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 )))),t) . (intpos 7) = 0 & (IExec (((((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 )))),t) . (intpos 3) = t . (intpos 3) & (IExec (((((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 )))),t) . (intpos 5) = t . (intpos 7) ) ) by A6, A54, A57, A58, Lm14;
A72: me = t . (intpos 3) ;
then A73: (IExec (((((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 )))),t) . GBP = 0 by A6, A54, A57, A58, Lm14;
then A74: (IExec (((((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 )))),t) . (DataLoc ((IExec (((((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 )))),t) . GBP ),7) = 0 by A55, A59, A71, SCMP_GCD:5;

A75: now

let x be Int_position ; :: thesis:
thus (IExec (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 ))))),t) . x = (IExec (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 ))))),(IExec (((((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 )))),t)) . x by A55, A57, A60, A61, Lm12, Th6
.= (IExec (((((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 )))),t) . x by A74, SCMPDS_8:23 ; :: thesis:

end;

hence (IExec (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 ))))),t) . GBP = 0 by A73; :: thesis:
(IExec (((((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 )))),t) . (intpos 1) = t . (intpos 1) by A6, A54, A57, A58, A72, Lm14;
hence (IExec (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 ))))),t) . (intpos 1) = t . (intpos 1) by A75; :: thesis:
thus (IExec (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 ))))),t) . (intpos 7) = 0 by A55, A59, A71, A75; :: thesis:
(IExec (((((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 )))),t) . (intpos 2) = t . (intpos 2) by A6, A54, A57, A58, A72, Lm14;
hence (IExec (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 ))))),t) . (intpos 2) = t . (intpos 2) by A75; :: thesis:
(IExec (((((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 )))),t) . (intpos 4) = t . (intpos 4) by A6, A54, A57, A58, A72, Lm14;
hence (IExec (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 ))))),t) . (intpos 4) = t . (intpos 4) by A75; :: thesis:

A76: now

let i be Element of NAT ; :: thesis:
assume A77: i >= 8 ; :: thesis:
thus (IExec (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 ))))),t) . (intpos i) = (IExec (((((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 )))),t) . (intpos i) by A75
.= t . (intpos i) by A6, A54, A57, A58, A72, A77, Lm14 ; :: thesis:

end;

hereby :: thesis:

per cases ;

suppose A79: t . (intpos md) > t . (intpos me) ; :: thesis:

take m5 = 0 ; :: thesis:
take mE3 = m3; :: thesis:
thus (IExec (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 ))))),t) . (intpos 5) = m5 by A55, A59, A75, A79; :: thesis:
thus (IExec (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 ))))),t) . (intpos 3) = mE3 by A55, A56, A59, A75, A79; :: thesis:
thus mE3 + m5 = m3 ; :: thesis:
thus m5 <= t . (intpos 7) by A55; :: thesis:

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume that
A80: t . (intpos 3) <= i and
A81: i < mE3 ; :: thesis:
i <= me by A55, A56, A81, NAT_1:13;
then i = t . (intpos 3) by A80, XXREAL_0:1;
hence (IExec (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 ))))),t) . (intpos md) > (IExec (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 ))))),t) . (intpos i) by A6, A76, A78, A79; :: thesis:

end;

suppose A82: t . (intpos md) <= t . (intpos me) ; :: thesis:

take m5 = 1; :: thesis:
take mE3 = me; :: thesis:
thus (IExec (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 ))))),t) . (intpos 5) = m5 by A55, A71, A75, A82; :: thesis:
thus (IExec (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 ))))),t) . (intpos 3) = mE3 by A71, A75, A82; :: thesis:
thus mE3 + m5 = m3 by A55, A56; :: thesis:
thus m5 <= t . (intpos 7) by A55; :: thesis:
thus for i being Element of NAT st t . (intpos 3) <= i & i < mE3 holds
(IExec (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 ))))),t) . (intpos md) > (IExec (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 ))))),t) . (intpos i) ; :: thesis:
thus ( m5 = 0 or (IExec (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 ))))),t) . (intpos md) <= (IExec (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 ))))),t) . (intpos mE3) ) by A6, A76, A78, A82; :: thesis:

end;

then A83: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A83, A8);
hence ( (IExec (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 ))))),s) . GBP = 0 & (IExec (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 ))))),s) . (intpos 1) = s . (intpos 1) & (IExec (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 ))))),s) . (intpos 7) = 0 & (IExec (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 ))))),s) . (intpos 2) = s . (intpos 2) & (IExec (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 ))))),s) . (intpos 4) = s . (intpos 4) & ( for i being Element of NAT st i >= 8 holds
(IExec (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 ))))),s) . (intpos i) = s . (intpos i) ) & ex m5, mE3 being Element of NAT st
( m5 = (IExec (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 ))))),s) . (intpos 5) & (IExec (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 ))))),s) . (intpos 3) = mE3 & mE3 + m5 = m3 & m5 <= s . (intpos 7) & ( for i being Element of NAT st s . (intpos 3) <= i & i < mE3 holds
(IExec (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 ))))),s) . (intpos md) > (IExec (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 ))))),s) . (intpos i) ) & ( m5 = 0 or (IExec (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 ))))),s) . (intpos md) <= (IExec (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 ))))),s) . (intpos mE3) ) ) ) by A1, A3, A4, A5, A7; :: thesis: