:: 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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty set
Seg 2 is non empty finite V39(2) Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT : ( 1 <= b₁ & b₁ <= E ) } is set
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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT : ( 1 <= b₁ & b₁ <= E ) } is set
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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT : ( 1 <= b₁ & b₁ <= s ) } is set
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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT : ( 1 <= b₁ & b₁ <= s ) } is set
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,w,u),1) is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
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 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
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)
w ^ s 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 ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of K237(E)
x ^ t 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)
w ^ t 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
(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))
w is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,S)
w . 1 is set
len w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
w . (len w) is set
Rev w is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Rev w) . (len w) is set
len (Rev w) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
(Rev w) . (len (Rev w)) is set
(E,S) ~ is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))
(Rev w) . 1 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
(E,S) is Relation-like Element of K6(([#] ((E ^omega),(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
((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))))
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,(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))))
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
(E,({} ((E ^omega),(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 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
(E,(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
{[s,t]} is non empty Relation-like Function-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
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
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
{[s,t]} is non empty Relation-like Function-like Element of K6(([#] ((E ^omega),(E ^omega))))
S \/ {[s,t]} is non empty 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
(E,(S \/ {[s,t]})) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))
(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))
u is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set
u + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() Element of NAT
t is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,(S \/ {[s,t]}))
len t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
t . 1 is set
t . (len t) is set
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
dom t is non empty Element of K6(NAT)
<*u*> is non empty Relation-like NAT -defined E ^omega -valued Function-like finite V39(1) FinSequence-like FinSubsequence-like () FinSequence of E ^omega
[1,u] is set
{1,u} is non empty set
{{1,u},{1}} is non empty set
{[1,u]} is non empty Relation-like Function-like set
w is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,S)
w . 1 is set
len w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
w . (len w) is set
dom t is non empty Element of K6(NAT)
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() Element of NAT
dom t is non empty Element of K6(NAT)
t . u is set
t . (u + 1) is set
[(t . u),(t . (u + 1))] is set
{(t . u),(t . (u + 1))} is non empty set
{(t . u)} is non empty set
{{(t . u),(t . (u + 1))},{(t . u)}} is non empty set
w is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
c₁₃ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,(S \/ {[s,t]}))
len c₁₃ is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
c₁₃ . 1 is set
c₁₃ . (len c₁₃) is set
c₁₃ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,S)
c₁₃ . 1 is set
len c₁₃ is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
c₁₃ . (len c₁₃) is set
dom t is non empty Element of K6(NAT)
u is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,(S \/ {[s,t]}))
len u is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
u . 1 is set
t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
u . (len u) is set
u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
u is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,(S \/ {[s,t]}))
u . 1 is set
len u is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
u . (len u) is set
u is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,S)
u . 1 is set
len u is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
u . (len u) 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
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,s,b₁) } is set
K6((E ^omega)) is set
w is set
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))))
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,S,t) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,t,b₁) } is set
w 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
(E,S,s) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,s,b₁) } is set
E is non empty 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,s) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,s,b₁) } 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
(E,S,t) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,t,b₁) } is set
(E,s,t) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,s,t,b₁) } is set
w is set
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
((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))))
s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
(E,S,s) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,s,b₁) } is set
(E,(S \/ ((E ^omega))),s) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S \/ ((E ^omega)),s,b₁) } is set
t is set
w 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 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
(E,({} ((E ^omega),(E ^omega))),S) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E, {} ((E ^omega),(E ^omega)),S,b₁) } is set
{S} is non empty functional Element of K6(K237(E))
K237(E) is non empty functional M11(E)
K6(K237(E)) is set
s is set
t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
s is set
t is set
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
S is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
(E,((E ^omega)),S) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,((E ^omega)),S,b₁) } is set
{S} is non empty functional Element of K6(K237(E))
K237(E) is non empty functional M11(E)
K6(K237(E)) is set
{} ((E ^omega),(E ^omega)) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))
({} ((E ^omega),(E ^omega))) \/ ((E ^omega)) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))
{} \/ ((E ^omega)) is Relation-like set
(E,({} ((E ^omega),(E ^omega))),S) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E, {} ((E ^omega),(E ^omega)),S,b₁) } 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
(E,S,s) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,s,b₁) } 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
(E,S,t) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,t,b₁) } is set
(E,s,t) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,s,t,b₁) } 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 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
(E,S,w) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,w,b₁) } is set
(E,s,w) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,s,w,b₁) } is set
(E,t,w) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,t,w,b₁) } 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 ^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))))
s is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
(E,S,s) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,s,b₁) } is set
(E,(S \/ ((E ^omega))),s) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S \/ ((E ^omega)),s,b₁) } 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 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
(E,S,w) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,w,b₁) } is set
(E,s,w) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,s,w,b₁) } is set
(E,t,w) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,t,w,b₁) } 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))))
(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
(E,(E,S),s) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,(E,S),s,b₁) } is set
(E,S,s) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,s,b₁) } is set
t is set
w 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 Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))
S \/ s is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))
(E,(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
(E,S,t) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,t,b₁) } is set
(E,s,t) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,s,t,b₁) } is set
x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() Element of NAT
u is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,(S \/ s))
len u is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
u . 1 is set
u . (len u) is set
t is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
dom u is non empty Element of K6(NAT)
<*t*> is non empty Relation-like NAT -defined E ^omega -valued Function-like finite V39(1) FinSequence-like FinSubsequence-like () FinSequence of E ^omega
[1,t] is set
{1,t} is non empty set
{{1,t},{1}} is non empty set
{[1,t]} is non empty Relation-like Function-like set
u is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,S)
u . 1 is set
len u is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
u . (len u) is set
dom u is non empty Element of K6(NAT)
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative V81() Element of NAT
dom u is non empty Element of K6(NAT)
u . x is set
u . (x + 1) is set
[(u . x),(u . (x + 1))] is set
{(u . x),(u . (x + 1))} is non empty set
{(u . x)} is non empty set
{{(u . x),(u . (x + 1))},{(u . x)}} is non empty set
u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
w is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,(S \/ s))
len w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
w . 1 is set
w . (len w) is set
w is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,S)
w . 1 is set
len w is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
w . (len w) is set
dom u is non empty Element of K6(NAT)
x is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,(S \/ s))
len x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative V81() Element of NAT
x . 1 is set
x . (len x) is set
u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega
x is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like RedSequence of (E,(S \/ 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
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
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
(E,(S \/ s)) is Relation-like Element of K6(([#] ((E ^omega),(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 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
(E,(S \/ s),t) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S \/ s,t,b₁) } is set
(E,S,t) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,t,b₁) } is set
w is set
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))))
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
{[s,t]} is non empty Relation-like Function-like Element of K6(([#] ((E ^omega),(E ^omega))))
S \/ {[s,t]} is non empty 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
(E,S) is Relation-like Element of K6(([#] ((E ^omega),(E ^omega))))
S \/ (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
{[s,t]} is non empty Relation-like Function-like Element of K6(([#] ((E ^omega),(E ^omega))))
S \/ {[s,t]} is non empty 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
(E,(S \/ {[s,t]}),w) is functional Element of K6((E ^omega))
K6((E ^omega)) is set
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S \/ {[s,t]},w,b₁) } is set
(E,S,w) is functional Element of K6((E ^omega))
{ b₁ where b₁ is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega : (E,S,w,b₁) } is set
x is set
u is T-Sequence-like Relation-like NAT -defined Function-like finite V60() Element of E ^omega