let m, n be Nat; :: thesis: for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) > 0 & 1 < m & m <= n + 1 holds
(Comput (P,s,7)) . (intpos m) = s . (intpos m)
let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) > 0 & 1 < m & m <= n + 1 holds
(Comput (P,s,7)) . (intpos m) = s . (intpos m)
let P be Instruction-Sequence of SCMPDS; :: thesis: ( GCD-Algorithm c= P & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) > 0 & 1 < m & m <= n + 1 implies (Comput (P,s,7)) . (intpos m) = s . (intpos m) )
assume A1: GCD-Algorithm c= P ; :: thesis: ( not IC s = 5 or not n = s . SBP or not s . GBP = 0 or not s . (DataLoc ((s . SBP),3)) > 0 or not 1 < m or not m <= n + 1 or (Comput (P,s,7)) . (intpos m) = s . (intpos m) )
assume A2: IC s = 5 ; :: thesis: ( not n = s . SBP or not s . GBP = 0 or not s . (DataLoc ((s . SBP),3)) > 0 or not 1 < m or not m <= n + 1 or (Comput (P,s,7)) . (intpos m) = s . (intpos m) )
assume A3: n = s . SBP ; :: thesis: ( not s . GBP = 0 or not s . (DataLoc ((s . SBP),3)) > 0 or not 1 < m or not m <= n + 1 or (Comput (P,s,7)) . (intpos m) = s . (intpos m) )
assume A4: s . GBP = 0 ; :: thesis: ( not s . (DataLoc ((s . SBP),3)) > 0 or not 1 < m or not m <= n + 1 or (Comput (P,s,7)) . (intpos m) = s . (intpos m) )
assume A5: s . (DataLoc ((s . SBP),3)) > 0 ; :: thesis: ( not 1 < m or not m <= n + 1 or (Comput (P,s,7)) . (intpos m) = s . (intpos m) )
assume A6: 1 < m ; :: thesis: ( not m <= n + 1 or (Comput (P,s,7)) . (intpos m) = s . (intpos m) )
assume A7: m <= n + 1 ; :: thesis: (Comput (P,s,7)) . (intpos m) = s . (intpos m)
A8: P /. (IC s) = P . (IC s) by PBOOLE:143;
A9: P /. (IC (Comput (P,s,1))) = P . (IC (Comput (P,s,1))) by PBOOLE:143;
A10: 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, A8, Lm1, A1 ;
then A11: IC (Comput (P,s,1)) = (IC s) + 1 by A5, SCMPDS_2:56
.= 5 + 1 by A2 ;
then A12: CurInstr (P,(Comput (P,s,1))) = P . 6 by A9
.= (SBP,6) := (SBP,3) by Lm1, A1 ;
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 A12 ;
A14: (Comput (P,s,1)) . SBP = n by A3, A10, SCMPDS_2:56;
A15: (Comput (P,s,1)) . GBP = 0 by A4, A10, SCMPDS_2:56;
A16: (Comput (P,s,1)) . (intpos m) = s . (intpos m) by A10, SCMPDS_2:56;
A17: P /. (IC (Comput (P,s,2))) = P . (IC (Comput (P,s,2))) by PBOOLE:143;
A18: IC (Comput (P,s,2)) = (IC (Comput (P,s,1))) + 1 by A13, SCMPDS_2:47
.= 6 + 1 by A11 ;
then A19: CurInstr (P,(Comput (P,s,2))) = P . 7 by A17
.= Divide (SBP,2,SBP,3) by Lm1, A1 ;
A20: 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 A19 ;
A21: DataLoc (((Comput (P,s,1)) . SBP),6) = intpos (n + 6) by A14, Th1;
then A22: (Comput (P,s,2)) . SBP = n by A13, A14, Lm3, SCMPDS_2:47;
A23: (Comput (P,s,2)) . GBP = 0 by A13, A15, A21, Lm2, SCMPDS_2:47;
n + 1 < n + 6 by XREAL_1:6;
then A24: (Comput (P,s,2)) . (intpos m) = s . (intpos m) by A7, A13, A16, A21, AMI_3:10, SCMPDS_2:47;
A25: P /. (IC (Comput (P,s,3))) = P . (IC (Comput (P,s,3))) by PBOOLE:143;
A26: IC (Comput (P,s,3)) = (IC (Comput (P,s,2))) + 1 by A20, SCMPDS_2:52
.= 7 + 1 by A18 ;
then A27: CurInstr (P,(Comput (P,s,3))) = P . 8 by A25
.= (SBP,7) := (SBP,3) by Lm1, A1 ;
A28: 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 A27 ;
A29: DataLoc (((Comput (P,s,2)) . SBP),2) = intpos (n + 2) by A22, Th1;
then A30: SBP <> DataLoc (((Comput (P,s,2)) . SBP),2) by Lm3;
A31: DataLoc (((Comput (P,s,2)) . SBP),3) = intpos (n + 3) by A22, Th1;
then SBP <> DataLoc (((Comput (P,s,2)) . SBP),3) by Lm3;
then A32: (Comput (P,s,3)) . SBP = n by A20, A22, A30, SCMPDS_2:52;
A33: GBP <> DataLoc (((Comput (P,s,2)) . SBP),2) by A29, Lm2;
GBP <> DataLoc (((Comput (P,s,2)) . SBP),3) by A31, Lm2;
then A34: (Comput (P,s,3)) . GBP = 0 by A20, A23, A33, SCMPDS_2:52;
n + 1 < n + 2 by XREAL_1:6;
then A35: intpos m <> DataLoc (((Comput (P,s,2)) . SBP),2) by A7, A29, AMI_3:10;
n + 1 < n + 3 by XREAL_1:6;
then intpos m <> DataLoc (((Comput (P,s,2)) . SBP),3) by A7, A31, AMI_3:10;
then A36: (Comput (P,s,3)) . (intpos m) = s . (intpos m) by A20, A24, A35, SCMPDS_2:52;
A37: P /. (IC (Comput (P,s,4))) = P . (IC (Comput (P,s,4))) by PBOOLE:143;
A38: IC (Comput (P,s,4)) = (IC (Comput (P,s,3))) + 1 by A28, SCMPDS_2:47
.= 8 + 1 by A26 ;
then A39: CurInstr (P,(Comput (P,s,4))) = P . 9 by A37
.= (SBP,(4 + RetSP)) := (GBP,1) by Lm1, A1 ;
A40: 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 A39 ;
A41: DataLoc (((Comput (P,s,3)) . SBP),7) = intpos (n + 7) by A32, Th1;
then A42: (Comput (P,s,4)) . SBP = n by A28, A32, Lm3, SCMPDS_2:47;
A43: (Comput (P,s,4)) . GBP = 0 by A28, A34, A41, Lm2, SCMPDS_2:47;
n + 1 < n + 7 by XREAL_1:6;
then A44: (Comput (P,s,4)) . (intpos m) = s . (intpos m) by A7, A28, A36, A41, AMI_3:10, SCMPDS_2:47;
A45: P /. (IC (Comput (P,s,5))) = P . (IC (Comput (P,s,5))) by PBOOLE:143;
A46: IC (Comput (P,s,5)) = (IC (Comput (P,s,4))) + 1 by A40, SCMPDS_2:47
.= 9 + 1 by A38 ;
then A47: CurInstr (P,(Comput (P,s,5))) = P . 10 by A45
.= AddTo (GBP,1,4) by Lm1, A1 ;
A48: 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 A47 ;
A49: DataLoc (((Comput (P,s,4)) . SBP),(4 + RetSP)) = intpos (n + (4 + 0)) by A42, Th1, SCMPDS_I:def 13;
then A50: (Comput (P,s,5)) . SBP = n by A40, A42, Lm3, SCMPDS_2:47;
A51: (Comput (P,s,5)) . GBP = 0 by A40, A43, A49, Lm2, SCMPDS_2:47;
n + 1 < n + 4 by XREAL_1:6;
then A52: (Comput (P,s,5)) . (intpos m) = s . (intpos m) by A7, A40, A44, A49, AMI_3:10, SCMPDS_2:47;
A53: P /. (IC (Comput (P,s,6))) = P . (IC (Comput (P,s,6))) by PBOOLE:143;
IC (Comput (P,s,6)) = (IC (Comput (P,s,5))) + 1 by A48, SCMPDS_2:48
.= 10 + 1 by A46 ;
then A54: CurInstr (P,(Comput (P,s,6))) = P . 11 by A53
.= saveIC (SBP,RetIC) by Lm1, A1 ;
A55: Comput (P,s,(6 + 1)) = Following (P,(Comput (P,s,6))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P,s,6))) by A54 ;
A56: DataLoc (((Comput (P,s,5)) . GBP),1) = intpos (0 + 1) by A51, Th1;
then A57: (Comput (P,s,6)) . SBP = n + 4 by A48, A50, SCMPDS_2:48;
A58: (Comput (P,s,6)) . (intpos m) = s . (intpos m) by A6, A48, A52, A56, AMI_3:10, SCMPDS_2:48;
A59: DataLoc (((Comput (P,s,6)) . SBP),RetIC) = intpos ((n + 4) + 1) by A57, Th1, SCMPDS_I:def 14
.= intpos (n + (4 + 1)) ;
n + 1 < n + 5 by XREAL_1:6;
hence (Comput (P,s,7)) . (intpos m) = s . (intpos m) by A7, A55, A58, A59, AMI_3:10, SCMPDS_2:59; :: thesis: verum