let P be Instruction-Sequence of SCMPDS; :: thesis:
set I = Load (AddTo (GBP,3,1));
let s be 0 -started State of SCMPDS; :: thesis:
assume A1: s . GBP = 0 ; :: thesis:

per cases ;

suppose s . (DataLoc ((s . GBP),2)) <= 0 ; :: thesis:

hence ( for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_closed_on s,P & for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_halting_on s,P ) by Th42; :: thesis:

end;

suppose A2: s . (DataLoc ((s . GBP),2)) > 0 ; :: thesis:

A3: now :: thesis:

set cv = DataLoc ((s . GBP),2);
let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
A4: Initialize t = t by MEMSTR_0:44;
assume that
for x being Int_position st x in {GBP} holds
t . x = s . x and
A5: t . GBP = s . GBP ; :: thesis:
set t0 = Initialize t;
(Initialize t) . GBP = 0 by A1, A5, SCMPDS_5:15;
then A6: DataLoc (((Initialize t) . GBP),3) = intpos (0 + 3) by SCMP_GCD:1;
thus A7: (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . GBP = (Exec ((AddTo (GBP,3,1)),(Initialize t))) . GBP by A4, SCMPDS_5:40
.= (Initialize t) . GBP by A6, AMI_3:10, SCMPDS_2:48
.= t . GBP by SCMPDS_5:15 ; :: thesis:
A8: DataLoc ((s . GBP),2) = intpos (0 + 2) by A1, SCMP_GCD:1;
thus (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . (DataLoc ((s . GBP),2)) = (Exec ((AddTo (GBP,3,1)),(Initialize t))) . (DataLoc ((s . GBP),2)) by A4, SCMPDS_5:40
.= (Initialize t) . (DataLoc ((s . GBP),2)) by A6, A8, AMI_3:10, SCMPDS_2:48
.= t . (DataLoc ((s . GBP),2)) by SCMPDS_5:15 ; :: thesis:
thus ( Load (AddTo (GBP,3,1)) is_closed_on t,Q & Load (AddTo (GBP,3,1)) is_halting_on t,Q ) by SCMPDS_6:20, SCMPDS_6:21; :: thesis:
let y be Int_position; :: thesis:
assume y in {GBP} ; :: thesis:
then y = GBP by TARSKI:def 1;
hence (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y by A7; :: thesis:

end;

DataLoc ((s . GBP),2) = intpos (0 + 2) by A1, SCMP_GCD:1;
then DataLoc ((s . GBP),2) <> GBP by AMI_3:10;
then not DataLoc ((s . GBP),2) in {GBP} by TARSKI:def 1;
hence ( for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_closed_on s,P & for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_halting_on s,P ) by A1, A2, A3, Th46; :: thesis:

end;

end;