set a = GBP ;
let s be State of SCMPDS ; :: thesis: ( s . GBP = 0 implies ( (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . GBP = 0 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 1) = (s . (intpos 1)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 2) = s . (intpos 2) & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Element of NAT st i >= 7 holds
(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = s . (intpos i) ) ) )
set t0 = Initialize s;
set t1 = IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s;
set t2 = IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s;
set t3 = IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s;
set t4 = Exec (AddTo GBP ,3,1),(Initialize s);
assume s . GBP = 0 ; :: thesis: ( (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . GBP = 0 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 1) = (s . (intpos 1)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 2) = s . (intpos 2) & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Element of NAT st i >= 7 holds
(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = s . (intpos i) ) )
then A1: (Initialize s) . GBP = 0 by SCMPDS_5:40;
then A2: DataLoc ((Initialize s) . GBP ),3 = intpos (0 + 3) by SCMP_GCD:5;
then A3: (Exec (AddTo GBP ,3,1),(Initialize s)) . GBP = 0 by A1, AMI_3:52, SCMPDS_2:60;
then A4: DataLoc ((Exec (AddTo GBP ,3,1),(Initialize s)) . GBP ),4 = intpos (0 + 4) by SCMP_GCD:5;
(Initialize s) . (intpos 2) = s . (intpos 2) by SCMPDS_5:40;
then A5: (Exec (AddTo GBP ,3,1),(Initialize s)) . (intpos 2) = s . (intpos 2) by A2, AMI_3:52, SCMPDS_2:60;
A6: (IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s) . (intpos 2) = (Exec (GBP ,4 := GBP ,3),(Exec (AddTo GBP ,3,1),(Initialize s))) . (intpos 2) by SCMPDS_5:47
.= s . (intpos 2) by A5, A4, AMI_3:52, SCMPDS_2:59 ;
(Initialize s) . (intpos 1) = s . (intpos 1) by SCMPDS_5:40;
then A7: (Exec (AddTo GBP ,3,1),(Initialize s)) . (intpos 1) = s . (intpos 1) by A2, AMI_3:52, SCMPDS_2:60;
A8: (IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s) . (intpos 1) = (Exec (GBP ,4 := GBP ,3),(Exec (AddTo GBP ,3,1),(Initialize s))) . (intpos 1) by SCMPDS_5:47
.= s . (intpos 1) by A7, A4, AMI_3:52, SCMPDS_2:59 ;
(Initialize s) . (intpos 3) = s . (intpos 3) by SCMPDS_5:40;
then A9: (Exec (AddTo GBP ,3,1),(Initialize s)) . (intpos 3) = (s . (intpos 3)) + 1 by A2, SCMPDS_2:60;
A10: (IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s) . GBP = (Exec (GBP ,4 := GBP ,3),(Exec (AddTo GBP ,3,1),(Initialize s))) . GBP by SCMPDS_5:47
.= 0 by A3, A4, AMI_3:52, SCMPDS_2:59 ;
then A11: DataLoc ((IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s) . GBP ),1 = intpos (0 + 1) by SCMP_GCD:5;
A12: DataLoc ((Exec (AddTo GBP ,3,1),(Initialize s)) . GBP ),3 = intpos (0 + 3) by A3, SCMP_GCD:5;
A13: (IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s) . (intpos 4) = (Exec (GBP ,4 := GBP ,3),(Exec (AddTo GBP ,3,1),(Initialize s))) . (intpos 4) by SCMPDS_5:47
.= (s . (intpos 3)) + 1 by A9, A4, A12, SCMPDS_2:59 ;
A14: (IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s) . (intpos 4) = (Exec (AddTo GBP ,1,1),(IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s)) . (intpos 4) by SCMPDS_5:46
.= (s . (intpos 3)) + 1 by A13, A11, AMI_3:52, SCMPDS_2:60 ;
A15: (IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s) . (intpos 2) = (Exec (AddTo GBP ,1,1),(IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s)) . (intpos 2) by SCMPDS_5:46
.= s . (intpos 2) by A6, A11, AMI_3:52, SCMPDS_2:60 ;
A16: (IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s) . (intpos 1) = (Exec (AddTo GBP ,1,1),(IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s)) . (intpos 1) by SCMPDS_5:46
.= (s . (intpos 1)) + 1 by A8, A11, SCMPDS_2:60 ;
A17: (IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s) . (intpos 3) = (Exec (GBP ,4 := GBP ,3),(Exec (AddTo GBP ,3,1),(Initialize s))) . (intpos 3) by SCMPDS_5:47
.= (s . (intpos 3)) + 1 by A9, A4, AMI_3:52, SCMPDS_2:59 ;
A18: (IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s) . (intpos 3) = (Exec (AddTo GBP ,1,1),(IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s)) . (intpos 3) by SCMPDS_5:46
.= (s . (intpos 3)) + 1 by A17, A11, AMI_3:52, SCMPDS_2:60 ;
A19: (IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s) . GBP = (Exec (AddTo GBP ,1,1),(IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s)) . GBP by SCMPDS_5:46
.= 0 by A10, A11, AMI_3:52, SCMPDS_2:60 ;
then A20: DataLoc ((IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s) . GBP ),6 = intpos (0 + 6) by SCMP_GCD:5;
thus (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . GBP = (Exec (GBP ,6 := GBP ,1),(IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s)) . GBP by SCMPDS_5:46
.= 0 by A19, A20, AMI_3:52, SCMPDS_2:59 ; :: thesis: ( (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 1) = (s . (intpos 1)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 2) = s . (intpos 2) & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Element of NAT st i >= 7 holds
(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 1) = (Exec (GBP ,6 := GBP ,1),(IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s)) . (intpos 1) by SCMPDS_5:46
.= (s . (intpos 1)) + 1 by A16, A20, AMI_3:52, SCMPDS_2:59 ; :: thesis: ( (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 2) = s . (intpos 2) & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Element of NAT st i >= 7 holds
(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 2) = (Exec (GBP ,6 := GBP ,1),(IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s)) . (intpos 2) by SCMPDS_5:46
.= s . (intpos 2) by A15, A20, AMI_3:52, SCMPDS_2:59 ; :: thesis: ( (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Element of NAT st i >= 7 holds
(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = s . (intpos i) ) )
A21: DataLoc ((IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s) . GBP ),1 = intpos (0 + 1) by A19, SCMP_GCD:5;
thus (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 3) = (Exec (GBP ,6 := GBP ,1),(IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s)) . (intpos 3) by SCMPDS_5:46
.= (s . (intpos 3)) + 1 by A18, A20, AMI_3:52, SCMPDS_2:59 ; :: thesis: ( (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Element of NAT st i >= 7 holds
(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 4) = (Exec (GBP ,6 := GBP ,1),(IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s)) . (intpos 4) by SCMPDS_5:46
.= (s . (intpos 3)) + 1 by A14, A20, AMI_3:52, SCMPDS_2:59 ; :: thesis: ( (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Element of NAT st i >= 7 holds
(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 6) = (Exec (GBP ,6 := GBP ,1),(IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s)) . (intpos 6) by SCMPDS_5:46
.= (s . (intpos 1)) + 1 by A16, A20, A21, SCMPDS_2:59 ; :: thesis: for i being Element of NAT st i >= 7 holds
(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = s . (intpos i)

A22: now

let i be Element of NAT ; :: thesis: ( i >= 7 implies (Exec (AddTo GBP ,3,1),(Initialize s)) . (intpos i) = s . (intpos i) )
assume i >= 7 ; :: thesis: (Exec (AddTo GBP ,3,1),(Initialize s)) . (intpos i) = s . (intpos i)
then i > 3 by XXREAL_0:2;
hence (Exec (AddTo GBP ,3,1),(Initialize s)) . (intpos i) = (Initialize s) . (intpos i) by A2, AMI_3:52, SCMPDS_2:60
.= s . (intpos i) by SCMPDS_5:40 ;
:: thesis: verum

end;

A23: now

let i be Element of NAT ; :: thesis: ( i >= 7 implies (IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s) . (intpos i) = s . (intpos i) )
assume A24: i >= 7 ; :: thesis: (IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s) . (intpos i) = s . (intpos i)
then A25: i > 4 by XXREAL_0:2;
thus (IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s) . (intpos i) = (Exec (GBP ,4 := GBP ,3),(Exec (AddTo GBP ,3,1),(Initialize s))) . (intpos i) by SCMPDS_5:47
.= (Exec (AddTo GBP ,3,1),(Initialize s)) . (intpos i) by A4, A25, AMI_3:52, SCMPDS_2:59
.= s . (intpos i) by A22, A24 ; :: thesis: verum

end;

A26: now

let i be Element of NAT ; :: thesis: ( i >= 7 implies (IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s) . (intpos i) = s . (intpos i) )
assume A27: i >= 7 ; :: thesis: (IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s) . (intpos i) = s . (intpos i)
then A28: i > 1 by XXREAL_0:2;
thus (IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s) . (intpos i) = (Exec (AddTo GBP ,1,1),(IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s)) . (intpos i) by SCMPDS_5:46
.= (IExec ((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)),s) . (intpos i) by A11, A28, AMI_3:52, SCMPDS_2:60
.= s . (intpos i) by A23, A27 ; :: thesis: verum

end;

hereby :: thesis: verum

let i be Element of NAT ; :: thesis: ( i >= 7 implies (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = s . (intpos i) )
assume A29: i >= 7 ; :: thesis: (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = s . (intpos i)
then A30: i > 6 by XXREAL_0:2;
thus (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = (Exec (GBP ,6 := GBP ,1),(IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s)) . (intpos i) by SCMPDS_5:46
.= (IExec (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)),s) . (intpos i) by A20, A30, AMI_3:52, SCMPDS_2:59
.= s . (intpos i) by A26, A29 ; :: thesis: verum

end;