let n be Nat; :: thesis: 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); :: thesis: ( A is diophantine implies A is recursively_enumerable )

assume A is diophantine ; :: thesis: 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 ; :: according to HILB10_5:def 4 :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 ) ) :: thesis: ( 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 )

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 ) ; :: thesis: 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; :: thesis: verum

A is recursively_enumerable

let A be Subset of (n -xtuples_of NAT); :: thesis: ( A is diophantine implies A is recursively_enumerable )

assume A is diophantine ; :: thesis: 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 ; :: according to HILB10_5:def 4 :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 ) ) :: thesis: ( 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

given a being Element of NAT such that A10:
for z being Element of NAT st z <= a holds
assume
X in A
; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( ( 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 :: thesis: eval (Q,(@ ((<%b,a%> ^ X) ^ y))) = 0

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; :: thesis: verum

end;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 ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( ( 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 :: thesis: eval (Q,(@ ((<%b,a%> ^ X) ^ y))) = 0

proof

reconsider A = @ (S ^ (x ^ y)) as Function of (0 + (n + m)),F_Real ;
let i be object ; :: thesis: ( i in dom y implies y . i <= a )

assume i in dom y ; :: thesis: y . i <= a

then y . i in rng y by FUNCT_1:def 3;

then y . i in R by XBOOLE_0:def 3;

hence y . i <= a by XXREAL_2:def 8; :: thesis: verum

end;assume i in dom y ; :: thesis: y . i <= a

then y . i in rng y by FUNCT_1:def 3;

then y . i in R by XBOOLE_0:def 3;

hence y . i <= a by XXREAL_2:def 8; :: thesis: verum

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; :: thesis: verum

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 ) ; :: thesis: 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; :: thesis: verum