let s be State of SCMPDS ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:

end;

set s0 = Initialized s;
set m1 = SubFrom GBP ,1,GBP ,2;
set m2 = SubFrom GBP ,2,GBP ,1;
assume A17: s . GBP = 0 ; :: thesis:
then A18: (Initialized s) . GBP = 0 by SCMPDS_5:40;
A19: DataLoc (s . GBP ),3 = intpos (0 + 3) by A17, SCMP_GCD:5;
A20: (Initialized s) . (intpos 2) = s . (intpos 2) by SCMPDS_5:40;

A21: now

2 <> abs (((Initialized s) . GBP ) + 1) by A18, ABSVALUE:def 1;
then A22: intpos 2 <> DataLoc ((Initialized s) . GBP ),1 by ZFMISC_1:33;
0 <> abs (((Initialized s) . GBP ) + 1) by A18, ABSVALUE:def 1;
then A23: GBP <> DataLoc ((Initialized s) . GBP ),1 by ZFMISC_1:33;
assume A24: s . (intpos 3) > 0 ; :: thesis:
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),(Initialized s)) . GBP by SCMPDS_5:45
.= 0 by A18, A23, SCMPDS_2:62 ;
:: thesis:
A25: DataLoc ((Initialized 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),(Initialized s)) . (intpos 1) by SCMPDS_5:45
.= ((Initialized s) . (intpos 1)) - ((Initialized s) . (DataLoc ((Initialized s) . GBP ),2)) by A25, SCMPDS_2:62
.= ((Initialized s) . (intpos 1)) - ((Initialized s) . (intpos (0 + 2))) by A18, SCMP_GCD:5
.= (s . (intpos 1)) - (s . (intpos 2)) by A20, SCMPDS_5:40 ; :: thesis:
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),(Initialized s)) . (intpos 2) by SCMPDS_5:45
.= s . (intpos 2) by A20, A22, SCMPDS_2:62 ; :: thesis:

end;

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; :: thesis:
A26: (Initialized s) . (intpos 1) = s . (intpos 1) by SCMPDS_5:40;

A27: now

1 <> abs (((Initialized s) . GBP ) + 2) by A18, ABSVALUE:def 1;
then A28: intpos 1 <> DataLoc ((Initialized s) . GBP ),2 by ZFMISC_1:33;
0 <> abs (((Initialized s) . GBP ) + 2) by A18, ABSVALUE:def 1;
then A29: GBP <> DataLoc ((Initialized s) . GBP ),2 by ZFMISC_1:33;
assume A30: s . (intpos 3) <= 0 ; :: thesis:
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),(Initialized s)) . GBP by SCMPDS_5:45
.= 0 by A18, A29, SCMPDS_2:62 ;
:: thesis:
A31: DataLoc ((Initialized 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),(Initialized s)) . (intpos 2) by SCMPDS_5:45
.= ((Initialized s) . (intpos 2)) - ((Initialized s) . (DataLoc ((Initialized s) . GBP ),1)) by A31, SCMPDS_2:62
.= ((Initialized s) . (intpos 2)) - ((Initialized s) . (intpos (0 + 1))) by A18, SCMP_GCD:5
.= (s . (intpos 2)) - (s . (intpos 1)) by A20, SCMPDS_5:40 ; :: thesis:
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),(Initialized s)) . (intpos 1) by SCMPDS_5:45
.= s . (intpos 1) by A26, A28, SCMPDS_2:62 ; :: thesis:

end;

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; :: thesis:

now

per cases ;

suppose s . (intpos 3) > 0 ; :: thesis:

hence (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP = 0 by A21; :: thesis:

end;

suppose s . (intpos 3) <= 0 ; :: thesis:

hence (IExec (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))),s) . GBP = 0 by A27; :: thesis:

end;

end;

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; :: thesis: