defpred S1[ object ] means ( $1 in F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & $1 = q ^ r ) );
consider T being set such that
A1:
for x being object holds
( x in T iff ( x in NAT * & S1[x] ) )
from XBOOLE_0:sch 1();
set t = the Element of F1();
the Element of F1() in NAT *
by FINSEQ_1:def 11;
then reconsider T = T as non empty set by A1;
T is Tree-like
proof
thus
T c= NAT *
by A1;
TREES_1:def 3 ( ( 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 set holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T ) ) )
thus
for
p being
FinSequence of
NAT st
p in T holds
ProperPrefixes p c= T
for b1 being FinSequence of NAT
for b2, b3 being set holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T )proof
let p be
FinSequence of
NAT ;
( p in T implies ProperPrefixes p c= T )
assume A2:
p in T
;
ProperPrefixes p c= T
let x be
object ;
TARSKI:def 3 ( not x in ProperPrefixes p or x in T )
assume
x in ProperPrefixes p
;
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
;
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 F1() &
q in NAT * & (
q ^ r in F1() implies
q in F1() ) ) or ex
q being
Element of
F1() ex
r being
Element of
F2() st
(
P1[
q] &
p = q ^ r ) )
by A1, A2, A6, FINSEQ_1:def 11, TREES_1:21;
then consider q9 being
Element of
F1(),
r9 being
Element of
F2()
such that A7:
P1[
q9]
and A8:
q ^ r = q9 ^ r9
by A1, A3, A5, A6;
then consider s being
FinSequence such that 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
F2() )
by FINSEQ_1:def 11, TREES_1:21;
hence
contradiction
by A1, A3, A5, A7, A10;
verum
end;
let p be
FinSequence of
NAT ;
for b1, b2 being set holds
( not p ^ <*b1*> in T or not b2 <= b1 or p ^ <*b2*> in T )let k,
n be
Nat;
( 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
;
p ^ <*n*> in T
now ( not p ^ <*k*> in F1() implies p ^ <*n*> in T )assume A15:
not
p ^ <*k*> in F1()
;
p ^ <*n*> in Tthen consider q being
Element of
F1(),
r being
Element of
F2()
such that A16:
P1[
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 F2()
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;
verum end;
hence
p ^ <*n*> in T
by A13;
verum
end;
then reconsider T = T as Tree ;
take
T
; for p being FinSequence holds
( p in T iff ( p in F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & p = q ^ r ) ) )
let p be FinSequence; ( p in T iff ( p in F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & p = q ^ r ) ) )
( ( p is Element of F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & p = q ^ r ) ) implies p in NAT * )
by FINSEQ_1:def 11;
hence
( p in T iff ( p in F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & p = q ^ r ) ) )
by A1; verum