set a = GBP ;
let s be 0 -started 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;