:: 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