let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis:
let s be State of SCMPDS; :: thesis:
assume A1: ( s . (intpos 1) > 0 & s . (intpos 2) > 0 ) ; :: thesis:
set t0 = Initialize s;
set Q0 = P;
set t1 = IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s);
set t2 = IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s);
set Q1 = P;
set t3 = Exec ((GBP := 0),(Initialize s));
set a = GBP ;
A2: Initialize s = Initialize (Initialize s) ;
A3: IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s) = IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,(Initialize s)) by SCMPDS_5:48;
A4: IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s) = IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,(Initialize s)) by SCMPDS_5:48;
A5: (Exec ((GBP := 0),(Initialize s))) . (intpos 1) = (Initialize s) . (intpos 1) by AMI_3:52, SCMPDS_2:57
.= s . (intpos 1) by SCMPDS_5:40 ;
A6: (Exec ((GBP := 0),(Initialize s))) . GBP = 0 by SCMPDS_2:57;
then A7: DataLoc (((Exec ((GBP := 0),(Initialize s))) . GBP),3) = intpos (0 + 3) by SCMP_GCD:5;
1 <> abs (((Exec ((GBP := 0),(Initialize s))) . GBP) + 3) by A6, ABSVALUE:def 1;
then A8: intpos 1 <> DataLoc (((Exec ((GBP := 0),(Initialize s))) . GBP),3) by ZFMISC_1:33;
A9: (IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . (intpos 1) = (Exec (((GBP,3) := (GBP,1)),(Exec ((GBP := 0),(Initialize s))))) . (intpos 1) by A2, A4, SCMPDS_5:47
.= s . (intpos 1) by A5, A8, SCMPDS_2:59 ;
A10: (Exec ((GBP := 0),(Initialize s))) . (intpos 2) = (Initialize s) . (intpos 2) by AMI_3:52, SCMPDS_2:57
.= s . (intpos 2) by SCMPDS_5:40 ;
A11: (IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . (intpos 3) = (Exec (((GBP,3) := (GBP,1)),(Exec ((GBP := 0),(Initialize s))))) . (intpos 3) by A2, A4, SCMPDS_5:47
.= (Exec ((GBP := 0),(Initialize s))) . (DataLoc (((Exec ((GBP := 0),(Initialize s))) . GBP),1)) by A7, SCMPDS_2:59
.= s . (intpos 1) by A6, A5, SCMP_GCD:5 ;
2 <> abs (((Exec ((GBP := 0),(Initialize s))) . GBP) + 3) by A6, ABSVALUE:def 1;
then A12: intpos 2 <> DataLoc (((Exec ((GBP := 0),(Initialize s))) . GBP),3) by ZFMISC_1:33;
A13: (IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . (intpos 2) = (Exec (((GBP,3) := (GBP,1)),(Exec ((GBP := 0),(Initialize s))))) . (intpos 2) by A2, A4, SCMPDS_5:47
.= s . (intpos 2) by A10, A12, SCMPDS_2:59 ;
0 <> abs (((Exec ((GBP := 0),(Initialize s))) . GBP) + 3) by A6, ABSVALUE:def 1;
then A14: GBP <> DataLoc (((Exec ((GBP := 0),(Initialize s))) . GBP),3) by ZFMISC_1:33;
A15: (IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP = (Exec (((GBP,3) := (GBP,1)),(Exec ((GBP := 0),(Initialize s))))) . GBP by A2, A4, SCMPDS_5:47
.= 0 by A6, A14, SCMPDS_2:59 ;
then A16: DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP),3) = intpos (0 + 3) by SCMP_GCD:5;
0 <> abs (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP) + 3) by A15, ABSVALUE:def 1;
then A17: GBP <> DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP),3) by ZFMISC_1:33;
A18: (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . GBP = (Exec ((SubFrom (GBP,3,GBP,2)),(IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)))) . GBP by A3, A4, SCMPDS_5:46
.= 0 by A15, A17, SCMPDS_2:62 ;
1 <> abs (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP) + 3) by A15, ABSVALUE:def 1;
then A19: intpos 1 <> DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP),3) by ZFMISC_1:33;
A20: (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 1) = (Exec ((SubFrom (GBP,3,GBP,2)),(IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)))) . (intpos 1) by A3, A4, SCMPDS_5:46
.= s . (intpos 1) by A9, A19, SCMPDS_2:62 ;
2 <> abs (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP) + 3) by A15, ABSVALUE:def 1;
then A21: intpos 2 <> DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP),3) by ZFMISC_1:33;
A22: (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 2) = (Exec ((SubFrom (GBP,3,GBP,2)),(IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)))) . (intpos 2) by A3, A4, SCMPDS_5:46
.= s . (intpos 2) by A13, A21, SCMPDS_2:62 ;
A23: (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 3) = (Exec ((SubFrom (GBP,3,GBP,2)),(IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)))) . (intpos 3) by A3, A4, SCMPDS_5:46
.= ((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . (intpos 3)) - ((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . (DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),P,s)) . GBP),2))) by A16, SCMPDS_2:62
.= ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 1)) - ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 2)) by A15, A13, A11, A20, A22, SCMP_GCD:5 ;
then A24: ( while<>0 (GBP,3,(((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)))) is_closed_on IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s),P & while<>0 (GBP,3,(((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)))) is_halting_on IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s),P ) by A1, A18, A20, A22, Lm15;
(IExec ((while<>0 (GBP,3,(((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))))),P,(IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)))) . (intpos 1) = ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 1)) gcd ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 2)) by A1, A18, A20, A22, A23, Lm15;
hence (IExec (((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) ';' (while<>0 (GBP,3,(((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)))))),P,s)) . (intpos 1) = (s . (intpos 1)) gcd (s . (intpos 2)) by A20, A22, A24, SCPISORT:8; :: thesis:
(IExec ((while<>0 (GBP,3,(((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))))),P,(IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)))) . (intpos 2) = ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 1)) gcd ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 2)) by A1, A18, A20, A22, A23, Lm15;
hence (IExec (((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) ';' (while<>0 (GBP,3,(((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)))))),P,s)) . (intpos 2) = (s . (intpos 1)) gcd (s . (intpos 2)) by A20, A22, A24, SCPISORT:8; :: thesis:
thus ( (((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) ';' (while<>0 (GBP,3,(((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))))) is_closed_on s,P & (((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) ';' (while<>0 (GBP,3,(((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))))) is_halting_on s,P ) by A24, SCPISORT:10; :: thesis: