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

proof

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

end;

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 State of SCMPDS ; :: thesis: ( s . (intpos 2) = k + 1 & s . GBP = 0 implies (IExec (for-down GBP ,2,1,(Load (AddTo GBP ,3,1))),s) . (intpos 3) = (k + 1) + (s . (intpos 3)) )
assume A6: ( s . (intpos 2) = k + 1 & s . GBP = 0 ) ; :: thesis: (IExec (for-down GBP ,2,1,(Load (AddTo GBP ,3,1))),s) . (intpos 3) = (k + 1) + (s . (intpos 3))
then A7: DataLoc (s . GBP ),2 = intpos (0 + 2) by SCMP_GCD:5;
GBP <> DataLoc (s . GBP ),2 by A6, SCMP_GCD:5;
then A8: not DataLoc (s . GBP ),2 in {GBP } by TARSKI:def 1;
A9: card (Load (AddTo GBP ,3,1)) = 1 by SCMPDS_5:6;

A10: 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 A11: ( ( 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 A6, A11, SCMPDS_5:40;
then A12: DataLoc ((Initialized t) . GBP ),3 = intpos (0 + 3) by SCMP_GCD:5;
thus A14: (IExec (Load (AddTo GBP ,3,1)),t) . GBP = (Exec (AddTo GBP ,3,1),(Initialized t)) . GBP by SCMPDS_5:45
.= (Initialized t) . GBP by A12, 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;
A15: DataLoc (s . GBP ),2 <> DataLoc ((Initialized t) . GBP ),3 by A6, A12, AMI_3:52, 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 A15, 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 A14; :: thesis: verum

end;

end;

set j = AddTo GBP ,2,(- 1);
set s0 = Initialized s;
set s1 = IExec (Load (AddTo GBP ,3,1)),s;
set s2 = IExec ((Load (AddTo GBP ,3,1)) ';' (AddTo GBP ,2,(- 1))),s;
set l2 = intpos 2;
A16: (Initialized s) . GBP = 0 by A6, SCMPDS_5:40;
then A17: DataLoc ((Initialized s) . GBP ),3 = intpos (0 + 3) by SCMP_GCD:5;
A20: (IExec (Load (AddTo GBP ,3,1)),s) . GBP = (Exec (AddTo GBP ,3,1),(Initialized s)) . GBP by SCMPDS_5:45
.= 0 by A16, A17, AMI_3:52, SCMPDS_2:60 ;
then A21: DataLoc ((IExec (Load (AddTo GBP ,3,1)),s) . GBP ),2 = intpos (0 + 2) by SCMP_GCD:5;
A23: (IExec ((Load (AddTo GBP ,3,1)) ';' (AddTo GBP ,2,(- 1))),s) . (intpos 3) = (Exec (AddTo GBP ,2,(- 1)),(IExec (Load (AddTo GBP ,3,1)),s)) . (intpos 3) by SCMPDS_5:46
.= (IExec (Load (AddTo GBP ,3,1)),s) . (intpos 3) by A21, AMI_3:52, SCMPDS_2:60
.= (Exec (AddTo GBP ,3,1),(Initialized s)) . (intpos 3) by SCMPDS_5:45
.= ((Initialized s) . (intpos 3)) + 1 by A17, SCMPDS_2:60
.= (s . (intpos 3)) + 1 by SCMPDS_5:40 ;
A24: (IExec ((Load (AddTo GBP ,3,1)) ';' (AddTo GBP ,2,(- 1))),s) . (intpos 2) = (Exec (AddTo GBP ,2,(- 1)),(IExec (Load (AddTo GBP ,3,1)),s)) . (intpos 2) by SCMPDS_5:46
.= ((IExec (Load (AddTo GBP ,3,1)),s) . (intpos 2)) + (- 1) by A21, SCMPDS_2:60
.= ((Exec (AddTo GBP ,3,1),(Initialized s)) . (intpos 2)) + (- 1) by SCMPDS_5:45
.= ((Initialized s) . (intpos 2)) + (- 1) by A17, AMI_3:52, SCMPDS_2:60
.= (k + 1) + (- 1) by A6, SCMPDS_5:40
.= k ;
A26: (IExec ((Load (AddTo GBP ,3,1)) ';' (AddTo GBP ,2,(- 1))),s) . GBP = (Exec (AddTo GBP ,2,(- 1)),(IExec (Load (AddTo GBP ,3,1)),s)) . GBP by SCMPDS_5:46
.= 0 by A20, A21, AMI_3:52, SCMPDS_2:60 ;
thus (IExec (for-down GBP ,2,1,(Load (AddTo GBP ,3,1))),s) . (intpos 3) = (IExec (for-down GBP ,2,1,(Load (AddTo GBP ,3,1))),(IExec ((Load (AddTo GBP ,3,1)) ';' (AddTo GBP ,2,(- 1))),s)) . (intpos 3) by A6, A7, A8, A9, A10, Th68
.= k + ((IExec ((Load (AddTo GBP ,3,1)) ';' (AddTo GBP ,2,(- 1))),s) . (intpos 3)) by A5, A24, A26
.= (k + 1) + (s . (intpos 3)) by A23 ; :: thesis: verum

end;

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

end;

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