defpred S_{1}[ object ] means ( $1 in F_{1}() or ex q being Element of F_{1}() ex r being Element of F_{2}() st

( P_{1}[q] & $1 = q ^ r ) );

consider T being set such that

A1: for x being object holds

( x in T iff ( x in NAT * & S_{1}[x] ) )
from XBOOLE_0:sch 1();

set t = the Element of F_{1}();

the Element of F_{1}() in NAT *
by FINSEQ_1:def 11;

then reconsider T = T as non empty set by A1;

T is Tree-like

take T ; :: thesis: for p being FinSequence holds

( p in T iff ( p in F_{1}() or ex q being Element of F_{1}() ex r being Element of F_{2}() st

( P_{1}[q] & p = q ^ r ) ) )

let p be FinSequence; :: thesis: ( p in T iff ( p in F_{1}() or ex q being Element of F_{1}() ex r being Element of F_{2}() st

( P_{1}[q] & p = q ^ r ) ) )

( ( p is Element of F_{1}() or ex q being Element of F_{1}() ex r being Element of F_{2}() st

( P_{1}[q] & p = q ^ r ) ) implies p in NAT * )
by FINSEQ_1:def 11;

hence ( p in T iff ( p in F_{1}() or ex q being Element of F_{1}() ex r being Element of F_{2}() st

( P_{1}[q] & p = q ^ r ) ) )
by A1; :: thesis: verum

( P

consider T being set such that

A1: for x being object holds

( x in T iff ( x in NAT * & S

set t = the Element of F

the Element of F

then reconsider T = T as non empty set by A1;

T is Tree-like

proof

then reconsider T = T as Tree ;
thus
T c= NAT *
by A1; :: according to TREES_1:def 3 :: thesis: ( ( for b_{1} being FinSequence of NAT holds

( not b_{1} in T or ProperPrefixes b_{1} c= T ) ) & ( for b_{1} being FinSequence of NAT

for b_{2}, b_{3} being set holds

( not b_{1} ^ <*b_{2}*> in T or not b_{3} <= b_{2} or b_{1} ^ <*b_{3}*> in T ) ) )

thus for p being FinSequence of NAT st p in T holds

ProperPrefixes p c= T :: thesis: for b_{1} being FinSequence of NAT

for b_{2}, b_{3} being set holds

( not b_{1} ^ <*b_{2}*> in T or not b_{3} <= b_{2} or b_{1} ^ <*b_{3}*> in T )_{1}, b_{2} being set holds

( not p ^ <*b_{1}*> in T or not b_{2} <= b_{1} or p ^ <*b_{2}*> in T )

let k, n be Nat; :: thesis: ( not p ^ <*k*> in T or not n <= k or p ^ <*n*> in T )

assume that

A11: p ^ <*k*> in T and

A12: n <= k ; :: thesis: p ^ <*n*> in T

end;( not b

for b

( not b

thus for p being FinSequence of NAT st p in T holds

ProperPrefixes p c= T :: thesis: for b

for b

( not b

proof

let p be FinSequence of NAT ; :: thesis: for b
let p be FinSequence of NAT ; :: thesis: ( p in T implies ProperPrefixes p c= T )

assume A2: p in T ; :: thesis: ProperPrefixes p c= T

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes p or x in T )

assume x in ProperPrefixes p ; :: thesis: x in T

then consider q being FinSequence such that

A3: x = q and

A4: q is_a_proper_prefix_of p by TREES_1:def 2;

assume A5: not x in T ; :: thesis: contradiction

q is_a_prefix_of p by A4, XBOOLE_0:def 8;

then consider r being FinSequence such that

A6: p = q ^ r by TREES_1:1;

reconsider q = q, r = r as FinSequence of NAT by A6, FINSEQ_1:36;

( ( q ^ r in F_{1}() & q in NAT * & ( q ^ r in F_{1}() implies q in F_{1}() ) ) or ex q being Element of F_{1}() ex r being Element of F_{2}() st

( P_{1}[q] & p = q ^ r ) )
by A1, A2, A6, FINSEQ_1:def 11, TREES_1:21;

then consider q9 being Element of F_{1}(), r9 being Element of F_{2}() such that

A7: P_{1}[q9]
and

A8: q ^ r = q9 ^ r9 by A1, A3, A5, A6;

A10: q9 ^ s = q by A8, FINSEQ_1:47;

reconsider s = s as FinSequence of NAT by A10, FINSEQ_1:36;

q9 ^ r9 = q9 ^ (s ^ r) by A8, A10, FINSEQ_1:32;

then s ^ r = r9 by FINSEQ_1:33;

then ( q in NAT * & s is Element of F_{2}() )
by FINSEQ_1:def 11, TREES_1:21;

hence contradiction by A1, A3, A5, A7, A10; :: thesis: verum

end;assume A2: p in T ; :: thesis: ProperPrefixes p c= T

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes p or x in T )

assume x in ProperPrefixes p ; :: thesis: x in T

then consider q being FinSequence such that

A3: x = q and

A4: q is_a_proper_prefix_of p by TREES_1:def 2;

assume A5: not x in T ; :: thesis: contradiction

q is_a_prefix_of p by A4, XBOOLE_0:def 8;

then consider r being FinSequence such that

A6: p = q ^ r by TREES_1:1;

reconsider q = q, r = r as FinSequence of NAT by A6, FINSEQ_1:36;

( ( q ^ r in F

( P

then consider q9 being Element of F

A7: P

A8: q ^ r = q9 ^ r9 by A1, A3, A5, A6;

now :: thesis: not len q <= len q9

then consider s being FinSequence such that assume
len q <= len q9
; :: thesis: contradiction

then ex s being FinSequence st q ^ s = q9 by A8, FINSEQ_1:47;

then A9: q in F_{1}()
by TREES_1:21;

q in NAT * by FINSEQ_1:def 11;

hence contradiction by A1, A3, A5, A9; :: thesis: verum

end;then ex s being FinSequence st q ^ s = q9 by A8, FINSEQ_1:47;

then A9: q in F

q in NAT * by FINSEQ_1:def 11;

hence contradiction by A1, A3, A5, A9; :: thesis: verum

A10: q9 ^ s = q by A8, FINSEQ_1:47;

reconsider s = s as FinSequence of NAT by A10, FINSEQ_1:36;

q9 ^ r9 = q9 ^ (s ^ r) by A8, A10, FINSEQ_1:32;

then s ^ r = r9 by FINSEQ_1:33;

then ( q in NAT * & s is Element of F

hence contradiction by A1, A3, A5, A7, A10; :: thesis: verum

( not p ^ <*b

let k, n be Nat; :: thesis: ( not p ^ <*k*> in T or not n <= k or p ^ <*n*> in T )

assume that

A11: p ^ <*k*> in T and

A12: n <= k ; :: thesis: p ^ <*n*> in T

A13: now :: thesis: ( p ^ <*k*> in F_{1}() implies p ^ <*n*> in T )

assume
p ^ <*k*> in F_{1}()
; :: thesis: p ^ <*n*> in T

then A14: p ^ <*n*> in F_{1}()
by A12, TREES_1:def 3;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

p ^ <*n*> in NAT * by FINSEQ_1:def 11;

hence p ^ <*n*> in T by A1, A14; :: thesis: verum

end;then A14: p ^ <*n*> in F

reconsider n = n as Element of NAT by ORDINAL1:def 12;

p ^ <*n*> in NAT * by FINSEQ_1:def 11;

hence p ^ <*n*> in T by A1, A14; :: thesis: verum

now :: thesis: ( not p ^ <*k*> in F_{1}() implies p ^ <*n*> in T )

hence
p ^ <*n*> in T
by A13; :: thesis: verumassume A15:
not p ^ <*k*> in F_{1}()
; :: thesis: p ^ <*n*> in T

then consider q being Element of F_{1}(), r being Element of F_{2}() such that

A16: P_{1}[q]
and

A17: p ^ <*k*> = q ^ r by A1, A11;

q ^ {} = q by FINSEQ_1:34;

then r <> {} by A15, A17;

then consider w being FinSequence, z being object such that

A18: r = w ^ <*z*> by FINSEQ_1:46;

reconsider w = w as FinSequence of NAT by A18, FINSEQ_1:36;

A19: p ^ <*k*> = (q ^ w) ^ <*z*> by A17, A18, FINSEQ_1:32;

A20: ( (p ^ <*k*>) . ((len p) + 1) = k & ((q ^ w) ^ <*z*>) . ((len (q ^ w)) + 1) = z ) by FINSEQ_1:42;

A21: ( len <*k*> = 1 & len <*z*> = 1 ) by FINSEQ_1:40;

A22: ( len (p ^ <*k*>) = (len p) + (len <*k*>) & len ((q ^ w) ^ <*z*>) = (len (q ^ w)) + (len <*z*>) ) by FINSEQ_1:22;

then A23: p = q ^ w by A19, A20, A21, FINSEQ_1:33;

A24: w ^ <*n*> in F_{2}()
by A12, A18, A19, A20, A21, A22, TREES_1:def 3;

A25: p ^ <*n*> = q ^ (w ^ <*n*>) by A23, FINSEQ_1:32;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

p ^ <*n*> in NAT * by FINSEQ_1:def 11;

hence p ^ <*n*> in T by A1, A16, A24, A25; :: thesis: verum

end;then consider q being Element of F

A16: P

A17: p ^ <*k*> = q ^ r by A1, A11;

q ^ {} = q by FINSEQ_1:34;

then r <> {} by A15, A17;

then consider w being FinSequence, z being object such that

A18: r = w ^ <*z*> by FINSEQ_1:46;

reconsider w = w as FinSequence of NAT by A18, FINSEQ_1:36;

A19: p ^ <*k*> = (q ^ w) ^ <*z*> by A17, A18, FINSEQ_1:32;

A20: ( (p ^ <*k*>) . ((len p) + 1) = k & ((q ^ w) ^ <*z*>) . ((len (q ^ w)) + 1) = z ) by FINSEQ_1:42;

A21: ( len <*k*> = 1 & len <*z*> = 1 ) by FINSEQ_1:40;

A22: ( len (p ^ <*k*>) = (len p) + (len <*k*>) & len ((q ^ w) ^ <*z*>) = (len (q ^ w)) + (len <*z*>) ) by FINSEQ_1:22;

then A23: p = q ^ w by A19, A20, A21, FINSEQ_1:33;

A24: w ^ <*n*> in F

A25: p ^ <*n*> = q ^ (w ^ <*n*>) by A23, FINSEQ_1:32;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

p ^ <*n*> in NAT * by FINSEQ_1:def 11;

hence p ^ <*n*> in T by A1, A16, A24, A25; :: thesis: verum

take T ; :: thesis: for p being FinSequence holds

( p in T iff ( p in F

( P

let p be FinSequence; :: thesis: ( p in T iff ( p in F

( P

( ( p is Element of F

( P

hence ( p in T iff ( p in F

( P