let P be Instruction-Sequence of SCMPDS; for s being 0 -started 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 0 -started 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 = 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)),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)))),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 A1:
s . GBP = 0
;
then
DataLoc ((s . GBP),4) = intpos (0 + 4)
by SCMP_GCD:1;
then A2: (Exec (((GBP,4) := (GBP,2)),s)) . (intpos 4) =
s . (DataLoc ((s . GBP),2))
by SCMPDS_2:47
.=
s . (intpos (0 + 2))
by A1, SCMP_GCD:1
.=
s . (intpos 2)
;
0 <> |.((s . GBP) + 4).|
by A1, ABSVALUE:def 1;
then
GBP <> DataLoc ((s . GBP),4)
by XTUPLE_0:1;
then A3:
(Exec (((GBP,4) := (GBP,2)),s)) . GBP = 0
by A1, SCMPDS_2:47;
then A4:
DataLoc (((Exec (((GBP,4) := (GBP,2)),s)) . GBP),2) = intpos (0 + 2)
by SCMP_GCD:1;
0 <> |.(((Exec (((GBP,4) := (GBP,2)),s)) . GBP) + 2).|
by A3, ABSVALUE:def 1;
then A5:
GBP <> DataLoc (((Exec (((GBP,4) := (GBP,2)),s)) . GBP),2)
by XTUPLE_0:1;
A6: (IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP =
(Exec ((AddTo (GBP,2,GBP,1)),(Exec (((GBP,4) := (GBP,2)),s)))) . GBP
by SCMPDS_5:42
.=
0
by A3, A5, SCMPDS_2:49
;
then A7:
DataLoc (((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP),1) = intpos (0 + 1)
by SCMP_GCD:1;
4 <> |.(((Exec (((GBP,4) := (GBP,2)),s)) . GBP) + 2).|
by A3, ABSVALUE:def 1;
then A8:
intpos 4 <> DataLoc (((Exec (((GBP,4) := (GBP,2)),s)) . GBP),2)
by XTUPLE_0:1;
A9: (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)),s)))) . (intpos 4)
by SCMPDS_5:42
.=
s . (intpos 2)
by A2, A8, SCMPDS_2:49
;
A10: (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 SCMPDS_5:41
.=
(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 A7, SCMPDS_2:47
.=
s . (intpos 2)
by A6, A9, SCMP_GCD:1
;
3 <> |.(((Exec (((GBP,4) := (GBP,2)),s)) . GBP) + 2).|
by A3, ABSVALUE:def 1;
then A11:
intpos 3 <> DataLoc (((Exec (((GBP,4) := (GBP,2)),s)) . GBP),2)
by XTUPLE_0:1;
2 <> |.((s . GBP) + 4).|
by A1, ABSVALUE:def 1;
then
intpos 2 <> DataLoc ((s . GBP),4)
by XTUPLE_0:1;
then A12: (Exec (((GBP,4) := (GBP,2)),s)) . (intpos 2) =
s . (intpos 2)
by SCMPDS_2:47
.=
s . (intpos 2)
;
1 <> |.((s . GBP) + 4).|
by A1, ABSVALUE:def 1;
then
intpos 1 <> DataLoc ((s . GBP),4)
by XTUPLE_0:1;
then A13: (Exec (((GBP,4) := (GBP,2)),s)) . (intpos 1) =
s . (intpos 1)
by SCMPDS_2:47
.=
s . (intpos 1)
;
3 <> |.((s . GBP) + 4).|
by A1, ABSVALUE:def 1;
then
intpos 3 <> DataLoc ((s . GBP),4)
by XTUPLE_0:1;
then A14: (Exec (((GBP,4) := (GBP,2)),s)) . (intpos 3) =
s . (intpos 3)
by SCMPDS_2:47
.=
s . (intpos 3)
;
0 <> |.(((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP) + 1).|
by A6, ABSVALUE:def 1;
then A15:
GBP <> DataLoc (((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP),1)
by XTUPLE_0:1;
A16: (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 SCMPDS_5:41
.=
0
by A6, A15, SCMPDS_2:47
;
then A17:
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:1;
2 <> |.(((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP) + 1).|
by A6, ABSVALUE:def 1;
then A18:
intpos 2 <> DataLoc (((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP),1)
by XTUPLE_0:1;
A19: (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)),s)))) . (intpos 2)
by SCMPDS_5:42
.=
((Exec (((GBP,4) := (GBP,2)),s)) . (intpos 2)) + ((Exec (((GBP,4) := (GBP,2)),s)) . (DataLoc (((Exec (((GBP,4) := (GBP,2)),s)) . GBP),1)))
by A4, SCMPDS_2:49
.=
(s . (intpos 2)) + (s . (intpos 1))
by A3, A13, A12, SCMP_GCD:1
;
A20: (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 SCMPDS_5:41
.=
(s . (intpos 2)) + (s . (intpos 1))
by A19, A18, SCMPDS_2:47
;
3 <> |.(((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP) + 1).|
by A6, ABSVALUE:def 1;
then A21:
intpos 3 <> DataLoc (((IExec ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))),P,s)) . GBP),1)
by XTUPLE_0:1;
0 <> |.(((IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,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))),P,s)) . GBP),3)
by XTUPLE_0:1;
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 SCMPDS_5:41
.=
0
by A16, A22, SCMPDS_2:48
; ( (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 <> |.(((IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,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))),P,s)) . GBP),3)
by XTUPLE_0:1;
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 SCMPDS_5:41
.=
s . (intpos 2)
by A10, A23, SCMPDS_2:48
; ( (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 <> |.(((IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,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))),P,s)) . GBP),3)
by XTUPLE_0:1;
A25: (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)),s)))) . (intpos 3)
by SCMPDS_5:42
.=
s . (intpos 3)
by A14, A11, SCMPDS_2:49
;
A26: (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 SCMPDS_5:41
.=
s . (intpos 3)
by A25, A21, SCMPDS_2:47
;
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 SCMPDS_5:41
.=
(s . (intpos 1)) + (s . (intpos 2))
by A20, A24, SCMPDS_2:48
; (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 SCMPDS_5:41
.=
((IExec (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))),P,s)) . (intpos 3)) + (- 1)
by A17, SCMPDS_2:48
.=
(s . (intpos 3)) - 1
by A26
; verum