let n be Nat; for A being Subset of (n -xtuples_of NAT) st A is diophantine holds
A is recursively_enumerable
let A be Subset of (n -xtuples_of NAT); ( A is diophantine implies A is recursively_enumerable )
assume
A is diophantine
; A is recursively_enumerable
then consider m being Nat, P being INT -valued Polynomial of (n + m),F_Real such that
A1:
for s being object holds
( s in A iff ex x being n -element XFinSequence of NAT ex y being m -element XFinSequence of NAT st
( s = x & eval (P,(@ (x ^ y))) = 0 ) )
by HILB10_2:def 6;
set nm = n + m;
reconsider P0 = P as INT -valued Polynomial of (0 + (n + m)),F_Real ;
consider q being Polynomial of ((0 + 2) + (n + m)),F_Real such that
A2:
rng q c= (rng P0) \/ {(0. F_Real)}
and
A3:
for XY being Function of (0 + (n + m)),F_Real
for XanyY being Function of ((0 + 2) + (n + m)),F_Real st XY | 0 = XanyY | 0 & (@ XY) /^ 0 = (@ XanyY) /^ (0 + 2) holds
eval (P0,XY) = eval (q,XanyY)
by HILB10_2:28;
A4:
rng P0 c= INT
by RELAT_1:def 19;
0. F_Real in INT
by INT_1:def 1;
then
{(0. F_Real)} c= INT
by ZFMISC_1:31;
then
(rng P0) \/ {(0. F_Real)} c= INT
by A4, XBOOLE_1:8;
then reconsider Q = q as INT -valued Polynomial of ((2 + n) + m),F_Real by RELAT_1:def 19, A2, XBOOLE_1:1;
take
m
; HILB10_5:def 4 ex P being INT -valued Polynomial of ((2 + n) + m),F_Real st
for X being n -element XFinSequence of NAT holds
( X in A iff ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) )
take
Q
; for X being n -element XFinSequence of NAT holds
( X in A iff ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (Q,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) )
let X be n -element XFinSequence of NAT ; ( X in A iff ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (Q,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) )
reconsider S = <*> INT as 0 -element XFinSequence of NAT ;
thus
( X in A implies ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (Q,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) )
( ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (Q,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) implies X in A )proof
assume
X in A
;
ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (Q,(@ ((<%z,x%> ^ X) ^ Y))) = 0 )
then consider x being
n -element XFinSequence of
NAT ,
y being
m -element XFinSequence of
NAT such that A5:
(
X = x &
eval (
P,
(@ (x ^ y)))
= 0 )
by A1;
reconsider R =
(rng y) \/ {0} as non
empty finite natural-membered set ;
reconsider a =
max R as
Element of
NAT by ORDINAL1:def 12;
take
a
;
for z being Element of NAT st z <= a holds
ex Y being m -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= a ) & eval (Q,(@ ((<%z,a%> ^ X) ^ Y))) = 0 )
let b be
Element of
NAT ;
( b <= a implies ex Y being m -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= a ) & eval (Q,(@ ((<%b,a%> ^ X) ^ Y))) = 0 ) )
assume
b <= a
;
ex Y being m -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= a ) & eval (Q,(@ ((<%b,a%> ^ X) ^ Y))) = 0 )
take
y
;
( ( for i being object st i in dom y holds
y . i <= a ) & eval (Q,(@ ((<%b,a%> ^ X) ^ y))) = 0 )
thus
for
i being
object st
i in dom y holds
y . i <= a
eval (Q,(@ ((<%b,a%> ^ X) ^ y))) = 0
reconsider A =
@ (S ^ (x ^ y)) as
Function of
(0 + (n + m)),
F_Real ;
reconsider B =
@ ((S ^ <%b,a%>) ^ (x ^ y)) as
Function of
((0 + 2) + (n + m)),
F_Real ;
reconsider R =
(rng y) \/ {0} as
finite ext-real-membered set ;
A6:
(
A | 0 = {} &
{} = B | 0 )
;
A7:
(
(@ A) /^ 0 = @ A &
@ A = A &
A = S ^ (x ^ y) )
by AFINSQ_2:10, HILB10_2:def 1, HILB10_2:def 2;
@ B = B
by HILB10_2:def 2;
then A8:
@ B = (S ^ <%b,a%>) ^ (x ^ y)
by HILB10_2:def 1;
len (S ^ <%b,a%>) = 0 + 2
by CARD_1:def 7;
then A9:
(@ A) /^ 0 = (@ B) /^ (0 + 2)
by A7, A8, AFINSQ_2:12;
B = @ ((<%b,a%> ^ x) ^ y)
by AFINSQ_1:27;
hence
eval (
Q,
(@ ((<%b,a%> ^ X) ^ y)))
= 0
by A5, A3, A6, A9;
verum
end;
given a being Element of NAT such that A10:
for z being Element of NAT st z <= a holds
ex y being m -element XFinSequence of NAT st
( ( for i being object st i in dom y holds
y . i <= a ) & eval (Q,(@ ((<%z,a%> ^ X) ^ y))) = 0 )
; X in A
consider y being m -element XFinSequence of NAT such that
A11:
( ( for i being object st i in dom y holds
y . i <= a ) & eval (Q,(@ ((<%a,a%> ^ X) ^ y))) = 0 )
by A10;
reconsider C = @ (S ^ (X ^ y)) as Function of (0 + (n + m)),F_Real ;
reconsider B = @ ((S ^ <%a,a%>) ^ (X ^ y)) as Function of ((0 + 2) + (n + m)),F_Real ;
A12:
( C | 0 = {} & {} = B | 0 )
;
A13:
( (@ C) /^ 0 = @ C & @ C = C & C = S ^ (X ^ y) )
by AFINSQ_2:10, HILB10_2:def 1, HILB10_2:def 2;
@ B = B
by HILB10_2:def 2;
then A14:
@ B = (S ^ <%a,a%>) ^ (X ^ y)
by HILB10_2:def 1;
len (S ^ <%a,a%>) = 0 + 2
by CARD_1:def 7;
then A15:
(@ C) /^ 0 = (@ B) /^ (0 + 2)
by A13, A14, AFINSQ_2:12;
A16:
B = @ ((<%a,a%> ^ X) ^ y)
by AFINSQ_1:27;
eval (P,(@ (X ^ y))) = 0
by A11, A16, A3, A12, A15;
hence
X in A
by A1; verum