let s be State of SCMPDS; :: thesis:
assume A1: ( s . (intpos 1) > 0 & s . (intpos 2) > 0 ) ; :: thesis:
set t0 = Initialize s;
set t1 = IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s);
set t2 = IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s);
set t3 = Exec ((GBP := 0),(Initialize s));
set a = GBP ;
X0: Initialize s = Initialize (Initialize s) ;
X1: IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s) = IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),(Initialize s)) by SCMPDS_5:48;
X2: IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s) = IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),(Initialize s)) by SCMPDS_5:48;
A2: (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 ;
A3: (Exec ((GBP := 0),(Initialize s))) . GBP = 0 by SCMPDS_2:57;
then A4: 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 A3, ABSVALUE:def 1;
then A5: intpos 1 <> DataLoc (((Exec ((GBP := 0),(Initialize s))) . GBP),3) by ZFMISC_1:33;
A6: (IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . (intpos 1) = (Exec (((GBP,3) := (GBP,1)),(Exec ((GBP := 0),(Initialize s))))) . (intpos 1) by X0, X2, SCMPDS_5:47
.= s . (intpos 1) by A2, A5, SCMPDS_2:59 ;
A7: (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 ;
A8: (IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . (intpos 3) = (Exec (((GBP,3) := (GBP,1)),(Exec ((GBP := 0),(Initialize s))))) . (intpos 3) by X0, X2, SCMPDS_5:47
.= (Exec ((GBP := 0),(Initialize s))) . (DataLoc (((Exec ((GBP := 0),(Initialize s))) . GBP),1)) by A4, SCMPDS_2:59
.= s . (intpos 1) by A3, A2, SCMP_GCD:5 ;
2 <> abs (((Exec ((GBP := 0),(Initialize s))) . GBP) + 3) by A3, ABSVALUE:def 1;
then A9: intpos 2 <> DataLoc (((Exec ((GBP := 0),(Initialize s))) . GBP),3) by ZFMISC_1:33;
A10: (IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . (intpos 2) = (Exec (((GBP,3) := (GBP,1)),(Exec ((GBP := 0),(Initialize s))))) . (intpos 2) by X0, X2, SCMPDS_5:47
.= s . (intpos 2) by A7, A9, SCMPDS_2:59 ;
0 <> abs (((Exec ((GBP := 0),(Initialize s))) . GBP) + 3) by A3, ABSVALUE:def 1;
then A11: GBP <> DataLoc (((Exec ((GBP := 0),(Initialize s))) . GBP),3) by ZFMISC_1:33;
A12: (IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . GBP = (Exec (((GBP,3) := (GBP,1)),(Exec ((GBP := 0),(Initialize s))))) . GBP by X0, X2, SCMPDS_5:47
.= 0 by A3, A11, SCMPDS_2:59 ;
then A13: DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . GBP),3) = intpos (0 + 3) by SCMP_GCD:5;
0 <> abs (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . GBP) + 3) by A12, ABSVALUE:def 1;
then A14: GBP <> DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . GBP),3) by ZFMISC_1:33;
A15: (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s)) . GBP = (Exec ((SubFrom (GBP,3,GBP,2)),(IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)))) . GBP by X1, X2, SCMPDS_5:46
.= 0 by A12, A14, SCMPDS_2:62 ;
1 <> abs (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . GBP) + 3) by A12, ABSVALUE:def 1;
then A16: intpos 1 <> DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . GBP),3) by ZFMISC_1:33;
A17: (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s)) . (intpos 1) = (Exec ((SubFrom (GBP,3,GBP,2)),(IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)))) . (intpos 1) by X1, X2, SCMPDS_5:46
.= s . (intpos 1) by A6, A16, SCMPDS_2:62 ;
2 <> abs (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . GBP) + 3) by A12, ABSVALUE:def 1;
then A18: intpos 2 <> DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . GBP),3) by ZFMISC_1:33;
A19: (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s)) . (intpos 2) = (Exec ((SubFrom (GBP,3,GBP,2)),(IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)))) . (intpos 2) by X1, X2, SCMPDS_5:46
.= s . (intpos 2) by A10, A18, SCMPDS_2:62 ;
A20: (IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s)) . (intpos 3) = (Exec ((SubFrom (GBP,3,GBP,2)),(IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)))) . (intpos 3) by X1, X2, SCMPDS_5:46
.= ((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . (intpos 3)) - ((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . (DataLoc (((IExec (((GBP := 0) ';' ((GBP,3) := (GBP,1))),s)) . GBP),2))) by A13, SCMPDS_2:62
.= ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s)) . (intpos 1)) - ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s)) . (intpos 2)) by A12, A10, A8, A17, A19, SCMP_GCD:5 ;
then A21: ( 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))),s) & 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))),s) ) by A1, A15, A17, A19, 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))))),(IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s)))) . (intpos 1) = ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s)) . (intpos 1)) gcd ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s)) . (intpos 2)) by A1, A15, A17, A19, A20, 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)))))),s)) . (intpos 1) = (s . (intpos 1)) gcd (s . (intpos 2)) by A17, A19, A21, 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))))),(IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s)))) . (intpos 2) = ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s)) . (intpos 1)) gcd ((IExec ((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),s)) . (intpos 2)) by A1, A15, A17, A19, A20, 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)))))),s)) . (intpos 2) = (s . (intpos 1)) gcd (s . (intpos 2)) by A17, A19, A21, 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 & (((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 ) by A21, SCPISORT:10; :: thesis: