let n be Element of 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 A2: GCD-Algorithm c= P ; :: thesis:
assume A3: IC s = 5 ; :: thesis:
assume A4: n = s . SBP ; :: thesis:
assume A5: s . GBP = 0 ; :: thesis:
assume A6: s . (DataLoc ((s . SBP),3)) > 0 ; :: thesis:
A7: P /. (IC s) = P . (IC s) by PBOOLE:143;
A8: P /. (IC (Comput (P,s,1))) = P . (IC (Comput (P,s,1))) by PBOOLE:143;
A9: 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 A3, A7, Lm1, A2 ;
then A10: IC (Comput (P,s,1)) = succ (IC s) by A6, SCMPDS_2:56
.= 5 + 1 by A3 ;
then A11: CurInstr (P,(Comput (P,s,1))) = P . 6 by A8
.= (SBP,6) := (SBP,3) by Lm1, A2 ;
A13: 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 A11 ;
A14: (Comput (P,s,1)) . SBP = n by A4, A9, SCMPDS_2:56;
A15: (Comput (P,s,1)) . GBP = 0 by A5, A9, SCMPDS_2:56;
A16: (Comput (P,s,1)) . (intpos (n + 3)) = (Comput (P,s,1)) . (DataLoc (n,3)) by Th5
.= s . (DataLoc ((s . SBP),3)) by A4, A9, SCMPDS_2:56 ;
A17: (Comput (P,s,1)) . (intpos (n + 2)) = (Comput (P,s,1)) . (DataLoc (n,2)) by Th5
.= s . (DataLoc ((s . SBP),2)) by A4, A9, SCMPDS_2:56 ;
A18: P /. (IC (Comput (P,s,2))) = P . (IC (Comput (P,s,2))) by PBOOLE:143;
A19: IC (Comput (P,s,2)) = succ (IC (Comput (P,s,1))) by A13, SCMPDS_2:47
.= 6 + 1 by A10 ;
then A20: CurInstr (P,(Comput (P,s,2))) = P . 7 by A18
.= Divide (SBP,2,SBP,3) by Lm1, A2 ;
A22: 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 A20 ;
A23: DataLoc (((Comput (P,s,1)) . SBP),6) = intpos (n + 6) by A14, Th5;
then A24: (Comput (P,s,2)) . SBP = n by A13, A14, Lm3, SCMPDS_2:47;
A25: (Comput (P,s,2)) . GBP = 0 by A13, A15, A23, Lm2, SCMPDS_2:47;
A26: (Comput (P,s,2)) . (intpos (n + 6)) = (Comput (P,s,1)) . (DataLoc (n,3)) by A13, A14, A23, SCMPDS_2:47
.= s . (DataLoc ((s . SBP),3)) by A16, Th5 ;
n + 3 <> n + 6 ;
then A27: (Comput (P,s,2)) . (intpos (n + 3)) = s . (DataLoc ((s . SBP),3)) by A13, A16, A23, AMI_3:10, SCMPDS_2:47;
n + 2 <> n + 6 ;
then A28: (Comput (P,s,2)) . (intpos (n + 2)) = s . (DataLoc ((s . SBP),2)) by A13, A17, A23, AMI_3:10, SCMPDS_2:47;
A29: P /. (IC (Comput (P,s,3))) = P . (IC (Comput (P,s,3))) by PBOOLE:143;
A30: IC (Comput (P,s,3)) = succ (IC (Comput (P,s,2))) by A22, SCMPDS_2:52
.= 7 + 1 by A19 ;
then A31: CurInstr (P,(Comput (P,s,3))) = P . 8 by A29
.= (SBP,7) := (SBP,3) by Lm1, A2 ;
A33: 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 A31 ;
A34: DataLoc (((Comput (P,s,2)) . SBP),2) = intpos (n + 2) by A24, Th5;
then A35: SBP <> DataLoc (((Comput (P,s,2)) . SBP),2) by Lm3;
A36: DataLoc (((Comput (P,s,2)) . SBP),3) = intpos (n + 3) by A24, Th5;
then SBP <> DataLoc (((Comput (P,s,2)) . SBP),3) by Lm3;
then A37: (Comput (P,s,3)) . SBP = n by A22, A24, A35, SCMPDS_2:52;
A38: GBP <> DataLoc (((Comput (P,s,2)) . SBP),2) by A34, Lm2;
GBP <> DataLoc (((Comput (P,s,2)) . SBP),3) by A36, Lm2;
then A39: (Comput (P,s,3)) . GBP = 0 by A22, A25, A38, SCMPDS_2:52;
A40: (Comput (P,s,3)) . (intpos (n + 3)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) by A22, A27, A28, A34, A36, SCMPDS_2:52;
n + 6 <> n + 2 ;
then A41: intpos (n + 6) <> DataLoc (((Comput (P,s,2)) . SBP),2) by A34, AMI_3:10;
n + 6 <> n + 3 ;
then intpos (n + 6) <> DataLoc (((Comput (P,s,2)) . SBP),3) by A36, AMI_3:10;
then A42: (Comput (P,s,3)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) by A22, A26, A41, SCMPDS_2:52;
A43: P /. (IC (Comput (P,s,4))) = P . (IC (Comput (P,s,4))) by PBOOLE:143;
A44: IC (Comput (P,s,4)) = succ (IC (Comput (P,s,3))) by A33, SCMPDS_2:47
.= 8 + 1 by A30 ;
then A45: CurInstr (P,(Comput (P,s,4))) = P . 9 by A43
.= (SBP,(4 + RetSP)) := (GBP,1) by Lm1, A2 ;
A47: 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 A45 ;
A48: DataLoc (((Comput (P,s,3)) . SBP),7) = intpos (n + 7) by A37, Th5;
then A49: (Comput (P,s,4)) . SBP = n by A33, A37, Lm3, SCMPDS_2:47;
A50: (Comput (P,s,4)) . GBP = 0 by A33, A39, A48, Lm2, SCMPDS_2:47;
A51: (Comput (P,s,4)) . (intpos (n + 7)) = (Comput (P,s,3)) . (DataLoc (n,3)) by A33, A37, A48, SCMPDS_2:47
.= (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) by A40, Th5 ;
n + 6 <> n + 7 ;
then A52: (Comput (P,s,4)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) by A33, A42, A48, AMI_3:10, SCMPDS_2:47;
A53: P /. (IC (Comput (P,s,5))) = P . (IC (Comput (P,s,5))) by PBOOLE:143;
A54: IC (Comput (P,s,5)) = succ (IC (Comput (P,s,4))) by A47, SCMPDS_2:47
.= 9 + 1 by A44 ;
then A55: CurInstr (P,(Comput (P,s,5))) = P . 10 by A53
.= AddTo (GBP,1,4) by Lm1, A2 ;
A57: 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 A55 ;
A58: DataLoc (((Comput (P,s,4)) . SBP),(4 + RetSP)) = intpos (n + (4 + 0)) by A49, Th5, SCMPDS_1:def 20;
then A59: (Comput (P,s,5)) . SBP = n by A47, A49, Lm3, SCMPDS_2:47;
A60: (Comput (P,s,5)) . GBP = 0 by A47, A50, A58, Lm2, SCMPDS_2:47;
n + 7 <> n + 4 ;
then A61: (Comput (P,s,5)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) by A47, A51, A58, AMI_3:10, SCMPDS_2:47;
n + 6 <> n + 4 ;
then A62: (Comput (P,s,5)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) by A47, A52, A58, AMI_3:10, SCMPDS_2:47;
A63: (Comput (P,s,5)) . (intpos (n + 4)) = (Comput (P,s,4)) . (DataLoc (0,1)) by A47, A50, A58, SCMPDS_2:47
.= (Comput (P,s,4)) . (intpos (0 + 1)) by Th5
.= n by A33, A37, A48, Lm3, SCMPDS_2:47 ;
A64: P /. (IC (Comput (P,s,6))) = P . (IC (Comput (P,s,6))) by PBOOLE:143;
A65: IC (Comput (P,s,6)) = succ (IC (Comput (P,s,5))) by A57, SCMPDS_2:48
.= 10 + 1 by A54 ;
then A66: CurInstr (P,(Comput (P,s,6))) = P . 11 by A64
.= saveIC (SBP,RetIC) by Lm1, A2 ;
A68: Comput (P,s,(6 + 1)) = Following (P,(Comput (P,s,6))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P,s,6))) by A66 ;
A69: DataLoc (((Comput (P,s,5)) . GBP),1) = intpos (0 + 1) by A60, Th5;
then A70: (Comput (P,s,6)) . SBP = n + 4 by A57, A59, SCMPDS_2:48;
A71: (Comput (P,s,6)) . GBP = 0 by A57, A60, A69, AMI_3:10, SCMPDS_2:48;
n + 7 <> 1 by NAT_1:11;
then A72: (Comput (P,s,6)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) by A57, A61, A69, AMI_3:10, SCMPDS_2:48;
n + 6 <> 1 by NAT_1:11;
then A73: (Comput (P,s,6)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) by A57, A62, A69, AMI_3:10, SCMPDS_2:48;
n + 4 <> 1 by NAT_1:11;
then A74: (Comput (P,s,6)) . (intpos (n + 4)) = n by A57, A63, A69, AMI_3:10, SCMPDS_2:48;
A75: P /. (IC (Comput (P,s,7))) = P . (IC (Comput (P,s,7))) by PBOOLE:143;
thus IC (Comput (P,s,7)) = succ (IC (Comput (P,s,6))) by A68, SCMPDS_2:59
.= 11 + 1 by A65
.= 5 + 7 ; :: thesis:
then A76: CurInstr (P,(Comput (P,s,7))) = P . 12 by A75
.= goto (- 7) by Lm1, A2 ;
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 A76 ; :: thesis:
A78: DataLoc (((Comput (P,s,6)) . SBP),RetIC) = intpos ((n + 4) + 1) by A70, Th5, SCMPDS_1:def 21
.= intpos (n + (4 + 1)) ;
then SBP <> DataLoc (((Comput (P,s,6)) . SBP),RetIC) by Lm3;
hence (Comput (P,s,7)) . SBP = n + 4 by A68, A70, SCMPDS_2:59; :: thesis:
GBP <> DataLoc (((Comput (P,s,6)) . SBP),RetIC) by A78, Lm2;
hence (Comput (P,s,7)) . GBP = 0 by A68, A71, 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 A68, A72, A78, 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 A68, A73, A78, AMI_3:10, SCMPDS_2:59; :: thesis:
n + 4 <> n + 5 ;
hence (Comput (P,s,7)) . (intpos (n + 4)) = n by A68, A74, A78, AMI_3:10, SCMPDS_2:59; :: thesis:
thus (Comput (P,s,7)) . (intpos (n + 5)) = 11 by A65, A68, A78, SCMPDS_2:59; :: thesis: