let P be Instruction-Sequence of SCMPDS; :: thesis:
let s be 0 -started State of SCMPDS; :: thesis:
let sp, cv, fr, pp, pD be Element of 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 Th63; :: 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 abs (n + cv) <> sp by ABSVALUE:def 1;
then A8: DataLoc ((s . (intpos sp)),cv) <> intpos sp by ZFMISC_1:27;
A9: n + fr > n + cv by A2, XREAL_1:6;

A10: now

set Dv = DataLoc ((s . (intpos sp)),cv);
let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
II: Initialize t = t by MEMSTR_0:44;
assume that
A11: for x being Int_position st x in {(intpos sp),(intpos pp)} holds
t . x = s . x and
A12: t . (intpos sp) = s . (intpos sp) ; :: thesis:
set t0 = Initialize t;
set t1 = Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t));
A13: DataLoc (((Initialize t) . (intpos sp)),fr) = DataLoc (n,fr) by A12, SCMPDS_5:15
.= intpos (n + fr) by SCMP_GCD:1 ;
then DataLoc (((Initialize t) . (intpos sp)),fr) <> intpos pp by A4, ZFMISC_1:27;
then A14: (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 A13, ZFMISC_1:27;
then A15: (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, A11, A14;
then A16: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)),0) = intpos (pD + 0) by SCMP_GCD:1;
then A17: abs (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)) + 0) = pD by ZFMISC_1:27;
n <= n + fr by NAT_1:11;
then sp < n + fr by A1, XXREAL_0:2;
then abs (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)) + 0) <> sp by A4, A5, A17, XXREAL_0:2;
then A18: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)),0) <> intpos sp by ZFMISC_1:27;
DataLoc ((s . (intpos sp)),cv) = intpos (n + cv) by SCMP_GCD:1;
then A19: abs ((s . (intpos sp)) + cv) = n + cv by ZFMISC_1:27;
then abs (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)) + 0) <> abs ((s . (intpos sp)) + cv) by A4, A5, A9, A17, XXREAL_0:2;
then A20: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)),0) <> DataLoc ((s . (intpos sp)),cv) by ZFMISC_1:27;
abs (((Initialize t) . (intpos sp)) + fr) = n + fr by A13, ZFMISC_1:27;
then abs (((Initialize t) . (intpos sp)) + fr) <> abs ((s . (intpos sp)) + cv) by A2, A19;
then A21: DataLoc (((Initialize t) . (intpos sp)),fr) <> DataLoc ((s . (intpos sp)),cv) by ZFMISC_1:27;
thus A22: (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 SCMPDS_5:42, II
.= t . (intpos sp) by A15, A18, 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 SCMPDS_5:42, II
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (DataLoc ((s . (intpos sp)),cv)) by A20, SCMPDS_2:48
.= (Initialize t) . (DataLoc ((s . (intpos sp)),cv)) by A21, 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:
A23: (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, A14, A16, SCMPDS_2:48 ;

hereby :: thesis:

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

per cases by A24, 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 A22; :: 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 A23, MEMSTR_0:44; :: thesis:

end;

end;

end;

end;

n + cv <> pp by A2, A4, XREAL_1:6;
then abs (n + cv) <> pp by ABSVALUE:def 1;
then DataLoc ((s . (intpos sp)),cv) <> intpos pp by ZFMISC_1:27;
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, Th67; :: thesis:

end;

end;