let s be State of SCMPDS ; ( s . GBP = 0 implies ( ( s . (intpos 3) > 0 implies ( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) = (s . (intpos 1)) - (s . (intpos 2)) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) = s . (intpos 2) ) ) & ( s . (intpos 3) <= 0 implies ( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) = (s . (intpos 2)) - (s . (intpos 1)) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) = s . (intpos 1) ) ) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . GBP = 0 & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 3) = ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) - ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2)) ) )
set s1 = IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s;
set s2 = IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s;
set a = GBP ;
A1:
now assume A2:
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP = 0
;
( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . GBP = 0 & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) = (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 1) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) = (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 2) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 3) = ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) - ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2)) )then A3:
DataLoc ((IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP ),3
= intpos (0 + 3)
by SCMP_GCD:5;
A4:
(IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . (intpos 3) =
(Exec (GBP ,3 := GBP ,1),(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s)) . (intpos 3)
by SCMPDS_5:46
.=
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (DataLoc ((IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP ),1)
by A3, SCMPDS_2:59
.=
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos (0 + 1))
by A2, SCMP_GCD:5
;
1
<> abs (((IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP ) + 3)
by A2, ABSVALUE:def 1;
then A5:
intpos 1
<> DataLoc ((IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP ),3
by ZFMISC_1:33;
A6:
(IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . (intpos 1) =
(Exec (GBP ,3 := GBP ,1),(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s)) . (intpos 1)
by SCMPDS_5:46
.=
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 1)
by A5, SCMPDS_2:59
;
2
<> abs (((IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP ) + 3)
by A2, ABSVALUE:def 1;
then A7:
intpos 2
<> DataLoc ((IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP ),3
by ZFMISC_1:33;
A8:
(IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . (intpos 2) =
(Exec (GBP ,3 := GBP ,1),(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s)) . (intpos 2)
by SCMPDS_5:46
.=
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 2)
by A7, SCMPDS_2:59
;
0 <> abs (((IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP ) + 3)
by A2, ABSVALUE:def 1;
then A9:
GBP <> DataLoc ((IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP ),3
by ZFMISC_1:33;
A10:
(IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . GBP =
(Exec (GBP ,3 := GBP ,1),(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s)) . GBP
by SCMPDS_5:46
.=
0
by A2, A9, SCMPDS_2:59
;
then A11:
DataLoc ((IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . GBP ),3
= intpos (0 + 3)
by SCMP_GCD:5;
0 <> abs (((IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . GBP ) + 3)
by A10, ABSVALUE:def 1;
then A12:
GBP <> DataLoc ((IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . GBP ),3
by ZFMISC_1:33;
thus (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . GBP =
(Exec (SubFrom GBP ,3,GBP ,2),(IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s)) . GBP
by SCMPDS_5:46
.=
0
by A10, A12, SCMPDS_2:62
;
( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) = (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 1) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) = (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 2) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 3) = ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) - ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2)) )
1
<> abs (((IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . GBP ) + 3)
by A10, ABSVALUE:def 1;
then A13:
intpos 1
<> DataLoc ((IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . GBP ),3
by ZFMISC_1:33;
thus A14:
(IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) =
(Exec (SubFrom GBP ,3,GBP ,2),(IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s)) . (intpos 1)
by SCMPDS_5:46
.=
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 1)
by A6, A13, SCMPDS_2:62
;
( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) = (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 2) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 3) = ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) - ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2)) )
2
<> abs (((IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . GBP ) + 3)
by A10, ABSVALUE:def 1;
then A15:
intpos 2
<> DataLoc ((IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . GBP ),3
by ZFMISC_1:33;
thus A16:
(IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) =
(Exec (SubFrom GBP ,3,GBP ,2),(IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s)) . (intpos 2)
by SCMPDS_5:46
.=
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 2)
by A8, A15, SCMPDS_2:62
;
(IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 3) = ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) - ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2))thus (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 3) =
(Exec (SubFrom GBP ,3,GBP ,2),(IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s)) . (intpos 3)
by SCMPDS_5:46
.=
((IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . (intpos 3)) - ((IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . (DataLoc ((IExec ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)),s) . GBP ),2))
by A11, SCMPDS_2:62
.=
((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) - ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2))
by A10, A8, A4, A14, A16, SCMP_GCD:5
;
verum end;
set s0 = Initialize s;
set m1 = SubFrom GBP ,1,GBP ,2;
set m2 = SubFrom GBP ,2,GBP ,1;
assume A17:
s . GBP = 0
; ( ( s . (intpos 3) > 0 implies ( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) = (s . (intpos 1)) - (s . (intpos 2)) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) = s . (intpos 2) ) ) & ( s . (intpos 3) <= 0 implies ( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) = (s . (intpos 2)) - (s . (intpos 1)) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) = s . (intpos 1) ) ) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . GBP = 0 & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 3) = ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) - ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2)) )
then A18:
(Initialize s) . GBP = 0
by SCMPDS_5:40;
A19:
DataLoc (s . GBP ),3 = intpos (0 + 3)
by A17, SCMP_GCD:5;
A20:
(Initialize s) . (intpos 2) = s . (intpos 2)
by SCMPDS_5:40;
A21:
now
2
<> abs (((Initialize s) . GBP ) + 1)
by A18, ABSVALUE:def 1;
then A22:
intpos 2
<> DataLoc ((Initialize s) . GBP ),1
by ZFMISC_1:33;
0 <> abs (((Initialize s) . GBP ) + 1)
by A18, ABSVALUE:def 1;
then A23:
GBP <> DataLoc ((Initialize s) . GBP ),1
by ZFMISC_1:33;
assume A24:
s . (intpos 3) > 0
;
( (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP = 0 & (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 1) = (s . (intpos 1)) - (s . (intpos 2)) & (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 2) = s . (intpos 2) )hence (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP =
(IExec (Load (SubFrom GBP ,1,GBP ,2)),s) . GBP
by A19, SCMPDS_6:87
.=
(Exec (SubFrom GBP ,1,GBP ,2),(Initialize s)) . GBP
by SCMPDS_5:45
.=
0
by A18, A23, SCMPDS_2:62
;
( (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 1) = (s . (intpos 1)) - (s . (intpos 2)) & (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 2) = s . (intpos 2) )A25:
DataLoc ((Initialize s) . GBP ),1
= intpos (0 + 1)
by A18, SCMP_GCD:5;
thus (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 1) =
(IExec (Load (SubFrom GBP ,1,GBP ,2)),s) . (intpos 1)
by A19, A24, SCMPDS_6:87
.=
(Exec (SubFrom GBP ,1,GBP ,2),(Initialize s)) . (intpos 1)
by SCMPDS_5:45
.=
((Initialize s) . (intpos 1)) - ((Initialize s) . (DataLoc ((Initialize s) . GBP ),2))
by A25, SCMPDS_2:62
.=
((Initialize s) . (intpos 1)) - ((Initialize s) . (intpos (0 + 2)))
by A18, SCMP_GCD:5
.=
(s . (intpos 1)) - (s . (intpos 2))
by A20, SCMPDS_5:40
;
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 2) = s . (intpos 2)thus (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 2) =
(IExec (Load (SubFrom GBP ,1,GBP ,2)),s) . (intpos 2)
by A19, A24, SCMPDS_6:87
.=
(Exec (SubFrom GBP ,1,GBP ,2),(Initialize s)) . (intpos 2)
by SCMPDS_5:45
.=
s . (intpos 2)
by A20, A22, SCMPDS_2:62
;
verum
hence
( s . (intpos 3) > 0 implies ( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) = (s . (intpos 1)) - (s . (intpos 2)) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) = s . (intpos 2) ) )
by A1; ( ( s . (intpos 3) <= 0 implies ( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) = (s . (intpos 2)) - (s . (intpos 1)) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) = s . (intpos 1) ) ) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . GBP = 0 & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 3) = ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) - ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2)) )
A26:
(Initialize s) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:40;
A27:
now
1
<> abs (((Initialize s) . GBP ) + 2)
by A18, ABSVALUE:def 1;
then A28:
intpos 1
<> DataLoc ((Initialize s) . GBP ),2
by ZFMISC_1:33;
0 <> abs (((Initialize s) . GBP ) + 2)
by A18, ABSVALUE:def 1;
then A29:
GBP <> DataLoc ((Initialize s) . GBP ),2
by ZFMISC_1:33;
assume A30:
s . (intpos 3) <= 0
;
( (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP = 0 & (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 2) = (s . (intpos 2)) - (s . (intpos 1)) & (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 1) = s . (intpos 1) )hence (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP =
(IExec (Load (SubFrom GBP ,2,GBP ,1)),s) . GBP
by A19, SCMPDS_6:88
.=
(Exec (SubFrom GBP ,2,GBP ,1),(Initialize s)) . GBP
by SCMPDS_5:45
.=
0
by A18, A29, SCMPDS_2:62
;
( (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 2) = (s . (intpos 2)) - (s . (intpos 1)) & (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 1) = s . (intpos 1) )A31:
DataLoc ((Initialize s) . GBP ),2
= intpos (0 + 2)
by A18, SCMP_GCD:5;
thus (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 2) =
(IExec (Load (SubFrom GBP ,2,GBP ,1)),s) . (intpos 2)
by A19, A30, SCMPDS_6:88
.=
(Exec (SubFrom GBP ,2,GBP ,1),(Initialize s)) . (intpos 2)
by SCMPDS_5:45
.=
((Initialize s) . (intpos 2)) - ((Initialize s) . (DataLoc ((Initialize s) . GBP ),1))
by A31, SCMPDS_2:62
.=
((Initialize s) . (intpos 2)) - ((Initialize s) . (intpos (0 + 1)))
by A18, SCMP_GCD:5
.=
(s . (intpos 2)) - (s . (intpos 1))
by A20, SCMPDS_5:40
;
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 1) = s . (intpos 1)thus (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . (intpos 1) =
(IExec (Load (SubFrom GBP ,2,GBP ,1)),s) . (intpos 1)
by A19, A30, SCMPDS_6:88
.=
(Exec (SubFrom GBP ,2,GBP ,1),(Initialize s)) . (intpos 1)
by SCMPDS_5:45
.=
s . (intpos 1)
by A26, A28, SCMPDS_2:62
;
verum
hence
( s . (intpos 3) <= 0 implies ( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) = (s . (intpos 2)) - (s . (intpos 1)) & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) = s . (intpos 1) ) )
by A1; ( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . GBP = 0 & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 3) = ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) - ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2)) )
now per cases
( s . (intpos 3) > 0 or s . (intpos 3) <= 0 )
;
suppose
s . (intpos 3) > 0
;
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP = 0 hence
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP = 0
by A21;
verum end; suppose
s . (intpos 3) <= 0
;
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP = 0 hence
(IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP = 0
by A27;
verum end;
hence
( (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . GBP = 0 & (IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 3) = ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) - ((IExec (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2)) )
by A1; verum