let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS st s . GBP = 0 holds
( (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . GBP = 0 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 1) = (s . (intpos 1)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 2) = s . (intpos 2) & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Nat st i >= 7 holds
(IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = s . (intpos i) ) )
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))),P,s)) . GBP = 0 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 1) = (s . (intpos 1)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 2) = s . (intpos 2) & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Nat st i >= 7 holds
(IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = s . (intpos i) ) ) )
A1: Initialize s = s by MEMSTR_0:44;
set t0 = Initialize s;
set t1 = IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s);
set t2 = IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s);
set t3 = IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s);
set t4 = Exec ((AddTo (GBP,3,1)),s);
assume A2: s . GBP = 0 ; :: thesis: ( (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . GBP = 0 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 1) = (s . (intpos 1)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 2) = s . (intpos 2) & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Nat st i >= 7 holds
(IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = s . (intpos i) ) )
then A3: (Initialize s) . GBP = 0 by SCMPDS_5:15;
then A4: DataLoc (((Initialize s) . GBP),3) = intpos (0 + 3) by SCMP_GCD:1;
then A5: (Exec ((AddTo (GBP,3,1)),s)) . GBP = 0 by A3, A2, AMI_3:10, SCMPDS_2:48;
then A6: DataLoc (((Exec ((AddTo (GBP,3,1)),s)) . GBP),4) = intpos (0 + 4) by SCMP_GCD:1;
A7: (Exec ((AddTo (GBP,3,1)),s)) . (intpos 2) = s . (intpos 2) by A4, A2, A3, AMI_3:10, SCMPDS_2:48;
A8: (IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . (intpos 2) = (Exec (((GBP,4) := (GBP,3)),(Exec ((AddTo (GBP,3,1)),s)))) . (intpos 2) by SCMPDS_5:42
.= s . (intpos 2) by A7, A6, AMI_3:10, SCMPDS_2:47 ;
A9: (Exec ((AddTo (GBP,3,1)),s)) . (intpos 1) = s . (intpos 1) by A4, A2, A3, AMI_3:10, SCMPDS_2:48;
A10: (IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . (intpos 1) = (Exec (((GBP,4) := (GBP,3)),(Exec ((AddTo (GBP,3,1)),s)))) . (intpos 1) by SCMPDS_5:42
.= s . (intpos 1) by A9, A6, AMI_3:10, SCMPDS_2:47 ;
A11: (Exec ((AddTo (GBP,3,1)),s)) . (intpos 3) = (s . (intpos 3)) + 1 by A4, A1, SCMPDS_2:48;
A12: (IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . GBP = (Exec (((GBP,4) := (GBP,3)),(Exec ((AddTo (GBP,3,1)),s)))) . GBP by SCMPDS_5:42
.= 0 by A5, A6, AMI_3:10, SCMPDS_2:47 ;
then A13: DataLoc (((IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . GBP),1) = intpos (0 + 1) by SCMP_GCD:1;
A14: DataLoc (((Exec ((AddTo (GBP,3,1)),s)) . GBP),3) = intpos (0 + 3) by A5, SCMP_GCD:1;
A15: (IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . (intpos 4) = (Exec (((GBP,4) := (GBP,3)),(Exec ((AddTo (GBP,3,1)),s)))) . (intpos 4) by SCMPDS_5:42
.= (s . (intpos 3)) + 1 by A11, A6, A14, SCMPDS_2:47 ;
A16: (IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . (intpos 4) = (Exec ((AddTo (GBP,1,1)),(IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)))) . (intpos 4) by SCMPDS_5:41
.= (s . (intpos 3)) + 1 by A15, A13, AMI_3:10, SCMPDS_2:48 ;
A17: (IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . (intpos 2) = (Exec ((AddTo (GBP,1,1)),(IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)))) . (intpos 2) by SCMPDS_5:41
.= s . (intpos 2) by A8, A13, AMI_3:10, SCMPDS_2:48 ;
A18: (IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . (intpos 1) = (Exec ((AddTo (GBP,1,1)),(IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)))) . (intpos 1) by SCMPDS_5:41
.= (s . (intpos 1)) + 1 by A10, A13, SCMPDS_2:48 ;
A19: (IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . (intpos 3) = (Exec (((GBP,4) := (GBP,3)),(Exec ((AddTo (GBP,3,1)),s)))) . (intpos 3) by SCMPDS_5:42
.= (s . (intpos 3)) + 1 by A11, A6, AMI_3:10, SCMPDS_2:47 ;
A20: (IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . (intpos 3) = (Exec ((AddTo (GBP,1,1)),(IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)))) . (intpos 3) by SCMPDS_5:41
.= (s . (intpos 3)) + 1 by A19, A13, AMI_3:10, SCMPDS_2:48 ;
A21: (IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . GBP = (Exec ((AddTo (GBP,1,1)),(IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)))) . GBP by SCMPDS_5:41
.= 0 by A12, A13, AMI_3:10, SCMPDS_2:48 ;
then A22: DataLoc (((IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . GBP),6) = intpos (0 + 6) by SCMP_GCD:1;
thus (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . GBP = (Exec (((GBP,6) := (GBP,1)),(IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)))) . GBP by SCMPDS_5:41
.= 0 by A21, A22, AMI_3:10, SCMPDS_2:47 ; :: thesis: ( (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 1) = (s . (intpos 1)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 2) = s . (intpos 2) & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Nat st i >= 7 holds
(IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = s . (intpos i) ) )
thus (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 1) = (Exec (((GBP,6) := (GBP,1)),(IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)))) . (intpos 1) by SCMPDS_5:41
.= (s . (intpos 1)) + 1 by A18, A22, AMI_3:10, SCMPDS_2:47 ; :: thesis: ( (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 2) = s . (intpos 2) & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Nat st i >= 7 holds
(IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = s . (intpos i) ) )
thus (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 2) = (Exec (((GBP,6) := (GBP,1)),(IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)))) . (intpos 2) by SCMPDS_5:41
.= s . (intpos 2) by A17, A22, AMI_3:10, SCMPDS_2:47 ; :: thesis: ( (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Nat st i >= 7 holds
(IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = s . (intpos i) ) )
A23: DataLoc (((IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . GBP),1) = intpos (0 + 1) by A21, SCMP_GCD:1;
thus (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 3) = (Exec (((GBP,6) := (GBP,1)),(IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)))) . (intpos 3) by SCMPDS_5:41
.= (s . (intpos 3)) + 1 by A20, A22, AMI_3:10, SCMPDS_2:47 ; :: thesis: ( (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Nat st i >= 7 holds
(IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = s . (intpos i) ) )
thus (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 4) = (Exec (((GBP,6) := (GBP,1)),(IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)))) . (intpos 4) by SCMPDS_5:41
.= (s . (intpos 3)) + 1 by A16, A22, AMI_3:10, SCMPDS_2:47 ; :: thesis: ( (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Nat st i >= 7 holds
(IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = s . (intpos i) ) )
thus (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 6) = (Exec (((GBP,6) := (GBP,1)),(IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)))) . (intpos 6) by SCMPDS_5:41
.= (s . (intpos 1)) + 1 by A18, A22, A23, SCMPDS_2:47 ; :: thesis: for i being Nat st i >= 7 holds
(IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = s . (intpos i)

A24: now :: thesis: for i being Nat st i >= 7 holds
(Exec ((AddTo (GBP,3,1)),s)) . (intpos i) = s . (intpos i)

let i be Nat; :: thesis: ( i >= 7 implies (Exec ((AddTo (GBP,3,1)),s)) . (intpos i) = s . (intpos i) )
assume i >= 7 ; :: thesis: (Exec ((AddTo (GBP,3,1)),s)) . (intpos i) = s . (intpos i)
then i > 3 by XXREAL_0:2;
hence (Exec ((AddTo (GBP,3,1)),s)) . (intpos i) = (Initialize s) . (intpos i) by A4, A1, AMI_3:10, SCMPDS_2:48
.= s . (intpos i) by SCMPDS_5:15 ;
:: thesis: verum

end;

A25: now :: thesis: for i being Nat st i >= 7 holds
(IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . (intpos i) = s . (intpos i)

let i be Nat; :: thesis: ( i >= 7 implies (IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . (intpos i) = s . (intpos i) )
assume A26: i >= 7 ; :: thesis: (IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . (intpos i) = s . (intpos i)
then A27: i > 4 by XXREAL_0:2;
thus (IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . (intpos i) = (Exec (((GBP,4) := (GBP,3)),(Exec ((AddTo (GBP,3,1)),s)))) . (intpos i) by SCMPDS_5:42
.= (Exec ((AddTo (GBP,3,1)),s)) . (intpos i) by A6, A27, AMI_3:10, SCMPDS_2:47
.= s . (intpos i) by A24, A26 ; :: thesis: verum

end;

A28: now :: thesis: for i being Nat st i >= 7 holds
(IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . (intpos i) = s . (intpos i)

let i be Nat; :: thesis: ( i >= 7 implies (IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . (intpos i) = s . (intpos i) )
assume A29: i >= 7 ; :: thesis: (IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . (intpos i) = s . (intpos i)
then A30: i > 1 by XXREAL_0:2;
thus (IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . (intpos i) = (Exec ((AddTo (GBP,1,1)),(IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)))) . (intpos i) by SCMPDS_5:41
.= (IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . (intpos i) by A13, A30, AMI_3:10, SCMPDS_2:48
.= s . (intpos i) by A25, A29 ; :: thesis: verum

end;

hereby :: thesis: verum

let i be Nat; :: thesis: ( i >= 7 implies (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = s . (intpos i) )
assume A31: i >= 7 ; :: thesis: (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = s . (intpos i)
then A32: i > 6 by XXREAL_0:2;
thus (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = (Exec (((GBP,6) := (GBP,1)),(IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)))) . (intpos i) by SCMPDS_5:41
.= (IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . (intpos i) by A22, A32, AMI_3:10, SCMPDS_2:47
.= s . (intpos i) by A28, A31 ; :: thesis: verum

end;