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