REAL is V77() V78() V79() V83() set
NAT is V6() non finite V37() V38() V77() V78() V79() V80() V81() V82() V83() Element of bool REAL
bool REAL is non empty set
NAT is V6() non finite V37() V38() V77() V78() V79() V80() V81() V82() V83() set
bool NAT is non empty non finite set
bool NAT is non empty non finite set
0 is empty V6() V8() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V47() V77() V78() V79() V80() V81() V82() V83() co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V98() V100() Element of NAT
{} is empty V6() V8() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V47() V77() V78() V79() V80() V81() V82() V83() co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V98() V100() set
1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
K201(NAT,0,1) is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
K201(NAT,0,1) ^omega is non empty functional set
bool (K201(NAT,0,1) ^omega) is non empty set
[:NAT,REAL:] is Relation-like set
bool [:NAT,REAL:] is non empty set
2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
3 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 {} is empty V6() V8() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V47() V77() V78() V79() V80() V81() V82() V83() co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V98() V100() set
proj2 {} is empty trivial V6() V8() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() V47() V77() V78() V79() V80() V81() V82() V83() co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V98() V100() set
x is set
<*x*> is non empty trivial Relation-like NAT -defined Function-like constant finite V39(1) FinSequence-like FinSubsequence-like set
X is V6() V10() V11() ext-real non negative finite V37() V100() set
X + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
E is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom E is V77() V78() V79() V80() V81() V82() Element of bool NAT
<*x*> ^ E is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*x*> ^ E) . (X + 1) is set
E . X is set
len <*x*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len <*x*>) + 0 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
(len <*x*>) + X is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom (<*x*> ^ E) is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
len (<*x*> ^ E) is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(X + 1) - (len <*x*>) is V11() ext-real V100() set
E . ((X + 1) - (len <*x*>)) is set
(X + 1) - 1 is V11() ext-real V100() set
E . ((X + 1) - 1) is set
1 - 1 is V11() ext-real V100() set
X + (1 - 1) is V11() ext-real V100() set
E . (X + (1 - 1)) is set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
E is set
<*E*> is non empty trivial Relation-like NAT -defined Function-like constant finite V39(1) FinSequence-like FinSubsequence-like set
X ^ <*E*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len X) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
len <*E*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len X) + (len <*E*>) is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
x is V6() V10() V11() ext-real non negative finite V37() V100() set
x + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom X is V77() V78() V79() V80() V81() V82() Element of bool NAT
len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
1 + 0 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
x is Relation-like set
X is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of x
E is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
F1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
E ^ F1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len E is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
F2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom E is V77() V78() V79() V80() V81() V82() Element of bool NAT
F2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
E . (F2 + 1) is set
(E ^ F1) . (F2 + 1) is set
len X is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom X is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
E . F2 is set
(E ^ F1) . F2 is set
[(E . F2),(E . (F2 + 1))] is V26() set
{(E . F2),(E . (F2 + 1))} is non empty set
{(E . F2)} is non empty trivial V39(1) set
{{(E . F2),(E . (F2 + 1))},{(E . F2)}} is non empty set
F2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom F1 is V77() V78() V79() V80() V81() V82() Element of bool NAT
F2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
(F2 + 1) + (len E) is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F2 + (len E) is V6() V10() V11() ext-real non negative finite V37() V100() set
F1 . (F2 + 1) is set
(len E) + (F2 + 1) is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
(E ^ F1) . ((len E) + (F2 + 1)) is set
(len E) + (len F1) is V6() V10() V11() ext-real non negative finite V37() V100() set
(len X) - (len F1) is V11() ext-real V100() set
((len X) - (len F1)) + (len F1) is V11() ext-real V100() set
(len E) + F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
((len E) + F2) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F1 . F2 is set
(E ^ F1) . ((len E) + F2) is set
[(F1 . F2),(F1 . (F2 + 1))] is V26() set
{(F1 . F2),(F1 . (F2 + 1))} is non empty set
{(F1 . F2)} is non empty trivial V39(1) set
{{(F1 . F2),(F1 . (F2 + 1))},{(F1 . F2)}} is non empty set
x is Relation-like set
X is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of x
len X is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
X . 1 is set
<*(X . 1)*> is non empty trivial Relation-like NAT -defined Function-like constant finite V39(1) FinSequence-like FinSubsequence-like set
E is set
<*E*> is non empty trivial Relation-like NAT -defined Function-like constant finite V39(1) FinSequence-like FinSubsequence-like set
F1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*E*> ^ F1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len F1) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
1 + (len F1) is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
1 + 0 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
len <*E*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
x is Relation-like set
X is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of x
len X is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
X . (len X) is set
<*(X . (len X))*> is non empty trivial Relation-like NAT -defined Function-like constant finite V39(1) FinSequence-like FinSubsequence-like set
E is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
F1 is set
<*F1*> is non empty trivial Relation-like NAT -defined Function-like constant finite V39(1) FinSequence-like FinSubsequence-like set
E ^ <*F1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len E is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len E) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
1 + (len E) is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
1 + 0 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
len <*F1*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
x is Relation-like set
X is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of x
len X is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
X . 1 is set
<*(X . 1)*> is non empty trivial Relation-like NAT -defined Function-like constant finite V39(1) FinSequence-like FinSubsequence-like set
E is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of x
<*(X . 1)*> ^ E is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len E is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len E) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom E is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
F1 is V6() V10() V11() ext-real non negative finite V37() V100() set
E . F1 is set
F1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
X . (F1 + 1) is set
x is set
X is set
<*x,X*> is non empty Relation-like NAT -defined Function-like finite V39(2) FinSequence-like FinSubsequence-like set
[x,X] is V26() set
{x,X} is non empty set
{x} is non empty trivial V39(1) set
{{x,X},{x}} is non empty set
E is Relation-like set
<*x,X*> . 1 is set
<*x,X*> . 2 is set
len <*x,X*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom <*x,X*> is non empty V39(2) V77() V78() V79() V80() V81() V82() Element of bool NAT
1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
x is non empty set
x ^omega is non empty functional set
X is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 X is V6() V10() V11() ext-real non negative finite V37() V100() set
E is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
len E is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 E is V6() V10() V11() ext-real non negative finite V37() V100() set
F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
E ^ F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
K266(x) is non empty functional M12(x)
len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set
(len E) + (len F1) is V6() V10() V11() ext-real non negative finite V37() V100() set
((len E) + (len F1)) + 0 is V6() V10() V11() ext-real non negative finite V37() V100() set
(len X) + (len E) is V6() V10() V11() ext-real non negative finite V37() V100() set
(len X) + (len F1) is V6() V10() V11() ext-real non negative finite V37() V100() set
x is non empty set
x ^omega is non empty functional set
<%> x is empty V6() V8() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined x -valued Function-like one-to-one constant functional finite V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V47() V77() V78() V79() V80() V81() V82() V83() co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V98() V100() Element of K266(x)
K266(x) is non empty functional M12(x)
X is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 X is V6() V10() V11() ext-real non negative finite V37() V100() set
E is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
len E is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 E is V6() V10() V11() ext-real non negative finite V37() V100() set
F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
E ^ F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set
(len E) + (len F1) is V6() V10() V11() ext-real non negative finite V37() V100() set
(len X) + (len E) is V6() V10() V11() ext-real non negative finite V37() V100() set
((len E) + (len F1)) + 0 is V6() V10() V11() ext-real non negative finite V37() V100() set
x is non empty set
x ^omega is non empty functional set
X is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 X is V6() V10() V11() ext-real non negative finite V37() V100() set
E is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
X ^ E is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
K266(x) is non empty functional M12(x)
len E is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 E is V6() V10() V11() ext-real non negative finite V37() V100() set
F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
F1 ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
len F2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
(len X) + (len E) is V6() V10() V11() ext-real non negative finite V37() V100() set
len (F1 ^ F2) is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 (F1 ^ F2) is V6() V10() V11() ext-real non negative finite V37() V100() set
(len F1) + (len F2) is V6() V10() V11() ext-real non negative finite V37() V100() set
TS1 is V6() V10() V11() ext-real non negative finite V37() V100() set
dom X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of bool NAT
X . TS1 is set
(F1 ^ F2) . TS1 is set
F1 . TS1 is set
x is non empty set
x ^omega is non empty functional set
X is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 X is V6() V10() V11() ext-real non negative finite V37() V100() set
E is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
X ^ E is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
K266(x) is non empty functional M12(x)
len E is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 E is V6() V10() V11() ext-real non negative finite V37() V100() set
F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
F1 ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
len F2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
(len X) + (len E) is V6() V10() V11() ext-real non negative finite V37() V100() set
len (F1 ^ F2) is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 (F1 ^ F2) is V6() V10() V11() ext-real non negative finite V37() V100() set
(len F1) + (len F2) is V6() V10() V11() ext-real non negative finite V37() V100() set
((len X) + (len E)) - (len E) is V11() ext-real V100() set
((len F1) + (len F2)) - (len F2) is V11() ext-real V100() set
TS1 is V8() Relation-like NAT -defined Function-like finite V98() set
X ^ TS1 is V8() Relation-like NAT -defined Function-like finite V98() set
TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
X ^ TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
TS2 ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
X ^ (TS2 ^ F2) is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
x is non empty set
x ^omega is non empty functional set
X is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
E is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
X ^ E is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
K266(x) is non empty functional M12(x)
F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
F1 ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set
len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 X is V6() V10() V11() ext-real non negative finite V37() V100() set
x is non empty set
x ^omega is non empty functional set
bool (x ^omega) is non empty set
X is functional Element of bool (x ^omega)
x is non empty set
x ^omega is non empty functional set
bool (x ^omega) is non empty set
X is functional Element of bool (x ^omega)
E is (X)
the of E is Relation-like [: the carrier of E,X:] -defined the carrier of E -valued Element of bool [:[: the carrier of E,X:], the carrier of E:]
the carrier of E is set
[: the carrier of E,X:] is Relation-like set
[:[: the carrier of E,X:], the carrier of E:] is Relation-like set
bool [:[: the carrier of E,X:], the carrier of E:] is non empty set
proj1 the of E is Relation-like set
F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
F1 is Element of the carrier of E
[F1,F2] is V26() set
{F1,F2} is non empty set
{F1} is non empty trivial V39(1) set
{{F1,F2},{F1}} is non empty set
[F1,TS1] is V26() set
{F1,TS1} is non empty set
{{F1,TS1},{F1}} is non empty set
TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
F2 ^ TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
K266(x) is non empty functional M12(x)
y is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
TS1 ^ y is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
x is non empty set
x ^omega is non empty functional set
bool (x ^omega) is non empty set
X is functional Element of bool (x ^omega)
the non empty finite set is non empty finite set
[: the non empty finite set ,X:] is Relation-like set
[:[: the non empty finite set ,X:], the non empty finite set :] is Relation-like set
bool [:[: the non empty finite set ,X:], the non empty finite set :] is non empty set
F1 is Relation-like [: the non empty finite set ,X:] -defined the non empty finite set -valued Element of bool [:[: the non empty finite set ,X:], the non empty finite set :]
(X, the non empty finite set ,F1) is (X) (X)
F2 is (X) (X)
the carrier of F2 is set
x is set
x is set
X is set
E is set
F1 is set
F2 is (x)
the of F2 is Relation-like [: the carrier of F2,x:] -defined the carrier of F2 -valued Element of bool [:[: the carrier of F2,x:], the carrier of F2:]
the carrier of F2 is set
[: the carrier of F2,x:] is Relation-like set
[:[: the carrier of F2,x:], the carrier of F2:] is Relation-like set
bool [:[: the carrier of F2,x:], the carrier of F2:] is non empty set
proj1 the of F2 is Relation-like set
proj1 (proj1 the of F2) is set
proj2 (proj1 the of F2) is set
proj2 the of F2 is set
[X,E] is V26() set
{X,E} is non empty set
{X} is non empty trivial V39(1) set
{{X,E},{X}} is non empty set
[[X,E],F1] is V26() set
{[X,E],F1} is non empty set
{[X,E]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[X,E],F1},{[X,E]}} is non empty set
x is set
X is set
E is set
F1 is set
F2 is set
TS1 is (x)
the of TS1 is Relation-like [: the carrier of TS1,x:] -defined the carrier of TS1 -valued Element of bool [:[: the carrier of TS1,x:], the carrier of TS1:]
the carrier of TS1 is set
[: the carrier of TS1,x:] is Relation-like set
[:[: the carrier of TS1,x:], the carrier of TS1:] is Relation-like set
bool [:[: the carrier of TS1,x:], the carrier of TS1:] is non empty set
TS2 is (X)
the of TS2 is Relation-like [: the carrier of TS2,X:] -defined the carrier of TS2 -valued Element of bool [:[: the carrier of TS2,X:], the carrier of TS2:]
the carrier of TS2 is set
[: the carrier of TS2,X:] is Relation-like set
[:[: the carrier of TS2,X:], the carrier of TS2:] is Relation-like set
bool [:[: the carrier of TS2,X:], the carrier of TS2:] is non empty set
[E,F1] is V26() set
{E,F1} is non empty set
{E} is non empty trivial V39(1) set
{{E,F1},{E}} is non empty set
[[E,F1],F2] is V26() set
{[E,F1],F2} is non empty set
{[E,F1]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[E,F1],F2},{[E,F1]}} is non empty set
x is set
X is set
E is set
F1 is set
F2 is non empty set
F2 ^omega is non empty functional set
bool (F2 ^omega) is non empty set
TS1 is functional Element of bool (F2 ^omega)
TS2 is (TS1)
the of TS2 is Relation-like [: the carrier of TS2,TS1:] -defined the carrier of TS2 -valued Element of bool [:[: the carrier of TS2,TS1:], the carrier of TS2:]
the carrier of TS2 is set
[: the carrier of TS2,TS1:] is Relation-like set
[:[: the carrier of TS2,TS1:], the carrier of TS2:] is Relation-like set
bool [:[: the carrier of TS2,TS1:], the carrier of TS2:] is non empty set
[x,X] is V26() set
{x,X} is non empty set
{x} is non empty trivial V39(1) set
{{x,X},{x}} is non empty set
[[x,X],E] is V26() set
{[x,X],E} is non empty set
{[x,X]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,X],E},{[x,X]}} is non empty set
[[x,X],F1] is V26() set
{[x,X],F1} is non empty set
{{[x,X],F1},{[x,X]}} is non empty set
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined E -valued Function-like one-to-one constant functional finite V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V47() V77() V78() V79() V80() V81() V82() V83() co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V98() V100() Element of K266(E)
K266(E) is non empty functional M12(E)
F1 is functional Element of bool (E ^omega)
F2 is (F1)
the of F2 is Relation-like [: the carrier of F2,F1:] -defined the carrier of F2 -valued Element of bool [:[: the carrier of F2,F1:], the carrier of F2:]
the carrier of F2 is set
[: the carrier of F2,F1:] is Relation-like set
[:[: the carrier of F2,F1:], the carrier of F2:] is Relation-like set
bool [:[: the carrier of F2,F1:], the carrier of F2:] is non empty set
proj1 the of F2 is Relation-like set
proj2 (proj1 the of F2) is set
[x,(<%> E)] is V26() set
{x,(<%> E)} is non empty set
{x} is non empty trivial V39(1) set
{{x,(<%> E)},{x}} is non empty set
[[x,(<%> E)],X] is V26() set
{[x,(<%> E)],X} is non empty set
{[x,(<%> E)]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,(<%> E)],X},{[x,(<%> E)]}} is non empty set
x is set
X is set
E is set
F1 is non empty set
F1 ^omega is non empty functional set
bool (F1 ^omega) is non empty set
F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^omega
TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^omega
TS2 is functional Element of bool (F1 ^omega)
y is (F1,TS2) (TS2)
the carrier of y is set
q is Element of the carrier of y
[q,TS1] is V26() set
{q,TS1} is non empty set
{q} is non empty trivial V39(1) set
{{q,TS1},{q}} is non empty set
[[q,TS1],E] is V26() set
{[q,TS1],E} is non empty set
{[q,TS1]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[q,TS1],E},{[q,TS1]}} is non empty set
the of y is Relation-like [: the carrier of y,TS2:] -defined the carrier of y -valued Element of bool [:[: the carrier of y,TS2:], the carrier of y:]
[: the carrier of y,TS2:] is Relation-like set
[:[: the carrier of y,TS2:], the carrier of y:] is Relation-like set
bool [:[: the carrier of y,TS2:], the carrier of y:] is non empty set
proj1 the of y is Relation-like set
[q,F2] is V26() set
{q,F2} is non empty set
{{q,F2},{q}} is non empty set
[[q,F2],X] is V26() set
{[q,F2],X} is non empty set
{[q,F2]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[q,F2],X},{[q,F2]}} is non empty set
p is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^omega
F2 ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(F1)
K266(F1) is non empty functional M12(F1)
q is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^omega
TS1 ^ q is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(F1)
x is non empty set
x ^omega is non empty functional set
bool (x ^omega) is non empty set
X is functional Element of bool (x ^omega)
x is set
X is set
E is set
F1 is set
F2 is non empty set
F2 ^omega is non empty functional set
bool (F2 ^omega) is non empty set
TS1 is functional Element of bool (F2 ^omega)
TS2 is (TS1)
the of TS2 is Relation-like [: the carrier of TS2,TS1:] -defined the carrier of TS2 -valued Element of bool [:[: the carrier of TS2,TS1:], the carrier of TS2:]
the carrier of TS2 is set
[: the carrier of TS2,TS1:] is Relation-like set
[:[: the carrier of TS2,TS1:], the carrier of TS2:] is Relation-like set
bool [:[: the carrier of TS2,TS1:], the carrier of TS2:] is non empty set
proj1 the of TS2 is Relation-like set
proj1 (proj1 the of TS2) is set
proj2 the of TS2 is set
y is V8() Relation-like NAT -defined Function-like finite V98() Element of F2 ^omega
q is V8() Relation-like NAT -defined Function-like finite V98() Element of F2 ^omega
q ^ y is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(F2)
K266(F2) is non empty functional M12(F2)
x is set
X is set
E is set
F1 is set
F2 is non empty set
F2 ^omega is non empty functional set
bool (F2 ^omega) is non empty set
TS1 is functional Element of bool (F2 ^omega)
TS2 is functional Element of bool (F2 ^omega)
y is (TS1)
the of y is Relation-like [: the carrier of y,TS1:] -defined the carrier of y -valued Element of bool [:[: the carrier of y,TS1:], the carrier of y:]
the carrier of y is set
[: the carrier of y,TS1:] is Relation-like set
[:[: the carrier of y,TS1:], the carrier of y:] is Relation-like set
bool [:[: the carrier of y,TS1:], the carrier of y:] is non empty set
q is (TS2)
the of q is Relation-like [: the carrier of q,TS2:] -defined the carrier of q -valued Element of bool [:[: the carrier of q,TS2:], the carrier of q:]
the carrier of q is set
[: the carrier of q,TS2:] is Relation-like set
[:[: the carrier of q,TS2:], the carrier of q:] is Relation-like set
bool [:[: the carrier of q,TS2:], the carrier of q:] is non empty set
p is V8() Relation-like NAT -defined Function-like finite V98() Element of F2 ^omega
q is V8() Relation-like NAT -defined Function-like finite V98() Element of F2 ^omega
q ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(F2)
K266(F2) is non empty functional M12(F2)
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
TS1 is functional Element of bool (E ^omega)
TS2 is (TS1)
y is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
q is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
q ^ y is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
K266(E) is non empty functional M12(E)
q ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
x is set
X is set
E is set
F1 is non empty set
F1 ^omega is non empty functional set
bool (F1 ^omega) is non empty set
<%> F1 is empty V6() V8() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined F1 -valued Function-like one-to-one constant functional finite V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V47() V77() V78() V79() V80() V81() V82() V83() co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V98() V100() Element of K266(F1)
K266(F1) is non empty functional M12(F1)
F2 is functional Element of bool (F1 ^omega)
TS1 is (F2)
TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^omega
TS2 ^ {} is V8() Relation-like NAT -defined Function-like finite V98() set
TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^omega
TS2 ^ {} is V8() Relation-like NAT -defined Function-like finite V98() set
TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^omega
y is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^omega
y ^ TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(F1)
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
F1 ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
K266(E) is non empty functional M12(E)
TS1 is functional Element of bool (E ^omega)
TS2 is (TS1)
y is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
y ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
F1 ^ TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
K266(E) is non empty functional M12(E)
F2 ^ TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
TS2 is functional Element of bool (E ^omega)
y is (TS2)
q is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
q ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
q ^ (F2 ^ TS1) is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
len F2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
TS1 is functional Element of bool (E ^omega)
TS2 is (TS1)
y is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
y ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
K266(E) is non empty functional M12(E)
x is set
X is set
E is set
F1 is set
F2 is set
TS1 is non empty set
TS1 ^omega is non empty functional set
bool (TS1 ^omega) is non empty set
TS2 is functional Element of bool (TS1 ^omega)
y is (TS2)
the of y is Relation-like [: the carrier of y,TS2:] -defined the carrier of y -valued Element of bool [:[: the carrier of y,TS2:], the carrier of y:]
the carrier of y is set
[: the carrier of y,TS2:] is Relation-like set
[:[: the carrier of y,TS2:], the carrier of y:] is Relation-like set
bool [:[: the carrier of y,TS2:], the carrier of y:] is non empty set
q is V8() Relation-like NAT -defined Function-like finite V98() Element of TS1 ^omega
p is V8() Relation-like NAT -defined Function-like finite V98() Element of TS1 ^omega
p ^ q is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS1)
K266(TS1) is non empty functional M12(TS1)
q is V8() Relation-like NAT -defined Function-like finite V98() Element of TS1 ^omega
p is V8() Relation-like NAT -defined Function-like finite V98() Element of TS1 ^omega
p ^ q is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS1)
x is set
X is set
E is set
F1 is non empty set
F1 ^omega is non empty functional set
bool (F1 ^omega) is non empty set
<%> F1 is empty V6() V8() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined F1 -valued Function-like one-to-one constant functional finite V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V47() V77() V78() V79() V80() V81() V82() V83() co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V98() V100() Element of K266(F1)
K266(F1) is non empty functional M12(F1)
F2 is functional Element of bool (F1 ^omega)
TS1 is (F2)
the of TS1 is Relation-like [: the carrier of TS1,F2:] -defined the carrier of TS1 -valued Element of bool [:[: the carrier of TS1,F2:], the carrier of TS1:]
the carrier of TS1 is set
[: the carrier of TS1,F2:] is Relation-like set
[:[: the carrier of TS1,F2:], the carrier of TS1:] is Relation-like set
bool [:[: the carrier of TS1,F2:], the carrier of TS1:] is non empty set
proj1 the of TS1 is Relation-like set
proj2 (proj1 the of TS1) is set
TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^omega
y is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^omega
y ^ TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(F1)
[x,y] is V26() set
{x,y} is non empty set
{x} is non empty trivial V39(1) set
{{x,y},{x}} is non empty set
[[x,y],E] is V26() set
{[x,y],E} is non empty set
{[x,y]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,y],E},{[x,y]}} is non empty set
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined E -valued Function-like one-to-one constant functional finite V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V47() V77() V78() V79() V80() V81() V82() V83() co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V98() V100() Element of K266(E)
K266(E) is non empty functional M12(E)
F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
len F2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
TS1 is functional Element of bool (E ^omega)
TS2 is (TS1)
the of TS2 is Relation-like [: the carrier of TS2,TS1:] -defined the carrier of TS2 -valued Element of bool [:[: the carrier of TS2,TS1:], the carrier of TS2:]
the carrier of TS2 is set
[: the carrier of TS2,TS1:] is Relation-like set
[:[: the carrier of TS2,TS1:], the carrier of TS2:] is Relation-like set
bool [:[: the carrier of TS2,TS1:], the carrier of TS2:] is non empty set
proj1 the of TS2 is Relation-like set
proj2 (proj1 the of TS2) is set
y is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
y ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
x is set
X is set
E is set
F1 is set
F2 is set
TS1 is set
TS2 is non empty set
TS2 ^omega is non empty functional set
bool (TS2 ^omega) is non empty set
y is functional Element of bool (TS2 ^omega)
q is (TS2,y) (y)
p is V8() Relation-like NAT -defined Function-like finite V98() Element of TS2 ^omega
q is V8() Relation-like NAT -defined Function-like finite V98() Element of TS2 ^omega
q ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS2)
K266(TS2) is non empty functional M12(TS2)
p is V8() Relation-like NAT -defined Function-like finite V98() Element of TS2 ^omega
v is V8() Relation-like NAT -defined Function-like finite V98() Element of TS2 ^omega
v ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS2)
the of q is Relation-like [: the carrier of q,y:] -defined the carrier of q -valued Element of bool [:[: the carrier of q,y:], the carrier of q:]
the carrier of q is set
[: the carrier of q,y:] is Relation-like set
[:[: the carrier of q,y:], the carrier of q:] is Relation-like set
bool [:[: the carrier of q,y:], the carrier of q:] is non empty set
v is V8() Relation-like NAT -defined Function-like finite V98() Element of TS2 ^omega
v ^ v is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS2)
v ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS2)
l is V8() Relation-like NAT -defined Function-like finite V98() Element of TS2 ^omega
q ^ l is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS2)
l ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS2)
x is non empty set
x ^omega is non empty functional set
bool (x ^omega) is non empty set
X is functional Element of bool (x ^omega)
E is non empty (X)
the carrier of E is non empty set
[: the carrier of E,(x ^omega):] is non empty Relation-like set
[:[: the carrier of E,(x ^omega):],[: the carrier of E,(x ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of E,(x ^omega):],[: the carrier of E,(x ^omega):]:] is non empty set
F1 is Relation-like [: the carrier of E,(x ^omega):] -defined [: the carrier of E,(x ^omega):] -valued Element of bool [:[: the carrier of E,(x ^omega):],[: the carrier of E,(x ^omega):]:]
F2 is set
TS1 is set
[F2,TS1] is V26() set
{F2,TS1} is non empty set
{F2} is non empty trivial V39(1) set
{{F2,TS1},{F2}} is non empty set
TS2 is set
y is set
[TS2,y] is V26() set
{TS2,y} is non empty set
{TS2} is non empty trivial V39(1) set
{{TS2,y},{TS2}} is non empty set
proj1 F1 is Relation-like set
proj2 F1 is Relation-like set
[[F2,TS1],[TS2,y]] is V26() set
{[F2,TS1],[TS2,y]} is non empty Relation-like set
{[F2,TS1]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[F2,TS1],[TS2,y]},{[F2,TS1]}} is non empty set
q is set
p is set
[q,p] is V26() set
{q,p} is non empty set
{q} is non empty trivial V39(1) set
{{q,p},{q}} is non empty set
v is set
v is set
[v,v] is V26() set
{v,v} is non empty set
{v} is non empty trivial V39(1) set
{{v,v},{v}} is non empty set
F2 is set
TS1 is set
[F2,TS1] is V26() set
{F2,TS1} is non empty set
{F2} is non empty trivial V39(1) set
{{F2,TS1},{F2}} is non empty set
TS2 is set
y is set
[TS2,y] is V26() set
{TS2,y} is non empty set
{TS2} is non empty trivial V39(1) set
{{TS2,y},{TS2}} is non empty set
[[F2,TS1],[TS2,y]] is V26() set
{[F2,TS1],[TS2,y]} is non empty Relation-like set
{[F2,TS1]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[F2,TS1],[TS2,y]},{[F2,TS1]}} is non empty set
q is set
p is set
q is set
p is set
[q,p] is V26() set
{q,p} is non empty set
{q} is non empty trivial V39(1) set
{{q,p},{q}} is non empty set
[q,p] is V26() set
{q,p} is non empty set
{q} is non empty trivial V39(1) set
{{q,p},{q}} is non empty set
[[q,p],[q,p]] is V26() set
{[q,p],[q,p]} is non empty Relation-like set
{[q,p]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[q,p],[q,p]},{[q,p]}} is non empty set
F1 is Relation-like [: the carrier of E,(x ^omega):] -defined [: the carrier of E,(x ^omega):] -valued Element of bool [:[: the carrier of E,(x ^omega):],[: the carrier of E,(x ^omega):]:]
F2 is Relation-like [: the carrier of E,(x ^omega):] -defined [: the carrier of E,(x ^omega):] -valued Element of bool [:[: the carrier of E,(x ^omega):],[: the carrier of E,(x ^omega):]:]
TS1 is Element of [: the carrier of E,(x ^omega):]
y is set
q is set
[y,q] is V26() set
{y,q} is non empty set
{y} is non empty trivial V39(1) set
{{y,q},{y}} is non empty set
TS2 is Element of [: the carrier of E,(x ^omega):]
p is set
v is set
[p,v] is V26() set
{p,v} is non empty set
{p} is non empty trivial V39(1) set
{{p,v},{p}} is non empty set
[TS1,TS2] is V26() set
{TS1,TS2} is non empty set
{TS1} is non empty trivial V39(1) set
{{TS1,TS2},{TS1}} is non empty set
q is Element of the carrier of E
p is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
l is Element of the carrier of E
v is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
x is set
X is set
[x,X] is V26() set
{x,X} is non empty set
{x} is non empty trivial V39(1) set
{{x,X},{x}} is non empty set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
F1 is functional Element of bool (E ^omega)
F2 is non empty (F1)
(E,F1,F2) is Relation-like [: the carrier of F2,(E ^omega):] -defined [: the carrier of F2,(E ^omega):] -valued Element of bool [:[: the carrier of F2,(E ^omega):],[: the carrier of F2,(E ^omega):]:]
the carrier of F2 is non empty set
[: the carrier of F2,(E ^omega):] is non empty Relation-like set
[:[: the carrier of F2,(E ^omega):],[: the carrier of F2,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of F2,(E ^omega):],[: the carrier of F2,(E ^omega):]:] is non empty set
TS1 is set
TS2 is set
[TS1,TS2] is V26() set
{TS1,TS2} is non empty set
{TS1} is non empty trivial V39(1) set
{{TS1,TS2},{TS1}} is non empty set
y is set
q is set
[y,q] is V26() set
{y,q} is non empty set
{y} is non empty trivial V39(1) set
{{y,q},{y}} is non empty set
x is set
X is set
[x,X] is V26() set
{x,X} is non empty set
{x} is non empty trivial V39(1) set
{{x,X},{x}} is non empty set
E is set
F1 is set
[E,F1] is V26() set
{E,F1} is non empty set
{E} is non empty trivial V39(1) set
{{E,F1},{E}} is non empty set
[[x,X],[E,F1]] is V26() set
{[x,X],[E,F1]} is non empty Relation-like set
{[x,X]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,X],[E,F1]},{[x,X]}} is non empty set
F2 is non empty set
F2 ^omega is non empty functional set
bool (F2 ^omega) is non empty set
TS1 is functional Element of bool (F2 ^omega)
TS2 is non empty (TS1)
(F2,TS1,TS2) is Relation-like [: the carrier of TS2,(F2 ^omega):] -defined [: the carrier of TS2,(F2 ^omega):] -valued Element of bool [:[: the carrier of TS2,(F2 ^omega):],[: the carrier of TS2,(F2 ^omega):]:]
the carrier of TS2 is non empty set
[: the carrier of TS2,(F2 ^omega):] is non empty Relation-like set
[:[: the carrier of TS2,(F2 ^omega):],[: the carrier of TS2,(F2 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS2,(F2 ^omega):],[: the carrier of TS2,(F2 ^omega):]:] is non empty set
the of TS2 is Relation-like [: the carrier of TS2,TS1:] -defined the carrier of TS2 -valued Element of bool [:[: the carrier of TS2,TS1:], the carrier of TS2:]
[: the carrier of TS2,TS1:] is Relation-like set
[:[: the carrier of TS2,TS1:], the carrier of TS2:] is Relation-like set
bool [:[: the carrier of TS2,TS1:], the carrier of TS2:] is non empty set
proj1 the of TS2 is Relation-like set
proj1 (proj1 the of TS2) is set
proj2 the of TS2 is set
x is set
X is non empty set
X ^omega is non empty functional set
bool (X ^omega) is non empty set
E is functional Element of bool (X ^omega)
F1 is non empty (E)
(X,E,F1) is Relation-like [: the carrier of F1,(X ^omega):] -defined [: the carrier of F1,(X ^omega):] -valued Element of bool [:[: the carrier of F1,(X ^omega):],[: the carrier of F1,(X ^omega):]:]
the carrier of F1 is non empty set
[: the carrier of F1,(X ^omega):] is non empty Relation-like set
[:[: the carrier of F1,(X ^omega):],[: the carrier of F1,(X ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of F1,(X ^omega):],[: the carrier of F1,(X ^omega):]:] is non empty set
F2 is set
TS1 is set
[F2,TS1] is V26() set
{F2,TS1} is non empty set
{F2} is non empty trivial V39(1) set
{{F2,TS1},{F2}} is non empty set
TS2 is Element of the carrier of F1
y is V8() Relation-like NAT -defined Function-like finite V98() Element of X ^omega
[TS2,y] is V26() set
{TS2,y} is non empty set
{TS2} is non empty trivial V39(1) set
{{TS2,y},{TS2}} is non empty set
q is Element of the carrier of F1
p is V8() Relation-like NAT -defined Function-like finite V98() Element of X ^omega
[q,p] is V26() set
{q,p} is non empty set
{q} is non empty trivial V39(1) set
{{q,p},{q}} is non empty set
x is non empty set
x ^omega is non empty functional set
bool (x ^omega) is non empty set
X is functional Element of bool (x ^omega)
E is functional Element of bool (x ^omega)
F1 is non empty (X)
the of F1 is Relation-like [: the carrier of F1,X:] -defined the carrier of F1 -valued Element of bool [:[: the carrier of F1,X:], the carrier of F1:]
the carrier of F1 is non empty set
[: the carrier of F1,X:] is Relation-like set
[:[: the carrier of F1,X:], the carrier of F1:] is Relation-like set
bool [:[: the carrier of F1,X:], the carrier of F1:] is non empty set
(x,X,F1) is Relation-like [: the carrier of F1,(x ^omega):] -defined [: the carrier of F1,(x ^omega):] -valued Element of bool [:[: the carrier of F1,(x ^omega):],[: the carrier of F1,(x ^omega):]:]
[: the carrier of F1,(x ^omega):] is non empty Relation-like set
[:[: the carrier of F1,(x ^omega):],[: the carrier of F1,(x ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of F1,(x ^omega):],[: the carrier of F1,(x ^omega):]:] is non empty set
F2 is non empty (E)
the of F2 is Relation-like [: the carrier of F2,E:] -defined the carrier of F2 -valued Element of bool [:[: the carrier of F2,E:], the carrier of F2:]
the carrier of F2 is non empty set
[: the carrier of F2,E:] is Relation-like set
[:[: the carrier of F2,E:], the carrier of F2:] is Relation-like set
bool [:[: the carrier of F2,E:], the carrier of F2:] is non empty set
(x,E,F2) is Relation-like [: the carrier of F2,(x ^omega):] -defined [: the carrier of F2,(x ^omega):] -valued Element of bool [:[: the carrier of F2,(x ^omega):],[: the carrier of F2,(x ^omega):]:]
[: the carrier of F2,(x ^omega):] is non empty Relation-like set
[:[: the carrier of F2,(x ^omega):],[: the carrier of F2,(x ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of F2,(x ^omega):],[: the carrier of F2,(x ^omega):]:] is non empty set
TS1 is set
TS2 is Element of the carrier of F1
q is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[TS2,q] is V26() set
{TS2,q} is non empty set
{TS2} is non empty trivial V39(1) set
{{TS2,q},{TS2}} is non empty set
y is Element of the carrier of F1
p is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[y,p] is V26() set
{y,p} is non empty set
{y} is non empty trivial V39(1) set
{{y,p},{y}} is non empty set
[[TS2,q],[y,p]] is V26() set
{[TS2,q],[y,p]} is non empty Relation-like set
{[TS2,q]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[TS2,q],[y,p]},{[TS2,q]}} is non empty set
TS1 is set
TS2 is Element of the carrier of F2
q is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[TS2,q] is V26() set
{TS2,q} is non empty set
{TS2} is non empty trivial V39(1) set
{{TS2,q},{TS2}} is non empty set
y is Element of the carrier of F2
p is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[y,p] is V26() set
{y,p} is non empty set
{y} is non empty trivial V39(1) set
{{y,p},{y}} is non empty set
[[TS2,q],[y,p]] is V26() set
{[TS2,q],[y,p]} is non empty Relation-like set
{[TS2,q]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[TS2,q],[y,p]},{[TS2,q]}} is non empty set
x is set
X is set
[x,X] is V26() set
{x,X} is non empty set
{x} is non empty trivial V39(1) set
{{x,X},{x}} is non empty set
E is set
F1 is set
[E,F1] is V26() set
{E,F1} is non empty set
{E} is non empty trivial V39(1) set
{{E,F1},{E}} is non empty set
[[x,X],[E,F1]] is V26() set
{[x,X],[E,F1]} is non empty Relation-like set
{[x,X]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,X],[E,F1]},{[x,X]}} is non empty set
F2 is non empty set
F2 ^omega is non empty functional set
bool (F2 ^omega) is non empty set
TS1 is functional Element of bool (F2 ^omega)
TS2 is non empty (TS1)
(F2,TS1,TS2) is Relation-like [: the carrier of TS2,(F2 ^omega):] -defined [: the carrier of TS2,(F2 ^omega):] -valued Element of bool [:[: the carrier of TS2,(F2 ^omega):],[: the carrier of TS2,(F2 ^omega):]:]
the carrier of TS2 is non empty set
[: the carrier of TS2,(F2 ^omega):] is non empty Relation-like set
[:[: the carrier of TS2,(F2 ^omega):],[: the carrier of TS2,(F2 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS2,(F2 ^omega):],[: the carrier of TS2,(F2 ^omega):]:] is non empty set
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
[x,F1] is V26() set
{x,F1} is non empty set
{x} is non empty trivial V39(1) set
{{x,F1},{x}} is non empty set
F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
[X,F2] is V26() set
{X,F2} is non empty set
{X} is non empty trivial V39(1) set
{{X,F2},{X}} is non empty set
[[x,F1],[X,F2]] is V26() set
{[x,F1],[X,F2]} is non empty Relation-like set
{[x,F1]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,F1],[X,F2]},{[x,F1]}} is non empty set
TS1 is functional Element of bool (E ^omega)
TS2 is non empty (TS1)
(E,TS1,TS2) is Relation-like [: the carrier of TS2,(E ^omega):] -defined [: the carrier of TS2,(E ^omega):] -valued Element of bool [:[: the carrier of TS2,(E ^omega):],[: the carrier of TS2,(E ^omega):]:]
the carrier of TS2 is non empty set
[: the carrier of TS2,(E ^omega):] is non empty Relation-like set
[:[: the carrier of TS2,(E ^omega):],[: the carrier of TS2,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS2,(E ^omega):],[: the carrier of TS2,(E ^omega):]:] is non empty set
x is set
X is set
[x,X] is V26() set
{x,X} is non empty set
{x} is non empty trivial V39(1) set
{{x,X},{x}} is non empty set
E is set
F1 is non empty set
F1 ^omega is non empty functional set
bool (F1 ^omega) is non empty set
<%> F1 is empty V6() V8() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined F1 -valued Function-like one-to-one constant functional finite V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V47() V77() V78() V79() V80() V81() V82() V83() co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V98() V100() Element of K266(F1)
K266(F1) is non empty functional M12(F1)
[E,(<%> F1)] is V26() set
{E,(<%> F1)} is non empty set
{E} is non empty trivial V39(1) set
{{E,(<%> F1)},{E}} is non