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

DataLoc (s . GBP ),2 = intpos (0 + 2) by A1, SCMP_GCD:5;
then DataLoc (s . GBP ),2 <> GBP by AMI_3:52;
then A3: not DataLoc (s . GBP ),2 in {GBP } by TARSKI:def 1;
A4: card (Load (AddTo GBP ,3,1)) = 1 by SCMPDS_5:6;

now

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 A5: ( ( for x being Int_position st x in {GBP } holds
t . x = s . x ) & 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, A5, SCMPDS_5:40;
then A6: DataLoc ((Initialized t) . GBP ),3 = intpos (0 + 3) by SCMP_GCD:5;
thus A8: (IExec (Load (AddTo GBP ,3,1)),t) . GBP = (Exec (AddTo GBP ,3,1),(Initialized t)) . GBP by SCMPDS_5:45
.= (Initialized t) . GBP by A6, 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 ) )
set cv = DataLoc (s . GBP ),2;
B9: 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 B9, A6, 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 A8; :: thesis: verum

end;

end;

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, A4, Th67; :: thesis: verum

end;

end;