let s be State of SCMPDS ; :: thesis: ( s . GBP = 0 implies ( (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . GBP = 0 & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 1) = s . (intpos 2) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 2) = (s . (intpos 1)) + (s . (intpos 2)) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 3) = (s . (intpos 3)) - 1 ) )
set a = GBP ;
assume A1: s . GBP = 0 ; :: thesis: ( (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . GBP = 0 & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 1) = s . (intpos 2) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 2) = (s . (intpos 1)) + (s . (intpos 2)) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 3) = (s . (intpos 3)) - 1 )
set t0 = Initialized s;
set t1 = IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s;
set t2 = IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s;
set t3 = IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s;
set t4 = Exec (GBP ,4 := GBP ,2),(Initialized s);
set a4 = intpos 4;
A2: (Initialized s) . GBP = 0 by A1, SCMPDS_5:40;
then A3: DataLoc ((Initialized s) . GBP ),4 = intpos (0 + 4) by SCMP_GCD:5;
0 <> abs (((Initialized s) . GBP ) + 4) by A2, ABSVALUE:def 1;
then GBP <> DataLoc ((Initialized s) . GBP ),4 by ZFMISC_1:33;
then A4: (Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP = 0 by A2, SCMPDS_2:59;
1 <> abs (((Initialized s) . GBP ) + 4) by A2, ABSVALUE:def 1;
then intpos 1 <> DataLoc ((Initialized s) . GBP ),4 by ZFMISC_1:33;
then A5: (Exec (GBP ,4 := GBP ,2),(Initialized s)) . (intpos 1) = (Initialized s) . (intpos 1) by SCMPDS_2:59
.= s . (intpos 1) by SCMPDS_5:40 ;
2 <> abs (((Initialized s) . GBP ) + 4) by A2, ABSVALUE:def 1;
then intpos 2 <> DataLoc ((Initialized s) . GBP ),4 by ZFMISC_1:33;
then A6: (Exec (GBP ,4 := GBP ,2),(Initialized s)) . (intpos 2) = (Initialized s) . (intpos 2) by SCMPDS_2:59
.= s . (intpos 2) by SCMPDS_5:40 ;
3 <> abs (((Initialized s) . GBP ) + 4) by A2, ABSVALUE:def 1;
then intpos 3 <> DataLoc ((Initialized s) . GBP ),4 by ZFMISC_1:33;
then A7: (Exec (GBP ,4 := GBP ,2),(Initialized s)) . (intpos 3) = (Initialized s) . (intpos 3) by SCMPDS_2:59
.= s . (intpos 3) by SCMPDS_5:40 ;
A8: (Exec (GBP ,4 := GBP ,2),(Initialized s)) . (intpos 4) = (Initialized s) . (DataLoc ((Initialized s) . GBP ),2) by A3, SCMPDS_2:59
.= (Initialized s) . (intpos (0 + 2)) by A2, SCMP_GCD:5
.= s . (intpos 2) by SCMPDS_5:40 ;
A9: DataLoc ((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ),2 = intpos (0 + 2) by A4, SCMP_GCD:5;
0 <> abs (((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ) + 2) by A4, ABSVALUE:def 1;
then A10: GBP <> DataLoc ((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ),2 by ZFMISC_1:33;
A11: (IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP = (Exec (AddTo GBP ,2,GBP ,1),(Exec (GBP ,4 := GBP ,2),(Initialized s))) . GBP by SCMPDS_5:47
.= 0 by A4, A10, SCMPDS_2:61 ;
A12: (IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . (intpos 2) = (Exec (AddTo GBP ,2,GBP ,1),(Exec (GBP ,4 := GBP ,2),(Initialized s))) . (intpos 2) by SCMPDS_5:47
.= ((Exec (GBP ,4 := GBP ,2),(Initialized s)) . (intpos 2)) + ((Exec (GBP ,4 := GBP ,2),(Initialized s)) . (DataLoc ((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ),1)) by A9, SCMPDS_2:61
.= (s . (intpos 2)) + (s . (intpos 1)) by A4, A5, A6, SCMP_GCD:5 ;
3 <> abs (((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ) + 2) by A4, ABSVALUE:def 1;
then A13: intpos 3 <> DataLoc ((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ),2 by ZFMISC_1:33;
A14: (IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . (intpos 3) = (Exec (AddTo GBP ,2,GBP ,1),(Exec (GBP ,4 := GBP ,2),(Initialized s))) . (intpos 3) by SCMPDS_5:47
.= s . (intpos 3) by A7, A13, SCMPDS_2:61 ;
4 <> abs (((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ) + 2) by A4, ABSVALUE:def 1;
then A15: intpos 4 <> DataLoc ((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ),2 by ZFMISC_1:33;
A16: (IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . (intpos 4) = (Exec (AddTo GBP ,2,GBP ,1),(Exec (GBP ,4 := GBP ,2),(Initialized s))) . (intpos 4) by SCMPDS_5:47
.= s . (intpos 2) by A8, A15, SCMPDS_2:61 ;
A17: DataLoc ((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ),1 = intpos (0 + 1) by A11, SCMP_GCD:5;
0 <> abs (((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ) + 1) by A11, ABSVALUE:def 1;
then A18: GBP <> DataLoc ((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ),1 by ZFMISC_1:33;
A19: (IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . GBP = (Exec (GBP ,1 := GBP ,4),(IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s)) . GBP by SCMPDS_5:46
.= 0 by A11, A18, SCMPDS_2:59 ;
A20: (IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . (intpos 1) = (Exec (GBP ,1 := GBP ,4),(IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s)) . (intpos 1) by SCMPDS_5:46
.= (IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . (DataLoc ((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ),4) by A17, SCMPDS_2:59
.= s . (intpos 2) by A11, A16, SCMP_GCD:5 ;
2 <> abs (((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ) + 1) by A11, ABSVALUE:def 1;
then A21: intpos 2 <> DataLoc ((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ),1 by ZFMISC_1:33;
A22: (IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . (intpos 2) = (Exec (GBP ,1 := GBP ,4),(IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s)) . (intpos 2) by SCMPDS_5:46
.= (s . (intpos 2)) + (s . (intpos 1)) by A12, A21, SCMPDS_2:59 ;
3 <> abs (((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ) + 1) by A11, ABSVALUE:def 1;
then A23: intpos 3 <> DataLoc ((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ),1 by ZFMISC_1:33;
A24: (IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . (intpos 3) = (Exec (GBP ,1 := GBP ,4),(IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s)) . (intpos 3) by SCMPDS_5:46
.= s . (intpos 3) by A14, A23, SCMPDS_2:59 ;
A25: DataLoc ((IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . GBP ),3 = intpos (0 + 3) by A19, SCMP_GCD:5;
0 <> abs (((IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . GBP ) + 3) by A19, ABSVALUE:def 1;
then A26: GBP <> DataLoc ((IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . GBP ),3 by ZFMISC_1:33;
thus (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . GBP = (Exec (AddTo GBP ,3,(- 1)),(IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s)) . GBP by SCMPDS_5:46
.= 0 by A19, A26, SCMPDS_2:60 ; :: thesis: ( (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 1) = s . (intpos 2) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 2) = (s . (intpos 1)) + (s . (intpos 2)) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 3) = (s . (intpos 3)) - 1 )
1 <> abs (((IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . GBP ) + 3) by A19, ABSVALUE:def 1;
then A27: intpos 1 <> DataLoc ((IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . GBP ),3 by ZFMISC_1:33;
thus (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 1) = (Exec (AddTo GBP ,3,(- 1)),(IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s)) . (intpos 1) by SCMPDS_5:46
.= s . (intpos 2) by A20, A27, SCMPDS_2:60 ; :: thesis: ( (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 2) = (s . (intpos 1)) + (s . (intpos 2)) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 3) = (s . (intpos 3)) - 1 )
2 <> abs (((IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . GBP ) + 3) by A19, ABSVALUE:def 1;
then A28: intpos 2 <> DataLoc ((IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . GBP ),3 by ZFMISC_1:33;
thus (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 2) = (Exec (AddTo GBP ,3,(- 1)),(IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s)) . (intpos 2) by SCMPDS_5:46
.= (s . (intpos 1)) + (s . (intpos 2)) by A22, A28, SCMPDS_2:60 ; :: thesis: (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 3) = (s . (intpos 3)) - 1
thus (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),s) . (intpos 3) = (Exec (AddTo GBP ,3,(- 1)),(IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s)) . (intpos 3) by SCMPDS_5:46
.= ((IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . (intpos 3)) + (- 1) by A25, SCMPDS_2:60
.= (s . (intpos 3)) - 1 by A24 ; :: thesis: verum