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 = 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 SBP <> DataLoc ((Computation s,1) . SBP ),6 by Lm3;
then A18: (Computation s,2) . SBP = n by A9, A10, SCMPDS_2:59;
GBP <> DataLoc ((Computation s,1) . SBP ),6 by A17, Lm2;
then A19: (Computation s,2) . GBP = 0 by A9, A11, 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 intpos (n + 3) <> DataLoc ((Computation s,1) . SBP ),6 by A17, AMI_3:52;
then A21: (Computation s,2) . (intpos (n + 3)) = s . (DataLoc (s . SBP ),3) by A9, A12, SCMPDS_2:59;
n + 2 <> n + 6 ;
then intpos (n + 2) <> DataLoc ((Computation s,1) . SBP ),6 by A17, AMI_3:52;
then A22: (Computation s,2) . (intpos (n + 2)) = s . (DataLoc (s . SBP ),2) by A9, A13, 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: SBP <> DataLoc ((Computation s,3) . SBP ),7 by Lm3;
then A40: (Computation s,4) . SBP = n by A25, A29, SCMPDS_2:59;
GBP <> DataLoc ((Computation s,3) . SBP ),7 by A38, Lm2;
then A41: (Computation s,4) . GBP = 0 by A25, A31, SCMPDS_2:59;
A42: (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 intpos (n + 6) <> DataLoc ((Computation s,3) . SBP ),7 by A38, AMI_3:52;
then A43: (Computation s,4) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) by A25, A34, SCMPDS_2:59;
A44: IC (Computation s,5) = Next (IC (Computation s,4)) by A37, SCMPDS_2:59
.= inspos (9 + 1) by A35 ;
then A45: CurInstr (Computation s,5) = s . (inspos 10) by AMI_1:54
.= AddTo GBP ,1,4 by A1, Lm1 ;
A46: Computation s,(5 + 1) = Following (Computation s,5) by AMI_1:14
.= Exec (AddTo GBP ,1,4),(Computation s,5) by A45 ;
A47: DataLoc ((Computation s,4) . SBP ),(4 + RetSP ) = intpos (n + (4 + 0 )) by A40, Th5, SCMPDS_1:def 22;
then SBP <> DataLoc ((Computation s,4) . SBP ),(4 + RetSP ) by Lm3;
then A48: (Computation s,5) . SBP = n by A37, A40, SCMPDS_2:59;
GBP <> DataLoc ((Computation s,4) . SBP ),(4 + RetSP ) by A47, Lm2;
then A49: (Computation s,5) . GBP = 0 by A37, A41, SCMPDS_2:59;
n + 7 <> n + 4 ;
then intpos (n + 7) <> DataLoc ((Computation s,4) . SBP ),(4 + RetSP ) by A47, AMI_3:52;
then A50: (Computation s,5) . (intpos (n + 7)) = (s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)) by A37, A42, SCMPDS_2:59;
n + 6 <> n + 4 ;
then intpos (n + 6) <> DataLoc ((Computation s,4) . SBP ),(4 + RetSP ) by A47, AMI_3:52;
then A51: (Computation s,5) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) by A37, A43, SCMPDS_2:59;
A52: (Computation s,5) . (intpos (n + 4)) = (Computation s,4) . (DataLoc 0 ,1) by A37, A41, A47, SCMPDS_2:59
.= (Computation s,4) . (intpos (0 + 1)) by Th5
.= n by A25, A29, A39, SCMPDS_2:59 ;
A53: IC (Computation s,6) = Next (IC (Computation s,5)) by A46, SCMPDS_2:60
.= inspos (10 + 1) by A44 ;
then A54: CurInstr (Computation s,6) = s . (inspos 11) by AMI_1:54
.= saveIC SBP ,RetIC by A1, Lm1 ;
A55: Computation s,(6 + 1) = Following (Computation s,6) by AMI_1:14
.= Exec (saveIC SBP ,RetIC ),(Computation s,6) by A54 ;
A56: DataLoc ((Computation s,5) . GBP ),1 = intpos (0 + 1) by A49, Th5;
then A57: (Computation s,6) . SBP = n + 4 by A46, A48, SCMPDS_2:60;
A58: (Computation s,6) . GBP = 0 by A46, A49, A56, Th7, SCMPDS_2:60;
n + 7 <> 1 by NAT_1:11;
then intpos (n + 7) <> DataLoc ((Computation s,5) . GBP ),1 by A56, AMI_3:52;
then A59: (Computation s,6) . (intpos (n + 7)) = (s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)) by A46, A50, SCMPDS_2:60;
n + 6 <> 1 by NAT_1:11;
then intpos (n + 6) <> DataLoc ((Computation s,5) . GBP ),1 by A56, AMI_3:52;
then A60: (Computation s,6) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) by A46, A51, SCMPDS_2:60;
n + 4 <> 1 by NAT_1:11;
then intpos (n + 4) <> DataLoc ((Computation s,5) . GBP ),1 by A56, AMI_3:52;
then A61: (Computation s,6) . (intpos (n + 4)) = n by A46, A52, SCMPDS_2:60;
thus IC (Computation s,7) = Next (IC (Computation s,6)) by A55, SCMPDS_2:71
.= inspos (11 + 1) by A53
.= inspos (5 + 7) ; :: thesis:
then A62: 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 A62 ; :: thesis:
A63: DataLoc ((Computation s,6) . SBP ),RetIC = intpos ((n + 4) + 1) by A57, 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 A55, A57, SCMPDS_2:71; :: thesis:
GBP <> DataLoc ((Computation s,6) . SBP ),RetIC by A63, Lm2;
hence (Computation s,7) . GBP = 0 by A55, A58, SCMPDS_2:71; :: thesis:
n + 7 <> n + 5 ;
then intpos (n + 7) <> DataLoc ((Computation s,6) . SBP ),RetIC by A63, AMI_3:52;
hence (Computation s,7) . (intpos (n + 7)) = (s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)) by A55, A59, SCMPDS_2:71; :: thesis:
n + 6 <> n + 5 ;
then intpos (n + 6) <> DataLoc ((Computation s,6) . SBP ),RetIC by A63, AMI_3:52;
hence (Computation s,7) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) by A55, A60, SCMPDS_2:71; :: thesis:
n + 4 <> n + 5 ;
then intpos (n + 4) <> DataLoc ((Computation s,6) . SBP ),RetIC by A63, AMI_3:52;
hence (Computation s,7) . (intpos (n + 4)) = n by A55, A61, SCMPDS_2:71; :: thesis:
thus (Computation s,7) . (intpos (n + 5)) = inspos 11 by A53, A55, A63, SCMPDS_2:71; :: thesis: