let n be Nat; :: thesis:
let s be State of SCMPDS; :: thesis:
let P be Instruction-Sequence of SCMPDS; :: thesis:
set x = s . (DataLoc ((s . SBP),2));
set y = s . (DataLoc ((s . SBP),3));
assume A1: GCD-Algorithm c= P ; :: thesis:
assume A2: IC s = 5 ; :: thesis:
assume A3: n = s . SBP ; :: thesis:
assume A4: s . GBP = 0 ; :: thesis:
assume A5: s . (DataLoc ((s . SBP),3)) > 0 ; :: thesis:
A6: P /. (IC s) = P . (IC s) by PBOOLE:143;
A7: P /. (IC (Comput (P,s,1))) = P . (IC (Comput (P,s,1))) by PBOOLE:143;
A8: Comput (P,s,(1 + 0)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s) by EXTPRO_1:2
.= Exec (((SBP,3) <=0_goto 9),s) by A2, A6, Lm1, A1 ;
then A9: IC (Comput (P,s,1)) = (IC s) + 1 by A5, SCMPDS_2:56
.= 5 + 1 by A2 ;
then A10: CurInstr (P,(Comput (P,s,1))) = P . 6 by A7
.= (SBP,6) := (SBP,3) by Lm1, A1 ;
A11: Comput (P,s,(1 + 1)) = Following (P,(Comput (P,s,1))) by EXTPRO_1:3
.= Exec (((SBP,6) := (SBP,3)),(Comput (P,s,1))) by A10 ;
A12: (Comput (P,s,1)) . SBP = n by A3, A8, SCMPDS_2:56;
A13: (Comput (P,s,1)) . GBP = 0 by A4, A8, SCMPDS_2:56;
A14: (Comput (P,s,1)) . (intpos (n + 3)) = (Comput (P,s,1)) . (DataLoc (n,3)) by Th1
.= s . (DataLoc ((s . SBP),3)) by A3, A8, SCMPDS_2:56 ;
A15: (Comput (P,s,1)) . (intpos (n + 2)) = (Comput (P,s,1)) . (DataLoc (n,2)) by Th1
.= s . (DataLoc ((s . SBP),2)) by A3, A8, SCMPDS_2:56 ;
A16: P /. (IC (Comput (P,s,2))) = P . (IC (Comput (P,s,2))) by PBOOLE:143;
A17: IC (Comput (P,s,2)) = (IC (Comput (P,s,1))) + 1 by A11, SCMPDS_2:47
.= 6 + 1 by A9 ;
then A18: CurInstr (P,(Comput (P,s,2))) = P . 7 by A16
.= Divide (SBP,2,SBP,3) by Lm1, A1 ;
A19: Comput (P,s,(2 + 1)) = Following (P,(Comput (P,s,2))) by EXTPRO_1:3
.= Exec ((Divide (SBP,2,SBP,3)),(Comput (P,s,2))) by A18 ;
A20: DataLoc (((Comput (P,s,1)) . SBP),6) = intpos (n + 6) by A12, Th1;
then A21: (Comput (P,s,2)) . SBP = n by A11, A12, Lm3, SCMPDS_2:47;
A22: (Comput (P,s,2)) . GBP = 0 by A11, A13, A20, Lm2, SCMPDS_2:47;
A23: (Comput (P,s,2)) . (intpos (n + 6)) = (Comput (P,s,1)) . (DataLoc (n,3)) by A11, A12, A20, SCMPDS_2:47
.= s . (DataLoc ((s . SBP),3)) by A14, Th1 ;
n + 3 <> n + 6 ;
then A24: (Comput (P,s,2)) . (intpos (n + 3)) = s . (DataLoc ((s . SBP),3)) by A11, A14, A20, AMI_3:10, SCMPDS_2:47;
n + 2 <> n + 6 ;
then A25: (Comput (P,s,2)) . (intpos (n + 2)) = s . (DataLoc ((s . SBP),2)) by A11, A15, A20, AMI_3:10, SCMPDS_2:47;
A26: P /. (IC (Comput (P,s,3))) = P . (IC (Comput (P,s,3))) by PBOOLE:143;
A27: IC (Comput (P,s,3)) = (IC (Comput (P,s,2))) + 1 by A19, SCMPDS_2:52
.= 7 + 1 by A17 ;
then A28: CurInstr (P,(Comput (P,s,3))) = P . 8 by A26
.= (SBP,7) := (SBP,3) by Lm1, A1 ;
A29: Comput (P,s,(3 + 1)) = Following (P,(Comput (P,s,3))) by EXTPRO_1:3
.= Exec (((SBP,7) := (SBP,3)),(Comput (P,s,3))) by A28 ;
A30: DataLoc (((Comput (P,s,2)) . SBP),2) = intpos (n + 2) by A21, Th1;
then A31: SBP <> DataLoc (((Comput (P,s,2)) . SBP),2) by Lm3;
A32: DataLoc (((Comput (P,s,2)) . SBP),3) = intpos (n + 3) by A21, Th1;
then SBP <> DataLoc (((Comput (P,s,2)) . SBP),3) by Lm3;
then A33: (Comput (P,s,3)) . SBP = n by A19, A21, A31, SCMPDS_2:52;
A34: GBP <> DataLoc (((Comput (P,s,2)) . SBP),2) by A30, Lm2;
GBP <> DataLoc (((Comput (P,s,2)) . SBP),3) by A32, Lm2;
then A35: (Comput (P,s,3)) . GBP = 0 by A19, A22, A34, SCMPDS_2:52;
A36: (Comput (P,s,3)) . (intpos (n + 3)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) by A19, A24, A25, A30, A32, SCMPDS_2:52;
n + 6 <> n + 2 ;
then A37: intpos (n + 6) <> DataLoc (((Comput (P,s,2)) . SBP),2) by A30, AMI_3:10;
n + 6 <> n + 3 ;
then intpos (n + 6) <> DataLoc (((Comput (P,s,2)) . SBP),3) by A32, AMI_3:10;
then A38: (Comput (P,s,3)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) by A19, A23, A37, SCMPDS_2:52;
A39: P /. (IC (Comput (P,s,4))) = P . (IC (Comput (P,s,4))) by PBOOLE:143;
A40: IC (Comput (P,s,4)) = (IC (Comput (P,s,3))) + 1 by A29, SCMPDS_2:47
.= 8 + 1 by A27 ;
then A41: CurInstr (P,(Comput (P,s,4))) = P . 9 by A39
.= (SBP,(4 + RetSP)) := (GBP,1) by Lm1, A1 ;
A42: Comput (P,s,(4 + 1)) = Following (P,(Comput (P,s,4))) by EXTPRO_1:3
.= Exec (((SBP,(4 + RetSP)) := (GBP,1)),(Comput (P,s,4))) by A41 ;
A43: DataLoc (((Comput (P,s,3)) . SBP),7) = intpos (n + 7) by A33, Th1;
then A44: (Comput (P,s,4)) . SBP = n by A29, A33, Lm3, SCMPDS_2:47;
A45: (Comput (P,s,4)) . GBP = 0 by A29, A35, A43, Lm2, SCMPDS_2:47;
A46: (Comput (P,s,4)) . (intpos (n + 7)) = (Comput (P,s,3)) . (DataLoc (n,3)) by A29, A33, A43, SCMPDS_2:47
.= (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) by A36, Th1 ;
n + 6 <> n + 7 ;
then A47: (Comput (P,s,4)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) by A29, A38, A43, AMI_3:10, SCMPDS_2:47;
A48: P /. (IC (Comput (P,s,5))) = P . (IC (Comput (P,s,5))) by PBOOLE:143;
A49: IC (Comput (P,s,5)) = (IC (Comput (P,s,4))) + 1 by A42, SCMPDS_2:47
.= 9 + 1 by A40 ;
then A50: CurInstr (P,(Comput (P,s,5))) = P . 10 by A48
.= AddTo (GBP,1,4) by Lm1, A1 ;
A51: Comput (P,s,(5 + 1)) = Following (P,(Comput (P,s,5))) by EXTPRO_1:3
.= Exec ((AddTo (GBP,1,4)),(Comput (P,s,5))) by A50 ;
A52: DataLoc (((Comput (P,s,4)) . SBP),(4 + RetSP)) = intpos (n + (4 + 0)) by A44, Th1, SCMPDS_I:def 13;
then A53: (Comput (P,s,5)) . SBP = n by A42, A44, Lm3, SCMPDS_2:47;
A54: (Comput (P,s,5)) . GBP = 0 by A42, A45, A52, Lm2, SCMPDS_2:47;
n + 7 <> n + 4 ;
then A55: (Comput (P,s,5)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) by A42, A46, A52, AMI_3:10, SCMPDS_2:47;
n + 6 <> n + 4 ;
then A56: (Comput (P,s,5)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) by A42, A47, A52, AMI_3:10, SCMPDS_2:47;
A57: (Comput (P,s,5)) . (intpos (n + 4)) = (Comput (P,s,4)) . (DataLoc (0,1)) by A42, A45, A52, SCMPDS_2:47
.= (Comput (P,s,4)) . (intpos (0 + 1)) by Th1
.= n by A29, A33, A43, Lm3, SCMPDS_2:47 ;
A58: P /. (IC (Comput (P,s,6))) = P . (IC (Comput (P,s,6))) by PBOOLE:143;
A59: IC (Comput (P,s,6)) = (IC (Comput (P,s,5))) + 1 by A51, SCMPDS_2:48
.= 10 + 1 by A49 ;
then A60: CurInstr (P,(Comput (P,s,6))) = P . 11 by A58
.= saveIC (SBP,RetIC) by Lm1, A1 ;
A61: Comput (P,s,(6 + 1)) = Following (P,(Comput (P,s,6))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P,s,6))) by A60 ;
A62: DataLoc (((Comput (P,s,5)) . GBP),1) = intpos (0 + 1) by A54, Th1;
then A63: (Comput (P,s,6)) . SBP = n + 4 by A51, A53, SCMPDS_2:48;
A64: (Comput (P,s,6)) . GBP = 0 by A51, A54, A62, AMI_3:10, SCMPDS_2:48;
n + 7 <> 1 by NAT_1:11;
then A65: (Comput (P,s,6)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) by A51, A55, A62, AMI_3:10, SCMPDS_2:48;
n + 6 <> 1 by NAT_1:11;
then A66: (Comput (P,s,6)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) by A51, A56, A62, AMI_3:10, SCMPDS_2:48;
n + 4 <> 1 by NAT_1:11;
then A67: (Comput (P,s,6)) . (intpos (n + 4)) = n by A51, A57, A62, AMI_3:10, SCMPDS_2:48;
A68: P /. (IC (Comput (P,s,7))) = P . (IC (Comput (P,s,7))) by PBOOLE:143;
thus IC (Comput (P,s,7)) = (IC (Comput (P,s,6))) + 1 by A61, SCMPDS_2:59
.= 11 + 1 by A59
.= 5 + 7 ; :: thesis:
then A69: CurInstr (P,(Comput (P,s,7))) = P . 12 by A68
.= goto (- 7) by Lm1, A1 ;
thus Comput (P,s,8) = Comput (P,s,(7 + 1))
.= Following (P,(Comput (P,s,7))) by EXTPRO_1:3
.= Exec ((goto (- 7)),(Comput (P,s,7))) by A69 ; :: thesis:
A70: DataLoc (((Comput (P,s,6)) . SBP),RetIC) = intpos ((n + 4) + 1) by A63, Th1, SCMPDS_I:def 14
.= intpos (n + (4 + 1)) ;
then SBP <> DataLoc (((Comput (P,s,6)) . SBP),RetIC) by Lm3;
hence (Comput (P,s,7)) . SBP = n + 4 by A61, A63, SCMPDS_2:59; :: thesis:
GBP <> DataLoc (((Comput (P,s,6)) . SBP),RetIC) by A70, Lm2;
hence (Comput (P,s,7)) . GBP = 0 by A61, A64, SCMPDS_2:59; :: thesis:
n + 7 <> n + 5 ;
hence (Comput (P,s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) by A61, A65, A70, AMI_3:10, SCMPDS_2:59; :: thesis:
n + 6 <> n + 5 ;
hence (Comput (P,s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) by A61, A66, A70, AMI_3:10, SCMPDS_2:59; :: thesis:
n + 4 <> n + 5 ;
hence (Comput (P,s,7)) . (intpos (n + 4)) = n by A61, A67, A70, AMI_3:10, SCMPDS_2:59; :: thesis:
thus (Comput (P,s,7)) . (intpos (n + 5)) = 11 by A59, A61, A70, SCMPDS_2:59; :: thesis: