let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS st s . GBP = 0 holds

let s be 0 -started State of SCMPDS; :: thesis: ( s . GBP = 0 implies ( 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 ) )
assume A1: s . GBP = 0 ; :: thesis: ( 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 )
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,P & for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_halting_on s,P )
end;
suppose A2: s . (DataLoc ((s . GBP),2)) > 0 ; :: thesis: ( 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 )
A3: now :: thesis: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in holds
t . x = s . x ) & t . GBP = s . GBP holds
( (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . GBP = t . GBP & (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . (DataLoc ((s . GBP),2)) = t . (DataLoc ((s . GBP),2)) & Load (AddTo (GBP,3,1)) is_closed_on t,Q & Load (AddTo (GBP,3,1)) is_halting_on t,Q & ( for y being Int_position st y in holds
(IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y ) )
set cv = DataLoc ((s . GBP),2);
let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in holds
t . x = s . x ) & t . GBP = s . GBP holds
( (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . GBP = t . GBP & (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . (DataLoc ((s . GBP),2)) = t . (DataLoc ((s . GBP),2)) & Load (AddTo (GBP,3,1)) is_closed_on t,Q & Load (AddTo (GBP,3,1)) is_halting_on t,Q & ( for y being Int_position st y in holds
(IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y ) )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( ( for x being Int_position st x in holds
t . x = s . x ) & t . GBP = s . GBP implies ( (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . GBP = t . GBP & (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . (DataLoc ((s . GBP),2)) = t . (DataLoc ((s . GBP),2)) & Load (AddTo (GBP,3,1)) is_closed_on t,Q & Load (AddTo (GBP,3,1)) is_halting_on t,Q & ( for y being Int_position st y in holds
(IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y ) ) )

A4: Initialize t = t by MEMSTR_0:44;
assume that
for x being Int_position st x in holds
t . x = s . x and
A5: t . GBP = s . GBP ; :: thesis: ( (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . GBP = t . GBP & (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . (DataLoc ((s . GBP),2)) = t . (DataLoc ((s . GBP),2)) & Load (AddTo (GBP,3,1)) is_closed_on t,Q & Load (AddTo (GBP,3,1)) is_halting_on t,Q & ( for y being Int_position st y in holds
(IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y ) )

set t0 = Initialize t;
(Initialize t) . GBP = 0 by ;
then A6: DataLoc ((() . GBP),3) = intpos (0 + 3) by SCMP_GCD:1;
.= () . GBP by
.= t . GBP by SCMPDS_5:15 ; :: thesis: ( (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . (DataLoc ((s . GBP),2)) = t . (DataLoc ((s . GBP),2)) & Load (AddTo (GBP,3,1)) is_closed_on t,Q & Load (AddTo (GBP,3,1)) is_halting_on t,Q & ( for y being Int_position st y in holds
(IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y ) )

A8: DataLoc ((s . GBP),2) = intpos (0 + 2) by ;
thus (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . (DataLoc ((s . GBP),2)) = (Exec ((AddTo (GBP,3,1)),())) . (DataLoc ((s . GBP),2)) by
.= () . (DataLoc ((s . GBP),2)) by
.= t . (DataLoc ((s . GBP),2)) by SCMPDS_5:15 ; :: thesis: ( Load (AddTo (GBP,3,1)) is_closed_on t,Q & Load (AddTo (GBP,3,1)) is_halting_on t,Q & ( for y being Int_position st y in holds
(IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y ) )

thus ( Load (AddTo (GBP,3,1)) is_closed_on t,Q & Load (AddTo (GBP,3,1)) is_halting_on t,Q ) by ; :: thesis: for y being Int_position st y in holds