let P be Instruction-Sequence of SCMPDS; :: thesis:
let s be 0 -started State of SCMPDS; :: thesis:
let sp, cv, fr, pp, pD be Nat; :: thesis:
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:
set i2 = AddTo ((intpos sp),fr,(intpos pD),0);
set i3 = AddTo ((intpos pp),0,1);
set I = (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1));

suppose s . (DataLoc ((s . (intpos sp)),cv)) <= 0 ; :: thesis:

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:

end;

suppose A7: s . (DataLoc ((s . (intpos sp)),cv)) > 0 ; :: thesis:

reconsider n = s . (intpos sp) as Element of NAT by A1, INT_1:3;
n + cv <> sp by A1, NAT_1:11;
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 A2, XREAL_1:6;

A10: now :: thesis:

set Dv = DataLoc ((s . (intpos sp)),cv);
let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
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:
set t0 = Initialize t;
set t1 = Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t));
A14: DataLoc (((Initialize t) . (intpos sp)),fr) = DataLoc (n,fr) by A13, SCMPDS_5:15
.= intpos (n + fr) by SCMP_GCD:1 ;
then DataLoc (((Initialize t) . (intpos sp)),fr) <> intpos pp by A4, XTUPLE_0:1;
then A15: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp) = (Initialize t) . (intpos pp) by SCMPDS_2:49
.= t . (intpos pp) by SCMPDS_5:15 ;
n + fr <> sp by A1, NAT_1:11;
then DataLoc (((Initialize t) . (intpos sp)),fr) <> intpos sp by A14, XTUPLE_0:1;
then A16: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos sp) = (Initialize t) . (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)),(Initialize t))) . (intpos pp) = pD by A3, A12, A15;
then A17: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)),0) = intpos (pD + 0) by SCMP_GCD:1;
then A18: |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)) + 0).| = pD by XTUPLE_0:1;
n <= n + fr by NAT_1:11;
then sp < n + fr by A1, XXREAL_0:2;
then |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)) + 0).| <> sp by A4, A5, A18, XXREAL_0:2;
then A19: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (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)),(Initialize t))) . (intpos pp)) + 0).| <> |.((s . (intpos sp)) + cv).| by A4, A5, A9, A18, XXREAL_0:2;
then A21: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)),0) <> DataLoc ((s . (intpos sp)),cv) by XTUPLE_0:1;
|.(((Initialize t) . (intpos sp)) + fr).| = n + fr by A14, XTUPLE_0:1;
then |.(((Initialize t) . (intpos sp)) + fr).| <> |.((s . (intpos sp)) + cv).| by A2, A20;
then A22: DataLoc (((Initialize t) . (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)),(Initialize t))))) . (intpos sp) by A11, SCMPDS_5:42
.= t . (intpos sp) by A16, A19, SCMPDS_2:48 ; :: thesis:
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)),(Initialize t))))) . (DataLoc ((s . (intpos sp)),cv)) by A11, SCMPDS_5:42
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (DataLoc ((s . (intpos sp)),cv)) by A21, SCMPDS_2:48
.= (Initialize t) . (DataLoc ((s . (intpos sp)),cv)) by A22, SCMPDS_2:49
.= t . (DataLoc ((s . (intpos sp)),cv)) by SCMPDS_5:15 ; :: thesis:
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 SCMPDS_6:20, SCMPDS_6:21; :: thesis:
A24: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,(Initialize t))) . (intpos pp) = (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))))) . (intpos pp) by SCMPDS_5:42
.= t . (intpos pp) by A3, A6, A15, A17, SCMPDS_2:48 ;

hereby :: thesis:

let y be Int_position; :: thesis:
assume A25: y in {(intpos sp),(intpos pp)} ; :: thesis:

per cases by A25, TARSKI:def 2;

suppose y = intpos sp ; :: thesis:

hence (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . y = t . y by A23; :: thesis:

end;

suppose y = intpos pp ; :: thesis:

hence (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . y = t . y by A24, MEMSTR_0:44; :: thesis:

end;

end;

end;

end;

n + cv <> pp by A2, A4, XREAL_1:6;
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 A8, TARSKI:def 2;
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:

end;

end;