set a = GBP ;
let s be State of SCMPDS ; :: thesis: for m being Element of NAT st s . GBP = 0 & s . (intpos 3) = m holds
( (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . GBP = 0 & (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 1) = (s . (intpos 1)) + (s . (intpos m)) & (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = (s . (intpos 2)) + 1 & (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = m + 1 & ( for i being Element of NAT st i > 3 holds
(IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
let m be Element of NAT ; :: thesis: ( s . GBP = 0 & s . (intpos 3) = m implies ( (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . GBP = 0 & (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 1) = (s . (intpos 1)) + (s . (intpos m)) & (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = (s . (intpos 2)) + 1 & (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = m + 1 & ( for i being Element of NAT st i > 3 holds
(IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) ) )
assume that
A1: s . GBP = 0 and
A2: s . (intpos 3) = m ; :: thesis: ( (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . GBP = 0 & (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 1) = (s . (intpos 1)) + (s . (intpos m)) & (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = (s . (intpos 2)) + 1 & (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = m + 1 & ( for i being Element of NAT st i > 3 holds
(IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
set t0 = Initialized s;
set t1 = IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s;
set t2 = IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s;
set t3 = Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s);
A3: (Initialized s) . (intpos 3) = m by A2, SCMPDS_5:40;
A4: (Initialized s) . GBP = 0 by A1, SCMPDS_5:40;
then 0 <> abs (((Initialized s) . GBP ) + 1) by ABSVALUE:def 1;
then GBP <> DataLoc ((Initialized s) . GBP ),1 by ZFMISC_1:33;
then A5: (Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . GBP = 0 by A4, SCMPDS_2:61;
then 0 <> abs (((Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . GBP ) + 2) by ABSVALUE:def 1;
then A6: GBP <> DataLoc ((Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . GBP ),2 by ZFMISC_1:33;
3 <> abs (((Initialized s) . GBP ) + 1) by A4, ABSVALUE:def 1;
then intpos 3 <> DataLoc ((Initialized s) . GBP ),1 by ZFMISC_1:33;
then A7: (Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . (intpos 3) = m by A3, SCMPDS_2:61;
3 <> abs (((Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . GBP ) + 2) by A5, ABSVALUE:def 1;
then A8: intpos 3 <> DataLoc ((Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . GBP ),2 by ZFMISC_1:33;
A9: (IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . (intpos 3) = (Exec (AddTo GBP ,2,1),(Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s))) . (intpos 3) by SCMPDS_5:47
.= m by A7, A8, SCMPDS_2:60 ;
A10: (Initialized s) . (intpos 1) = s . (intpos 1) by SCMPDS_5:40;
A11: DataLoc ((Initialized s) . GBP ),1 = intpos (0 + 1) by A4, SCMP_GCD:5;
then A12: (Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . (intpos 1) = ((Initialized s) . (intpos 1)) + ((Initialized s) . (DataLoc ((Initialized s) . (intpos 3)),0 )) by SCMPDS_2:61
.= ((Initialized s) . (intpos 1)) + ((Initialized s) . (intpos (m + 0 ))) by A3, SCMP_GCD:5
.= (s . (intpos 1)) + (s . (intpos m)) by A10, SCMPDS_5:40 ;
1 <> abs (((Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . GBP ) + 2) by A5, ABSVALUE:def 1;
then A13: intpos 1 <> DataLoc ((Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . GBP ),2 by ZFMISC_1:33;
A14: DataLoc ((Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . GBP ),2 = intpos (0 + 2) by A5, SCMP_GCD:5;
then A15: abs (((Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . GBP ) + 2) = 0 + 2 by ZFMISC_1:33;
2 <> abs (((Initialized s) . GBP ) + 1) by A4, ABSVALUE:def 1;
then intpos 2 <> DataLoc ((Initialized s) . GBP ),1 by ZFMISC_1:33;
then A16: (Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . (intpos 2) = (Initialized s) . (intpos 2) by SCMPDS_2:61
.= s . (intpos 2) by SCMPDS_5:40 ;
A17: (IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . GBP = (Exec (AddTo GBP ,2,1),(Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s))) . GBP by SCMPDS_5:47
.= 0 by A5, A6, SCMPDS_2:60 ;
then A18: DataLoc ((IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . GBP ),3 = intpos (0 + 3) by SCMP_GCD:5;
A19: (IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . (intpos 2) = (Exec (AddTo GBP ,2,1),(Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s))) . (intpos 2) by SCMPDS_5:47
.= (s . (intpos 2)) + 1 by A16, A14, SCMPDS_2:60 ;
A20: (IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . (intpos 1) = (Exec (AddTo GBP ,2,1),(Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s))) . (intpos 1) by SCMPDS_5:47
.= (s . (intpos 1)) + (s . (intpos m)) by A12, A13, SCMPDS_2:60 ;
0 <> abs (((IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . GBP ) + 3) by A17, ABSVALUE:def 1;
then A21: GBP <> DataLoc ((IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . GBP ),3 by ZFMISC_1:33;
thus (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . GBP = (Exec (AddTo GBP ,3,1),(IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s)) . GBP by SCMPDS_5:46
.= 0 by A17, A21, SCMPDS_2:60 ; :: thesis: ( (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 1) = (s . (intpos 1)) + (s . (intpos m)) & (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = (s . (intpos 2)) + 1 & (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = m + 1 & ( for i being Element of NAT st i > 3 holds
(IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
1 <> abs (((IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . GBP ) + 3) by A17, ABSVALUE:def 1;
then A22: intpos 1 <> DataLoc ((IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . GBP ),3 by ZFMISC_1:33;
thus (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 1) = (Exec (AddTo GBP ,3,1),(IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s)) . (intpos 1) by SCMPDS_5:46
.= (s . (intpos 1)) + (s . (intpos m)) by A20, A22, SCMPDS_2:60 ; :: thesis: ( (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = (s . (intpos 2)) + 1 & (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = m + 1 & ( for i being Element of NAT st i > 3 holds
(IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
2 <> abs (((IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . GBP ) + 3) by A17, ABSVALUE:def 1;
then A23: intpos 2 <> DataLoc ((IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . GBP ),3 by ZFMISC_1:33;
thus (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = (Exec (AddTo GBP ,3,1),(IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s)) . (intpos 2) by SCMPDS_5:46
.= (s . (intpos 2)) + 1 by A19, A23, SCMPDS_2:60 ; :: thesis: ( (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = m + 1 & ( for i being Element of NAT st i > 3 holds
(IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
thus (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = (Exec (AddTo GBP ,3,1),(IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s)) . (intpos 3) by SCMPDS_5:46
.= m + 1 by A9, A18, SCMPDS_2:60 ; :: thesis: for i being Element of NAT st i > 3 holds
(IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i)
A24: abs (((Initialized s) . GBP ) + 1) = 0 + 1 by A11, ZFMISC_1:33;

hereby :: thesis: verum

let i be Element of NAT ; :: thesis: ( i > 3 implies (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) )
assume A25: i > 3 ; :: thesis: (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i)
then A26: intpos i <> DataLoc ((IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . GBP ),3 by A18, ZFMISC_1:33;
i <> abs (((Initialized s) . GBP ) + 1) by A24, A25;
then A27: intpos i <> DataLoc ((Initialized s) . GBP ),1 by ZFMISC_1:33;
i <> abs (((Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . GBP ) + 2) by A15, A25;
then A28: intpos i <> DataLoc ((Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . GBP ),2 by ZFMISC_1:33;
thus (IExec (((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = (Exec (AddTo GBP ,3,1),(IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s)) . (intpos i) by SCMPDS_5:46
.= (IExec ((AddTo GBP ,1,(intpos 3),0 ) ';' (AddTo GBP ,2,1)),s) . (intpos i) by A26, SCMPDS_2:60
.= (Exec (AddTo GBP ,2,1),(Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s))) . (intpos i) by SCMPDS_5:47
.= (Exec (AddTo GBP ,1,(intpos 3),0 ),(Initialized s)) . (intpos i) by A28, SCMPDS_2:60
.= (Initialized s) . (intpos i) by A27, SCMPDS_2:61
.= s . (intpos i) by SCMPDS_5:40 ; :: thesis: verum

end;