let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for n being Nat st s . GBP = 0 & s . () = n & s . () = 0 holds
(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = n

set i = AddTo (GBP,3,1);
set I = Load (AddTo (GBP,3,1));
set FD = for-down (GBP,2,1,(Load (AddTo (GBP,3,1))));
set a = intpos 3;
let s be 0 -started State of SCMPDS; :: thesis: for n being Nat st s . GBP = 0 & s . () = n & s . () = 0 holds
(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = n

let n be Nat; :: thesis: ( s . GBP = 0 & s . () = n & s . () = 0 implies (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = n )
assume that
A1: s . GBP = 0 and
A2: s . () = n and
A3: s . () = 0 ; :: thesis: (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = n
defpred S1[ Nat] means for s being 0 -started State of SCMPDS st s . () = \$1 & s . GBP = 0 holds
(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = \$1 + (s . ());
A4: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for s being 0 -started State of SCMPDS st s . () = k + 1 & s . GBP = 0 holds
(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = (k + 1) + (s . ())
let s be 0 -started State of SCMPDS; :: thesis: ( s . () = k + 1 & s . GBP = 0 implies (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = (k + 1) + (s . ()) )
assume that
A6: s . () = k + 1 and
A7: s . GBP = 0 ; :: thesis: (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = (k + 1) + (s . ())
GBP <> DataLoc ((s . GBP),2) by ;
then A8: not DataLoc ((s . GBP),2) in by TARSKI:def 1;
A9: 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 ) ) )

A10: Initialize t = t by MEMSTR_0:44;
assume that
for x being Int_position st x in holds
t . x = s . x and
A11: 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 A12: DataLoc ((() . GBP),3) = intpos (0 + 3) by SCMP_GCD:1;
then A13: DataLoc ((s . GBP),2) <> DataLoc ((() . GBP),3) by ;
thus A14: (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . GBP = (Exec ((AddTo (GBP,3,1)),())) . GBP by
.= () . 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 ) )

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
(IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y

let y be Int_position; :: thesis: ( y in implies (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y )
assume y in ; :: thesis: (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y
then y = GBP by TARSKI:def 1;
hence (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y by A14; :: thesis: verum
end;
set j = AddTo (GBP,2,(- 1));
set s0 = s;
set s1 = IExec ((Load (AddTo (GBP,3,1))),P,s);
set s2 = IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s);
set l2 = intpos 2;
set P2 = P;
A15: DataLoc ((s . GBP),3) = intpos (0 + 3) by ;
A16: (IExec ((Load (AddTo (GBP,3,1))),P,s)) . GBP = (Exec ((AddTo (GBP,3,1)),s)) . GBP by SCMPDS_5:40
.= 0 by ;
then A17: DataLoc (((IExec ((Load (AddTo (GBP,3,1))),P,s)) . GBP),2) = intpos (0 + 2) by SCMP_GCD:1;
A18: (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)) . () = (Exec ((AddTo (GBP,2,(- 1))),(IExec ((Load (AddTo (GBP,3,1))),P,s)))) . () by SCMPDS_5:41
.= ((IExec ((Load (AddTo (GBP,3,1))),P,s)) . ()) + (- 1) by
.= ((Exec ((AddTo (GBP,3,1)),s)) . ()) + (- 1) by SCMPDS_5:40
.= (s . ()) + (- 1) by
.= k by A6 ;
A19: (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)) . () = (Exec ((AddTo (GBP,2,(- 1))),(IExec ((Load (AddTo (GBP,3,1))),P,s)))) . () by SCMPDS_5:41
.= (IExec ((Load (AddTo (GBP,3,1))),P,s)) . () by
.= (Exec ((AddTo (GBP,3,1)),s)) . () by SCMPDS_5:40
.= (s . ()) + 1 by ;
A20: (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)) . GBP = (Exec ((AddTo (GBP,2,(- 1))),(IExec ((Load (AddTo (GBP,3,1))),P,s)))) . GBP by SCMPDS_5:41
.= 0 by ;
A21: (Initialize (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s))) . () = (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)) . () by SCMPDS_5:15;
A22: (Initialize (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s))) . () = (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)) . () by SCMPDS_5:15;
A23: (Initialize (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s))) . GBP = (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)) . GBP by SCMPDS_5:15;
DataLoc ((s . GBP),2) = intpos (0 + 2) by ;
hence (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,(Initialize (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s))))) . () by A6, A7, A8, A9, Th47
.= k + ((IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)) . ()) by A5, A18, A20, A21, A22, A23
.= (k + 1) + (s . ()) by A19 ;
:: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A24: S1[ 0 ]
proof
let s be 0 -started State of SCMPDS; :: thesis: ( s . () = 0 & s . GBP = 0 implies (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = 0 + (s . ()) )
assume that
A25: s . () = 0 and
A26: s . GBP = 0 ; :: thesis: (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = 0 + (s . ())
A27: Initialize s = s by MEMSTR_0:44;
DataLoc ((s . GBP),2) = intpos (0 + 2) by ;
hence (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = 0 + (s . ()) by ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A24, A4);
hence (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . () = n + 0 by A1, A2, A3
.= n ;
:: thesis: verum