:: REWRITE3 semantic presentation

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 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 functional Element of bool (F1 ^omega)
TS1 is non empty (F2)
(F1,F2,TS1) is Relation-like [: the carrier of TS1,(F1 ^omega):] -defined [: the carrier of TS1,(F1 ^omega):] -valued Element of bool [:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:]
the carrier of TS1 is non empty set
[: the carrier of TS1,(F1 ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^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
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)
[x,(F1 ^ F2)] is V26() set
{x,(F1 ^ F2)} is non empty set
{x} is non empty trivial V39(1) set
{{x,(F1 ^ F2)},{x}} is non empty set
[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 ^ F2)],[X,F2]] is V26() set
{[x,(F1 ^ F2)],[X,F2]} is non empty Relation-like set
{[x,(F1 ^ F2)]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,(F1 ^ F2)],[X,F2]},{[x,(F1 ^ F2)]}} 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
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 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)
[x,(F1 ^ TS1)] is V26() set
{x,(F1 ^ TS1)} is non empty set
{{x,(F1 ^ TS1)},{x}} is non empty set
F2 ^ TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
[X,(F2 ^ TS1)] is V26() set
{X,(F2 ^ TS1)} is non empty set
{{X,(F2 ^ TS1)},{X}} is non empty set
[[x,(F1 ^ TS1)],[X,(F2 ^ TS1)]] is V26() set
{[x,(F1 ^ TS1)],[X,(F2 ^ TS1)]} is non empty Relation-like set
{[x,(F1 ^ TS1)]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,(F1 ^ TS1)],[X,(F2 ^ TS1)]},{[x,(F1 ^ TS1)]}} is non empty set
TS2 is functional Element of bool (E ^omega)
y is non empty (TS2)
(E,TS2,y) is Relation-like [: the carrier of y,(E ^omega):] -defined [: the carrier of y,(E ^omega):] -valued Element of bool [:[: the carrier of y,(E ^omega):],[: the carrier of y,(E ^omega):]:]
the carrier of y is non empty set
[: the carrier of y,(E ^omega):] is non empty Relation-like set
[:[: the carrier of y,(E ^omega):],[: the carrier of y,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of y,(E ^omega):],[: the carrier of y,(E ^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
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
[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
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 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
E 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,[X,E]] is V26() set
{x,[X,E]} is non empty set
{x} is non empty trivial V39(1) set
{{x,[X,E]},{x}} is non empty set
F1 is set
[F1,E] is V26() set
{F1,E} is non empty set
{F1} is non empty trivial V39(1) set
{{F1,E},{F1}} is non empty set
[x,[F1,E]] is V26() set
{x,[F1,E]} is non empty set
{{x,[F1,E]},{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)
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 non empty 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
(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,(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
y is Element of the carrier of TS2
q is V8() Relation-like NAT -defined Function-like finite V98() Element of F2 ^omega
[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
p is Element of the carrier of TS2
q is V8() Relation-like NAT -defined Function-like finite V98() Element of F2 ^omega
[p,q] is V26() set
{p,q} is non empty set
{p} is non empty trivial V39(1) set
{{p,q},{p}} 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
[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
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
[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
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 non empty (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 non empty 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
(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,(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
[E,X] is V26() set
{E,X} is non empty set
{E} is non empty trivial V39(1) set
{{E,X},{E}} is non empty set
[[x,X],[E,X]] is V26() set
{[x,X],[E,X]} is non empty Relation-like set
{[x,X]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,X],[E,X]},{[x,X]}} is non empty 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 non empty (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 non empty 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
(F1,F2,TS1) is Relation-like [: the carrier of TS1,(F1 ^omega):] -defined [: the carrier of TS1,(F1 ^omega):] -valued Element of bool [:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:]
[: the carrier of TS1,(F1 ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^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
[x,E] is V26() set
{x,E} is non empty set
{{x,E},{x}} is non empty set
F1 is non empty set
F1 ^omega is non empty functional set
bool (F1 ^omega) is non empty set
F2 is functional Element of bool (F1 ^omega)
TS1 is non empty (F2)
(F1,F2,TS1) is Relation-like [: the carrier of TS1,(F1 ^omega):] -defined [: the carrier of TS1,(F1 ^omega):] -valued Element of bool [:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:]
the carrier of TS1 is non empty set
[: the carrier of TS1,(F1 ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:] is non empty set
TS2 is Element of the carrier of TS1
y is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^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 TS1
p is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^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
q is Element of the carrier of TS1
p is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^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
v is Element of the carrier of TS1
v is V8() Relation-like NAT -defined Function-like finite V98() Element of F1 ^omega
[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
x is set
X is set
E 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,[X,E]] is V26() set
{x,[X,E]} is non empty set
{x} is non empty trivial V39(1) set
{{x,[X,E]},{x}} is non empty set
F1 is set
F2 is set
[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
[x,[F1,F2]] is V26() set
{x,[F1,F2]} is non empty set
{{x,[F1,F2]},{x}} is non empty 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 non empty (TS2)
(TS1,TS2,y) is Relation-like [: the carrier of y,(TS1 ^omega):] -defined [: the carrier of y,(TS1 ^omega):] -valued Element of bool [:[: the carrier of y,(TS1 ^omega):],[: the carrier of y,(TS1 ^omega):]:]
the carrier of y is non empty set
[: the carrier of y,(TS1 ^omega):] is non empty Relation-like set
[:[: the carrier of y,(TS1 ^omega):],[: the carrier of y,(TS1 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of y,(TS1 ^omega):],[: the carrier of y,(TS1 ^omega):]:] 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 non empty (X)
(x,X,E) 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):]:]
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 set
F2 is set
[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
TS1 is set
[F1,TS1] is V26() set
{F1,TS1} is non empty set
{{F1,TS1},{F1}} is non empty set
X is non empty set
X ^omega is non empty functional set
x is set
x `2 is set
E is set
F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of X ^omega
[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 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 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)
(x,X,E) 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):]:]
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 non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F1 . F2 is set
F1 . (F2 + 1) 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 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)
(x,X,E) 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):]:]
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 non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F1 . F2 is set
(F1 . F2) `1 is set
(F1 . F2) `2 is set
[((F1 . F2) `1),((F1 . F2) `2)] is V26() set
{((F1 . F2) `1),((F1 . F2) `2)} is non empty set
{((F1 . F2) `1)} is non empty trivial V39(1) set
{{((F1 . F2) `1),((F1 . F2) `2)},{((F1 . F2) `1)}} is non empty set
F1 . (F2 + 1) is set
(F1 . (F2 + 1)) `1 is set
(F1 . (F2 + 1)) `2 is set
[((F1 . (F2 + 1)) `1),((F1 . (F2 + 1)) `2)] is V26() set
{((F1 . (F2 + 1)) `1),((F1 . (F2 + 1)) `2)} is non empty set
{((F1 . (F2 + 1)) `1)} is non empty trivial V39(1) set
{{((F1 . (F2 + 1)) `1),((F1 . (F2 + 1)) `2)},{((F1 . (F2 + 1)) `1)}} is non empty set
TS1 is Element of the carrier of E
TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[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 Element of the carrier of E
q is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[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 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)
(x,X,E) 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):]:]
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
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,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
proj1 (proj1 the of E) is set
proj2 the of E is set
F1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F1 . F2 is set
(F1 . F2) `1 is set
(F1 . F2) `2 is set
F1 . (F2 + 1) is set
(F1 . (F2 + 1)) `1 is set
(F1 . (F2 + 1)) `2 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
TS1 is Element of the carrier of E
TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[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 Element of the carrier of E
q is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[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 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 carrier of F1 is non empty set
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,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 carrier of F2 is non empty set
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,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 non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,F1)
TS2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom TS1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
TS2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
TS1 . TS2 is set
TS1 . (TS2 + 1) is set
[(TS1 . TS2),(TS1 . (TS2 + 1))] is V26() set
{(TS1 . TS2),(TS1 . (TS2 + 1))} is non empty set
{(TS1 . TS2)} is non empty trivial V39(1) set
{{(TS1 . TS2),(TS1 . (TS2 + 1))},{(TS1 . TS2)}} is non empty set
len TS1 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 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)
(x,X,E) 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):]:]
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 non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
F1 . 1 is set
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
F2 is set
TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[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 V6() V10() V11() ext-real non negative finite V37() V100() set
F1 . TS2 is set
((F1 . TS2),x) is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
(F1 . TS2) `2 is 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
y is V6() V10() V11() ext-real non negative finite V37() V100() set
y + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F1 . y is set
[(F1 . y),(F1 . TS2)] is V26() set
{(F1 . y),(F1 . TS2)} is non empty set
{(F1 . y)} is non empty trivial V39(1) set
{{(F1 . y),(F1 . TS2)},{(F1 . y)}} is non empty set
proj2 (x,X,E) is Relation-like 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
x is set
X is non empty set
X ^omega is non empty functional set
bool (X ^omega) is non empty set
E is V8() Relation-like NAT -defined Function-like finite V98() Element of X ^omega
[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
F1 is functional Element of bool (X ^omega)
F2 is non empty (F1)
(X,F1,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 is non empty set
[: 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 non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (X,F1,F2)
len TS1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
TS1 . (len TS1) is set
dom TS1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
(TS1 . (len TS1)) `2 is set
{} ^ E is V8() Relation-like NAT -defined Function-like finite V98() 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) ^ E is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(X)
TS2 is V6() V10() V11() ext-real non negative finite V37() V100() set
(len TS1) - TS2 is V11() ext-real V100() set
TS1 . ((len TS1) - TS2) is set
(TS1 . ((len TS1) - TS2)) `2 is set
TS2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
(len TS1) - (TS2 + 1) is V11() ext-real V100() set
((len TS1) - (TS2 + 1)) + 1 is V11() ext-real V100() set
TS1 . ((len TS1) - (TS2 + 1)) is set
(TS1 . ((len TS1) - (TS2 + 1))) `2 is set
p is V8() Relation-like NAT -defined Function-like finite V98() Element of X ^omega
p ^ E is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(X)
p is V8() Relation-like NAT -defined Function-like finite V98() Element of X ^omega
p ^ E is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(X)
[(TS1 . ((len TS1) - (TS2 + 1))),(TS1 . ((len TS1) - TS2))] is V26() set
{(TS1 . ((len TS1) - (TS2 + 1))),(TS1 . ((len TS1) - TS2))} is non empty set
{(TS1 . ((len TS1) - (TS2 + 1)))} is non empty trivial V39(1) set
{{(TS1 . ((len TS1) - (TS2 + 1))),(TS1 . ((len TS1) - TS2))},{(TS1 . ((len TS1) - (TS2 + 1)))}} is non empty set
q is Element of the carrier of F2
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
v is Element of the carrier of F2
v is V8() Relation-like NAT -defined Function-like finite V98() Element of X ^omega
[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
l is V8() Relation-like NAT -defined Function-like finite V98() Element of X ^omega
l ^ v is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(X)
l ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(X)
(l ^ p) ^ E is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(X)
l ^ (p ^ E) is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(X)
(len TS1) - 0 is non empty V11() ext-real positive non negative V100() set
y is V8() Relation-like NAT -defined Function-like finite V98() Element of X ^omega
y ^ E is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(X)
(len TS1) - 0 is non empty V11() ext-real positive non negative V100() set
TS1 . ((len TS1) - 0) is set
(TS1 . ((len TS1) - 0)) `2 is set
TS2 is V6() V10() V11() ext-real non negative finite V37() V100() set
y is V6() V10() V11() ext-real non negative finite V37() V100() set
TS2 + y is V6() V10() V11() ext-real non negative finite V37() V100() set
(TS2 + y) - y is V11() ext-real V100() set
(len TS1) - y is V11() ext-real V100() set
TS1 . TS2 is set
(TS1 . TS2) `2 is 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
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
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,TS1,TS2)
y . 1 is set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is set
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom y is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
(y . 1) `2 is set
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)
K266(E) is non empty functional M12(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
[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
[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 functional Element of bool (E ^omega)
TS1 is non empty (F2)
(E,F2,TS1) is Relation-like [: the carrier of TS1,(E ^omega):] -defined [: the carrier of TS1,(E ^omega):] -valued Element of bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:]
the carrier of TS1 is non empty set
[: the carrier of TS1,(E ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty set
TS2 is V6() V10() V11() ext-real non negative finite V37() V100() set
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
y . 1 is set
q is set
[q,F1] is V26() set
{q,F1} is non empty set
{q} is non empty trivial V39(1) set
{{q,F1},{q}} is non empty set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is set
p is set
[p,F1] is V26() set
{p,F1} is non empty set
{p} is non empty trivial V39(1) set
{{p,F1},{p}} is non empty set
TS2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
q is V6() V10() V11() ext-real non negative finite V37() V100() set
dom y is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
y . q is set
(y . q) `2 is set
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom y is non empty 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
y . (1 + 1) is set
(y . (1 + 1)) `1 is set
(y . (1 + 1)) `2 is set
[((y . (1 + 1)) `1),((y . (1 + 1)) `2)] is V26() set
{((y . (1 + 1)) `1),((y . (1 + 1)) `2)} is non empty set
{((y . (1 + 1)) `1)} is non empty trivial V39(1) set
{{((y . (1 + 1)) `1),((y . (1 + 1)) `2)},{((y . (1 + 1)) `1)}} is non empty set
q is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
p is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
p . 1 is set
len p is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
p . (len p) is set
p is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
p ^ q is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
K266(E) is non empty functional M12(E)
<*(y . 1)*> is non empty trivial Relation-like NAT -defined Function-like constant finite V39(1) FinSequence-like FinSubsequence-like set
len <*(y . 1)*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
v is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
<*(y . 1)*> ^ v is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len v is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len v) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
v . 1 is set
v . (len v) is set
v is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
v ^ F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
{} ^ q is V8() Relation-like NAT -defined Function-like finite V98() set
p ^ v is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
(p ^ v) ^ F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
[((y . (1 + 1)) `1),F1] is V26() set
{((y . (1 + 1)) `1),F1} is non empty set
{{((y . (1 + 1)) `1),F1},{((y . (1 + 1)) `1)}} is non empty set
l is V6() V10() V11() ext-real non negative finite V37() V100() set
l - 1 is V11() ext-real V100() set
l + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
(1 + 1) - 1 is V11() ext-real V100() set
((len v) + 1) - 1 is V11() ext-real V100() set
l9 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom v is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
y . l is set
(y . l) `2 is set
(l - 1) + 1 is V11() ext-real V100() set
1 + 0 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
v . (l - 1) is set
(v . (l - 1)) `2 is set
y . l is set
(y . l) `2 is set
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
y . 1 is set
q is set
[q,F1] is V26() set
{q,F1} is non empty set
{q} is non empty trivial V39(1) set
{{q,F1},{q}} is non empty set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is set
p is set
[p,F1] is V26() set
{p,F1} is non empty set
{p} is non empty trivial V39(1) set
{{p,F1},{p}} is non empty set
q is V6() V10() V11() ext-real non negative finite V37() V100() set
dom y is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
y . q is set
(y . q) `2 is set
TS2 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
TS2 . 1 is set
y is set
[y,F1] is V26() set
{y,F1} is non empty set
{y} is non empty trivial V39(1) set
{{y,F1},{y}} is non empty set
len TS2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
TS2 . (len TS2) is set
q is set
[q,F1] is V26() set
{q,F1} is non empty set
{q} is non empty trivial V39(1) set
{{q,F1},{q}} is non empty set
p is V6() V10() V11() ext-real non negative finite V37() V100() set
dom TS2 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
TS2 . p is set
(TS2 . p) `2 is set
TS2 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
TS2 . 1 is set
len TS2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
TS2 . (len TS2) is set
y is V6() V10() V11() ext-real non negative finite V37() V100() set
dom TS2 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
TS2 . y is set
(TS2 . y) `2 is 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 non empty (X)
(x,X,E) 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):]:]
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 non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F1 . (F2 + 1) is set
(F1 . (F2 + 1)) `2 is set
F1 . F2 is set
(F1 . F2) `1 is set
(F1 . (F2 + 1)) `1 is set
(F1 . F2) `2 is set
TS1 is Element of the carrier of E
TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[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 Element of the carrier of E
q is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[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
[[TS1,TS2],[y,q]] is V26() set
{[TS1,TS2],[y,q]} is non empty Relation-like set
{[TS1,TS2]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[TS1,TS2],[y,q]},{[TS1,TS2]}} is non empty set
p is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
q is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
q ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
K266(x) is non empty functional M12(x)
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
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
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,TS1,TS2)
dom y is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
q is V6() V10() V11() ext-real non negative finite V37() V100() set
q + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
y . q is set
y . (q + 1) is 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
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 empty set
<*[x,X],[E,(<%> F1)]*> is non empty Relation-like NAT -defined Function-like finite V39(2) FinSequence-like FinSubsequence-like set
F2 is functional Element of bool (F1 ^omega)
TS1 is non empty (F2)
(F1,F2,TS1) is Relation-like [: the carrier of TS1,(F1 ^omega):] -defined [: the carrier of TS1,(F1 ^omega):] -valued Element of bool [:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:]
the carrier of TS1 is non empty set
[: the carrier of TS1,(F1 ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:] 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
[[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
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)
[x,(F1 ^ F2)] is V26() set
{x,(F1 ^ F2)} is non empty set
{x} is non empty trivial V39(1) set
{{x,(F1 ^ F2)},{x}} is non empty set
[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 ^ F2)],[X,F2]*> is non empty Relation-like NAT -defined Function-like finite V39(2) FinSequence-like FinSubsequence-like 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,(F1 ^ F2)],[X,F2]] is V26() set
{[x,(F1 ^ F2)],[X,F2]} is non empty Relation-like set
{[x,(F1 ^ F2)]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,(F1 ^ F2)],[X,F2]},{[x,(F1 ^ F2)]}} is non empty set
[[x,(F1 ^ F2)],[X,F2]] is V26() set
{[x,(F1 ^ F2)],[X,F2]} is non empty Relation-like set
{[x,(F1 ^ F2)]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,(F1 ^ F2)],[X,F2]},{[x,(F1 ^ F2)]}} 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
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
[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
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 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
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,TS1,TS2)
y . 1 is set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is set
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)
K266(E) is non empty functional M12(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
<%> 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
[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
[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 functional Element of bool (E ^omega)
TS1 is non empty (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 non empty 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
(E,F2,TS1) is Relation-like [: the carrier of TS1,(E ^omega):] -defined [: the carrier of TS1,(E ^omega):] -valued Element of bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:]
[: the carrier of TS1,(E ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty set
TS2 is V6() V10() V11() ext-real non negative finite V37() V100() set
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
y . 1 is set
q is set
[q,F1] is V26() set
{q,F1} is non empty set
{q} is non empty trivial V39(1) set
{{q,F1},{q}} is non empty set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is set
p is set
[p,F1] is V26() set
{p,F1} is non empty set
{p} is non empty trivial V39(1) set
{{p,F1},{p}} is non empty set
TS2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
<*(y . 1)*> is non empty trivial Relation-like NAT -defined Function-like constant finite V39(1) FinSequence-like FinSubsequence-like set
q is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
<*(y . 1)*> ^ q is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len q is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len q) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom y is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
y . (1 + 1) is set
(y . (1 + 1)) `1 is set
(y . (1 + 1)) `2 is set
[((y . (1 + 1)) `1),((y . (1 + 1)) `2)] is V26() set
{((y . (1 + 1)) `1),((y . (1 + 1)) `2)} is non empty set
{((y . (1 + 1)) `1)} is non empty trivial V39(1) set
{{((y . (1 + 1)) `1),((y . (1 + 1)) `2)},{((y . (1 + 1)) `1)}} is non empty set
[((y . (1 + 1)) `1),F1] is V26() set
{((y . (1 + 1)) `1),F1} is non empty set
{{((y . (1 + 1)) `1),F1},{((y . (1 + 1)) `1)}} is non empty set
[[q,F1],[((y . (1 + 1)) `1),F1]] is V26() set
{[q,F1],[((y . (1 + 1)) `1),F1]} is non empty Relation-like set
{[q,F1]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[q,F1],[((y . (1 + 1)) `1),F1]},{[q,F1]}} is non empty set
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
y . 1 is set
q is set
[q,F1] is V26() set
{q,F1} is non empty set
{q} is non empty trivial V39(1) set
{{q,F1},{q}} is non empty set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is set
p is set
[p,F1] is V26() set
{p,F1} is non empty set
{p} is non empty trivial V39(1) set
{{p,F1},{p}} is non empty set
TS2 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
TS2 . 1 is set
len TS2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
TS2 . (len TS2) is set
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
y . 1 is set
q is set
[q,F1] is V26() set
{q,F1} is non empty set
{q} is non empty trivial V39(1) set
{{q,F1},{q}} is non empty set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is set
p is set
[p,F1] is V26() set
{p,F1} is non empty set
{p} is non empty trivial V39(1) set
{{p,F1},{p}} 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 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 functional Element of bool (x ^omega)
E is non empty (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 non empty 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
proj2 (proj1 the of E) is set
(x,X,E) 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):]:]
[: 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 non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
F1 . 1 is set
(F1 . 1) `2 is 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
F1 . (len F1) is set
(F1 . (len F1)) `2 is set
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
(len F1) - 1 is V11() ext-real V100() set
F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F1 . F2 is set
F1 . (F2 + 1) is set
TS1 is Element of the carrier of E
TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[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 Element of the carrier of E
q is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[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
F1 . (1 + 1) is set
p is Element of the carrier of E
q is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[p,q] is V26() set
{p,q} is non empty set
{p} is non empty trivial V39(1) set
{{p,q},{p}} is non empty set
p is Element of the carrier of E
v is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[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
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)
[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
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
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 F1) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F2 is functional Element of bool (E ^omega)
TS1 is non empty (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 non empty 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
(E,F2,TS1) is Relation-like [: the carrier of TS1,(E ^omega):] -defined [: the carrier of TS1,(E ^omega):] -valued Element of bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:]
[: the carrier of TS1,(E ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty set
TS2 is V6() V10() V11() ext-real non negative finite V37() V100() set
q is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
len q is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 q is V6() V10() V11() ext-real non negative finite V37() V100() set
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
y . 1 is set
p is set
[p,q] is V26() set
{p,q} is non empty set
{p} is non empty trivial V39(1) set
{{p,q},{p}} is non empty set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is set
(len q) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
<*(y . 1)*> is non empty trivial Relation-like NAT -defined Function-like constant finite V39(1) FinSequence-like FinSubsequence-like set
q is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
<*(y . 1)*> ^ q is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len q is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len q) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom y is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
y . (1 + 1) is set
(y . (1 + 1)) `1 is set
(y . (1 + 1)) `2 is set
[((y . (1 + 1)) `1),((y . (1 + 1)) `2)] is V26() set
{((y . (1 + 1)) `1),((y . (1 + 1)) `2)} is non empty set
{((y . (1 + 1)) `1)} is non empty trivial V39(1) set
{{((y . (1 + 1)) `1),((y . (1 + 1)) `2)},{((y . (1 + 1)) `1)}} is non empty set
[[p,q],[((y . (1 + 1)) `1),((y . (1 + 1)) `2)]] is V26() set
{[p,q],[((y . (1 + 1)) `1),((y . (1 + 1)) `2)]} is non empty Relation-like set
{[p,q]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[p,q],[((y . (1 + 1)) `1),((y . (1 + 1)) `2)]},{[p,q]}} is non empty set
len <*(y . 1)*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
q . 1 is set
p is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
[((y . (1 + 1)) `1),p] is V26() set
{((y . (1 + 1)) `1),p} is non empty set
{{((y . (1 + 1)) `1),p},{((y . (1 + 1)) `1)}} is non empty set
v is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
v ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
len p is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 p is V6() V10() V11() ext-real non negative finite V37() V100() set
len v is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 v is V6() V10() V11() ext-real non negative finite V37() V100() set
(len p) + (len v) is V6() V10() V11() ext-real non negative finite V37() V100() set
(len q) - 0 is V11() ext-real non negative V100() set
((len p) + (len v)) - (len v) is V11() ext-real V100() set
(len p) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
q . (len q) is set
(len q) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
q is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
len q is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 q is V6() V10() V11() ext-real non negative finite V37() V100() set
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
y . 1 is set
p is set
[p,q] is V26() set
{p,q} is non empty set
{p} is non empty trivial V39(1) set
{{p,q},{p}} is non empty set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is set
(len q) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
TS2 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
TS2 . 1 is set
len TS2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
TS2 . (len TS2) is 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)
[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
F1 is Element of E
<%F1%> is non empty trivial V8() Relation-like NAT -defined E -valued Function-like constant finite V39(1) V98() Element of K266(E)
[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 functional Element of bool (E ^omega)
TS1 is non empty (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 non empty 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
(E,F2,TS1) is Relation-like [: the carrier of TS1,(E ^omega):] -defined [: the carrier of TS1,(E ^omega):] -valued Element of bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:]
[: the carrier of TS1,(E ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty set
TS2 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
TS2 . 1 is set
len TS2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
TS2 . (len TS2) is 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
proj1 <%F1%> is non empty trivial V6() V10() V11() ext-real positive non negative finite V37() V39(1) V100() set
(len <%F1%>) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() 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
[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
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
[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
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 non empty (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 non empty 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
(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,(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
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,TS1,TS2)
y . 1 is set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is set
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)
len q is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 q is V6() V10() V11() ext-real non negative finite V37() V100() set
(len q) + (len F2) is V6() V10() V11() ext-real non negative finite V37() V100() set
{} ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() set
x is non empty set
x ^omega is non empty functional set
bool (x ^omega) is non empty 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 functional Element of bool (x ^omega)
E is non empty (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 non empty 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
proj2 (proj1 the of E) is set
(x,X,E) 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):]:]
[: 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 non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F1 . F2 is set
(F1 . F2) `2 is set
F1 . (F2 + 1) is set
(F1 . (F2 + 1)) `2 is set
TS1 is Element of the carrier of E
TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[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 Element of the carrier of E
q is V8() Relation-like NAT -defined Function-like finite V98() Element of x ^omega
[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
[[TS1,TS2],[y,q]] is V26() set
{[TS1,TS2],[y,q]} is non empty Relation-like set
{[TS1,TS2]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[TS1,TS2],[y,q]},{[TS1,TS2]}} 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 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 functional Element of bool (x ^omega)
E is non empty (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 non empty 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
proj2 (proj1 the of E) is set
(x,X,E) 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):]:]
[: 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 V6() V10() V11() ext-real non negative finite V37() V100() set
F2 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
len F2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
F1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
TS1 is V6() V10() V11() ext-real non negative finite V37() V100() set
dom F2 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
TS2 is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 . TS1 is set
(F2 . TS1) `2 is set
F2 . TS2 is set
(F2 . TS2) `2 is set
TS1 - 1 is V11() ext-real V100() set
y is V6() V10() V11() ext-real non negative finite V37() V100() set
1 - 1 is V11() ext-real V100() set
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
TS2 - 1 is V11() ext-real V100() set
q is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 . 1 is set
<*(F2 . 1)*> is non empty trivial Relation-like NAT -defined Function-like constant finite V39(1) FinSequence-like FinSubsequence-like set
p is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
<*(F2 . 1)*> ^ p is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len p is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len p) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
((len p) + 1) - 1 is V11() ext-real V100() set
dom p is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
len <*(F2 . 1)*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
F2 . TS2 is set
p . q is set
F2 . TS1 is set
p . y is set
(F2 . TS1) `2 is set
(F2 . TS2) `2 is set
F2 | F1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
F2 . TS1 is set
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
y . TS1 is set
F2 . TS2 is set
y . TS2 is set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom y is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
(F2 . TS1) `2 is set
(F2 . TS2) `2 is set
F2 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
len F2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
TS1 is V6() V10() V11() ext-real non negative finite V37() V100() set
dom F2 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
TS2 is V6() V10() V11() ext-real non negative finite V37() V100() set
F2 . TS1 is set
(F2 . TS1) `2 is set
F2 . TS2 is set
(F2 . TS2) `2 is set
F1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
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
F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
TS1 is V6() V10() V11() ext-real non negative finite V37() V100() set
F1 . F2 is set
(F1 . F2) `2 is set
F1 . TS1 is set
(F1 . TS1) `2 is set
F1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
F1 . F2 is set
(F1 . F2) `2 is set
TS1 is V6() V10() V11() ext-real non negative finite V37() V100() set
F1 . TS1 is set
(F1 . TS1) `2 is 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 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)
(x,X,E) 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):]:]
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 non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
F1 . 1 is set
F2 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
F2 . 1 is set
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
dom F2 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
TS1 is V6() V10() V11() ext-real non negative finite V37() V100() set
F1 . TS1 is set
F2 . TS1 is set
TS1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F1 . (TS1 + 1) is set
[(F1 . TS1),(F1 . (TS1 + 1))] is V26() set
{(F1 . TS1),(F1 . (TS1 + 1))} is non empty set
{(F1 . TS1)} is non empty trivial V39(1) set
{{(F1 . TS1),(F1 . (TS1 + 1))},{(F1 . TS1)}} is non empty set
F2 . (TS1 + 1) is set
[(F2 . TS1),(F2 . (TS1 + 1))] is V26() set
{(F2 . TS1),(F2 . (TS1 + 1))} is non empty set
{(F2 . TS1)} is non empty trivial V39(1) set
{{(F2 . TS1),(F2 . (TS1 + 1))},{(F2 . TS1)}} is non empty set
F1 . (TS1 + 1) is set
F2 . (TS1 + 1) is set
F1 . (TS1 + 1) is set
F2 . (TS1 + 1) is set
F1 . (TS1 + 1) is set
F2 . (TS1 + 1) is set
F1 . 0 is set
F2 . 0 is set
TS1 is V6() V10() V11() ext-real non negative finite V37() V100() set
F1 . TS1 is set
F2 . TS1 is 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 non empty (X)
(x,X,E) 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):]:]
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 non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
F1 . 1 is set
F2 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
F2 . 1 is 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
len F2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
TS1 is V6() V10() V11() ext-real non negative finite V37() V100() set
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
dom F2 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
F1 . TS1 is set
F2 . TS1 is 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 non empty (X)
(x,X,E) 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):]:]
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
<%> 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)
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,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
proj2 (proj1 the of E) is set
F1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
F1 . 1 is set
F2 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (x,X,E)
F2 . 1 is 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
F1 . (len F1) is set
(F1 . (len F1)) `2 is set
len F2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
F2 . (len F2) is set
(F2 . (len F2)) `2 is set
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
dom F2 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
F1 . (len F2) is set
(F1 . (len F2)) `2 is set
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom F2 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
dom F1 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
F2 . (len F1) is set
(F2 . (len F1)) `2 is 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
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
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,TS1,TS2)
y . 1 is set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is 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
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)
[x,(F1 ^ TS1)] is V26() set
{x,(F1 ^ TS1)} is non empty set
{{x,(F1 ^ TS1)},{x}} is non empty set
F2 ^ TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
[X,(F2 ^ TS1)] is V26() set
{X,(F2 ^ TS1)} is non empty set
{{X,(F2 ^ TS1)},{X}} is non empty set
TS2 is functional Element of bool (E ^omega)
y is non empty (TS2)
(E,TS2,y) is Relation-like [: the carrier of y,(E ^omega):] -defined [: the carrier of y,(E ^omega):] -valued Element of bool [:[: the carrier of y,(E ^omega):],[: the carrier of y,(E ^omega):]:]
the carrier of y is non empty set
[: the carrier of y,(E ^omega):] is non empty Relation-like set
[:[: the carrier of y,(E ^omega):],[: the carrier of y,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of y,(E ^omega):],[: the carrier of y,(E ^omega):]:] is non empty set
q is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,TS2,y)
q . 1 is set
len q is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
q . (len q) is set
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom q is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
((q . (len q)),E) is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
(q . (len q)) `2 is set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len p is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom p is V77() V78() V79() V80() V81() V82() Element of bool NAT
q is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
q + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
p . q is set
p . (q + 1) is set
[(p . q),(p . (q + 1))] is V26() set
{(p . q),(p . (q + 1))} is non empty set
{(p . q)} is non empty trivial V39(1) set
{{(p . q),(p . (q + 1))},{(p . q)}} is non empty set
q . q is set
q . (q + 1) is set
[(q . q),(q . (q + 1))] is V26() set
{(q . q),(q . (q + 1))} is non empty set
{(q . q)} is non empty trivial V39(1) set
{{(q . q),(q . (q + 1))},{(q . q)}} is non empty set
(q . q) `1 is set
(q . q) `2 is set
[((q . q) `1),((q . q) `2)] is V26() set
{((q . q) `1),((q . q) `2)} is non empty set
{((q . q) `1)} is non empty trivial V39(1) set
{{((q . q) `1),((q . q) `2)},{((q . q) `1)}} is non empty set
[[((q . q) `1),((q . q) `2)],(q . (q + 1))] is V26() set
{[((q . q) `1),((q . q) `2)],(q . (q + 1))} is non empty set
{[((q . q) `1),((q . q) `2)]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[((q . q) `1),((q . q) `2)],(q . (q + 1))},{[((q . q) `1),((q . q) `2)]}} is non empty set
(q . (q + 1)) `1 is set
(q . (q + 1)) `2 is set
[((q . (q + 1)) `1),((q . (q + 1)) `2)] is V26() set
{((q . (q + 1)) `1),((q . (q + 1)) `2)} is non empty set
{((q . (q + 1)) `1)} is non empty trivial V39(1) set
{{((q . (q + 1)) `1),((q . (q + 1)) `2)},{((q . (q + 1)) `1)}} is non empty set
[[((q . q) `1),((q . q) `2)],[((q . (q + 1)) `1),((q . (q + 1)) `2)]] is V26() set
{[((q . q) `1),((q . q) `2)],[((q . (q + 1)) `1),((q . (q + 1)) `2)]} is non empty Relation-like set
{{[((q . q) `1),((q . q) `2)],[((q . (q + 1)) `1),((q . (q + 1)) `2)]},{[((q . q) `1),((q . q) `2)]}} is non empty set
((q . q),E) is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
[((q . q) `1),((q . q),E)] is V26() set
{((q . q) `1),((q . q),E)} is non empty set
{{((q . q) `1),((q . q),E)},{((q . q) `1)}} is non empty set
[[((q . q) `1),((q . q),E)],[((q . (q + 1)) `1),((q . (q + 1)) `2)]] is V26() set
{[((q . q) `1),((q . q),E)],[((q . (q + 1)) `1),((q . (q + 1)) `2)]} is non empty Relation-like set
{[((q . q) `1),((q . q),E)]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[((q . q) `1),((q . q),E)],[((q . (q + 1)) `1),((q . (q + 1)) `2)]},{[((q . q) `1),((q . q),E)]}} is non empty set
((q . (q + 1)),E) is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
[((q . (q + 1)) `1),((q . (q + 1)),E)] is V26() set
{((q . (q + 1)) `1),((q . (q + 1)),E)} is non empty set
{{((q . (q + 1)) `1),((q . (q + 1)),E)},{((q . (q + 1)) `1)}} is non empty set
[[((q . q) `1),((q . q),E)],[((q . (q + 1)) `1),((q . (q + 1)),E)]] is V26() set
{[((q . q) `1),((q . q),E)],[((q . (q + 1)) `1),((q . (q + 1)),E)]} is non empty Relation-like set
{{[((q . q) `1),((q . q),E)],[((q . (q + 1)) `1),((q . (q + 1)),E)]},{[((q . q) `1),((q . q),E)]}} is non empty set
((q . q),E) ^ TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
((q . (q + 1)),E) ^ TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
[((q . q) `1),(((q . q),E) ^ TS1)] is V26() set
{((q . q) `1),(((q . q),E) ^ TS1)} is non empty set
{{((q . q) `1),(((q . q),E) ^ TS1)},{((q . q) `1)}} is non empty set
[((q . (q + 1)) `1),(((q . (q + 1)),E) ^ TS1)] is V26() set
{((q . (q + 1)) `1),(((q . (q + 1)),E) ^ TS1)} is non empty set
{{((q . (q + 1)) `1),(((q . (q + 1)),E) ^ TS1)},{((q . (q + 1)) `1)}} is non empty set
[[((q . q) `1),(((q . q),E) ^ TS1)],[((q . (q + 1)) `1),(((q . (q + 1)),E) ^ TS1)]] is V26() set
{[((q . q) `1),(((q . q),E) ^ TS1)],[((q . (q + 1)) `1),(((q . (q + 1)),E) ^ TS1)]} is non empty Relation-like set
{[((q . q) `1),(((q . q),E) ^ TS1)]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[((q . q) `1),(((q . q),E) ^ TS1)],[((q . (q + 1)) `1),(((q . (q + 1)),E) ^ TS1)]},{[((q . q) `1),(((q . q),E) ^ TS1)]}} is non empty set
[[((q . q) `1),(((q . q),E) ^ TS1)],(p . (q + 1))] is V26() set
{[((q . q) `1),(((q . q),E) ^ TS1)],(p . (q + 1))} is non empty set
{{[((q . q) `1),(((q . q),E) ^ TS1)],(p . (q + 1))},{[((q . q) `1),(((q . q),E) ^ TS1)]}} is non empty set
q is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,TS2,y)
len q is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom q is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
q . (len q) is set
q . (len q) is set
(q . (len q)) `1 is set
((q . (len q)),E) is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
((q . (len q)),E) ^ TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
[((q . (len q)) `1),(((q . (len q)),E) ^ TS1)] is V26() set
{((q . (len q)) `1),(((q . (len q)),E) ^ TS1)} is non empty set
{((q . (len q)) `1)} is non empty trivial V39(1) set
{{((q . (len q)) `1),(((q . (len q)),E) ^ TS1)},{((q . (len q)) `1)}} is non empty set
((q . 1),E) is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
(q . 1) `2 is set
q . 1 is set
(q . 1) `1 is set
((q . 1),E) ^ TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
[((q . 1) `1),(((q . 1),E) ^ TS1)] is V26() set
{((q . 1) `1),(((q . 1),E) ^ TS1)} is non empty set
{((q . 1) `1)} is non empty trivial V39(1) set
{{((q . 1) `1),(((q . 1),E) ^ TS1)},{((q . 1) `1)}} 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 empty set
F2 is functional Element of bool (F1 ^omega)
TS1 is non empty (F2)
(F1,F2,TS1) is Relation-like [: the carrier of TS1,(F1 ^omega):] -defined [: the carrier of TS1,(F1 ^omega):] -valued Element of bool [:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:]
the carrier of TS1 is non empty set
[: the carrier of TS1,(F1 ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:] is non empty set
<*[x,X],[E,(<%> F1)]*> is non empty Relation-like NAT -defined Function-like finite V39(2) FinSequence-like FinSubsequence-like 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
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)
[x,(F1 ^ F2)] is V26() set
{x,(F1 ^ F2)} is non empty set
{x} is non empty trivial V39(1) set
{{x,(F1 ^ F2)},{x}} is non empty set
[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
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,(F1 ^ F2)],[X,F2]*> is non empty Relation-like NAT -defined Function-like finite V39(2) FinSequence-like FinSubsequence-like set
[[x,(F1 ^ F2)],[X,F2]] is V26() set
{[x,(F1 ^ F2)],[X,F2]} is non empty Relation-like set
{[x,(F1 ^ F2)]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,(F1 ^ F2)],[X,F2]},{[x,(F1 ^ F2)]}} 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
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,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
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
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
[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
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 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
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,TS1,TS2)
y . 1 is set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is 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
[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
F2 ^ F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
[X,(F2 ^ F1)] is V26() set
{X,(F2 ^ F1)} is non empty set
{X} is non empty trivial V39(1) set
{{X,(F2 ^ F1)},{X}} 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
len (F2 ^ F1) is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 (F2 ^ F1) is V6() V10() V11() ext-real non negative finite V37() V100() set
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 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 F2) + (len F1) is V6() V10() V11() ext-real non negative finite V37() V100() set
0 + (len F1) is V6() V10() V11() ext-real non negative finite V37() V100() 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
[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
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
[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
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 non empty (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 non empty 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
(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,(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
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,TS1,TS2)
y . 1 is set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is 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
[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
[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 functional Element of bool (E ^omega)
TS1 is non empty (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 non empty 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
(E,F2,TS1) is Relation-like [: the carrier of TS1,(E ^omega):] -defined [: the carrier of TS1,(E ^omega):] -valued Element of bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:]
[: the carrier of TS1,(E ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty set
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
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)
[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
F1 is Element of E
<%F1%> is non empty trivial V8() Relation-like NAT -defined E -valued Function-like constant finite V39(1) V98() Element of K266(E)
[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
[[x,<%F1%>],[X,(<%> E)]] is V26() set
{[x,<%F1%>],[X,(<%> E)]} is non empty Relation-like set
{[x,<%F1%>]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,<%F1%>],[X,(<%> E)]},{[x,<%F1%>]}} is non empty set
F2 is functional Element of bool (E ^omega)
TS1 is non empty (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 non empty 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
(E,F2,TS1) is Relation-like [: the carrier of TS1,(E ^omega):] -defined [: the carrier of TS1,(E ^omega):] -valued Element of bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:]
[: the carrier of TS1,(E ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty set
TS2 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
TS2 . 1 is set
len TS2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
TS2 . (len TS2) is set
1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom TS2 is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
x is set
X is set
E 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
F1 is set
[F1,E] is V26() set
{F1,E} is non empty set
{F1} is non empty trivial V39(1) set
{{F1,E},{F1}} 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
y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (F2,TS1,TS2)
y . 1 is set
len y is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
y . (len y) is set
q is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (F2,TS1,TS2)
q . 1 is set
len q is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
q . (len q) is set
(q . (len q)) `2 is set
(y . (len y)) `2 is 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 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 non empty (TS1)
the carrier of y is non empty set
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,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 non empty (TS2)
the carrier of q is non empty set
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,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
(F2,TS1,y) is Relation-like [: the carrier of y,(F2 ^omega):] -defined [: the carrier of y,(F2 ^omega):] -valued Element of bool [:[: the carrier of y,(F2 ^omega):],[: the carrier of y,(F2 ^omega):]:]
[: the carrier of y,(F2 ^omega):] is non empty Relation-like set
[:[: the carrier of y,(F2 ^omega):],[: the carrier of y,(F2 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of y,(F2 ^omega):],[: the carrier of y,(F2 ^omega):]:] 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
[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
(F2,TS2,q) is Relation-like [: the carrier of q,(F2 ^omega):] -defined [: the carrier of q,(F2 ^omega):] -valued Element of bool [:[: the carrier of q,(F2 ^omega):],[: the carrier of q,(F2 ^omega):]:]
[: the carrier of q,(F2 ^omega):] is non empty Relation-like set
[:[: the carrier of q,(F2 ^omega):],[: the carrier of q,(F2 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of q,(F2 ^omega):],[: the carrier of q,(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 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
[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 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 non empty (y)
(TS2,y,q) is Relation-like [: the carrier of q,(TS2 ^omega):] -defined [: the carrier of q,(TS2 ^omega):] -valued Element of bool [:[: the carrier of q,(TS2 ^omega):],[: the carrier of q,(TS2 ^omega):]:]
the carrier of q is non empty set
[: the carrier of q,(TS2 ^omega):] is non empty Relation-like set
[:[: the carrier of q,(TS2 ^omega):],[: the carrier of q,(TS2 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of q,(TS2 ^omega):],[: the carrier of q,(TS2 ^omega):]:] 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
[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
[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
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 non empty (F2)
(F1,F2,TS1) is Relation-like [: the carrier of TS1,(F1 ^omega):] -defined [: the carrier of TS1,(F1 ^omega):] -valued Element of bool [:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:]
the carrier of TS1 is non empty set
[: the carrier of TS1,(F1 ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(F1 ^omega):],[: the carrier of TS1,(F1 ^omega):]:] 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
[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 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 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,(F1 ^ F2)] is V26() set
{x,(F1 ^ F2)} is non empty set
{x} is non empty trivial V39(1) set
{{x,(F1 ^ F2)},{x}} is non empty set
[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 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 non empty (TS2)
(E,TS2,y) is Relation-like [: the carrier of y,(E ^omega):] -defined [: the carrier of y,(E ^omega):] -valued Element of bool [:[: the carrier of y,(E ^omega):],[: the carrier of y,(E ^omega):]:]
the carrier of y is non empty set
[: the carrier of y,(E ^omega):] is non empty Relation-like set
[:[: the carrier of y,(E ^omega):],[: the carrier of y,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of y,(E ^omega):],[: the carrier of y,(E ^omega):]:] is non empty set
[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
[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 ^ TS1)] is V26() set
{x,(F1 ^ TS1)} is non empty set
{{x,(F1 ^ TS1)},{x}} is non empty set
[X,(F2 ^ TS1)] is V26() set
{X,(F2 ^ TS1)} is non empty set
{{X,(F2 ^ TS1)},{X}} 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 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,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,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 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 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,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
[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 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 non empty (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 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
F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of E ^omega
F2 ^ F1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
TS1 is functional Element of bool (E ^omega)
TS2 is non empty (TS1)
len (F2 ^ F1) is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 (F2 ^ F1) is V6() V10() V11() ext-real non negative finite V37() V100() set
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 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 F2) + (len F1) is V6() V10() V11() ext-real non negative finite V37() V100() set
0 + (len F1) is V6() V10() V11() ext-real non negative finite V37() V100() 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
F2 is functional Element of bool (E ^omega)
TS1 is non empty (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 non empty 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
(E,F2,TS1) is Relation-like [: the carrier of TS1,(E ^omega):] -defined [: the carrier of TS1,(E ^omega):] -valued Element of bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:]
[: the carrier of TS1,(E ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty set
[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
[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
TS2 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,F2,TS1)
TS2 . 1 is set
len TS2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
TS2 . (len TS2) is 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 Element of E
<%F1%> is non empty trivial V8() Relation-like NAT -defined E -valued Function-like constant finite V39(1) V98() Element of K266(E)
F2 is functional Element of bool (E ^omega)
TS1 is non empty (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 non empty 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
(E,F2,TS1) is Relation-like [: the carrier of TS1,(E ^omega):] -defined [: the carrier of TS1,(E ^omega):] -valued Element of bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:]
[: the carrier of TS1,(E ^omega):] is non empty Relation-like set
[:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS1,(E ^omega):],[: the carrier of TS1,(E ^omega):]:] is non empty set
[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
[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,<%F1%>],[X,(<%> E)]] is V26() set
{[x,<%F1%>],[X,(<%> E)]} is non empty Relation-like set
{[x,<%F1%>]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,<%F1%>],[X,(<%> E)]},{[x,<%F1%>]}} is non empty set
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 non empty (TS2)
(TS1,TS2,y) is Relation-like [: the carrier of y,(TS1 ^omega):] -defined [: the carrier of y,(TS1 ^omega):] -valued Element of bool [:[: the carrier of y,(TS1 ^omega):],[: the carrier of y,(TS1 ^omega):]:]
the carrier of y is non empty set
[: the carrier of y,(TS1 ^omega):] is non empty Relation-like set
[:[: the carrier of y,(TS1 ^omega):],[: the carrier of y,(TS1 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of y,(TS1 ^omega):],[: the carrier of y,(TS1 ^omega):]:] 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
[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
[F2,F1] is V26() set
{F2,F1} is non empty set
{F2} is non empty trivial V39(1) set
{{F2,F1},{F2}} 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)
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 functional Element of bool (F1 ^omega)
TS1 is functional Element of bool (F1 ^omega)
TS2 is non empty (F2)
the carrier of TS2 is non empty set
the of TS2 is Relation-like [: the carrier of TS2,F2:] -defined the carrier of TS2 -valued Element of bool [:[: the carrier of TS2,F2:], the carrier of TS2:]
[: the carrier of TS2,F2:] is Relation-like set
[:[: the carrier of TS2,F2:], the carrier of TS2:] is Relation-like set
bool [:[: the carrier of TS2,F2:], the carrier of TS2:] is non empty set
y is non empty (TS1)
the carrier of y is non empty set
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,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
<%> 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)
x is set
X is non empty set
X ^omega is non empty functional set
bool (X ^omega) is non empty 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)
E is functional Element of bool (X ^omega)
F1 is non empty (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
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 non empty (TS1)
<%> 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)
{} ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() 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 functional Element of bool (F1 ^omega)
TS1 is non empty (F2)
<%> 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)
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 non empty (F2)
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
F2 ^ TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(F1)
K266(F1) is non empty functional M12(F1)
TS2 is functional Element of bool (F1 ^omega)
y is non empty (TS2)
(F2 ^ TS1) ^ {} is V8() Relation-like NAT -defined Function-like finite V98() 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)
(F2 ^ TS1) ^ (<%> F1) is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(F1)
TS1 ^ {} is V8() Relation-like NAT -defined Function-like finite V98() 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 non empty (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 non empty 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 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 Element of E
<%F1%> is non empty trivial V8() Relation-like NAT -defined E -valued Function-like constant finite V39(1) V98() Element of K266(E)
F2 is functional Element of bool (E ^omega)
TS1 is non empty (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 non empty 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
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 non empty (TS1)
<%> F2 is empty V6() V8() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined F2 -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(F2)
K266(F2) is non empty functional M12(F2)
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
F2 is set
F1 is set
{ b₁ where b₁ is Element of the carrier of E : ex b₂ being Element of the carrier of E st
( b₂ in F2 & (x,X,E,b₂,F1,b₁) ) } is set
bool the carrier of E is non empty set
TS2 is set
y is Element of the carrier of E
q is Element of the carrier of 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 functional Element of bool (E ^omega)
F2 is non empty (F1)
the carrier of F2 is non empty set
(E,F1,F2,x,X) is Element of bool the carrier of F2
bool the carrier of F2 is non empty set
{ b₁ where b₁ is Element of the carrier of F2 : ex b₂ being Element of the carrier of F2 st
( b₂ in X & (E,F1,F2,b₂,x,b₁) ) } is set
TS1 is Element of the carrier of F2
TS2 is Element of the carrier of F2
y is Element of the carrier of F2
TS2 is Element of the carrier of F2
x is non empty set
x ^omega is non empty functional set
bool (x ^omega) is non empty 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 functional Element of bool (x ^omega)
E is non empty (X)
the carrier of E is non empty set
bool the carrier of E is non empty set
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,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
proj2 (proj1 the of E) is set
F1 is Element of bool the carrier of E
(x,X,E,(<%> x),F1) is Element of bool the carrier of E
{ b₁ where b₁ is Element of the carrier of E : ex b₂ being Element of the carrier of E st
( b₂ in F1 & (x,X,E,b₂, <%> x,b₁) ) } is set
F2 is set
TS1 is Element of the carrier of E
F2 is 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 functional Element of bool (E ^omega)
F2 is functional Element of bool (E ^omega)
TS1 is non empty (F1)
the carrier of TS1 is non empty set
the of TS1 is Relation-like [: the carrier of TS1,F1:] -defined the carrier of TS1 -valued Element of bool [:[: the carrier of TS1,F1:], the carrier of TS1:]
[: the carrier of TS1,F1:] is Relation-like set
[:[: the carrier of TS1,F1:], the carrier of TS1:] is Relation-like set
bool [:[: the carrier of TS1,F1:], the carrier of TS1:] is non empty set
(E,F1,TS1,x,X) is Element of bool the carrier of TS1
bool the carrier of TS1 is non empty set
{ b₁ where b₁ is Element of the carrier of TS1 : ex b₂ being Element of the carrier of TS1 st
( b₂ in X & (E,F1,TS1,b₂,x,b₁) ) } is set
TS2 is non empty (F2)
the carrier of TS2 is non empty set
the of TS2 is Relation-like [: the carrier of TS2,F2:] -defined the carrier of TS2 -valued Element of bool [:[: the carrier of TS2,F2:], the carrier of TS2:]
[: the carrier of TS2,F2:] is Relation-like set
[:[: the carrier of TS2,F2:], the carrier of TS2:] is Relation-like set
bool [:[: the carrier of TS2,F2:], the carrier of TS2:] is non empty set
(E,F2,TS2,x,X) is Element of bool the carrier of TS2
bool the carrier of TS2 is non empty set
{ b₁ where b₁ is Element of the carrier of TS2 : ex b₂ being Element of the carrier of TS2 st
( b₂ in X & (E,F2,TS2,b₂,x,b₁) ) } is set
y is set
q is Element of the carrier of TS2
p is Element of the carrier of TS2
p is Element of the carrier of TS1
q is Element of the carrier of TS1
y is set
q is Element of the carrier of TS1
p is Element of the carrier of TS1
p is Element of the carrier of TS2
q is Element of the carrier of TS2