let s be 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 & for-down (intpos sp),cv,1,((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) is_halting_on s ) 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:16;
n + cv <> sp by A1, NAT_1:11;
then abs (n + cv) <> sp by ABSVALUE:def 1;
then A9: DataLoc (s . (intpos sp)),cv <> intpos sp by ZFMISC_1:33;
A10: n + fr > n + cv by A2, XREAL_1:8;

A11: now

set Dv = DataLoc (s . (intpos sp)),cv;
let t be State of SCMPDS ; :: thesis:
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:40
.= intpos (n + fr) by SCMP_GCD:5 ;
then DataLoc ((Initialize t) . (intpos sp)),fr <> intpos pp by A4, ZFMISC_1:33;
then A15: (Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t)) . (intpos pp) = (Initialize t) . (intpos pp) by SCMPDS_2:61
.= t . (intpos pp) by SCMPDS_5:40 ;
n + fr <> sp by A1, NAT_1:11;
then DataLoc ((Initialize t) . (intpos sp)),fr <> intpos sp by A14, ZFMISC_1:33;
then A16: (Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t)) . (intpos sp) = (Initialize t) . (intpos sp) by SCMPDS_2:61
.= t . (intpos sp) by SCMPDS_5:40 ;
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:5;
then A18: abs (((Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t)) . (intpos pp)) + 0 ) = pD by ZFMISC_1:33;
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, A18, XXREAL_0:2;
then A19: DataLoc ((Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t)) . (intpos pp)),0 <> intpos sp by ZFMISC_1:33;
DataLoc (s . (intpos sp)),cv = intpos (n + cv) by SCMP_GCD:5;
then A20: abs ((s . (intpos sp)) + cv) = n + cv by ZFMISC_1:33;
then abs (((Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t)) . (intpos pp)) + 0 ) <> abs ((s . (intpos sp)) + cv) by A4, A5, A10, 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 ZFMISC_1:33;
abs (((Initialize t) . (intpos sp)) + fr) = n + fr by A14, ZFMISC_1:33;
then abs (((Initialize t) . (intpos sp)) + fr) <> abs ((s . (intpos sp)) + cv) by A2, A20;
then A22: DataLoc ((Initialize t) . (intpos sp)),fr <> DataLoc (s . (intpos sp)),cv by ZFMISC_1:33;
thus A23: (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos sp) = (Exec (AddTo (intpos pp),0 ,1),(Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t))) . (intpos sp) by SCMPDS_5:47
.= t . (intpos sp) by A16, A19, SCMPDS_2:60 ; :: thesis:
thus (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),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:47
.= (Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t)) . (DataLoc (s . (intpos sp)),cv) by A21, SCMPDS_2:60
.= (Initialize t) . (DataLoc (s . (intpos sp)),cv) by A22, SCMPDS_2:61
.= t . (DataLoc (s . (intpos sp)),cv) by SCMPDS_5:40 ; :: thesis:
thus ( (AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1) is_closed_on t & (AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1) is_halting_on t ) by SCMPDS_6:34, SCMPDS_6:35; :: thesis:
A24: (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos pp) = (Exec (AddTo (intpos pp),0 ,1),(Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t))) . (intpos pp) by SCMPDS_5:47
.= t . (intpos pp) by A3, A6, A15, A17, SCMPDS_2:60 ;

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)),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)),t) . y = t . y by A24; :: thesis:

end;

end;

end;

end;

n + cv <> pp by A2, A4, XREAL_1:8;
then abs (n + cv) <> pp by ABSVALUE:def 1;
then DataLoc (s . (intpos sp)),cv <> intpos pp by ZFMISC_1:33;
then not DataLoc (s . (intpos sp)),cv in {(intpos sp),(intpos pp)} by A9, 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 & for-down (intpos sp),cv,1,((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) is_halting_on s ) by A7, A9, A11, Th67; :: thesis:

end;

end;