defpred S1[ set ] means ( $1 = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & $1 = <*n*> ^ q ) );
consider T being set such that
A1: for y being set holds
( y in T iff ( y in NAT * & S1[y] ) ) from XBOOLE_0:sch 1();
 <*> NAT in NAT * by FINSEQ_1:def 11;
then reconsider T = T as non empty set by A1;
A2: rng p is constituted-Trees by B1, Def9;
A3: now :: thesis: for n being Element of NAT st n < len p holds
p . (n + 1) is Tree
let n be Element of NAT ; :: thesis: ( n < len p implies p . (n + 1) is Tree )
assume n < len p ; :: thesis: p . (n + 1) is Tree
then p . (n + 1) in rng p by Lm3;
hence p . (n + 1) is Tree by A2; :: thesis: verum
end;
T is Tree-like
proof
thus T c= NAT * :: according to TREES_1:def 3 :: thesis: ( ( for b1 being FinSequence of NAT holds
( not b1 in T or ProperPrefixes b1 c= T ) ) & ( for b1 being FinSequence of NAT
for b2, b3 being Element of NAT holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T ) ) )
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in T or y in NAT * )
thus ( not y in T or y in NAT * ) by A1; :: thesis: verum
end;
thus for w being FinSequence of NAT st w in T holds
ProperPrefixes w c= T :: thesis: for b1 being FinSequence of NAT
for b2, b3 being Element of NAT holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T )
proof
let w be FinSequence of NAT ; :: thesis: ( w in T implies ProperPrefixes w c= T )
assume A4: w in T ; :: thesis: ProperPrefixes w c= T
now :: thesis: ( w <> {} implies ProperPrefixes w c= T )
assume w <> {} ; :: thesis: ProperPrefixes w c= T
then consider n being Element of NAT , q being FinSequence such that
A5: n < len p and
A6: q in p . (n + 1) and
A7: w = <*n*> ^ q by A1, A4;
reconsider q = q as FinSequence of NAT by A7, FINSEQ_1:36;
thus ProperPrefixes w c= T :: thesis: verum
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes w or x in T )
assume x in ProperPrefixes w ; :: thesis: x in T
then consider r being FinSequence such that
A8: x = r and
A9: r is_a_proper_prefix_of w by TREES_1:def 2;
r is_a_prefix_of w by A9, XBOOLE_0:def 8;
then consider k being Element of NAT such that
A10: r = w | (Seg k) by TREES_1:def 1;
rng r = w .: (Seg k) by A10, RELAT_1:115;
then reconsider r = r as FinSequence of NAT by FINSEQ_1:def 4;
A11: r in NAT * by FINSEQ_1:def 11;
hence x in T by A1, A8, A11; :: thesis: verum
end;
end;
hence ProperPrefixes w c= T by TREES_1:15, XBOOLE_1:2; :: thesis: verum
end;
let w be FinSequence of NAT ; :: thesis: for b1, b2 being Element of NAT holds
( not w ^ <*b1*> in T or not b2 <= b1 or w ^ <*b2*> in T )
let k, n be Element of NAT ; :: thesis: ( not w ^ <*k*> in T or not n <= k or w ^ <*n*> in T )
assume that
A21: w ^ <*k*> in T and
A22: n <= k ; :: thesis: w ^ <*n*> in T
A23: now :: thesis: ( w = {} implies w ^ <*n*> in T )
assume A24: w = {} ; :: thesis: w ^ <*n*> in T
then <*k*> in T by A21, FINSEQ_1:34;
then consider m being Element of NAT , q being FinSequence such that
A25: m < len p and
q in p . (m + 1) and
A26: <*k*> = <*m*> ^ q by A1;
A27: <*k*> . 1 = k by FINSEQ_1:def 8;
(<*m*> ^ q) . 1 = m by FINSEQ_1:41;
then A28: n < len p by A22, A25, A26, A27, XXREAL_0:2;
then p . (n + 1) in rng p by Lm3;
then A29: {} in p . (n + 1) by A2, TREES_1:22;
A30: <*n*> ^ {} = <*n*> by FINSEQ_1:34;
A31: {} ^ <*n*> = <*n*> by FINSEQ_1:34;
<*n*> in NAT * by FINSEQ_1:def 11;
hence w ^ <*n*> in T by A1, A24, A28, A29, A30, A31; :: thesis: verum
end;
now :: thesis: ( w <> {} implies w ^ <*n*> in T )
assume w <> {} ; :: thesis: w ^ <*n*> in T
then consider q being FinSequence of NAT , m being Element of NAT such that
A32: w = <*m*> ^ q by FINSEQ_2:130;
consider m9 being Element of NAT , r being FinSequence such that
A33: m9 < len p and
A34: r in p . (m9 + 1) and
A35: w ^ <*k*> = <*m9*> ^ r by A1, A21;
A36: w ^ <*k*> = <*m*> ^ (q ^ <*k*>) by A32, FINSEQ_1:32;
A37: w ^ <*n*> = <*m*> ^ (q ^ <*n*>) by A32, FINSEQ_1:32;
A38: (w ^ <*k*>) . 1 = m by A36, FINSEQ_1:41;
A39: (w ^ <*k*>) . 1 = m9 by A35, FINSEQ_1:41;
A40: <*m*> ^ (q ^ <*n*>) in NAT * by FINSEQ_1:def 11;
A41: r = q ^ <*k*> by A35, A36, A38, A39, FINSEQ_1:33;
p . (m + 1) in rng p by A33, A38, A39, Lm3;
then q ^ <*n*> in p . (m + 1) by A2, A22, A34, A38, A39, A41, TREES_1:def 3;
hence w ^ <*n*> in T by A1, A33, A37, A38, A39, A40; :: thesis: verum
end;
hence w ^ <*n*> in T by A23; :: thesis: verum
end;
then reconsider T = T as Tree ;
take T ; :: thesis: for x being set holds
( x in T iff ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) )
let x be set ; :: thesis: ( x in T iff ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) )
thus ( not x in T or x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) by A1; :: thesis: ( ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) implies x in T )
assume A42: ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ; :: thesis: x in T
A43: now :: thesis: ( ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) implies x in NAT * )
given n being Element of NAT , q being FinSequence such that A44: n < len p and
A45: q in p . (n + 1) and
A46: x = <*n*> ^ q ; :: thesis: x in NAT *
reconsider T1 = p . (n + 1) as Tree by A3, A44;
reconsider q = q as Element of T1 by A45;
<*n*> ^ q in NAT * by FINSEQ_1:def 11;
hence x in NAT * by A46; :: thesis: verum
end;
{} in NAT * by FINSEQ_1:49;
hence x in T by A1, A42, A43; :: thesis: verum