:: REWRITE2 semantic presentation

REAL is set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K6(REAL)

K6(REAL) is set

NAT is non empty epsilon-transitive epsilon-connected ordinal set

K6(NAT) is set

K6(NAT) is set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V60() V81() irreflexive Element of NAT

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() Element of NAT

{0,1} is non empty Element of K6(NAT)

{0,1} ^omega is non empty functional set

K6(({0,1} ^omega)) is set

[#] (NAT,REAL) is Relation-like set

K6(([#] (NAT,REAL))) is set

K346() is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() Element of NAT

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V60() V81() irreflexive set

Seg 1 is non empty finite V39(1) Element of K6(NAT)

{ b

{1} is non empty set

Seg 2 is non empty finite V39(2) Element of K6(NAT)

{ b

{1,2} is non empty set

E is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() Element of NAT

S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dom S is Element of K6(NAT)

len S is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

E is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len S is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

S ^ s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len (S ^ s) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len s is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() Element of NAT

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

(len S) + t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(len S) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(len S) + (len s) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

E is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

S is Relation-like set

s is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of S

s | E is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Seg E is finite V39(E) Element of K6(NAT)

{ b

s | (Seg E) is Relation-like NAT -defined Seg E -defined NAT -defined Function-like FinSubsequence-like set

len s is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len s is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

dom (s | E) is Element of K6(NAT)

dom s is non empty Element of K6(NAT)

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

t + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() Element of NAT

(s | E) . t is set

s . t is set

(s | E) . (t + 1) is set

s . (t + 1) is set

[((s | E) . t),((s | E) . (t + 1))] is set

{((s | E) . t),((s | E) . (t + 1))} is non empty set

{((s | E) . t)} is non empty set

{{((s | E) . t),((s | E) . (t + 1))},{((s | E) . t)}} is non empty set

len (s | E) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len s is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

E is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

S is Relation-like set

s is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of S

dom s is non empty Element of K6(NAT)

s . 1 is set

s . E is set

s | E is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Seg E is finite V39(E) Element of K6(NAT)

{ b

s | (Seg E) is Relation-like NAT -defined Seg E -defined NAT -defined Function-like FinSubsequence-like set

len (s | E) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(s | E) . 1 is set

(s | E) . (len (s | E)) is set

len s is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

E is Relation-like Function-like set

S is set

dom E is set

E . S is set

E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

<*E*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set

[1,E] is set

{1,E} is non empty set

{{1,E},{1}} is non empty set

{[1,E]} is non empty Relation-like Function-like set

S is set

dom <*E*> is non empty set

<*E*> . S is set

dom <*E*> is non empty Element of K6(NAT)

{1} is non empty Element of K6(NAT)

E is Relation-like Function-like () set

S is set

E . S is set

dom E is set

dom E is set

dom E is set

E is Relation-like Function-like () set

S is set

E . S is Relation-like Function-like finite set

dom E is set

dom E is set

dom E is set

E is set

E ^omega is non empty functional set

S is Relation-like NAT -defined E ^omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of E ^omega

s is set

dom S is set

S . s is Relation-like Function-like set

dom S is Element of K6(NAT)

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

S . t is Relation-like Function-like set

E is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

E ^ S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

s is set

dom (E ^ S) is Element of K6(NAT)

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

dom E is Element of K6(NAT)

E . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E ^ S) . t is set

(E ^ S) . s is set

dom S is Element of K6(NAT)

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len E is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

(len E) + w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(len E) + w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(E ^ S) . ((len E) + w) is set

S . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E ^ S) . s is set

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

dom E is Element of K6(NAT)

dom S is Element of K6(NAT)

len E is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

S is Relation-like Function-like () set

dom S is set

E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s is set

S . s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ (S . s) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

t is set

S . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ (S . t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s is Relation-like Function-like set

dom s is set

t is set

s . t is set

S . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ (S . t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

t is Relation-like Function-like () set

dom t is set

w is set

t . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ (S . w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s is Relation-like Function-like () set

dom s is set

t is Relation-like Function-like () set

dom t is set

w is set

s . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ (S . w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

t . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s is set

S . s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S . s) ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

t is set

S . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S . t) ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s is Relation-like Function-like set

dom s is set

t is set

s . t is set

S . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S . t) ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

t is Relation-like Function-like () set

dom t is set

w is set

t . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S . w) ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s is Relation-like Function-like () set

dom s is set

t is Relation-like Function-like () set

dom t is set

w is set

s . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S . w) ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

t . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,S) is Relation-like Function-like () set

dom S is Element of K6(NAT)

s is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

Seg s is finite V39(s) Element of K6(NAT)

{ b

dom (E,S) is set

(E,S) is Relation-like Function-like () set

dom S is Element of K6(NAT)

s is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

Seg s is finite V39(s) Element of K6(NAT)

{ b

dom (E,S) is set

E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,S) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

len (E,S) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len S is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(E,S) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

len (E,S) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

dom (E,S) is Element of K6(NAT)

dom S is Element of K6(NAT)

dom (E,S) is Element of K6(NAT)

E is set

<%> E is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural 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 FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V60() V81() irreflexive () Element of K237(E)

K237(E) is non empty functional M11(E)

S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

((<%> E),S) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

((<%> E),S) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

s is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

dom S is Element of K6(NAT)

((<%> E),S) . s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S . s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

{} ^ (S . s) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

dom ((<%> E),S) is Element of K6(NAT)

s is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

((<%> E),S) . s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S . s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S . s) ^ {} is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

dom ((<%> E),S) is Element of K6(NAT)

E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ S is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(S,s) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,(S,s)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

((E ^ S),s) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(S,s) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,(S,s)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

((S ^ E),s) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

dom (E,(S,s)) is Element of K6(NAT)

dom (S,s) is Element of K6(NAT)

dom s is Element of K6(NAT)

(E,(S,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S,s) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ ((S,s) . t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S ^ (s . t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ (S ^ (s . t)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E ^ S) ^ (s . t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E ^ S),s) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

dom ((E ^ S),s) is Element of K6(NAT)

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

dom (E,(S,s)) is Element of K6(NAT)

dom (S,s) is Element of K6(NAT)

(E,(S,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S,s) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((S,s) . t) ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(s . t) ^ S is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((s . t) ^ S) ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(s . t) ^ (S ^ E) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((S ^ E),s) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

dom ((S ^ E),s) is Element of K6(NAT)

E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(S,s) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,(S,s)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,s) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(S,(E,s)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

dom (E,(S,s)) is Element of K6(NAT)

dom (S,s) is Element of K6(NAT)

dom s is Element of K6(NAT)

dom (E,s) is Element of K6(NAT)

(E,(S,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S,s) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ ((S,s) . t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(s . t) ^ S is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ ((s . t) ^ S) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ (s . t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E ^ (s . t)) ^ S is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E,s) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,s) . t) ^ S is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S,(E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

dom (S,(E,s)) is Element of K6(NAT)

E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,S) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,S) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

S ^ s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,(S ^ s)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,s) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,S) ^ (E,s) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,(S ^ s)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,s) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

(E,S) ^ (E,s) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

dom (E,(S ^ s)) is Element of K6(NAT)

dom (S ^ s) is Element of K6(NAT)

dom S is Element of K6(NAT)

dom (E,S) is Element of K6(NAT)

(E,(S ^ s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S ^ s) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ ((S ^ s) . t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ (S . t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E,S) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

dom S is Element of K6(NAT)

len (S ^ s) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len S is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len s is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

(len S) + w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

dom s is Element of K6(NAT)

dom (E,s) is Element of K6(NAT)

len (E,S) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(E,(S ^ s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S ^ s) . ((len S) + w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ ((S ^ s) . ((len S) + w)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

E ^ (s . w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E,s) . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

dom S is Element of K6(NAT)

(E,(S ^ s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E,(S ^ s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

len (E,(S ^ s)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len (S ^ s) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len S is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len s is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(len S) + (len s) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len (E,S) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(len (E,S)) + (len s) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len (E,s) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(len (E,S)) + (len (E,s)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len ((E,S) ^ (E,s)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

dom ((E,S) ^ (E,s)) is Element of K6(NAT)

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

dom (E,(S ^ s)) is Element of K6(NAT)

dom S is Element of K6(NAT)

dom (E,S) is Element of K6(NAT)

(E,(S ^ s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S ^ s) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((S ^ s) . t) ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

S . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S . t) ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E,S) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

dom S is Element of K6(NAT)

w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

(len S) + w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

dom s is Element of K6(NAT)

dom (E,s) is Element of K6(NAT)

len (E,S) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(E,(S ^ s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(S ^ s) . ((len S) + w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((S ^ s) . ((len S) + w)) ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

s . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(s . w) ^ E is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E,s) . w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

dom S is Element of K6(NAT)

(E,(S ^ s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E,(S ^ s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

((E,S) ^ (E,s)) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

len (E,(S ^ s)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len (E,S) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(len (E,S)) + (len s) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len (E,s) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(len (E,S)) + (len (E,s)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len ((E,S) ^ (E,s)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

dom ((E,S) ^ (E,s)) is Element of K6(NAT)

E is set

E ^omega is non empty functional set

S is Relation-like NAT -defined E ^omega -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of E ^omega

s is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

S . s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

dom S is Element of K6(NAT)

dom S is Element of K6(NAT)

dom S is Element of K6(NAT)

E is set

E ^omega is non empty functional set

S is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

s is Relation-like NAT -defined E ^omega -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of E ^omega

(S,s) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

dom (S,s) is Element of K6(NAT)

dom s is Element of K6(NAT)

(S,s) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E,s,t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

S ^ (E,s,t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

(S,s) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set

t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set

dom (S,s) is Element of K6(NAT)

dom s is Element of K6(NAT)

(S,s) . t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

(E,s,t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(E,s,t) ^ S is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

E is Relation-like set

E ~ is Relation-like set

E \/ (E ~) is Relation-like set

(E ~) ~ is Relation-like set

((E ~) ~) \/ (E ~) is Relation-like set

(((E ~) ~) \/ (E ~)) ~ is Relation-like set

(E \/ (E ~)) ~ is Relation-like set

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

the Relation-like Element of K6(([#] ((E ^omega),(E ^omega)))) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

the Relation-like Element of K6(([#] ((E ^omega),(E ^omega)))) ~ is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

the Relation-like Element of K6(([#] ((E ^omega),(E ^omega)))) \/ ( the Relation-like Element of K6(([#] ((E ^omega),(E ^omega)))) ~) is Relation-like symmetric Element of K6(([#] ((E ^omega),(E ^omega))))

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

K237(E) is non empty functional M11(E)

<%> E is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural 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 FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V60() V81() irreflexive () Element of K237(E)

w is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural 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 FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V60() V81() irreflexive () Element of K237(E)

{} ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

({} ^ t) ^ {} is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

w ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(w ^ t) ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

{} ^ s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

({} ^ s) ^ {} is T-Sequence-like Relation-like NAT -defined Function-like finite V60() set

w ^ s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(w ^ s) ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(t ^ x) ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(t ^ u) ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w ^ s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

w ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

s ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

t ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(x ^ t) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(x ^ u) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

w ^ (x ^ u) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(w ^ (x ^ u)) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

w ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(w ^ x) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

((w ^ x) ^ u) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

w ^ (x ^ t) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(w ^ (x ^ t)) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(w ^ x) ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

((w ^ x) ^ t) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

u ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(x ^ t) ^ (u ^ w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(x ^ u) ^ (u ^ w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w ^ s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

w ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(w ^ s) ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(w ^ t) ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w ^ s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

w ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

s ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

t ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w ^ s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

w ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(w ^ s) ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(w ^ t) ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

S ~ is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

[s,t] is Element of [#] ((E ^omega),(E ^omega))

{s,t} is non empty functional set

{s} is non empty functional set

{{s,t},{s}} is non empty set

[t,s] is Element of [#] ((E ^omega),(E ^omega))

{t,s} is non empty functional set

{t} is non empty functional set

{{t,s},{t}} is non empty set

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(w ^ u) ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(w ^ t) ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

[t,w] is Element of [#] ((E ^omega),(E ^omega))

{t,w} is non empty functional set

{t} is non empty functional set

{{t,w},{t}} is non empty set

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(x ^ t) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(x ^ u) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

E is set

E ^omega is non empty functional set

{} ((E ^omega),(E ^omega)) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(t ^ x) ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(t ^ u) ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

[x,u] is Element of [#] ((E ^omega),(E ^omega))

{x,u} is non empty functional set

{x} is non empty functional set

{{x,u},{x}} is non empty set

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

S \/ s is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(x ^ t) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(x ^ u) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

[t,u] is Element of [#] ((E ^omega),(E ^omega))

{t,u} is non empty functional set

{t} is non empty functional set

{{t,u},{t}} is non empty set

E is set

id E is Relation-like E -defined E -valued Function-like one-to-one set

[#] (E,E) is Relation-like set

K6(([#] (E,E))) is set

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

[t,w] is Element of [#] ((E ^omega),(E ^omega))

{t,w} is non empty functional set

{t} is non empty functional set

{{t,w},{t}} is non empty set

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

[x,u] is Element of [#] ((E ^omega),(E ^omega))

{x,u} is non empty functional set

{x} is non empty functional set

{{x,u},{x}} is non empty set

s is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

t is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

[w,x] is Element of [#] ((E ^omega),(E ^omega))

{w,x} is non empty functional set

{w} is non empty functional set

{{w,x},{w}} is non empty set

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is set

t is set

w is set

[t,w] is set

{t,w} is non empty set

{t} is non empty set

{{t,w},{t}} is non empty set

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is Relation-like NAT -defined E ^omega -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of E ^omega

(E,s,t) is Relation-like NAT -defined E ^omega -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of E ^omega

(E,s,t) is Relation-like NAT -defined E ^omega -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of E ^omega

w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

dom (E,s,t) is Element of K6(NAT)

w + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() Element of NAT

dom t is Element of K6(NAT)

(E,(E,s,t),(w + 1)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(E,t,(w + 1)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(E,t,(w + 1)) ^ s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

(E,t,w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

[(E,t,w),(E,t,(w + 1))] is Element of [#] ((E ^omega),(E ^omega))

{(E,t,w),(E,t,(w + 1))} is non empty functional set

{(E,t,w)} is non empty functional set

{{(E,t,w),(E,t,(w + 1))},{(E,t,w)}} is non empty set

(E,t,w) ^ s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(E,(E,s,t),w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

[(E,(E,s,t),w),(E,(E,s,t),(w + 1))] is Element of [#] ((E ^omega),(E ^omega))

{(E,(E,s,t),w),(E,(E,s,t),(w + 1))} is non empty functional set

{(E,(E,s,t),w)} is non empty functional set

{{(E,(E,s,t),w),(E,(E,s,t),(w + 1))},{(E,(E,s,t),w)}} is non empty set

w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

dom (E,s,t) is Element of K6(NAT)

w + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() Element of NAT

(E,(E,s,t),(w + 1)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(E,t,(w + 1)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

s ^ (E,t,(w + 1)) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(E,t,w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

[(E,t,w),(E,t,(w + 1))] is Element of [#] ((E ^omega),(E ^omega))

{(E,t,w),(E,t,(w + 1))} is non empty functional set

{(E,t,w)} is non empty functional set

{{(E,t,w),(E,t,(w + 1))},{(E,t,w)}} is non empty set

s ^ (E,t,w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(E,(E,s,t),w) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

[(E,(E,s,t),w),(E,(E,s,t),(w + 1))] is Element of [#] ((E ^omega),(E ^omega))

{(E,(E,s,t),w),(E,(E,s,t),(w + 1))} is non empty functional set

{(E,(E,s,t),w)} is non empty functional set

{{(E,(E,s,t),w),(E,(E,s,t),(w + 1))},{(E,(E,s,t),w)}} is non empty set

len (E,s,t) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len (E,s,t) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is Relation-like NAT -defined E ^omega -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of E ^omega

(E,s,w) is Relation-like NAT -defined E ^omega -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of E ^omega

(E,t,(E,s,w)) is Relation-like NAT -defined E ^omega -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of E ^omega

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,S) ~ is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is set

t is set

w is set

[t,w] is set

{t,w} is non empty set

{t} is non empty set

{{t,w},{t}} is non empty set

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

[u,x] is Element of [#] ((E ^omega),(E ^omega))

{u,x} is non empty functional set

{u} is non empty functional set

{{u,x},{u}} is non empty set

t is set

w is set

[t,w] is set

{t,w} is non empty set

{t} is non empty set

{{t,w},{t}} is non empty set

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

[u,x] is Element of [#] ((E ^omega),(E ^omega))

{u,x} is non empty functional set

{u} is non empty functional set

{{u,x},{u}} is non empty set

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,s) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

t is set

w is set

x is set

[w,x] is set

{w,x} is non empty set

{w} is non empty set

{{w,x},{w}} is non empty set

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

E is set

E ^omega is non empty functional set

((E ^omega)) is Relation-like E ^omega -defined E ^omega -valued Function-like one-to-one Element of K6(([#] ((E ^omega),(E ^omega))))

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

(E,((E ^omega))) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

S is set

s is set

t is set

[s,t] is set

{s,t} is non empty set

{s} is non empty set

{{s,t},{s}} is non empty set

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

u ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(u ^ u) ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

u ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(u ^ u) ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

[u,u] is Element of [#] ((E ^omega),(E ^omega))

{u,u} is non empty functional set

{u} is non empty functional set

{{u,u},{u}} is non empty set

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

((E ^omega)) is Relation-like E ^omega -defined E ^omega -valued Function-like one-to-one Element of K6(([#] ((E ^omega),(E ^omega))))

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

S \/ ((E ^omega)) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,(S \/ ((E ^omega)))) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,S) \/ ((E ^omega)) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is set

t is set

w is set

[t,w] is set

{t,w} is non empty set

{t} is non empty set

{{t,w},{t}} is non empty set

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(t ^ u) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(t ^ w) ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

[u,w] is Element of [#] ((E ^omega),(E ^omega))

{u,w} is non empty functional set

{u} is non empty functional set

{{u,w},{u}} is non empty set

s is set

(E,((E ^omega))) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

E is set

E ^omega is non empty functional set

{} ((E ^omega),(E ^omega)) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

(E,({} ((E ^omega),(E ^omega)))) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

S is set

s is set

t is set

[s,t] is set

{s,t} is non empty set

{s} is non empty set

{{s,t},{s}} is non empty set

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w ^ u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(w ^ u) ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(w ^ t) ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

[u,t] is Element of [#] ((E ^omega),(E ^omega))

{u,t} is non empty functional set

{u} is non empty functional set

{{u,t},{u}} is non empty set

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

(E,(E,S)) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is set

t is set

w is set

[t,w] is set

{t,w} is non empty set

{t} is non empty set

{{t,w},{t}} is non empty set

x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

[s,t] is Element of [#] ((E ^omega),(E ^omega))

{s,t} is non empty functional set

{s} is non empty functional set

{{s,t},{s}} is non empty set

(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

E is set

E ^omega is non empty functional set

[#] ((E ^omega),(E ^omega)) is Relation-like set

K6(([#] ((E ^omega),(E ^omega)))) is set

S is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

s ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

K237(E) is non empty functional M11(E)

t ^ w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

w ^ s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

w ^ t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)

(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))

x is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,S)

x . 1 is set

len x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

x . (len x) is set

u is Relation-like NAT -defined E ^omega -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of E ^omega

dom u is Element of K6(NAT)

(E,w,u) is Relation-like NAT -defined E ^omega -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of E ^omega

(E,(E,w,u),1) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

len u is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

len (E,w,u) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT

(E,(E,w,u),(len (E,w,u))) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega

(E,w,u) is Relation-like NAT -defined E ^omega -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of E ^omega

(E,(E</