let n be Element of NAT ; :: thesis:
let s be State of SCMPDS ; :: thesis:
set x = s . (DataLoc (s . SBP ),2);
set y = s . (DataLoc (s . SBP ),3);
assume A1: GCD-Algorithm c= s ; :: 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:
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;
A6: 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 A7: IC (Comput (ProgramPart s),s,1) = succ (IC s) by A5, SCMPDS_2:68
.= 5 + 1 by A2 ;
then A8: 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;
A9: 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 A8, T ;
A10: (Comput (ProgramPart s),s,1) . SBP = n by A3, A6, SCMPDS_2:68;
A11: (Comput (ProgramPart s),s,1) . GBP = 0 by A4, A6, SCMPDS_2:68;
A12: (Comput (ProgramPart s),s,1) . (intpos (n + 3)) = (Comput (ProgramPart s),s,1) . (DataLoc n,3) by Th5
.= s . (DataLoc (s . SBP ),3) by A3, A6, SCMPDS_2:68 ;
A13: (Comput (ProgramPart s),s,1) . (intpos (n + 2)) = (Comput (ProgramPart s),s,1) . (DataLoc n,2) by Th5
.= s . (DataLoc (s . SBP ),2) by A3, A6, 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;
A14: IC (Comput (ProgramPart s),s,2) = succ (IC (Comput (ProgramPart s),s,1)) by A9, SCMPDS_2:59
.= 6 + 1 by A7 ;
then A15: 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;
A16: 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 A15, T ;
A17: DataLoc ((Comput (ProgramPart s),s,1) . SBP ),6 = intpos (n + 6) by A10, Th5;
then A18: (Comput (ProgramPart s),s,2) . SBP = n by A9, A10, Lm3, SCMPDS_2:59;
A19: (Comput (ProgramPart s),s,2) . GBP = 0 by A9, A11, A17, Lm2, SCMPDS_2:59;
A20: (Comput (ProgramPart s),s,2) . (intpos (n + 6)) = (Comput (ProgramPart s),s,1) . (DataLoc n,3) by A9, A10, A17, SCMPDS_2:59
.= s . (DataLoc (s . SBP ),3) by A12, Th5 ;
n + 3 <> n + 6 ;
then A21: (Comput (ProgramPart s),s,2) . (intpos (n + 3)) = s . (DataLoc (s . SBP ),3) by A9, A12, A17, AMI_3:52, SCMPDS_2:59;
n + 2 <> n + 6 ;
then A22: (Comput (ProgramPart s),s,2) . (intpos (n + 2)) = s . (DataLoc (s . SBP ),2) by A9, A13, A17, 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;
A23: IC (Comput (ProgramPart s),s,3) = succ (IC (Comput (ProgramPart s),s,2)) by A16, SCMPDS_2:64
.= 7 + 1 by A14 ;
then A24: 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;
A25: 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 A24, T ;
A26: DataLoc ((Comput (ProgramPart s),s,2) . SBP ),2 = intpos (n + 2) by A18, Th5;
then A27: SBP <> DataLoc ((Comput (ProgramPart s),s,2) . SBP ),2 by Lm3;
A28: DataLoc ((Comput (ProgramPart s),s,2) . SBP ),3 = intpos (n + 3) by A18, Th5;
then SBP <> DataLoc ((Comput (ProgramPart s),s,2) . SBP ),3 by Lm3;
then A29: (Comput (ProgramPart s),s,3) . SBP = n by A16, A18, A27, SCMPDS_2:64;
A30: GBP <> DataLoc ((Comput (ProgramPart s),s,2) . SBP ),2 by A26, Lm2;
GBP <> DataLoc ((Comput (ProgramPart s),s,2) . SBP ),3 by A28, Lm2;
then A31: (Comput (ProgramPart s),s,3) . GBP = 0 by A16, A19, A30, SCMPDS_2:64;
A32: (Comput (ProgramPart s),s,3) . (intpos (n + 3)) = (s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)) by A16, A21, A22, A26, A28, SCMPDS_2:64;
n + 6 <> n + 2 ;
then A33: intpos (n + 6) <> DataLoc ((Comput (ProgramPart s),s,2) . SBP ),2 by A26, AMI_3:52;
n + 6 <> n + 3 ;
then intpos (n + 6) <> DataLoc ((Comput (ProgramPart s),s,2) . SBP ),3 by A28, AMI_3:52;
then A34: (Comput (ProgramPart s),s,3) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) by A16, A20, A33, 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;
A35: IC (Comput (ProgramPart s),s,4) = succ (IC (Comput (ProgramPart s),s,3)) by A25, SCMPDS_2:59
.= 8 + 1 by A23 ;
then A36: 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;
A37: 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 A36, T ;
A38: DataLoc ((Comput (ProgramPart s),s,3) . SBP ),7 = intpos (n + 7) by A29, Th5;
then A39: (Comput (ProgramPart s),s,4) . SBP = n by A25, A29, Lm3, SCMPDS_2:59;
A40: (Comput (ProgramPart s),s,4) . GBP = 0 by A25, A31, A38, Lm2, SCMPDS_2:59;
A41: (Comput (ProgramPart s),s,4) . (intpos (n + 7)) = (Comput (ProgramPart s),s,3) . (DataLoc n,3) by A25, A29, A38, SCMPDS_2:59
.= (s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)) by A32, Th5 ;
n + 6 <> n + 7 ;
then A42: (Comput (ProgramPart s),s,4) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) by A25, A34, A38, 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;
A43: IC (Comput (ProgramPart s),s,5) = succ (IC (Comput (ProgramPart s),s,4)) by A37, SCMPDS_2:59
.= 9 + 1 by A35 ;
then A44: 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;
A45: 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 A44, T ;
A46: DataLoc ((Comput (ProgramPart s),s,4) . SBP ),(4 + RetSP ) = intpos (n + (4 + 0 )) by A39, Th5, SCMPDS_1:def 22;
then A47: (Comput (ProgramPart s),s,5) . SBP = n by A37, A39, Lm3, SCMPDS_2:59;
A48: (Comput (ProgramPart s),s,5) . GBP = 0 by A37, A40, A46, Lm2, SCMPDS_2:59;
n + 7 <> n + 4 ;
then A49: (Comput (ProgramPart s),s,5) . (intpos (n + 7)) = (s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)) by A37, A41, A46, AMI_3:52, SCMPDS_2:59;
n + 6 <> n + 4 ;
then A50: (Comput (ProgramPart s),s,5) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) by A37, A42, A46, AMI_3:52, SCMPDS_2:59;
A51: (Comput (ProgramPart s),s,5) . (intpos (n + 4)) = (Comput (ProgramPart s),s,4) . (DataLoc 0 ,1) by A37, A40, A46, SCMPDS_2:59
.= (Comput (ProgramPart s),s,4) . (intpos (0 + 1)) by Th5
.= n by A25, A29, A38, Lm3, 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;
A52: IC (Comput (ProgramPart s),s,6) = succ (IC (Comput (ProgramPart s),s,5)) by A45, SCMPDS_2:60
.= 10 + 1 by A43 ;
then A53: 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;
A54: 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 A53, T ;
A55: DataLoc ((Comput (ProgramPart s),s,5) . GBP ),1 = intpos (0 + 1) by A48, Th5;
then A56: (Comput (ProgramPart s),s,6) . SBP = n + 4 by A45, A47, SCMPDS_2:60;
A57: (Comput (ProgramPart s),s,6) . GBP = 0 by A45, A48, A55, AMI_3:52, SCMPDS_2:60;
n + 7 <> 1 by NAT_1:11;
then A58: (Comput (ProgramPart s),s,6) . (intpos (n + 7)) = (s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)) by A45, A49, A55, AMI_3:52, SCMPDS_2:60;
n + 6 <> 1 by NAT_1:11;
then A59: (Comput (ProgramPart s),s,6) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) by A45, A50, A55, AMI_3:52, SCMPDS_2:60;
n + 4 <> 1 by NAT_1:11;
then A60: (Comput (ProgramPart s),s,6) . (intpos (n + 4)) = n by A45, A51, A55, AMI_3:52, SCMPDS_2:60;
Y: (ProgramPart (Comput (ProgramPart s),s,7)) /. (IC (Comput (ProgramPart s),s,7)) = (Comput (ProgramPart s),s,7) . (IC (Comput (ProgramPart s),s,7)) by COMPOS_1:38;
thus IC (Comput (ProgramPart s),s,7) = succ (IC (Comput (ProgramPart s),s,6)) by A54, SCMPDS_2:71
.= 11 + 1 by A52
.= 5 + 7 ; :: thesis:
then A61: CurInstr (ProgramPart (Comput (ProgramPart s),s,7)),(Comput (ProgramPart s),s,7) = s . 12 by Y, AMI_1:54
.= goto (- 7) by A1, Lm1 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,7) by AMI_1:123;
thus Comput (ProgramPart s),s,8 = Comput (ProgramPart s),s,(7 + 1)
.= Following (ProgramPart s),(Comput (ProgramPart s),s,7) by AMI_1:14
.= Exec (goto (- 7)),(Comput (ProgramPart s),s,7) by A61, T ; :: thesis:
A62: DataLoc ((Comput (ProgramPart s),s,6) . SBP ),RetIC = intpos ((n + 4) + 1) by A56, Th5, SCMPDS_1:def 23
.= intpos (n + (4 + 1)) ;
then SBP <> DataLoc ((Comput (ProgramPart s),s,6) . SBP ),RetIC by Lm3;
hence (Comput (ProgramPart s),s,7) . SBP = n + 4 by A54, A56, SCMPDS_2:71; :: thesis:
GBP <> DataLoc ((Comput (ProgramPart s),s,6) . SBP ),RetIC by A62, Lm2;
hence (Comput (ProgramPart s),s,7) . GBP = 0 by A54, A57, SCMPDS_2:71; :: thesis:
n + 7 <> n + 5 ;
hence (Comput (ProgramPart s),s,7) . (intpos (n + 7)) = (s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)) by A54, A58, A62, AMI_3:52, SCMPDS_2:71; :: thesis:
n + 6 <> n + 5 ;
hence (Comput (ProgramPart s),s,7) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) by A54, A59, A62, AMI_3:52, SCMPDS_2:71; :: thesis:
n + 4 <> n + 5 ;
hence (Comput (ProgramPart s),s,7) . (intpos (n + 4)) = n by A54, A60, A62, AMI_3:52, SCMPDS_2:71; :: thesis:
thus (Comput (ProgramPart s),s,7) . (intpos (n + 5)) = 11 by A52, A54, A62, SCMPDS_2:71; :: thesis: