set GA = GCD-Algorithm ;
defpred S1[ Element of NAT ] means for s being State of SCMPDS st GCD-Algorithm c= s & IC s = inspos 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc (s . SBP ),3) <= $1 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) holds
ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & s . SBP = (Computation s,n) . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) );
now let s be
State of
SCMPDS ;
:: thesis: ( GCD-Algorithm c= s & IC s = inspos 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc (s . SBP ),3) <= 0 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & (Computation s,n) . SBP = s . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) ) )set x =
s . (DataLoc (s . SBP ),2);
set y =
s . (DataLoc (s . SBP ),3);
assume A1:
GCD-Algorithm c= s
;
:: thesis: ( IC s = inspos 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc (s . SBP ),3) <= 0 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & (Computation s,n) . SBP = s . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) ) )assume A2:
IC s = inspos 5
;
:: thesis: ( s . SBP > 0 & s . GBP = 0 & s . (DataLoc (s . SBP ),3) <= 0 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & (Computation s,n) . SBP = s . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) ) )assume
s . SBP > 0
;
:: thesis: ( s . GBP = 0 & s . (DataLoc (s . SBP ),3) <= 0 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & (Computation s,n) . SBP = s . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) ) )assume
s . GBP = 0
;
:: thesis: ( s . (DataLoc (s . SBP ),3) <= 0 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & (Computation s,n) . SBP = s . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) ) )assume A3:
s . (DataLoc (s . SBP ),3) <= 0
;
:: thesis: ( s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & (Computation s,n) . SBP = s . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) ) )assume A4:
s . (DataLoc (s . SBP ),3) >= 0
;
:: thesis: ( s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & (Computation s,n) . SBP = s . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) ) )assume A5:
s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3)
;
:: thesis: ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & (Computation s,n) . SBP = s . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )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) =
ICplusConst s,9
by A3, SCMPDS_2:68
.=
inspos (5 + 9)
by A2, SCMPDS_6:23
;
take n = 1;
:: thesis: ( CurInstr (Computation s,n) = return SBP & (Computation s,n) . SBP = s . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )thus CurInstr (Computation s,n) =
s . (inspos 14)
by A7, AMI_1:54
.=
return SBP
by A1, Lm1
;
:: thesis: ( (Computation s,n) . SBP = s . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )thus
(Computation s,n) . SBP = s . SBP
by A6, SCMPDS_2:68;
:: thesis: ( (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )A8:
s . (DataLoc (s . SBP ),3) = 0
by A3, A4, XXREAL_0:1;
then A9:
abs (s . (DataLoc (s . SBP ),3)) = 0
by ABSVALUE:def 1;
thus (Computation s,n) . (DataLoc (s . SBP ),2) =
s . (DataLoc (s . SBP ),2)
by A6, SCMPDS_2:68
.=
abs (s . (DataLoc (s . SBP ),2))
by A5, A8, ABSVALUE:def 1
.=
(abs (s . (DataLoc (s . SBP ),2))) gcd (abs (s . (DataLoc (s . SBP ),3)))
by A9, NEWTON:65
.=
(s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3))
by INT_2:51
;
:: thesis: for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j)thus
for
j being
Element of
NAT st 1
< j &
j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j)
by A6, SCMPDS_2:68;
:: thesis: verum end;
then A10:
S1[ 0 ]
;
A11:
now let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )assume A12:
S1[
k]
;
:: thesis: S1[k + 1]now let s be
State of
SCMPDS ;
:: thesis: ( GCD-Algorithm c= s & IC s = inspos 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc (s . SBP ),3) <= k + 1 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation n,b2) = return SBP & n . SBP = (Computation n,b2) . SBP & (Computation n,b2) . (DataLoc (n . SBP ),2) = (n . (DataLoc (n . SBP ),2)) gcd (n . (DataLoc (n . SBP ),3)) & ( for j being Element of NAT st 1 < b3 & b3 <= (n . SBP ) + 1 holds
n . (intpos b3) = (Computation n,j) . (intpos b3) ) ) )set x =
s . (DataLoc (s . SBP ),2);
set y =
s . (DataLoc (s . SBP ),3);
set yy =
s . (DataLoc (s . SBP ),3);
assume A13:
GCD-Algorithm c= s
;
:: thesis: ( IC s = inspos 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc (s . SBP ),3) <= k + 1 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation n,b2) = return SBP & n . SBP = (Computation n,b2) . SBP & (Computation n,b2) . (DataLoc (n . SBP ),2) = (n . (DataLoc (n . SBP ),2)) gcd (n . (DataLoc (n . SBP ),3)) & ( for j being Element of NAT st 1 < b3 & b3 <= (n . SBP ) + 1 holds
n . (intpos b3) = (Computation n,j) . (intpos b3) ) ) )assume A14:
IC s = inspos 5
;
:: thesis: ( s . SBP > 0 & s . GBP = 0 & s . (DataLoc (s . SBP ),3) <= k + 1 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation n,b2) = return SBP & n . SBP = (Computation n,b2) . SBP & (Computation n,b2) . (DataLoc (n . SBP ),2) = (n . (DataLoc (n . SBP ),2)) gcd (n . (DataLoc (n . SBP ),3)) & ( for j being Element of NAT st 1 < b3 & b3 <= (n . SBP ) + 1 holds
n . (intpos b3) = (Computation n,j) . (intpos b3) ) ) )assume A15:
s . SBP > 0
;
:: thesis: ( s . GBP = 0 & s . (DataLoc (s . SBP ),3) <= k + 1 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation n,b2) = return SBP & n . SBP = (Computation n,b2) . SBP & (Computation n,b2) . (DataLoc (n . SBP ),2) = (n . (DataLoc (n . SBP ),2)) gcd (n . (DataLoc (n . SBP ),3)) & ( for j being Element of NAT st 1 < b3 & b3 <= (n . SBP ) + 1 holds
n . (intpos b3) = (Computation n,j) . (intpos b3) ) ) )assume A16:
s . GBP = 0
;
:: thesis: ( s . (DataLoc (s . SBP ),3) <= k + 1 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation n,b2) = return SBP & n . SBP = (Computation n,b2) . SBP & (Computation n,b2) . (DataLoc (n . SBP ),2) = (n . (DataLoc (n . SBP ),2)) gcd (n . (DataLoc (n . SBP ),3)) & ( for j being Element of NAT st 1 < b3 & b3 <= (n . SBP ) + 1 holds
n . (intpos b3) = (Computation n,j) . (intpos b3) ) ) )assume A17:
s . (DataLoc (s . SBP ),3) <= k + 1
;
:: thesis: ( s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation n,b2) = return SBP & n . SBP = (Computation n,b2) . SBP & (Computation n,b2) . (DataLoc (n . SBP ),2) = (n . (DataLoc (n . SBP ),2)) gcd (n . (DataLoc (n . SBP ),3)) & ( for j being Element of NAT st 1 < b3 & b3 <= (n . SBP ) + 1 holds
n . (intpos b3) = (Computation n,j) . (intpos b3) ) ) )assume A18:
s . (DataLoc (s . SBP ),3) >= 0
;
:: thesis: ( s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation n,b2) = return SBP & n . SBP = (Computation n,b2) . SBP & (Computation n,b2) . (DataLoc (n . SBP ),2) = (n . (DataLoc (n . SBP ),2)) gcd (n . (DataLoc (n . SBP ),3)) & ( for j being Element of NAT st 1 < b3 & b3 <= (n . SBP ) + 1 holds
n . (intpos b3) = (Computation n,j) . (intpos b3) ) ) )assume A19:
s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3)
;
:: thesis: ex n being Element of NAT st
( CurInstr (Computation n,b2) = return SBP & n . SBP = (Computation n,b2) . SBP & (Computation n,b2) . (DataLoc (n . SBP ),2) = (n . (DataLoc (n . SBP ),2)) gcd (n . (DataLoc (n . SBP ),3)) & ( for j being Element of NAT st 1 < b3 & b3 <= (n . SBP ) + 1 holds
n . (intpos b3) = (Computation n,j) . (intpos b3) ) )then A20:
s . (DataLoc (s . SBP ),2) >= 0
by A18, XXREAL_0:2;
reconsider y =
s . (DataLoc (s . SBP ),3) as
Element of
NAT by A18, INT_1:16;
per cases
( y <= k or y = k + 1 )
by A17, NAT_1:8;
suppose
y <= k
;
:: thesis: ex n being Element of NAT st
( CurInstr (Computation n,b2) = return SBP & n . SBP = (Computation n,b2) . SBP & (Computation n,b2) . (DataLoc (n . SBP ),2) = (n . (DataLoc (n . SBP ),2)) gcd (n . (DataLoc (n . SBP ),3)) & ( for j being Element of NAT st 1 < b3 & b3 <= (n . SBP ) + 1 holds
n . (intpos b3) = (Computation n,j) . (intpos b3) ) )hence
ex
n being
Element of
NAT st
(
CurInstr (Computation s,n) = return SBP &
s . SBP = (Computation s,n) . SBP &
(Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for
j being
Element of
NAT st 1
< j &
j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )
by A12, A13, A14, A15, A16, A18, A19;
:: thesis: verum end; suppose A21:
y = k + 1
;
:: thesis: ex n being Element of NAT st
( CurInstr (Computation n,b2) = return SBP & (Computation n,b2) . SBP = n . SBP & (Computation n,b2) . (DataLoc (n . SBP ),2) = (n . (DataLoc (n . SBP ),2)) gcd (n . (DataLoc (n . SBP ),3)) & ( for j being Element of NAT st 1 < b3 & b3 <= (n . SBP ) + 1 holds
n . (intpos b3) = (Computation n,j) . (intpos b3) ) )then A22:
y > 0
by NAT_1:5;
reconsider pn =
s . SBP as
Element of
NAT by A15, INT_1:16;
A23:
pn = s . SBP
;
then A24:
(
IC (Computation s,7) = inspos (5 + 7) &
Computation s,8
= Exec (goto (- 7)),
(Computation s,7) &
(Computation s,7) . SBP = pn + 4 &
(Computation s,7) . GBP = 0 &
(Computation s,7) . (intpos (pn + 7)) = (s . (DataLoc (s . SBP ),2)) mod y &
(Computation s,7) . (intpos (pn + 6)) = y &
(Computation s,7) . (intpos (pn + 4)) = pn &
(Computation s,7) . (intpos (pn + 5)) = inspos 11 )
by A13, A14, A16, A22, Lm4;
set s8 =
Computation s,8;
A25:
IC (Computation s,8) =
ICplusConst (Computation s,7),
(- 7)
by A24, SCMPDS_2:66
.=
inspos 5
by A24, Th6
;
A26:
GCD-Algorithm c= Computation s,8
by A13, AMI_1:81;
A27:
(Computation s,8) . SBP = pn + 4
by A24, SCMPDS_2:66;
A28:
4
<= pn + 4
by NAT_1:11;
then A29:
(Computation s,8) . SBP > 0
by A27, XXREAL_0:2;
A30:
(Computation s,8) . GBP = 0
by A24, SCMPDS_2:66;
set x1 =
(Computation s,8) . (DataLoc ((Computation s,8) . SBP ),2);
set y1 =
(Computation s,8) . (DataLoc ((Computation s,8) . SBP ),3);
A31:
(Computation s,8) . (DataLoc ((Computation s,8) . SBP ),2) =
(Computation s,8) . (intpos ((pn + 4) + 2))
by A27, Th5
.=
y
by A24, SCMPDS_2:66
;
A32:
(Computation s,8) . (DataLoc ((Computation s,8) . SBP ),3) =
(Computation s,8) . (intpos ((pn + 4) + 3))
by A27, Th5
.=
(s . (DataLoc (s . SBP ),2)) mod y
by A24, SCMPDS_2:66
;
then A33:
(Computation s,8) . (DataLoc ((Computation s,8) . SBP ),3) < y
by A21, NAT_1:5, NEWTON:79;
then A34:
(Computation s,8) . (DataLoc ((Computation s,8) . SBP ),3) <= k
by A21, INT_1:20;
(Computation s,8) . (DataLoc ((Computation s,8) . SBP ),3) >= 0
by A22, A32, NEWTON:78;
then consider m being
Element of
NAT such that A35:
(
CurInstr (Computation (Computation s,8),m) = return SBP &
(Computation s,8) . SBP = (Computation (Computation s,8),m) . SBP &
(Computation (Computation s,8),m) . (DataLoc ((Computation s,8) . SBP ),2) = ((Computation s,8) . (DataLoc ((Computation s,8) . SBP ),2)) gcd ((Computation s,8) . (DataLoc ((Computation s,8) . SBP ),3)) & ( for
j being
Element of
NAT st 1
< j &
j <= ((Computation s,8) . SBP ) + 1 holds
(Computation s,8) . (intpos j) = (Computation (Computation s,8),m) . (intpos j) ) )
by A12, A25, A26, A29, A30, A31, A33, A34;
set s9 =
Computation s,
(m + 8);
A36:
(Computation s,8) . SBP = (Computation s,(m + 8)) . SBP
by A35, AMI_1:51;
A37:
Computation s,
(m + (8 + 1)) =
Computation s,
((m + 8) + 1)
.=
Following (Computation s,(m + 8))
by AMI_1:14
.=
Exec (return SBP ),
(Computation s,(m + 8))
by A35, AMI_1:51
;
A38:
1
< pn + 4
by A28, XXREAL_0:2;
pn + 4
< ((Computation s,8) . SBP ) + 1
by A27, XREAL_1:31;
then A39:
(Computation s,8) . (intpos (pn + 4)) =
(Computation (Computation s,8),m) . (intpos (pn + 4))
by A35, A38
.=
(Computation s,(m + 8)) . (intpos (pn + 4))
by AMI_1:51
;
5
<= pn + 5
by NAT_1:11;
then A40:
1
< pn + 5
by XXREAL_0:2;
A41:
inspos 11 =
(Computation s,8) . (intpos (pn + 5))
by A24, SCMPDS_2:66
.=
(Computation (Computation s,8),m) . (intpos (pn + 5))
by A27, A35, A40
.=
(Computation s,(m + 8)) . (intpos ((pn + 4) + 1))
by AMI_1:51
.=
(Computation s,(m + 8)) . (DataLoc ((Computation s,(m + 8)) . SBP ),RetIC )
by A27, A36, Th5, SCMPDS_1:def 23
;
A42:
IC (Computation s,(m + 9)) =
(abs ((Computation s,(m + 8)) . (DataLoc ((Computation s,(m + 8)) . SBP ),RetIC ))) + 2
by A37, SCMPDS_2:70
.=
inspos (11 + 2)
by A41, Th3
;
then A43:
CurInstr (Computation s,(m + 9)) =
s . (inspos 13)
by AMI_1:54
.=
SBP ,2
:= SBP ,6
by A13, Lm1
;
A44:
Computation s,
(m + (9 + 1)) =
Computation s,
((m + 9) + 1)
.=
Following (Computation s,(m + 9))
by AMI_1:14
.=
Exec (SBP ,2 := SBP ,6),
(Computation s,(m + 9))
by A43
;
A45:
(Computation s,(m + 9)) . SBP =
(Computation s,(m + 8)) . (DataLoc (pn + 4),RetSP )
by A27, A36, A37, SCMPDS_2:70
.=
(Computation s,(m + 8)) . (intpos ((pn + 4) + 0 ))
by Th5, SCMPDS_1:def 22
.=
pn
by A24, A39, SCMPDS_2:66
;
SBP <> intpos (pn + 6)
by Lm3;
then A46:
(Computation s,(m + 9)) . (intpos (pn + 6)) =
(Computation s,(m + 8)) . (intpos ((pn + 4) + 2))
by A37, SCMPDS_2:70
.=
(Computation s,(m + 8)) . (DataLoc ((Computation s,8) . SBP ),2)
by A27, Th5
.=
((Computation s,8) . (DataLoc ((Computation s,8) . SBP ),2)) gcd ((Computation s,8) . (DataLoc ((Computation s,8) . SBP ),3))
by A35, AMI_1:51
;
IC (Computation s,(m + 10)) =
Next (IC (Computation s,(m + 9)))
by A44, SCMPDS_2:59
.=
inspos (13 + 1)
by A42
;
then A47:
CurInstr (Computation s,(m + 10)) =
s . (inspos 14)
by AMI_1:54
.=
return SBP
by A13, Lm1
;
hereby :: thesis: verum
take n =
m + 10;
:: thesis: ( CurInstr (Computation s,n) = return SBP & (Computation s,n) . SBP = s . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )thus
CurInstr (Computation s,n) = return SBP
by A47;
:: thesis: ( (Computation s,n) . SBP = s . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )A48:
DataLoc ((Computation s,(m + 9)) . SBP ),2
= intpos (pn + 2)
by A45, Th5;
then
SBP <> DataLoc ((Computation s,(m + 9)) . SBP ),2
by Lm3;
hence
(Computation s,n) . SBP = s . SBP
by A44, A45, SCMPDS_2:59;
:: thesis: ( (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )thus (Computation s,n) . (DataLoc (s . SBP ),2) =
(Computation s,(m + 9)) . (DataLoc pn,6)
by A44, A45, SCMPDS_2:59
.=
(s . (DataLoc (s . SBP ),3)) gcd ((s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)))
by A31, A32, A46, Th5
.=
(s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3))
by A20, A21, NAT_1:5, NAT_D:30
;
:: thesis: for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j)hereby :: thesis: verum
let j be
Element of
NAT ;
:: thesis: ( 1 < j & j <= (s . SBP ) + 1 implies s . (intpos j) = (Computation s,n) . (intpos j) )assume A49:
( 1
< j &
j <= (s . SBP ) + 1 )
;
:: thesis: s . (intpos j) = (Computation s,n) . (intpos j)
s . SBP <= (Computation s,8) . SBP
by A27, NAT_1:11;
then
(s . SBP ) + 1
<= ((Computation s,8) . SBP ) + 1
by XREAL_1:8;
then A50:
j <= ((Computation s,8) . SBP ) + 1
by A49, XXREAL_0:2;
intpos j <> SBP
by A49, AMI_3:52;
then A51:
(Computation s,(m + 9)) . (intpos j) =
(Computation s,(m + 8)) . (intpos j)
by A37, SCMPDS_2:70
.=
(Computation (Computation s,8),m) . (intpos j)
by AMI_1:51
.=
(Computation s,8) . (intpos j)
by A35, A49, A50
;
pn + 1
< pn + 2
by XREAL_1:8;
then A52:
intpos j <> DataLoc ((Computation s,(m + 9)) . SBP ),2
by A48, A49, AMI_3:52;
(Computation s,7) . (intpos j) = s . (intpos j)
by A13, A14, A16, A21, A23, A49, Lm5, NAT_1:5;
hence s . (intpos j) =
(Computation s,8) . (intpos j)
by A24, SCMPDS_2:66
.=
(Computation s,n) . (intpos j)
by A44, A51, A52, SCMPDS_2:59
;
:: thesis: verum
end;
end; end; end; hence
S1[
k + 1]
;
:: thesis: verum end;
A53:
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A10, A11);
let s be State of SCMPDS ; :: thesis: ( GCD-Algorithm c= s & IC s = inspos 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) implies ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & s . SBP = (Computation s,n) . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) ) )
assume A54:
( GCD-Algorithm c= s & IC s = inspos 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) )
; :: thesis: ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & s . SBP = (Computation s,n) . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )
then reconsider m = s . (DataLoc (s . SBP ),3) as Element of NAT by INT_1:16;
S1[m]
by A53;
hence
ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & s . SBP = (Computation s,n) . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )
by A54; :: thesis: verum