let n be Nat; :: thesis: for A being Subset of (n -xtuples_of NAT) st A is recursively_enumerable holds

A is diophantine

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

assume A is recursively_enumerable ; :: thesis: A is diophantine

then consider m being Nat, P being INT -valued Polynomial of ((2 + n) + m),F_Real such that

A1: 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 ) ) ;

set X = { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } ;

A2: A c= { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) }

for z being Element of NAT st z <= x holds

ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } c= A

for z being Element of NAT st z <= x holds

ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } = A by A2, XBOOLE_0:def 10;

hence A is diophantine by Th19; :: thesis: verum

A is diophantine

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

assume A is recursively_enumerable ; :: thesis: A is diophantine

then consider m being Nat, P being INT -valued Polynomial of ((2 + n) + m),F_Real such that

A1: 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 ) ) ;

set X = { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } ;

A2: A c= { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) }

proof

{ X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } )

assume A3: a in A ; :: thesis: a in { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) }

reconsider a = a as n -element XFinSequence of NAT by A3, HILB10_2:def 5;

consider x being Element of NAT such that

A4: 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%> ^ a) ^ Y))) = 0 ) by A3, A1;

for z being Element of NAT st z <= x holds

ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } ; :: 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } )

assume A3: a in A ; :: thesis: a in { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) }

reconsider a = a as n -element XFinSequence of NAT by A3, HILB10_2:def 5;

consider x being Element of NAT such that

A4: 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%> ^ a) ^ Y))) = 0 ) by A3, A1;

now :: thesis: for z being Element of NAT st z <= x holds

ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 )

hence
a in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 )

let z be Element of NAT ; :: thesis: ( z <= x implies ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 ) )

assume A5: z <= x ; :: thesis: ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 )

consider Y being m -element XFinSequence of NAT such that

A6: ( ( for i being object st i in dom Y holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 ) by A4, A5;

take Y = Y; :: thesis: ( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 )

len Y = m by CARD_1:def 7;

hence ( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 ) by A6; :: thesis: verum

end;( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 ) )

assume A5: z <= x ; :: thesis: ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 )

consider Y being m -element XFinSequence of NAT such that

A6: ( ( for i being object st i in dom Y holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 ) by A4, A5;

take Y = Y; :: thesis: ( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 )

len Y = m by CARD_1:def 7;

hence ( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 ) by A6; :: thesis: verum

for z being Element of NAT st z <= x holds

ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } ; :: thesis: verum

for z being Element of NAT st z <= x holds

ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } c= A

proof

then
{ X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } or b in A )

assume A7: b in { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } ; :: thesis: b in A

consider X being n -element XFinSequence of NAT such that

A8: ( b = X & 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) ) by A7;

consider x being Element of NAT such that

A9: for z being Element of NAT st z <= x holds

ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) by A8;

end;for z being Element of NAT st z <= x holds

ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } or b in A )

assume A7: b in { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } ; :: thesis: b in A

consider X being n -element XFinSequence of NAT such that

A8: ( b = X & 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 Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) ) by A7;

consider x being Element of NAT such that

A9: for z being Element of NAT st z <= x holds

ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) by A8;

now :: thesis: 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 )

hence
b in A
by A1, A8; :: thesis: verumex 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 )

let z be Element of NAT ; :: thesis: ( z <= x implies 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 ) )

assume A10: z <= x ; :: thesis: 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 )

consider Y being m -element XFinSequence of NAT such that

A11: ( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) by A9, A10;

take Y = Y; :: thesis: ( ( for i being object st i in dom Y holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 )

m = len Y by CARD_1:def 7;

hence ( ( for i being object st i in dom Y holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) by A11; :: thesis: verum

end;( ( for i being object st i in dom Y holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) )

assume A10: z <= x ; :: thesis: 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 )

consider Y being m -element XFinSequence of NAT such that

A11: ( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) by A9, A10;

take Y = Y; :: thesis: ( ( for i being object st i in dom Y holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 )

m = len Y by CARD_1:def 7;

hence ( ( for i being object st i in dom Y holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) by A11; :: thesis: verum

for z being Element of NAT st z <= x holds

ex Y being m -element XFinSequence of NAT st

( ( for i being Nat st i in m holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } = A by A2, XBOOLE_0:def 10;

hence A is diophantine by Th19; :: thesis: verum