defpred S1[ set ] 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 set holds
( x in T iff ( x in NAT * & S1[x] ) )
from XBOOLE_0:sch 1();
consider t being Element of F1();
A2:
t in NAT *
by FINSEQ_1:def 11;
reconsider T = T as non empty set by A1, A2;
A3:
T is Tree-like
proof
thus
T c= NAT *
TREES_1:def 5 ( ( 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 ) ) )
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 Element of NAT 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 A4:
p in T
;
ProperPrefixes p c= T
let x be
set ;
TARSKI:def 3 ( not x in ProperPrefixes p or x in T )
assume A5:
x in ProperPrefixes p
;
x in T
consider q being
FinSequence such that A6:
x = q
and A7:
q is_a_proper_prefix_of p
by A5, TREES_1:def 4;
assume A8:
not
x in T
;
contradiction
A9:
q is_a_prefix_of p
by A7, XBOOLE_0:def 8;
consider r being
FinSequence such that A10:
p = q ^ r
by A9, TREES_1:8;
reconsider q =
q,
r =
r as
FinSequence of
NAT by A10, FINSEQ_1:50;
A11:
( (
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, A4, A10, FINSEQ_1:def 11, TREES_1:46;
consider q9 being
Element of
F1(),
r9 being
Element of
F2()
such that A12:
P1[
q9]
and A13:
q ^ r = q9 ^ r9
by A1, A6, A8, A10, A11;
consider s being
FinSequence such that A19:
q9 ^ s = q
by A13, A14, FINSEQ_1:64;
reconsider s =
s as
FinSequence of
NAT by A19, FINSEQ_1:50;
A20:
q9 ^ r9 = q9 ^ (s ^ r)
by A13, A19, FINSEQ_1:45;
A21:
s ^ r = r9
by A20, FINSEQ_1:46;
A22:
(
q in NAT * &
s is
Element of
F2() )
by A21, FINSEQ_1:def 11, TREES_1:46;
thus
contradiction
by A1, A6, A8, A12, A19, A22;
verum
end;
let p be
FinSequence of
NAT ;
for b1, b2 being Element of NAT holds
( not p ^ <*b1*> in T or not b2 <= b1 or p ^ <*b2*> in T )let k,
n be
Element of
NAT ;
( not p ^ <*k*> in T or not n <= k or p ^ <*n*> in T )
assume that A23:
p ^ <*k*> in T
and A24:
n <= k
;
p ^ <*n*> in T
A29:
now assume A30:
not
p ^ <*k*> in F1()
;
p ^ <*n*> in Tconsider q being
Element of
F1(),
r being
Element of
F2()
such that A31:
P1[
q]
and A32:
p ^ <*k*> = q ^ r
by A1, A23, A30;
A33:
q ^ {} = q
by FINSEQ_1:47;
A34:
r <> {}
by A30, A32, A33;
consider w being
FinSequence,
z being
set such that A35:
r = w ^ <*z*>
by A34, FINSEQ_1:63;
reconsider w =
w as
FinSequence of
NAT by A35, FINSEQ_1:50;
A36:
p ^ <*k*> = (q ^ w) ^ <*z*>
by A32, A35, FINSEQ_1:45;
A37:
(
(p ^ <*k*>) . ((len p) + 1) = k &
((q ^ w) ^ <*z*>) . ((len (q ^ w)) + 1) = z )
by FINSEQ_1:59;
A38:
(
len <*k*> = 1 &
len <*z*> = 1 )
by FINSEQ_1:57;
A39:
(
len (p ^ <*k*>) = (len p) + (len <*k*>) &
len ((q ^ w) ^ <*z*>) = (len (q ^ w)) + (len <*z*>) )
by FINSEQ_1:35;
A40:
p = q ^ w
by A36, A37, A38, A39, FINSEQ_1:46;
A41:
w ^ <*n*> in F2()
by A24, A35, A36, A37, A38, A39, TREES_1:def 5;
A42:
p ^ <*n*> = q ^ (w ^ <*n*>)
by A40, FINSEQ_1:45;
A43:
p ^ <*n*> in NAT *
by FINSEQ_1:def 11;
thus
p ^ <*n*> in T
by A1, A31, A41, A42, A43;
verum end;
thus
p ^ <*n*> in T
by A25, A29;
verum
end;
reconsider T = T as Tree by A3;
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 ) ) )
A44:
( ( 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;
thus
( 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, A44; verum