set a = GBP ;
let s be State of SCMPDS ; ( 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 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;
assume
s . GBP = 0
; ( (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 )
then A1:
(Initialized s) . GBP = 0
by SCMPDS_5:40;
then
DataLoc ((Initialized s) . GBP ),4 = intpos (0 + 4)
by SCMP_GCD:5;
then A2: (Exec (GBP ,4 := GBP ,2),(Initialized s)) . (intpos 4) =
(Initialized s) . (DataLoc ((Initialized s) . GBP ),2)
by SCMPDS_2:59
.=
(Initialized s) . (intpos (0 + 2))
by A1, SCMP_GCD:5
.=
s . (intpos 2)
by SCMPDS_5:40
;
0 <> abs (((Initialized s) . GBP ) + 4)
by A1, ABSVALUE:def 1;
then
GBP <> DataLoc ((Initialized s) . GBP ),4
by ZFMISC_1:33;
then A3:
(Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP = 0
by A1, SCMPDS_2:59;
then A4:
DataLoc ((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ),2 = intpos (0 + 2)
by SCMP_GCD:5;
0 <> abs (((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ) + 2)
by A3, ABSVALUE:def 1;
then A5:
GBP <> DataLoc ((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ),2
by ZFMISC_1:33;
A6: (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 A3, A5, SCMPDS_2:61
;
then A7:
DataLoc ((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ),1 = intpos (0 + 1)
by SCMP_GCD:5;
4 <> abs (((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ) + 2)
by A3, ABSVALUE:def 1;
then A8:
intpos 4 <> DataLoc ((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ),2
by ZFMISC_1:33;
A9: (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 A2, A8, SCMPDS_2:61
;
A10: (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 A7, SCMPDS_2:59
.=
s . (intpos 2)
by A6, A9, SCMP_GCD:5
;
3 <> abs (((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ) + 2)
by A3, ABSVALUE:def 1;
then A11:
intpos 3 <> DataLoc ((Exec (GBP ,4 := GBP ,2),(Initialized s)) . GBP ),2
by ZFMISC_1:33;
2 <> abs (((Initialized s) . GBP ) + 4)
by A1, ABSVALUE:def 1;
then
intpos 2 <> DataLoc ((Initialized s) . GBP ),4
by ZFMISC_1:33;
then A12: (Exec (GBP ,4 := GBP ,2),(Initialized s)) . (intpos 2) =
(Initialized s) . (intpos 2)
by SCMPDS_2:59
.=
s . (intpos 2)
by SCMPDS_5:40
;
1 <> abs (((Initialized s) . GBP ) + 4)
by A1, ABSVALUE:def 1;
then
intpos 1 <> DataLoc ((Initialized s) . GBP ),4
by ZFMISC_1:33;
then A13: (Exec (GBP ,4 := GBP ,2),(Initialized s)) . (intpos 1) =
(Initialized s) . (intpos 1)
by SCMPDS_2:59
.=
s . (intpos 1)
by SCMPDS_5:40
;
3 <> abs (((Initialized s) . GBP ) + 4)
by A1, ABSVALUE:def 1;
then
intpos 3 <> DataLoc ((Initialized s) . GBP ),4
by ZFMISC_1:33;
then A14: (Exec (GBP ,4 := GBP ,2),(Initialized s)) . (intpos 3) =
(Initialized s) . (intpos 3)
by SCMPDS_2:59
.=
s . (intpos 3)
by SCMPDS_5:40
;
0 <> abs (((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ) + 1)
by A6, ABSVALUE:def 1;
then A15:
GBP <> DataLoc ((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ),1
by ZFMISC_1:33;
A16: (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 A6, A15, SCMPDS_2:59
;
then A17:
DataLoc ((IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . GBP ),3 = intpos (0 + 3)
by SCMP_GCD:5;
2 <> abs (((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ) + 1)
by A6, ABSVALUE:def 1;
then A18:
intpos 2 <> 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)),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 A4, SCMPDS_2:61
.=
(s . (intpos 2)) + (s . (intpos 1))
by A3, A13, A12, SCMP_GCD:5
;
A20: (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 A19, A18, SCMPDS_2:59
;
3 <> abs (((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ) + 1)
by A6, ABSVALUE:def 1;
then A21:
intpos 3 <> DataLoc ((IExec ((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)),s) . GBP ),1
by ZFMISC_1:33;
0 <> abs (((IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . GBP ) + 3)
by A16, ABSVALUE:def 1;
then A22:
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 A16, A22, SCMPDS_2:60
; ( (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 A16, ABSVALUE:def 1;
then A23:
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 A10, A23, SCMPDS_2:60
; ( (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 A16, ABSVALUE:def 1;
then A24:
intpos 2 <> DataLoc ((IExec (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)),s) . GBP ),3
by ZFMISC_1:33;
A25: (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 A14, A11, SCMPDS_2:61
;
A26: (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 A25, A21, SCMPDS_2:59
;
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 A20, A24, SCMPDS_2:60
; (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 A17, SCMPDS_2:60
.=
(s . (intpos 3)) - 1
by A26
; verum