let n, m be Element of NAT ; :: thesis: for s being State of SCMPDS st GCD-Algorithm c= s & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc (s . SBP ),3) > 0 & 1 < m & m <= n + 1 holds
(Comput (ProgramPart s),s,7) . (intpos m) = s . (intpos m)
let s be State of SCMPDS ; :: thesis: ( GCD-Algorithm c= s & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc (s . SBP ),3) > 0 & 1 < m & m <= n + 1 implies (Comput (ProgramPart s),s,7) . (intpos m) = s . (intpos m) )
assume A1: GCD-Algorithm c= s ; :: 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 (ProgramPart s),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 (ProgramPart s),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 (ProgramPart s),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 (ProgramPart s),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 (ProgramPart s),s,7) . (intpos m) = s . (intpos m) )
assume A6: 1 < m ; :: thesis: ( not m <= n + 1 or (Comput (ProgramPart s),s,7) . (intpos m) = s . (intpos m) )
assume A7: m <= n + 1 ; :: thesis: (Comput (ProgramPart s),s,7) . (intpos m) = s . (intpos m)
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
Z: (ProgramPart (Comput (ProgramPart s),s,1)) /. (IC (Comput (ProgramPart s),s,1)) = (Comput (ProgramPart s),s,1) . (IC (Comput (ProgramPart s),s,1)) by COMPOS_1:38;
A8: Comput (ProgramPart s),s,(1 + 0 ) = Following (ProgramPart s),(Comput (ProgramPart s),s,0 ) by AMI_1:14
.= Following (ProgramPart s),s by AMI_1:13
.= Exec (SBP ,3 <=0_goto 9),s by A1, A2, Y, Lm1 ;
then A9: IC (Comput (ProgramPart s),s,1) = succ (IC s) by A5, SCMPDS_2:68
.= 5 + 1 by A2 ;
then A10: CurInstr (ProgramPart (Comput (ProgramPart s),s,1)),(Comput (ProgramPart s),s,1) = s . 6 by Z, AMI_1:54
.= SBP ,6 := SBP ,3 by A1, Lm1 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,1) by AMI_1:123;
A11: Comput (ProgramPart s),s,(1 + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,1) by AMI_1:14
.= Exec (SBP ,6 := SBP ,3),(Comput (ProgramPart s),s,1) by A10, T ;
A12: (Comput (ProgramPart s),s,1) . SBP = n by A3, A8, SCMPDS_2:68;
A13: (Comput (ProgramPart s),s,1) . GBP = 0 by A4, A8, SCMPDS_2:68;
A14: (Comput (ProgramPart s),s,1) . (intpos m) = s . (intpos m) by A8, SCMPDS_2:68;
Y: (ProgramPart (Comput (ProgramPart s),s,2)) /. (IC (Comput (ProgramPart s),s,2)) = (Comput (ProgramPart s),s,2) . (IC (Comput (ProgramPart s),s,2)) by COMPOS_1:38;
A15: IC (Comput (ProgramPart s),s,2) = succ (IC (Comput (ProgramPart s),s,1)) by A11, SCMPDS_2:59
.= 6 + 1 by A9 ;
then A16: CurInstr (ProgramPart (Comput (ProgramPart s),s,2)),(Comput (ProgramPart s),s,2) = s . 7 by Y, AMI_1:54
.= Divide SBP ,2,SBP ,3 by A1, Lm1 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,2) by AMI_1:123;
A17: Comput (ProgramPart s),s,(2 + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,2) by AMI_1:14
.= Exec (Divide SBP ,2,SBP ,3),(Comput (ProgramPart s),s,2) by A16, T ;
A18: DataLoc ((Comput (ProgramPart s),s,1) . SBP ),6 = intpos (n + 6) by A12, Th5;
then A19: (Comput (ProgramPart s),s,2) . SBP = n by A11, A12, Lm3, SCMPDS_2:59;
A20: (Comput (ProgramPart s),s,2) . GBP = 0 by A11, A13, A18, Lm2, SCMPDS_2:59;
n + 1 < n + 6 by XREAL_1:8;
then A21: (Comput (ProgramPart s),s,2) . (intpos m) = s . (intpos m) by A7, A11, A14, A18, AMI_3:52, SCMPDS_2:59;
Y: (ProgramPart (Comput (ProgramPart s),s,3)) /. (IC (Comput (ProgramPart s),s,3)) = (Comput (ProgramPart s),s,3) . (IC (Comput (ProgramPart s),s,3)) by COMPOS_1:38;
A22: IC (Comput (ProgramPart s),s,3) = succ (IC (Comput (ProgramPart s),s,2)) by A17, SCMPDS_2:64
.= 7 + 1 by A15 ;
then A23: CurInstr (ProgramPart (Comput (ProgramPart s),s,3)),(Comput (ProgramPart s),s,3) = s . 8 by Y, AMI_1:54
.= SBP ,7 := SBP ,3 by A1, Lm1 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,3) by AMI_1:123;
A24: Comput (ProgramPart s),s,(3 + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,3) by AMI_1:14
.= Exec (SBP ,7 := SBP ,3),(Comput (ProgramPart s),s,3) by A23, T ;
A25: DataLoc ((Comput (ProgramPart s),s,2) . SBP ),2 = intpos (n + 2) by A19, Th5;
then A26: SBP <> DataLoc ((Comput (ProgramPart s),s,2) . SBP ),2 by Lm3;
A27: DataLoc ((Comput (ProgramPart s),s,2) . SBP ),3 = intpos (n + 3) by A19, Th5;
then SBP <> DataLoc ((Comput (ProgramPart s),s,2) . SBP ),3 by Lm3;
then A28: (Comput (ProgramPart s),s,3) . SBP = n by A17, A19, A26, SCMPDS_2:64;
A29: GBP <> DataLoc ((Comput (ProgramPart s),s,2) . SBP ),2 by A25, Lm2;
GBP <> DataLoc ((Comput (ProgramPart s),s,2) . SBP ),3 by A27, Lm2;
then A30: (Comput (ProgramPart s),s,3) . GBP = 0 by A17, A20, A29, SCMPDS_2:64;
n + 1 < n + 2 by XREAL_1:8;
then A31: intpos m <> DataLoc ((Comput (ProgramPart s),s,2) . SBP ),2 by A7, A25, AMI_3:52;
n + 1 < n + 3 by XREAL_1:8;
then intpos m <> DataLoc ((Comput (ProgramPart s),s,2) . SBP ),3 by A7, A27, AMI_3:52;
then A32: (Comput (ProgramPart s),s,3) . (intpos m) = s . (intpos m) by A17, A21, A31, SCMPDS_2:64;
Y: (ProgramPart (Comput (ProgramPart s),s,4)) /. (IC (Comput (ProgramPart s),s,4)) = (Comput (ProgramPart s),s,4) . (IC (Comput (ProgramPart s),s,4)) by COMPOS_1:38;
A33: IC (Comput (ProgramPart s),s,4) = succ (IC (Comput (ProgramPart s),s,3)) by A24, SCMPDS_2:59
.= 8 + 1 by A22 ;
then A34: CurInstr (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4) = s . 9 by Y, AMI_1:54
.= SBP ,(4 + RetSP ) := GBP ,1 by A1, Lm1 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,4) by AMI_1:123;
A35: Comput (ProgramPart s),s,(4 + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,4) by AMI_1:14
.= Exec (SBP ,(4 + RetSP ) := GBP ,1),(Comput (ProgramPart s),s,4) by A34, T ;
A36: DataLoc ((Comput (ProgramPart s),s,3) . SBP ),7 = intpos (n + 7) by A28, Th5;
then A37: (Comput (ProgramPart s),s,4) . SBP = n by A24, A28, Lm3, SCMPDS_2:59;
A38: (Comput (ProgramPart s),s,4) . GBP = 0 by A24, A30, A36, Lm2, SCMPDS_2:59;
n + 1 < n + 7 by XREAL_1:8;
then A39: (Comput (ProgramPart s),s,4) . (intpos m) = s . (intpos m) by A7, A24, A32, A36, AMI_3:52, SCMPDS_2:59;
Y: (ProgramPart (Comput (ProgramPart s),s,5)) /. (IC (Comput (ProgramPart s),s,5)) = (Comput (ProgramPart s),s,5) . (IC (Comput (ProgramPart s),s,5)) by COMPOS_1:38;
A40: IC (Comput (ProgramPart s),s,5) = succ (IC (Comput (ProgramPart s),s,4)) by A35, SCMPDS_2:59
.= 9 + 1 by A33 ;
then A41: CurInstr (ProgramPart (Comput (ProgramPart s),s,5)),(Comput (ProgramPart s),s,5) = s . 10 by Y, AMI_1:54
.= AddTo GBP ,1,4 by A1, Lm1 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,5) by AMI_1:123;
A42: Comput (ProgramPart s),s,(5 + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,5) by AMI_1:14
.= Exec (AddTo GBP ,1,4),(Comput (ProgramPart s),s,5) by A41, T ;
A43: DataLoc ((Comput (ProgramPart s),s,4) . SBP ),(4 + RetSP ) = intpos (n + (4 + 0 )) by A37, Th5, SCMPDS_1:def 22;
then A44: (Comput (ProgramPart s),s,5) . SBP = n by A35, A37, Lm3, SCMPDS_2:59;
A45: (Comput (ProgramPart s),s,5) . GBP = 0 by A35, A38, A43, Lm2, SCMPDS_2:59;
n + 1 < n + 4 by XREAL_1:8;
then A46: (Comput (ProgramPart s),s,5) . (intpos m) = s . (intpos m) by A7, A35, A39, A43, AMI_3:52, SCMPDS_2:59;
Y: (ProgramPart (Comput (ProgramPart s),s,6)) /. (IC (Comput (ProgramPart s),s,6)) = (Comput (ProgramPart s),s,6) . (IC (Comput (ProgramPart s),s,6)) by COMPOS_1:38;
IC (Comput (ProgramPart s),s,6) = succ (IC (Comput (ProgramPart s),s,5)) by A42, SCMPDS_2:60
.= 10 + 1 by A40 ;
then A47: CurInstr (ProgramPart (Comput (ProgramPart s),s,6)),(Comput (ProgramPart s),s,6) = s . 11 by Y, AMI_1:54
.= saveIC SBP ,RetIC by A1, Lm1 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,6) by AMI_1:123;
A48: Comput (ProgramPart s),s,(6 + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,6) by AMI_1:14
.= Exec (saveIC SBP ,RetIC ),(Comput (ProgramPart s),s,6) by A47, T ;
A49: DataLoc ((Comput (ProgramPart s),s,5) . GBP ),1 = intpos (0 + 1) by A45, Th5;
then A50: (Comput (ProgramPart s),s,6) . SBP = n + 4 by A42, A44, SCMPDS_2:60;
A51: (Comput (ProgramPart s),s,6) . (intpos m) = s . (intpos m) by A6, A42, A46, A49, AMI_3:52, SCMPDS_2:60;
A52: DataLoc ((Comput (ProgramPart s),s,6) . SBP ),RetIC = intpos ((n + 4) + 1) by A50, Th5, SCMPDS_1:def 23
.= intpos (n + (4 + 1)) ;
n + 1 < n + 5 by XREAL_1:8;
hence (Comput (ProgramPart s),s,7) . (intpos m) = s . (intpos m) by A7, A48, A51, A52, AMI_3:52, SCMPDS_2:71; :: thesis: verum