set I = Load (AddTo GBP ,3,1);
let s be State of SCMPDS ; :: thesis: ( s . GBP = 0 implies ( 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 ) )
assume A1: s . GBP = 0 ; :: thesis: ( 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 )

per cases ( s . (DataLoc (s . GBP ),2) <= 0 or s . (DataLoc (s . GBP ),2) > 0 ) ;

suppose s . (DataLoc (s . GBP ),2) <= 0 ; :: thesis: ( 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 )

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: verum

end;

suppose A2: s . (DataLoc (s . GBP ),2) > 0 ; :: thesis: ( 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 )

A3: now

set cv = DataLoc (s . GBP ),2;
let t be State of SCMPDS ; :: thesis: ( ( for x being Int_position st x in {GBP } holds
t . x = s . x ) & t . GBP = s . GBP implies ( (IExec (Load (AddTo GBP ,3,1)),t) . GBP = t . GBP & (IExec (Load (AddTo GBP ,3,1)),t) . (DataLoc (s . GBP ),2) = t . (DataLoc (s . GBP ),2) & Load (AddTo GBP ,3,1) is_closed_on t & Load (AddTo GBP ,3,1) is_halting_on t & ( for y being Int_position st y in {GBP } holds
(IExec (Load (AddTo GBP ,3,1)),t) . y = t . y ) ) )
assume that
for x being Int_position st x in {GBP } holds
t . x = s . x and
A4: t . GBP = s . GBP ; :: thesis: ( (IExec (Load (AddTo GBP ,3,1)),t) . GBP = t . GBP & (IExec (Load (AddTo GBP ,3,1)),t) . (DataLoc (s . GBP ),2) = t . (DataLoc (s . GBP ),2) & Load (AddTo GBP ,3,1) is_closed_on t & Load (AddTo GBP ,3,1) is_halting_on t & ( for y being Int_position st y in {GBP } holds
(IExec (Load (AddTo GBP ,3,1)),t) . y = t . y ) )
set t0 = Initialized t;
(Initialized t) . GBP = 0 by A1, A4, SCMPDS_5:40;
then A5: DataLoc ((Initialized 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),(Initialized t)) . GBP by SCMPDS_5:45
.= (Initialized t) . GBP by A5, AMI_3:52, SCMPDS_2:60
.= t . GBP by SCMPDS_5:40 ; :: thesis: ( (IExec (Load (AddTo GBP ,3,1)),t) . (DataLoc (s . GBP ),2) = t . (DataLoc (s . GBP ),2) & Load (AddTo GBP ,3,1) is_closed_on t & Load (AddTo GBP ,3,1) is_halting_on t & ( for y being Int_position st y in {GBP } holds
(IExec (Load (AddTo GBP ,3,1)),t) . y = t . y ) )
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),(Initialized t)) . (DataLoc (s . GBP ),2) by SCMPDS_5:45
.= (Initialized t) . (DataLoc (s . GBP ),2) by A5, A7, AMI_3:52, SCMPDS_2:60
.= t . (DataLoc (s . GBP ),2) by SCMPDS_5:40 ; :: thesis: ( Load (AddTo GBP ,3,1) is_closed_on t & Load (AddTo GBP ,3,1) is_halting_on t & ( for y being Int_position st y in {GBP } holds
(IExec (Load (AddTo GBP ,3,1)),t) . y = t . y ) )
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: for y being Int_position st y in {GBP } holds
(IExec (Load (AddTo GBP ,3,1)),t) . y = t . y

hereby :: thesis: verum

let y be Int_position ; :: thesis: ( y in {GBP } implies (IExec (Load (AddTo GBP ,3,1)),t) . y = t . y )
assume y in {GBP } ; :: thesis: (IExec (Load (AddTo GBP ,3,1)),t) . y = t . y
then y = GBP by TARSKI:def 1;
hence (IExec (Load (AddTo GBP ,3,1)),t) . y = t . y by A6; :: thesis: verum

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: verum

end;

end;