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