set I = Load (AddTo GBP ,3,1);
let s be 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 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;