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

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))),P,(Initialize 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))),P,(Initialize s))) . (intpos i) = s . (intpos i)
then A26: intpos i <> DataLoc (((IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),P,(Initialize s))) . GBP),3) by A18, XTUPLE_0:1;
i <> |.(((Initialize s) . GBP) + 1).| by A24, A25;
then A27: intpos i <> DataLoc (((Initialize s) . GBP),1) by XTUPLE_0:1;
i <> |.(((Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize s))) . GBP) + 2).| by A15, A25;
then A28: intpos i <> DataLoc (((Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize s))) . GBP),2) by XTUPLE_0:1;
thus (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = (Exec ((AddTo (GBP,3,1)),(IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),P,(Initialize s))))) . (intpos i) by SCMPDS_5:41
.= (IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),P,(Initialize s))) . (intpos i) by A26, SCMPDS_2:48
.= (Exec ((AddTo (GBP,2,1)),(Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize s))))) . (intpos i) by SCMPDS_5:42
.= (Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize s))) . (intpos i) by A28, SCMPDS_2:48
.= (Initialize s) . (intpos i) by A27, SCMPDS_2:49
.= s . (intpos i) by SCMPDS_5:15 ; :: thesis: verum

end;