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

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

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

end;

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

A3: now

set cv = DataLoc ((s . GBP),2);
let t be 0 -started State of SCMPDS; :: thesis:
assume that
for x being Int_position st x in {GBP} holds
t . x = s . x and
A4: t . GBP = s . GBP ; :: thesis:
set t0 = Initialize t;
(Initialize t) . GBP = 0 by A1, A4, SCMPDS_5:40;
then A5: DataLoc (((Initialize t) . GBP),3) = intpos (0 + 3) by SCMP_GCD:5;
thus A6: (IExec ((Load (AddTo (GBP,3,1))),t)) . GBP = (Exec ((AddTo (GBP,3,1)),(Initialize t))) . GBP by SCMPDS_5:45
.= (Initialize t) . GBP by A5, AMI_3:52, SCMPDS_2:60
.= t . GBP by SCMPDS_5:40 ; :: thesis:
A7: DataLoc ((s . GBP),2) = intpos (0 + 2) by A1, SCMP_GCD:5;
thus (IExec ((Load (AddTo (GBP,3,1))),t)) . (DataLoc ((s . GBP),2)) = (Exec ((AddTo (GBP,3,1)),(Initialize t))) . (DataLoc ((s . GBP),2)) by SCMPDS_5:45
.= (Initialize t) . (DataLoc ((s . GBP),2)) by A5, A7, AMI_3:52, SCMPDS_2:60
.= t . (DataLoc ((s . GBP),2)) by SCMPDS_5:40 ; :: thesis:
thus ( Load (AddTo (GBP,3,1)) is_closed_on t & Load (AddTo (GBP,3,1)) is_halting_on t ) by SCMPDS_6:34, SCMPDS_6:35; :: thesis:

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

end;

end;

DataLoc ((s . GBP),2) = intpos (0 + 2) by A1, SCMP_GCD:5;
then DataLoc ((s . GBP),2) <> GBP by AMI_3:52;
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 & for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_halting_on s ) by A1, A2, A3, Th67; :: thesis:

end;

end;