let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being 0 -started State of SCMPDS
for n being Element of NAT st s . GBP = 0 & s . (intpos 2) = n & s . (intpos 3) = 0 holds
(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = 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 Element of NAT st s . GBP = 0 & s . (intpos 2) = n & s . (intpos 3) = 0 holds
(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = n
let n be Element of NAT ; :: thesis: ( s . GBP = 0 & s . (intpos 2) = n & s . (intpos 3) = 0 implies (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = n )
assume that
A1: s . GBP = 0 and
A2: s . (intpos 2) = n and
A3: s . (intpos 3) = 0 ; :: thesis: (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = n
defpred S₁[ Element of NAT ] means for s being 0 -started State of SCMPDS st s . (intpos 2) = $1 & s . GBP = 0 holds
(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = $1 + (s . (intpos 3));

A4: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]

now

let s be 0 -started State of SCMPDS; :: thesis: ( s . (intpos 2) = k + 1 & s . GBP = 0 implies (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = (k + 1) + (s . (intpos 3)) )
assume that
A6: s . (intpos 2) = k + 1 and
A7: s . GBP = 0 ; :: thesis: (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = (k + 1) + (s . (intpos 3))
GBP <> DataLoc ((s . GBP),2) by A6, A7, SCMP_GCD:5;
then A8: not DataLoc ((s . GBP),2) in {GBP} by TARSKI:def 1;

A9: now

set cv = DataLoc ((s . GBP),2);
let t be 0 -started State of SCMPDS; :: thesis: for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in {GBP} 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 {GBP} holds
(IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y ) )
let Q be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: 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))),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 {GBP} holds
(IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y ) ) )
assume that
for x being Int_position st x in {GBP} holds
t . x = s . x and
A10: 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 {GBP} holds
(IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y ) )
set t0 = Initialize t;
(Initialize t) . GBP = 0 by A7, A10, SCMPDS_5:40;
then A11: DataLoc (((Initialize t) . GBP),3) = intpos (0 + 3) by SCMP_GCD:5;
then A12: DataLoc ((s . GBP),2) <> DataLoc (((Initialize t) . GBP),3) by A6, A7, AMI_3:52, SCMP_GCD:5;
thus A13: (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . GBP = (Exec ((AddTo (GBP,3,1)),(Initialize t))) . GBP by SCMPDS_5:45
.= (Initialize t) . GBP by A11, AMI_3:52, SCMPDS_2:60
.= t . GBP by SCMPDS_5:40 ; :: 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 {GBP} 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)),(Initialize t))) . (DataLoc ((s . GBP),2)) by SCMPDS_5:45
.= (Initialize t) . (DataLoc ((s . GBP),2)) by A12, SCMPDS_2:60
.= t . (DataLoc ((s . GBP),2)) by SCMPDS_5:40 ; :: 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 {GBP} 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 SCMPDS_6:34, SCMPDS_6:35; :: thesis: for y being Int_position st y in {GBP} holds
(IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y

hereby :: thesis: verum

let y be Int_position ; :: thesis: ( y in {GBP} implies (IExec ((Load (AddTo (GBP,3,1))),Q,t)) . y = t . y )
assume y in {GBP} ; :: 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 A13; :: thesis: verum

end;

end;

set j = AddTo (GBP,2,(- 1));
set s0 = Initialize 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;
A14: (Initialize s) . GBP = 0 by A7, SCMPDS_5:40;
then A15: DataLoc (((Initialize s) . GBP),3) = intpos (0 + 3) by SCMP_GCD:5;
A16: (IExec ((Load (AddTo (GBP,3,1))),P,s)) . GBP = (Exec ((AddTo (GBP,3,1)),(Initialize s))) . GBP by SCMPDS_5:45
.= 0 by A14, A15, AMI_3:52, SCMPDS_2:60 ;
then A17: DataLoc (((IExec ((Load (AddTo (GBP,3,1))),P,s)) . GBP),2) = intpos (0 + 2) by SCMP_GCD:5;
A18: (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)) . (intpos 2) = (Exec ((AddTo (GBP,2,(- 1))),(IExec ((Load (AddTo (GBP,3,1))),P,s)))) . (intpos 2) by SCMPDS_5:46
.= ((IExec ((Load (AddTo (GBP,3,1))),P,s)) . (intpos 2)) + (- 1) by A17, SCMPDS_2:60
.= ((Exec ((AddTo (GBP,3,1)),(Initialize s))) . (intpos 2)) + (- 1) by SCMPDS_5:45
.= ((Initialize s) . (intpos 2)) + (- 1) by A15, AMI_3:52, SCMPDS_2:60
.= (k + 1) + (- 1) by A6, SCMPDS_5:40
.= k ;
A19: (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)) . (intpos 3) = (Exec ((AddTo (GBP,2,(- 1))),(IExec ((Load (AddTo (GBP,3,1))),P,s)))) . (intpos 3) by SCMPDS_5:46
.= (IExec ((Load (AddTo (GBP,3,1))),P,s)) . (intpos 3) by A17, AMI_3:52, SCMPDS_2:60
.= (Exec ((AddTo (GBP,3,1)),(Initialize s))) . (intpos 3) by SCMPDS_5:45
.= ((Initialize s) . (intpos 3)) + 1 by A15, SCMPDS_2:60
.= (s . (intpos 3)) + 1 by SCMPDS_5:40 ;
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:46
.= 0 by A16, A17, AMI_3:52, SCMPDS_2:60 ;
A21: (Initialize (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s))) . (intpos 2) = (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)) . (intpos 2) by SCMPDS_5:40;
A22: (Initialize (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s))) . (intpos 3) = (IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)) . (intpos 3) by SCMPDS_5:40;
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:40;
A24: 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)))) = IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,(IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s))) by SCMPDS_5:48;
DataLoc ((s . GBP),2) = intpos (0 + 2) by A7, SCMP_GCD:5;
hence (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,(IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)))) . (intpos 3) by A6, A7, A8, A9, Th68
.= k + ((IExec (((Load (AddTo (GBP,3,1))) ';' (AddTo (GBP,2,(- 1)))),P,s)) . (intpos 3)) by A5, A18, A20, A21, A22, A23, A24
.= (k + 1) + (s . (intpos 3)) by A19 ;
:: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A25: S₁[ 0 ]

proof

let s be 0 -started State of SCMPDS; :: thesis: ( s . (intpos 2) = 0 & s . GBP = 0 implies (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = 0 + (s . (intpos 3)) )
assume that
A26: s . (intpos 2) = 0 and
A27: s . GBP = 0 ; :: thesis: (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = 0 + (s . (intpos 3))
DataLoc ((s . GBP),2) = intpos (0 + 2) by A27, SCMP_GCD:5;
hence (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = 0 + (s . (intpos 3)) by A26, Th66; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A25, A4);
hence (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = n + 0 by A1, A2, A3
.= n ;
:: thesis: verum