let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; for s being State of SCMPDS st s . GBP = 0 holds
( (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s)) . GBP = 0 & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s)) . (intpos 1) = s . (intpos 2) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,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)))),P,s)) . (intpos 3) = (s . (intpos 3)) - 1 )
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)))),P,s)) . GBP = 0 & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s)) . (intpos 1) = s . (intpos 2) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,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)))),P,s)) . (intpos 3) = (s . (intpos 3)) - 1 ) )
set t0 = Initialize s;
set t1 = IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s);
set t2 = IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s);
set Q0 = P;
set t3 = IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s);
set t4 = Exec (((GBP,4) := (GBP,2)),(Initialize s));
set a4 = intpos 4;
A1:
Initialize (Initialize s) = Initialize s
;
A2:
IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s) = IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,(Initialize s))
by SCMPDS_5:48;
A3:
IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s) = IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,(Initialize s))
by SCMPDS_5:48;
A4:
IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s) = IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,(Initialize s))
by SCMPDS_5:48;
assume
s . GBP = 0
; ( (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s)) . GBP = 0 & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s)) . (intpos 1) = s . (intpos 2) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,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)))),P,s)) . (intpos 3) = (s . (intpos 3)) - 1 )
then A5:
(Initialize s) . GBP = 0
by SCMPDS_5:40;
then
DataLoc (((Initialize s) . GBP),4) = intpos (0 + 4)
by SCMP_GCD:5;
then A6: (Exec (((GBP,4) := (GBP,2)),(Initialize s))) . (intpos 4) =
(Initialize s) . (DataLoc (((Initialize s) . GBP),2))
by SCMPDS_2:59
.=
(Initialize s) . (intpos (0 + 2))
by A5, SCMP_GCD:5
.=
s . (intpos 2)
by SCMPDS_5:40
;
0 <> abs (((Initialize s) . GBP) + 4)
by A5, ABSVALUE:def 1;
then
GBP <> DataLoc (((Initialize s) . GBP),4)
by ZFMISC_1:33;
then A7:
(Exec (((GBP,4) := (GBP,2)),(Initialize s))) . GBP = 0
by A5, SCMPDS_2:59;
then A8:
DataLoc (((Exec (((GBP,4) := (GBP,2)),(Initialize s))) . GBP),2) = intpos (0 + 2)
by SCMP_GCD:5;
0 <> abs (((Exec (((GBP,4) := (GBP,2)),(Initialize s))) . GBP) + 2)
by A7, ABSVALUE:def 1;
then A9:
GBP <> DataLoc (((Exec (((GBP,4) := (GBP,2)),(Initialize s))) . GBP),2)
by ZFMISC_1:33;
A10: (IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP =
(Exec ((AddTo (GBP,2,GBP,1)),(Exec (((GBP,4) := (GBP,2)),(Initialize s))))) . GBP
by A1, A4, SCMPDS_5:47
.=
0
by A7, A9, SCMPDS_2:61
;
then A11:
DataLoc (((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP),1) = intpos (0 + 1)
by SCMP_GCD:5;
4 <> abs (((Exec (((GBP,4) := (GBP,2)),(Initialize s))) . GBP) + 2)
by A7, ABSVALUE:def 1;
then A12:
intpos 4 <> DataLoc (((Exec (((GBP,4) := (GBP,2)),(Initialize s))) . GBP),2)
by ZFMISC_1:33;
A13: (IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . (intpos 4) =
(Exec ((AddTo (GBP,2,GBP,1)),(Exec (((GBP,4) := (GBP,2)),(Initialize s))))) . (intpos 4)
by A1, A4, SCMPDS_5:47
.=
s . (intpos 2)
by A6, A12, SCMPDS_2:61
;
A14: (IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)) . (intpos 1) =
(Exec (((GBP,1) := (GBP,4)),(IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)))) . (intpos 1)
by A3, A4, SCMPDS_5:46
.=
(IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . (DataLoc (((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP),4))
by A11, SCMPDS_2:59
.=
s . (intpos 2)
by A10, A13, SCMP_GCD:5
;
3 <> abs (((Exec (((GBP,4) := (GBP,2)),(Initialize s))) . GBP) + 2)
by A7, ABSVALUE:def 1;
then A15:
intpos 3 <> DataLoc (((Exec (((GBP,4) := (GBP,2)),(Initialize s))) . GBP),2)
by ZFMISC_1:33;
2 <> abs (((Initialize s) . GBP) + 4)
by A5, ABSVALUE:def 1;
then
intpos 2 <> DataLoc (((Initialize s) . GBP),4)
by ZFMISC_1:33;
then A16: (Exec (((GBP,4) := (GBP,2)),(Initialize s))) . (intpos 2) =
(Initialize s) . (intpos 2)
by SCMPDS_2:59
.=
s . (intpos 2)
by SCMPDS_5:40
;
1 <> abs (((Initialize s) . GBP) + 4)
by A5, ABSVALUE:def 1;
then
intpos 1 <> DataLoc (((Initialize s) . GBP),4)
by ZFMISC_1:33;
then A17: (Exec (((GBP,4) := (GBP,2)),(Initialize s))) . (intpos 1) =
(Initialize s) . (intpos 1)
by SCMPDS_2:59
.=
s . (intpos 1)
by SCMPDS_5:40
;
3 <> abs (((Initialize s) . GBP) + 4)
by A5, ABSVALUE:def 1;
then
intpos 3 <> DataLoc (((Initialize s) . GBP),4)
by ZFMISC_1:33;
then A18: (Exec (((GBP,4) := (GBP,2)),(Initialize s))) . (intpos 3) =
(Initialize 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))),P,s)) . GBP) + 1)
by A10, ABSVALUE:def 1;
then A19:
GBP <> DataLoc (((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP),1)
by ZFMISC_1:33;
A20: (IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)) . GBP =
(Exec (((GBP,1) := (GBP,4)),(IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)))) . GBP
by A3, A4, SCMPDS_5:46
.=
0
by A10, A19, SCMPDS_2:59
;
then A21:
DataLoc (((IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)) . GBP),3) = intpos (0 + 3)
by SCMP_GCD:5;
2 <> abs (((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP) + 1)
by A10, ABSVALUE:def 1;
then A22:
intpos 2 <> DataLoc (((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP),1)
by ZFMISC_1:33;
A23: (IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . (intpos 2) =
(Exec ((AddTo (GBP,2,GBP,1)),(Exec (((GBP,4) := (GBP,2)),(Initialize s))))) . (intpos 2)
by A1, A4, SCMPDS_5:47
.=
((Exec (((GBP,4) := (GBP,2)),(Initialize s))) . (intpos 2)) + ((Exec (((GBP,4) := (GBP,2)),(Initialize s))) . (DataLoc (((Exec (((GBP,4) := (GBP,2)),(Initialize s))) . GBP),1)))
by A8, SCMPDS_2:61
.=
(s . (intpos 2)) + (s . (intpos 1))
by A7, A17, A16, SCMP_GCD:5
;
A24: (IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)) . (intpos 2) =
(Exec (((GBP,1) := (GBP,4)),(IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)))) . (intpos 2)
by A3, A4, SCMPDS_5:46
.=
(s . (intpos 2)) + (s . (intpos 1))
by A23, A22, SCMPDS_2:59
;
3 <> abs (((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP) + 1)
by A10, ABSVALUE:def 1;
then A25:
intpos 3 <> DataLoc (((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP),1)
by ZFMISC_1:33;
0 <> abs (((IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)) . GBP) + 3)
by A20, ABSVALUE:def 1;
then A26:
GBP <> DataLoc (((IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,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)))),P,s)) . GBP =
(Exec ((AddTo (GBP,3,(- 1))),(IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)))) . GBP
by A2, A3, SCMPDS_5:46
.=
0
by A20, A26, SCMPDS_2:60
; ( (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s)) . (intpos 1) = s . (intpos 2) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,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)))),P,s)) . (intpos 3) = (s . (intpos 3)) - 1 )
1 <> abs (((IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)) . GBP) + 3)
by A20, ABSVALUE:def 1;
then A27:
intpos 1 <> DataLoc (((IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,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)))),P,s)) . (intpos 1) =
(Exec ((AddTo (GBP,3,(- 1))),(IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)))) . (intpos 1)
by A2, A3, SCMPDS_5:46
.=
s . (intpos 2)
by A14, A27, SCMPDS_2:60
; ( (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,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)))),P,s)) . (intpos 3) = (s . (intpos 3)) - 1 )
2 <> abs (((IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)) . GBP) + 3)
by A20, ABSVALUE:def 1;
then A28:
intpos 2 <> DataLoc (((IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)) . GBP),3)
by ZFMISC_1:33;
A29: (IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . (intpos 3) =
(Exec ((AddTo (GBP,2,GBP,1)),(Exec (((GBP,4) := (GBP,2)),(Initialize s))))) . (intpos 3)
by A1, A4, SCMPDS_5:47
.=
s . (intpos 3)
by A18, A15, SCMPDS_2:61
;
A30: (IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)) . (intpos 3) =
(Exec (((GBP,1) := (GBP,4)),(IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)))) . (intpos 3)
by A3, A4, SCMPDS_5:46
.=
s . (intpos 3)
by A29, A25, SCMPDS_2:59
;
thus (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s)) . (intpos 2) =
(Exec ((AddTo (GBP,3,(- 1))),(IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)))) . (intpos 2)
by A2, A3, SCMPDS_5:46
.=
(s . (intpos 1)) + (s . (intpos 2))
by A24, A28, SCMPDS_2:60
; (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,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)))),P,s)) . (intpos 3) =
(Exec ((AddTo (GBP,3,(- 1))),(IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)))) . (intpos 3)
by A2, A3, SCMPDS_5:46
.=
((IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)) . (intpos 3)) + (- 1)
by A21, SCMPDS_2:60
.=
(s . (intpos 3)) - 1
by A30
; verum