let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for sp, cv, result, pp, pD being Nat st s . (intpos sp) > sp & cv < result & s . (intpos pp) = pD & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) holds
( for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on s,P & for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on s,P )

let s be 0 -started State of SCMPDS; :: thesis: for sp, cv, result, pp, pD being Nat st s . (intpos sp) > sp & cv < result & s . (intpos pp) = pD & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) holds
( for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on s,P & for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on s,P )

let sp, cv, fr, pp, pD be Nat; :: thesis: ( s . (intpos sp) > sp & cv < fr & s . (intpos pp) = pD & (s . (intpos sp)) + fr < pp & pp < pD & pD < s . (intpos pD) implies ( for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on s,P & for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on s,P ) )
set BP = intpos sp;
set PD = intpos pD;
set PP = intpos pp;
assume that
A1: s . (intpos sp) > sp and
A2: cv < fr and
A3: s . (intpos pp) = pD and
A4: (s . (intpos sp)) + fr < pp and
A5: pp < pD and
A6: pD < s . (intpos pD) ; :: thesis: ( for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on s,P & for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on s,P )
set i2 = AddTo ((intpos sp),fr,(intpos pD),0);
set i3 = AddTo ((intpos pp),0,1);
per cases ( s . (DataLoc ((s . (intpos sp)),cv)) <= 0 or s . (DataLoc ((s . (intpos sp)),cv)) > 0 ) ;
suppose s . (DataLoc ((s . (intpos sp)),cv)) <= 0 ; :: thesis: ( for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on s,P & for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on s,P )
hence ( for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on s,P & for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on s,P ) by Th42; :: thesis: verum
end;
suppose A7: s . (DataLoc ((s . (intpos sp)),cv)) > 0 ; :: thesis: ( for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on s,P & for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on s,P )
reconsider n = s . (intpos sp) as Element of NAT by ;
n + cv <> sp by ;
then |.(n + cv).| <> sp by ABSVALUE:def 1;
then A8: DataLoc ((s . (intpos sp)),cv) <> intpos sp by XTUPLE_0:1;
A9: n + fr > n + cv by ;
A10: now :: thesis: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in {(intpos sp),(intpos pp)} holds
t . x = s . x ) & t . (intpos sp) = s . (intpos sp) holds
( (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp) = t . (intpos sp) & (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (DataLoc ((s . (intpos sp)),cv)) = t . (DataLoc ((s . (intpos sp)),cv)) & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on t,Q & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on t,Q & ( for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . y = t . y ) )
set Dv = DataLoc ((s . (intpos sp)),cv);
let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in {(intpos sp),(intpos pp)} holds
t . x = s . x ) & t . (intpos sp) = s . (intpos sp) holds
( (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp) = t . (intpos sp) & (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (DataLoc ((s . (intpos sp)),cv)) = t . (DataLoc ((s . (intpos sp)),cv)) & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on t,Q & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on t,Q & ( for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . y = t . y ) )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( ( for x being Int_position st x in {(intpos sp),(intpos pp)} holds
t . x = s . x ) & t . (intpos sp) = s . (intpos sp) implies ( (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp) = t . (intpos sp) & (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (DataLoc ((s . (intpos sp)),cv)) = t . (DataLoc ((s . (intpos sp)),cv)) & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on t,Q & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on t,Q & ( for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . y = t . y ) ) )

A11: Initialize t = t by MEMSTR_0:44;
assume that
A12: for x being Int_position st x in {(intpos sp),(intpos pp)} holds
t . x = s . x and
A13: t . (intpos sp) = s . (intpos sp) ; :: thesis: ( (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp) = t . (intpos sp) & (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (DataLoc ((s . (intpos sp)),cv)) = t . (DataLoc ((s . (intpos sp)),cv)) & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on t,Q & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on t,Q & ( for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . y = t . y ) )

set t0 = Initialize t;
set t1 = Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),());
A14: DataLoc ((() . (intpos sp)),fr) = DataLoc (n,fr) by
.= intpos (n + fr) by SCMP_GCD:1 ;
then DataLoc ((() . (intpos sp)),fr) <> intpos pp by ;
then A15: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp) = () . (intpos pp) by SCMPDS_2:49
.= t . (intpos pp) by SCMPDS_5:15 ;
n + fr <> sp by ;
then DataLoc ((() . (intpos sp)),fr) <> intpos sp by ;
then A16: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos sp) = () . (intpos sp) by SCMPDS_2:49
.= t . (intpos sp) by SCMPDS_5:15 ;
intpos pp in {(intpos sp),(intpos pp)} by TARSKI:def 2;
then (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp) = pD by A3, A12, A15;
then A17: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)),0) = intpos (pD + 0) by SCMP_GCD:1;
then A18: |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)) + 0).| = pD by XTUPLE_0:1;
n <= n + fr by NAT_1:11;
then sp < n + fr by ;
then |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)) + 0).| <> sp by ;
then A19: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)),0) <> intpos sp by XTUPLE_0:1;
DataLoc ((s . (intpos sp)),cv) = intpos (n + cv) by SCMP_GCD:1;
then A20: |.((s . (intpos sp)) + cv).| = n + cv by XTUPLE_0:1;
then |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)) + 0).| <> |.((s . (intpos sp)) + cv).| by ;
then A21: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)),0) <> DataLoc ((s . (intpos sp)),cv) by XTUPLE_0:1;
|.((() . (intpos sp)) + fr).| = n + fr by ;
then |.((() . (intpos sp)) + fr).| <> |.((s . (intpos sp)) + cv).| by ;
then A22: DataLoc ((() . (intpos sp)),fr) <> DataLoc ((s . (intpos sp)),cv) by XTUPLE_0:1;
thus A23: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp) = (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())))) . (intpos sp) by
.= t . (intpos sp) by ; :: thesis: ( (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (DataLoc ((s . (intpos sp)),cv)) = t . (DataLoc ((s . (intpos sp)),cv)) & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on t,Q & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on t,Q & ( for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . y = t . y ) )

thus (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (DataLoc ((s . (intpos sp)),cv)) = (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())))) . (DataLoc ((s . (intpos sp)),cv)) by
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (DataLoc ((s . (intpos sp)),cv)) by
.= () . (DataLoc ((s . (intpos sp)),cv)) by
.= t . (DataLoc ((s . (intpos sp)),cv)) by SCMPDS_5:15 ; :: thesis: ( (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on t,Q & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on t,Q & ( for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . y = t . y ) )

thus ( (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on t,Q & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on t,Q ) by ; :: thesis: for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . y = t . y

A24: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,())) . (intpos pp) = (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())))) . (intpos pp) by SCMPDS_5:42
.= t . (intpos pp) by ;
hereby :: thesis: verum
let y be Int_position; :: thesis: ( y in {(intpos sp),(intpos pp)} implies (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . b1 = t . b1 )
assume A25: y in {(intpos sp),(intpos pp)} ; :: thesis: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . b1 = t . b1
per cases ( y = intpos sp or y = intpos pp ) by ;
suppose y = intpos sp ; :: thesis: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . b1 = t . b1
hence (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . y = t . y by A23; :: thesis: verum
end;
suppose y = intpos pp ; :: thesis: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . b1 = t . b1
hence (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . y = t . y by ; :: thesis: verum
end;
end;
end;
end;
n + cv <> pp by ;
then |.(n + cv).| <> pp by ABSVALUE:def 1;
then DataLoc ((s . (intpos sp)),cv) <> intpos pp by XTUPLE_0:1;
then not DataLoc ((s . (intpos sp)),cv) in {(intpos sp),(intpos pp)} by ;
hence ( for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on s,P & for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on s,P ) by A7, A8, A10, Th46; :: thesis: verum
end;
end;