let n, m be Element of 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 A2: 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 A3: 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 A4: 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 A5: 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 A6: 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 A7: 1 < m ; :: thesis: ( not m <= n + 1 or (Comput (P,s,7)) . (intpos m) = s . (intpos m) )
assume A8: m <= n + 1 ; :: thesis: (Comput (P,s,7)) . (intpos m) = s . (intpos m)
A9: P /. (IC s) = P . (IC s) by PBOOLE:143;
A10: P /. (IC (Comput (P,s,1))) = P . (IC (Comput (P,s,1))) by PBOOLE:143;
A11: 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, A9, Lm1, A2 ;
then A12: IC (Comput (P,s,1)) = succ (IC s) by A6, SCMPDS_2:56
.= 5 + 1 by A3 ;
then A13: CurInstr (P,(Comput (P,s,1))) = P . 6 by A10
.= (SBP,6) := (SBP,3) by Lm1, A2 ;
A15: 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 A13 ;
A16: (Comput (P,s,1)) . SBP = n by A4, A11, SCMPDS_2:56;
A17: (Comput (P,s,1)) . GBP = 0 by A5, A11, SCMPDS_2:56;
A18: (Comput (P,s,1)) . (intpos m) = s . (intpos m) by A11, SCMPDS_2:56;
A19: P /. (IC (Comput (P,s,2))) = P . (IC (Comput (P,s,2))) by PBOOLE:143;
A20: IC (Comput (P,s,2)) = succ (IC (Comput (P,s,1))) by A15, SCMPDS_2:47
.= 6 + 1 by A12 ;
then A21: CurInstr (P,(Comput (P,s,2))) = P . 7 by A19
.= Divide (SBP,2,SBP,3) by Lm1, A2 ;
A23: 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 A21 ;
A24: DataLoc (((Comput (P,s,1)) . SBP),6) = intpos (n + 6) by A16, Th5;
then A25: (Comput (P,s,2)) . SBP = n by A15, A16, Lm3, SCMPDS_2:47;
A26: (Comput (P,s,2)) . GBP = 0 by A15, A17, A24, Lm2, SCMPDS_2:47;
n + 1 < n + 6 by XREAL_1:6;
then A27: (Comput (P,s,2)) . (intpos m) = s . (intpos m) by A8, A15, A18, A24, AMI_3:10, SCMPDS_2:47;
A28: P /. (IC (Comput (P,s,3))) = P . (IC (Comput (P,s,3))) by PBOOLE:143;
A29: IC (Comput (P,s,3)) = succ (IC (Comput (P,s,2))) by A23, SCMPDS_2:52
.= 7 + 1 by A20 ;
then A30: CurInstr (P,(Comput (P,s,3))) = P . 8 by A28
.= (SBP,7) := (SBP,3) by Lm1, A2 ;
A32: 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 A30 ;
A33: DataLoc (((Comput (P,s,2)) . SBP),2) = intpos (n + 2) by A25, Th5;
then A34: SBP <> DataLoc (((Comput (P,s,2)) . SBP),2) by Lm3;
A35: DataLoc (((Comput (P,s,2)) . SBP),3) = intpos (n + 3) by A25, Th5;
then SBP <> DataLoc (((Comput (P,s,2)) . SBP),3) by Lm3;
then A36: (Comput (P,s,3)) . SBP = n by A23, A25, A34, SCMPDS_2:52;
A37: GBP <> DataLoc (((Comput (P,s,2)) . SBP),2) by A33, Lm2;
GBP <> DataLoc (((Comput (P,s,2)) . SBP),3) by A35, Lm2;
then A38: (Comput (P,s,3)) . GBP = 0 by A23, A26, A37, SCMPDS_2:52;
n + 1 < n + 2 by XREAL_1:6;
then A39: intpos m <> DataLoc (((Comput (P,s,2)) . SBP),2) by A8, A33, AMI_3:10;
n + 1 < n + 3 by XREAL_1:6;
then intpos m <> DataLoc (((Comput (P,s,2)) . SBP),3) by A8, A35, AMI_3:10;
then A40: (Comput (P,s,3)) . (intpos m) = s . (intpos m) by A23, A27, A39, SCMPDS_2:52;
A41: P /. (IC (Comput (P,s,4))) = P . (IC (Comput (P,s,4))) by PBOOLE:143;
A42: IC (Comput (P,s,4)) = succ (IC (Comput (P,s,3))) by A32, SCMPDS_2:47
.= 8 + 1 by A29 ;
then A43: CurInstr (P,(Comput (P,s,4))) = P . 9 by A41
.= (SBP,(4 + RetSP)) := (GBP,1) by Lm1, A2 ;
A45: 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 A43 ;
A46: DataLoc (((Comput (P,s,3)) . SBP),7) = intpos (n + 7) by A36, Th5;
then A47: (Comput (P,s,4)) . SBP = n by A32, A36, Lm3, SCMPDS_2:47;
A48: (Comput (P,s,4)) . GBP = 0 by A32, A38, A46, Lm2, SCMPDS_2:47;
n + 1 < n + 7 by XREAL_1:6;
then A49: (Comput (P,s,4)) . (intpos m) = s . (intpos m) by A8, A32, A40, A46, AMI_3:10, SCMPDS_2:47;
A50: P /. (IC (Comput (P,s,5))) = P . (IC (Comput (P,s,5))) by PBOOLE:143;
A51: IC (Comput (P,s,5)) = succ (IC (Comput (P,s,4))) by A45, SCMPDS_2:47
.= 9 + 1 by A42 ;
then A52: CurInstr (P,(Comput (P,s,5))) = P . 10 by A50
.= AddTo (GBP,1,4) by Lm1, A2 ;
A54: 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 A52 ;
A55: DataLoc (((Comput (P,s,4)) . SBP),(4 + RetSP)) = intpos (n + (4 + 0)) by A47, Th5, SCMPDS_1:def 20;
then A56: (Comput (P,s,5)) . SBP = n by A45, A47, Lm3, SCMPDS_2:47;
A57: (Comput (P,s,5)) . GBP = 0 by A45, A48, A55, Lm2, SCMPDS_2:47;
n + 1 < n + 4 by XREAL_1:6;
then A58: (Comput (P,s,5)) . (intpos m) = s . (intpos m) by A8, A45, A49, A55, AMI_3:10, SCMPDS_2:47;
A59: P /. (IC (Comput (P,s,6))) = P . (IC (Comput (P,s,6))) by PBOOLE:143;
IC (Comput (P,s,6)) = succ (IC (Comput (P,s,5))) by A54, SCMPDS_2:48
.= 10 + 1 by A51 ;
then A60: CurInstr (P,(Comput (P,s,6))) = P . 11 by A59
.= saveIC (SBP,RetIC) by Lm1, A2 ;
A62: 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 ;
A63: DataLoc (((Comput (P,s,5)) . GBP),1) = intpos (0 + 1) by A57, Th5;
then A64: (Comput (P,s,6)) . SBP = n + 4 by A54, A56, SCMPDS_2:48;
A65: (Comput (P,s,6)) . (intpos m) = s . (intpos m) by A7, A54, A58, A63, AMI_3:10, SCMPDS_2:48;
A66: DataLoc (((Comput (P,s,6)) . SBP),RetIC) = intpos ((n + 4) + 1) by A64, Th5, SCMPDS_1:def 21
.= intpos (n + (4 + 1)) ;
n + 1 < n + 5 by XREAL_1:6;
hence (Comput (P,s,7)) . (intpos m) = s . (intpos m) by A8, A62, A65, A66, AMI_3:10, SCMPDS_2:59; :: thesis: verum