REAL is non empty non trivial non finite set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty non trivial non finite set
omega is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
the Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty proper Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of NAT
[:NAT,NAT:] is Relation-like non empty non trivial non finite set
union {} is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
card {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y ^ D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y ^ D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
Seg X is finite X -element Element of bool NAT
Y | (Seg X) is Relation-like NAT -defined Seg X -defined NAT -defined Function-like finite FinSubsequence-like set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f . 1 is set
<*(f . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
B ^ <*(f . 1)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X + (len f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is set
<*X*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y ^ <*X*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
ProperPrefixes (Y ^ <*X*>) is finite set
ProperPrefixes Y is finite set
{Y} is functional non empty trivial finite V42() 1 -element set
(ProperPrefixes Y) \/ {Y} is non empty finite set
B is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
F1() is non empty Tree-like set
X is set
card X is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F1()
len X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F1()
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is set
<*f*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
B ^ <*f*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
rng <*f*> is non empty trivial finite 1 -element set
rng Y is finite Element of bool NAT
{f} is non empty trivial finite 1 -element set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F1()
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F1()
len X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is non empty Tree-like set
Y is non empty Tree-like set
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of Y
X is non empty Tree-like set
Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X | Y is non empty Tree-like set
X with-replacement (Y,(X | Y)) is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng f is finite set
rng B is finite Element of bool NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X with-replacement (B,Y) is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is non empty Tree-like set
B is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X with-replacement (f,Y) is non empty Tree-like set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(X with-replacement (f,Y)) with-replacement (D,B) is non empty Tree-like set
X with-replacement (D,B) is non empty Tree-like set
(X with-replacement (D,B)) with-replacement (f,Y) is non empty Tree-like set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{{}} is functional non empty trivial finite V42() 1 -element Tree-like set
X is non empty Tree-like set
<*0*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
Y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
bool X is non empty set
Y is Element of bool X
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{{}} is functional non empty trivial finite V42() 1 -element Tree-like set
Y is Element of bool X
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = 0 } is set
B is set
len {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is (X)
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = B } is set
f is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len Y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of X
B is (X)
Y /\ B is Element of bool X
bool X is non empty set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
{ the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X} is functional non empty trivial finite V42() 1 -element set
the Element of Y /\ B is Element of Y /\ B
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
{g} is functional non empty trivial finite V42() 1 -element set
y is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
{D} is functional non empty trivial finite V42() 1 -element set
X is non empty Tree-like set
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = Y } is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : S1[b1] } is set
bool X is non empty set
X is non empty Tree-like set
f is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*B*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*B*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of f
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(f,D) is Element of bool f
bool f is non empty set
{ (D ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : D ^ <*b1*> in f } is set
X is non empty Tree-like set
(X,1) is (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = 1 } is set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f . 1 is set
<*(f . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
rng f is finite Element of bool NAT
{(f . 1)} is non empty trivial finite 1 -element set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
len <*f*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
X is non empty Tree-like set
{ (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : verum } is set
union { (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : verum } is set
Y is set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,(len B)) is (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = len B } is set
Y is set
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,f) is (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = f } is set
X is non empty finite Tree-like set
height X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
{ (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 <= height X } is set
union { (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 <= height X } is set
Y is set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,(len B)) is finite (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = len B } is set
Y is set
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,f) is finite (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = f } is set
X is non empty Tree-like set
Y is (X)
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = B } is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,f) is (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = f } is set
F1() is non empty set
F2() is set
{ F3(b1) where b1 is Element of F1() : b1 in F2() } is set
card { F3(b1) where b1 is Element of F1() : b1 in F2() } is epsilon-transitive epsilon-connected ordinal cardinal set
card F2() is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like set
dom X is set
rng X is set
Y is set
B is Element of F1()
F3(B) is set
X . B is set
F3() is finite set
F1() is non empty set
F2() is finite set
{ F4(b1) where b1 is Element of F1() : b1 in F2() } is set
card F3() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
card F2() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
card { F4(b1) where b1 is Element of F1() : b1 in F2() } is epsilon-transitive epsilon-connected ordinal cardinal set
X is non empty Tree-like set
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*Y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Seg Y is finite Y -element Element of bool NAT
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,B) is Element of bool X
bool X is non empty set
{ (B ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : B ^ <*b1*> in X } is set
{ H1(b1) where b1 is ext-real V36() V37() Element of REAL : b1 in Seg Y } is set
{ (B ^ <*(b1 - 1)*>) where b1 is ext-real V36() V37() Element of REAL : b1 in Seg Y } is set
f is set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
B ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B ^ <*Y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
D + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(D + 1) - 1 is ext-real V36() V37() Element of REAL
f is finite set
card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
x is finite set
card x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
card (Seg Y) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is finite set
card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
X is non empty Tree-like () set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
X is non empty Tree-like set
bool X is non empty set
Y is Element of bool X
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{{}} is functional non empty trivial finite V42() 1 -element Tree-like set
X is non empty Tree-like set
bool X is non empty set
Y is Element of bool X
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
X is non empty Tree-like set
X is non empty Tree-like set
bool X is non empty set
Y is set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes B is finite set
B is set
union B is set
f is set
D is set
f is Element of bool X
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is set
y is set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is set
ProperPrefixes D is finite set
B is set
f is (X)
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes D is finite set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes D is finite set
{D} is functional non empty trivial finite V42() 1 -element set
(ProperPrefixes D) \/ {D} is non empty finite set
g is Element of bool X
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes y is finite set
y is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
X is non empty Tree-like set
Y is (X)
the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
ProperPrefixes B is finite set
f is (X)
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
X is non empty Tree-like set
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
ProperPrefixes f is finite set
D is (X)
ProperPrefixes B is finite set
X is non empty Tree-like set
Y is (X)
X is non empty Tree-like set
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is finite (X)
card B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
the Element of B is Element of B
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
Seg f is finite f -element Element of bool NAT
D | (Seg f) is Relation-like NAT -defined Seg f -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
ProperPrefixes x is finite set
card (ProperPrefixes x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
B \ (ProperPrefixes x) is finite Element of bool X
bool X is non empty set
the Element of B \ (ProperPrefixes x) is Element of B \ (ProperPrefixes x)
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
{y} is functional non empty trivial finite V42() 1 -element set
(ProperPrefixes x) \/ {y} is non empty finite set
card ((ProperPrefixes x) \/ {y}) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of omega
B \ ((ProperPrefixes x) \/ {y}) is finite Element of bool X
the Element of B \ ((ProperPrefixes x) \/ {y}) is Element of B \ ((ProperPrefixes x) \/ {y})
T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is non empty Tree-like set
Y is (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT st
( b2 in Y & b1 c= b2 ) } is set
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
bool X is non empty set
B is Element of bool X
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is non empty (X) (X)
ProperPrefixes B is finite set
X is non empty Tree-like set
Y is non empty (X) (X)
the Element of Y is Element of Y
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is (X)
ProperPrefixes Y is finite set
X is non empty Tree-like set
Y is (X)
bool X is non empty set
B is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT st
( b2 in Y & b1 c= b2 ) } is set
D is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes D is finite set
g is set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is set
union D is set
x is set
g is set
x is Element of bool X
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is set
T1 is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is set
ProperPrefixes g is finite set
the Element of D is Element of D
D is set
x is (X)
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes g is finite set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes g is finite set
{g} is functional non empty trivial finite V42() 1 -element set
(ProperPrefixes g) \/ {g} is non empty finite set
y is Element of bool X
T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes T1 is finite set
T1 is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
g is non empty (X) (X)
F1() is set
X is set
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is set
X /\ NAT is Element of bool REAL
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X /\ NAT is Element of bool REAL
Y is finite set
B is set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X /\ NAT is Element of bool REAL
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
F2() is set
F1() is set
X is set
Y is set
B is set
Y is Relation-like Function-like set
dom Y is set
B is Relation-like Function-like set
dom B is set
B . 0 is set
rng B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . f is set
f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . (f + 1) is set
Y . (B . f) is set
f is set
D is set
B . D is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . x is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . f is set
f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . (f + 1) is set
Y . (B . f) is set
X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
len (Y ^ <*f*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len (Y ^ <*f*>)) + D is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is non empty (X) (X)
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len g) + D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is Relation-like Function-like set
dom B is set
rng B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len Y) + (f + 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
D is non empty (X) (X)
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len Y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
Seg ((len Y) + 1) is non empty finite (len Y) + 1 -element Element of bool NAT
x | (Seg ((len Y) + 1)) is Relation-like NAT -defined Seg ((len Y) + 1) -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
((len Y) + 1) + f is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y ^ y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len Y) + (len y) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y . 1 is set
<*(y . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
dom g is finite Element of bool NAT
Seg (len g) is finite len g -element Element of bool NAT
1 + (len Y) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
Y ^ <*(y . 1)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(Y ^ <*(y . 1)*>) . ((len Y) + 1) is set
rng g is finite Element of bool NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . (Y ^ <*y*>) is set
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len g) + T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len Y) + B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
f is finite (X)
card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
D is non empty (X) (X)
B + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
len (f ^ <*D*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
x is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len g) + y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is Relation-like Function-like set
dom B is set
rng B is set
B . 0 is set
B is Relation-like Function-like set
dom B is set
rng B is set
B . 0 is set
bool X is non empty set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
B . D is set
D + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
B . (D + 0) is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
D + x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
B . (D + x) is set
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
D + (x + 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal set
B . (D + (x + 1)) is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D + (x + 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . (D + (x + 1)) is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y + T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . (y + T1) is set
(y + T1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . ((y + T1) + 1) is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
T2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*T2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
k1 ^ <*T2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . D is set
B . x is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
D + y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is Element of bool X
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is set
B . g is set
y is set
B . y is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is (X)
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . x is set
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . (x + 1) is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len <*y*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len y) + (len <*y*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
x is set
B . x is set
g is set
B . g is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . y is set
y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . (y + 1) is set
T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*k1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T1 ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . y is set
y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . (y + 1) is set
len T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*k2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ <*k2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like () set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,Y) is finite Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
the non empty Tree-like set is non empty Tree-like set
[: the non empty Tree-like set ,NAT:] is Relation-like non empty non trivial non finite set
bool [: the non empty Tree-like set ,NAT:] is non empty non trivial non finite set
the non empty Tree-like set --> 0 is Relation-like the non empty Tree-like set -defined NAT -valued Function-like constant non empty total V25( the non empty Tree-like set , NAT ) Function-yielding V32() Element of bool [: the non empty Tree-like set ,NAT:]
Y is Relation-like the non empty Tree-like set -defined NAT -valued Function-like constant non empty total V25( the non empty Tree-like set , NAT ) Function-yielding V32() Element of bool [: the non empty Tree-like set ,NAT:]
dom Y is non empty Element of bool the non empty Tree-like set
bool the non empty Tree-like set is non empty set
X is Relation-like Function-like () set
dom X is set
X is non empty set
the non empty Tree-like set is non empty Tree-like set
the Element of X is Element of X
the non empty Tree-like set --> the Element of X is Relation-like the non empty Tree-like set -defined X -valued Function-like constant non empty total V25( the non empty Tree-like set ,X) Element of bool [: the non empty Tree-like set ,X:]
[: the non empty Tree-like set ,X:] is Relation-like non empty set
bool [: the non empty Tree-like set ,X:] is non empty set
dom ( the non empty Tree-like set --> the Element of X) is non empty Element of bool the non empty Tree-like set
bool the non empty Tree-like set is non empty set
D is Relation-like Function-like () set
X is non empty set
Y is Relation-like X -valued Function-like () set
dom Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
Y . B is set
rng Y is Element of bool X
bool X is non empty set
X is Relation-like Function-like () set
dom X is non empty Tree-like set
Y is Relation-like Function-like () set
dom Y is non empty Tree-like set
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom X
X . f is set
Y . f is set
X . B is set
Y . B is set
F1() is non empty Tree-like set
X is set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F1()
B is set
X is Relation-like Function-like set
dom X is set
Y is Relation-like Function-like () set
dom Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . B is set
F1() is non empty Tree-like set
X is Relation-like Function-like set
dom X is set
Y is Relation-like Function-like () set
dom Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . B is set
F2(B) is set
X is Relation-like Function-like () set
dom X is non empty Tree-like set
Leaves (dom X) is Element of bool (dom X)
bool (dom X) is non empty set
X .: (Leaves (dom X)) is set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(dom X) | Y is non empty Tree-like set
B is Relation-like Function-like () set
dom B is non empty Tree-like set
f is Relation-like Function-like () set
dom f is non empty Tree-like set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . D is set
Y ^ D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X . (Y ^ D) is set
f . D is set
X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y is Relation-like Function-like () set
dom Y is non empty Tree-like set
(Y,X) is Relation-like Function-like () set
rng (Y,X) is set
rng Y is set
B is set
dom (Y,X) is non empty Tree-like set
f is set
(Y,X) . f is set
(dom Y) | X is non empty Tree-like set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom (Y,X)
X ^ D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . (X ^ D) is set
X is non empty set
Y is Relation-like X -valued Function-like () set
(Y) is set
dom Y is non empty Tree-like set
Leaves (dom Y) is Element of bool (dom Y)
bool (dom Y) is non empty set
Y .: (Leaves (dom Y)) is set
bool X is non empty set
rng Y is Element of bool X
X is non empty set
Y is Relation-like X -valued Function-like () set
dom Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
(Y,B) is Relation-like Function-like () set
rng (Y,B) is set
rng Y is Element of bool X
bool X is non empty set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is Relation-like Function-like () set
dom X is non empty Tree-like set
B is Relation-like Function-like () set
dom B is non empty Tree-like set
(dom X) with-replacement (Y,(dom B)) is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X . f is set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . D is set
{} NAT is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty proper Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of bool NAT
B . ({} NAT) is set
Y ^ (<*> NAT) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is set
B . g is set
f is Relation-like Function-like () set
dom f is non empty Tree-like set
D is Relation-like Function-like () set
dom D is non empty Tree-like set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f . x is set
D . x is set
X . x is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . g is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . y is set
X is non empty Tree-like set
Y is set
X --> Y is Relation-like X -defined {Y} -valued Function-like constant non empty total V25(X,{Y}) Element of bool [:X,{Y}:]
{Y} is non empty trivial finite 1 -element set
[:X,{Y}:] is Relation-like non empty set
bool [:X,{Y}:] is non empty set
dom (X --> Y) is non empty Element of bool X
bool X is non empty set
X is non empty set
union X is set
the Element of X is Element of X
Y is non empty Tree-like set
B is non empty set
f is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes f is finite set
D is set
x is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is set
y is non empty Tree-like set
X is set
union X is set
Y is set
B is set
f is Relation-like Function-like set
Y is set
B is set
[Y,B] is set
{Y,B} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,B},{Y}} is non empty finite V42() set
f is set
[Y,f] is set
{Y,f} is non empty finite set
{{Y,f},{Y}} is non empty finite V42() set
D is set
x is set
g is Relation-like Function-like set
y is Relation-like Function-like set
X is non empty set
union X is set
Y is set
B is set
f is Relation-like Function-like () set
dom f is non empty Tree-like set
B is Relation-like Function-like set
dom B is set
rng B is set
D is set
f is non empty set
x is set
B . x is set
g is Relation-like Function-like () set
dom g is non empty Tree-like set
union f is set
Y is Relation-like Function-like set
dom Y is set
D is set
x is set
[D,x] is set
{D,x} is non empty finite set
{D} is non empty trivial finite 1 -element set
{{D,x},{D}} is non empty finite V42() set
g is set
B . g is set
y is Relation-like Function-like () set
dom y is non empty Tree-like set
D is set
x is set
g is set
B . g is set
y is Relation-like Function-like () set
dom y is non empty Tree-like set
y . D is set
[D,(y . D)] is set
{D,(y . D)} is non empty finite set
{D} is non empty trivial finite 1 -element set
{{D,(y . D)},{D}} is non empty finite V42() set
X is non empty set
union X is set
Y is non empty set
B is set
B is Relation-like Function-like () set
rng B is set
f is set
dom B is non empty Tree-like set
D is set
B . D is set
[D,f] is set
{D,f} is non empty finite set
{D} is non empty trivial finite 1 -element set
{{D,f},{D}} is non empty finite V42() set
x is set
g is Relation-like Y -valued Function-like () set
dom g is non empty Tree-like set
g . D is set
rng g is Element of bool Y
bool Y is non empty set
F1() is non empty set
[:F1(),NAT:] is Relation-like non empty non trivial non finite set
[:[:F1(),NAT:],F1():] is Relation-like non empty non trivial non finite set
bool [:[:F1(),NAT:],F1():] is non empty non trivial non finite set
F2() is Element of F1()
F4() is Relation-like [:F1(),NAT:] -defined F1() -valued Function-like V25([:F1(),NAT:],F1()) Element of bool [:[:F1(),NAT:],F1():]
X is non empty Tree-like set
[:X,F1():] is Relation-like non empty set
bool [:X,F1():] is non empty set
X --> F2() is Relation-like X -defined F1() -valued Function-like constant non empty total V25(X,F1()) () Element of bool [:X,F1():]
Y is Relation-like X -defined F1() -valued Function-like constant non empty total V25(X,F1()) () Element of bool [:X,F1():]
Y . {} is set
dom Y is non empty Tree-like set
dom Y is non empty Tree-like Element of bool X
bool X is non empty set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
((dom Y),B) is Element of bool (dom Y)
bool (dom Y) is non empty set
{ (B ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : B ^ <*b1*> in dom Y } is set
(F1(),Y,B) is Element of F1()
F3((F1(),Y,B)) is set
{ (B ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 in F3((F1(),Y,B)) } is set
D is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
F3(D) is set
<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
B ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . (B ^ <*f*>) is set
F4() . (D,f) is set
[D,f] is set
{D,f} is non empty finite set
{D} is non empty trivial finite 1 -element set
{{D,f},{D}} is non empty finite V42() set
F4() . [D,f] is set
X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
Y is Relation-like F1() -valued Function-like () set
Y . {} is set
dom Y is non empty Tree-like set
{ (b2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT , b2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y : b1 in F3((F1(),Y,b2)) } is set
{ (b2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT , b2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y : b1 in F3((F1(),Y,b2)) } \/ (dom Y) is non empty set
B is non empty set
f is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,x) is Element of F1()
F3((F1(),Y,x)) is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes f is finite set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,x) is Element of F1()
F3((F1(),Y,x)) is set
ProperPrefixes x is finite set
{x} is functional non empty trivial finite V42() 1 -element set
(ProperPrefixes x) \/ {x} is non empty finite set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*g*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*g*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,y) is Element of F1()
F3((F1(),Y,y)) is set
len (f ^ <*D*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len <*D*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len f) + (len <*D*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len (y ^ <*g*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len <*g*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len y) + (len <*g*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(f ^ <*D*>) . ((len f) + 1) is set
(len y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(y ^ <*g*>) . ((len y) + 1) is set
f is non empty Tree-like set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . D is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
g ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,g) is Element of F1()
F3((F1(),Y,g)) is set
F4() . ((F1(),Y,g),x) is Element of F1()
[(F1(),Y,g),x] is set
{(F1(),Y,g),x} is non empty finite set
{(F1(),Y,g)} is non empty trivial finite 1 -element set
{{(F1(),Y,g),x},{(F1(),Y,g)}} is non empty finite V42() set
F4() . [(F1(),Y,g),x] is set
y is Element of F1()
x is Element of F1()
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Element of F1()
Y . y is set
F4() . ((Y . y),y) is set
[(Y . y),y] is set
{(Y . y),y} is non empty finite set
{(Y . y)} is non empty trivial finite 1 -element set
{{(Y . y),y},{(Y . y)}} is non empty finite V42() set
F4() . [(Y . y),y] is set
D is Relation-like Function-like () set
dom D is non empty Tree-like set
rng D is set
x is set
g is set
D . g is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom D
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
(F1(),Y,y) is Element of F1()
D . y is set
T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T1 ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . T1 is set
F4() . ((Y . T1),y) is set
[(Y . T1),y] is set
{(Y . T1),y} is non empty finite set
{(Y . T1)} is non empty trivial finite 1 -element set
{{(Y . T1),y},{(Y . T1)}} is non empty finite V42() set
F4() . [(Y . T1),y] is set
T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*k1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,T2) is Element of F1()
F3((F1(),Y,T2)) is set
len <*y*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len <*k1*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len (T1 ^ <*y*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len T1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len (T2 ^ <*k1*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len T2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len T2) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(T1 ^ <*y*>) . ((len T1) + 1) is set
(T2 ^ <*k1*>) . ((len T2) + 1) is set
x is Relation-like F1() -valued Function-like () set
x . {} is set
dom x is non empty Tree-like set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom x
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
((dom x),g) is Element of bool (dom x)
bool (dom x) is non empty set
{ (g ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : g ^ <*b1*> in dom x } is set
(F1(),x,g) is Element of F1()
F3((F1(),x,g)) is set
{ (g ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 in F3((F1(),x,g)) } is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,y) is Element of F1()
F3((F1(),Y,y)) is set
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len <*y*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,y) is Element of F1()
F3((F1(),Y,y)) is set
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len <*y*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len y) + (len <*y*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
((dom Y),y) is Element of bool (dom Y)
bool (dom Y) is non empty set
{ (y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : y ^ <*b1*> in dom Y } is set
{ (y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 in F3((F1(),Y,y)) } is set
Y . g is set
y is set
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*T1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
g ^ <*T1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
len k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len g) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
((dom Y),T2) is Element of bool (dom Y)
{ (T2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : T2 ^ <*b1*> in dom Y } is set
(F1(),Y,T2) is Element of F1()
F3((F1(),Y,T2)) is set
{ (T2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 in F3((F1(),Y,T2)) } is set
T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*k1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,T2) is Element of F1()
F3((F1(),Y,T2)) is set
y is set
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*T1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
g ^ <*T1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
y ^ <*T1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
g ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x . (g ^ <*y*>) is set
T1 is set
F3(T1) is set
F4() . (T1,y) is set
[T1,y] is set
{T1,y} is non empty finite set
{T1} is non empty trivial finite 1 -element set
{{T1,y},{T1}} is non empty finite V42() set
F4() . [T1,y] is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
len k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len g) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . (y ^ <*y*>) is set
T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*k1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . T2 is set
F4() . ((Y . T2),k1) is set
[(Y . T2),k1] is set
{(Y . T2),k1} is non empty finite set
{(Y . T2)} is non empty trivial finite 1 -element set
{{(Y . T2),k1},{(Y . T2)}} is non empty finite V42() set
F4() . [(Y . T2),k1] is set
X is set
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is Relation-like F1() -valued Function-like () set
B . {} is set
dom B is non empty Tree-like set
f is set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
((dom B),x) is Element of bool (dom B)
bool (dom B) is non empty set
{ (x ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : x ^ <*b1*> in dom B } is set
(F1(),B,x) is Element of F1()
F3((F1(),B,x)) is set
{ (x ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 in F3((F1(),B,x)) } is set
y is set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
F3(y) is set
<*g*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*g*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . (x ^ <*g*>) is set
F4() . (y,g) is set
[y,g] is set
{y,g} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,g},{y}} is non empty finite V42() set
F4() . [y,g] is set
X is Relation-like Function-like set
dom X is set
rng X is set
Y is non empty set
B is set
f is set
X . f is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is Relation-like F1() -valued Function-like () set
D . {} is set
dom D is non empty Tree-like set
B is Relation-like Function-like () set
f is Relation-like Function-like () set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X . D is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X . x is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
g is Relation-like F1() -valued Function-like () set
g . {} is set
dom g is non empty Tree-like set
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is Relation-like F1() -valued Function-like () set
y . {} is set
dom y is non empty Tree-like set
dom B is non empty Tree-like set
dom f is non empty Tree-like set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
len k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . k1 is set
f . k1 is set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
k1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
len T2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . T2 is set
f . T2 is set
Seg k1 is finite k1 -element Element of bool NAT
T2 | (Seg k1) is Relation-like NAT -defined Seg k1 -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
len t1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . t1 is set
f . t1 is set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x is set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
n ^ <*x*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len n) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
rng <*x*> is non empty trivial finite 1 -element set
{x} is non empty trivial finite 1 -element set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
t1 ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
((dom B),t1) is Element of bool (dom B)
bool (dom B) is non empty set
{ (t1 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : t1 ^ <*b1*> in dom B } is set
F3((B . t1)) is set
{ (t1 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 in F3((B . t1)) } is set
i is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*i*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
t1 ^ <*i*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
t2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom f
((dom f),t2) is Element of bool (dom f)
bool (dom f) is non empty set
{ (t2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : t2 ^ <*b1*> in dom f } is set
f . t2 is set
F3((f . t2)) is set
{ (t2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 in F3((f . t2)) } is set
g . T2 is set
g . t1 is set
F4() . ((g . t1),x) is set
[(g . t1),x] is set
{(g . t1),x} is non empty finite set
{(g . t1)} is non empty trivial finite 1 -element set
{{(g . t1),x},{(g . t1)}} is non empty finite V42() set
F4() . [(g . t1),x] is set
k1 is set
T2 is set
k2 is set
[T2,k2] is set
{T2,k2} is non empty finite set
{T2} is non empty trivial finite 1 -element set
{{T2,k2},{T2}} is non empty finite V42() set
B . T2 is set
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
len t1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . t1 is set
f . t1 is set
B is set
f is set
D is set
X . D is set
x is set
X . x is set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
union (rng X) is set
B is Relation-like F1() -valued Function-like () set
B . {} is set
dom B is non empty Tree-like set
X . 0 is set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is Relation-like F1() -valued Function-like () set
f . {} is set
dom f is non empty Tree-like set
[{},F2()] is set
{{},F2()} is non empty finite set
{{{},F2()},{{}}} is non empty finite V42() set
x is Relation-like Function-like () set
dom x is non empty Tree-like set
g is set
x . g is set
B . g is set
[g,(x . g)] is set
{g,(x . g)} is non empty finite set
{g} is non empty trivial finite 1 -element set
{{g,(x . g)},{g}} is non empty finite V42() set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
((dom B),x) is Element of bool (dom B)
bool (dom B) is non empty set
{ (x ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : x ^ <*b1*> in dom B } is set
(F1(),B,x) is Element of F1()
F3((F1(),B,x)) is set
{ (x ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 in F3((F1(),B,x)) } is set
g is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . g is set
[g,(B . g)] is set
{g,(B . g)} is non empty finite set
{g} is non empty trivial finite 1 -element set
{{g,(B . g)},{g}} is non empty finite V42() set
y is set
T1 is set
X . T1 is set
T2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
k1 is Relation-like F1() -valued Function-like () set
k1 . {} is set
dom k1 is non empty Tree-like set
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom k1
len t1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len x) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom k1
len k2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
((dom k1),k2) is Element of bool (dom k1)
bool (dom k1) is non empty set
{ (k2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : k2 ^ <*b1*> in dom k1 } is set
(F1(),k1,k2) is Element of F1()
F3((F1(),k1,k2)) is set
{ (k2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 in F3((F1(),k1,k2)) } is set
k1 . x is set
[x,(F1(),B,x)] is set
{x,(F1(),B,x)} is non empty finite set
{x} is functional non empty trivial finite V42() 1 -element set
{{x,(F1(),B,x)},{x}} is non empty finite V42() set
g is set
y is set
X . y is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X . y is set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
T1 is Relation-like F1() -valued Function-like () set
T1 . {} is set
dom T1 is non empty Tree-like set
y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
X . (y + 1) is set
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
T2 is Relation-like F1() -valued Function-like () set
T2 . {} is set
dom T2 is non empty Tree-like set
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom T1
len t1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
T2 . x is set
t2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom T2
len t2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
((dom T2),t2) is Element of bool (dom T2)
bool (dom T2) is non empty set
{ (t2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : t2 ^ <*b1*> in dom T2 } is set
(F1(),T2,t2) is Element of F1()
F3((F1(),T2,t2)) is set
{ (t2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 in F3((F1(),T2,t2)) } is set
n is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*n*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . (x ^ <*n*>) is set
F4() . ((F1(),B,x),n) is Element of F1()
[(F1(),B,x),n] is set
{(F1(),B,x),n} is non empty finite set
{(F1(),B,x)} is non empty trivial finite 1 -element set
{{(F1(),B,x),n},{(F1(),B,x)}} is non empty finite V42() set
F4() . [(F1(),B,x),n] is set
T2 . (x ^ <*n*>) is set
F1() is non empty set
[:F1(),NAT:] is Relation-like non empty non trivial non finite set
[:[:F1(),NAT:],F1():] is Relation-like non empty non trivial non finite set
bool [:[:F1(),NAT:],F1():] is non empty non trivial non finite set
F2() is Element of F1()
F4() is Relation-like [:F1(),NAT:] -defined F1() -valued Function-like V25([:F1(),NAT:],F1()) Element of bool [:[:F1(),NAT:],F1():]
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : not a1 <= b1 } is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : not F3(a1) <= b1 } is set
X is Element of F1()
F3(X) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : not F3(X) <= b1 } is set
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is Relation-like F1() -valued Function-like () set
X . {} is set
dom X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom X
((dom X),Y) is Element of bool (dom X)
bool (dom X) is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in dom X } is set
(F1(),X,Y) is Element of F1()
F3((F1(),X,Y)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : not F3((F1(),X,Y)) <= b1 } is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : not F3((F1(),X,Y)) <= b1 } is set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 in H1(F3((F1(),X,Y))) } is set
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*B*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*B*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
X . (Y ^ <*B*>) is set
F4() . ((F1(),X,Y),B) is Element of F1()
[(F1(),X,Y),B] is set
{(F1(),X,Y),B} is non empty finite set
{(F1(),X,Y)} is non empty trivial finite 1 -element set
{{(F1(),X,Y),B},{(F1(),X,Y)}} is non empty finite V42() set
F4() . [(F1(),X,Y),B] is set
X is non empty finite Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,Y) is finite Element of bool X
bool X is non empty finite V42() set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
X is non empty finite Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,Y) is finite Element of bool X
bool X is non empty finite V42() set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
card (X,Y) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
X is non empty Tree-like set
X --> {} is Relation-like X -defined {{}} -valued Function-like constant non empty total V25(X,{{}}) Function-yielding V32() () Element of bool [:X,{{}}:]
[:X,{{}}:] is Relation-like non empty set
bool [:X,{{}}:] is non empty set
X is non empty set
the Element of X is Element of X
B is non empty Tree-like set
B --> the Element of X is Relation-like B -defined X -valued Function-like constant non empty total V25(B,X) () Element of bool [:B,X:]
[:B,X:] is Relation-like non empty set
bool [:B,X:] is non empty set
X is non empty set
Y is non empty set
[:X,Y:] is Relation-like non empty set
bool [:X,Y:] is non empty set
X is non empty Tree-like set
Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X with-replacement (B,Y) is non empty Tree-like set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X with-replacement (B,Y)
((X with-replacement (B,Y)),D) is Element of bool (X with-replacement (B,Y))
bool (X with-replacement (B,Y)) is non empty set
{ (D ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : D ^ <*b1*> in X with-replacement (B,Y) } is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of Y
B ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(Y,x) is Element of bool Y
bool Y is non empty set
{ (x ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : x ^ <*b1*> in Y } is set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*g*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ <*g*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*g*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B ^ (x ^ <*g*>) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B ^ y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like Function-like set
dom g is set
y is set
rng g is set
y is set
g . y is set
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*T1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ <*T1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*T1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
g . (D ^ <*y*>) is set
y is set
g . y is set
y is set
g . y is set
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*T1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ <*T1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*k1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*T1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F1() is non empty set
[:F1(),NAT:] is Relation-like non empty non trivial non finite set
[:[:F1(),NAT:],F1():] is Relation-like non empty non trivial non finite set
bool [:[:F1(),NAT:],F1():] is non empty non trivial non finite set
F2() is Element of F1()
F3() is Relation-like [:F1(),NAT:] -defined F1() -valued Function-like V25([:F1(),NAT:],F1()) Element of bool [:[:F1(),NAT:],F1():]
X is non empty Tree-like set
[:X,F1():] is Relation-like non empty set
bool [:X,F1():] is non empty set
X --> F2() is Relation-like X -defined F1() -valued Function-like constant non empty total V25(X,F1()) () Element of bool [:X,F1():]
Y is Relation-like X -defined F1() -valued Function-like constant non empty total V25(X,F1()) () Element of bool [:X,F1():]
Y . {} is set
dom Y is non empty Tree-like set
dom Y is non empty Tree-like Element of bool X
bool X is non empty set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
((dom Y),B) is Element of bool (dom Y)
bool (dom Y) is non empty set
{ (B ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : B ^ <*b1*> in dom Y } is set
(F1(),Y,B) is Element of F1()
{ (B ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : P1[b1,(F1(),Y,B)] } is set
D is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
B ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . (B ^ <*f*>) is set
F3() . (D,f) is set
[D,f] is set
{D,f} is non empty finite set
{D} is non empty trivial finite 1 -element set
{{D,f},{D}} is non empty finite V42() set
F3() . [D,f] is set
X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
Y is Relation-like F1() -valued Function-like () set
Y . {} is set
dom Y is non empty Tree-like set
{ (b2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT , b2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y : P1[b1,(F1(),Y,b2)] } is set
{ (b2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT , b2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y : P1[b1,(F1(),Y,b2)] } \/ (dom Y) is non empty set
B is non empty set
f is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,x) is Element of F1()
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes f is finite set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,x) is Element of F1()
ProperPrefixes x is finite set
{x} is functional non empty trivial finite V42() 1 -element set
(ProperPrefixes x) \/ {x} is non empty finite set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*g*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*g*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,y) is Element of F1()
len (f ^ <*D*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len <*D*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len f) + (len <*D*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len (y ^ <*g*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len <*g*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len y) + (len <*g*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(f ^ <*D*>) . ((len f) + 1) is set
(len y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(y ^ <*g*>) . ((len y) + 1) is set
f is non empty Tree-like set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . D is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
g ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,g) is Element of F1()
F3() . ((F1(),Y,g),x) is Element of F1()
[(F1(),Y,g),x] is set
{(F1(),Y,g),x} is non empty finite set
{(F1(),Y,g)} is non empty trivial finite 1 -element set
{{(F1(),Y,g),x},{(F1(),Y,g)}} is non empty finite V42() set
F3() . [(F1(),Y,g),x] is set
y is Element of F1()
x is Element of F1()
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Element of F1()
Y . y is set
F3() . ((Y . y),y) is set
[(Y . y),y] is set
{(Y . y),y} is non empty finite set
{(Y . y)} is non empty trivial finite 1 -element set
{{(Y . y),y},{(Y . y)}} is non empty finite V42() set
F3() . [(Y . y),y] is set
D is Relation-like Function-like () set
dom D is non empty Tree-like set
rng D is set
x is set
g is set
D . g is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom D
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
(F1(),Y,y) is Element of F1()
D . y is set
T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T1 ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . T1 is set
F3() . ((Y . T1),y) is set
[(Y . T1),y] is set
{(Y . T1),y} is non empty finite set
{(Y . T1)} is non empty trivial finite 1 -element set
{{(Y . T1),y},{(Y . T1)}} is non empty finite V42() set
F3() . [(Y . T1),y] is set
T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*k1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,T2) is Element of F1()
len <*y*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len <*k1*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len (T1 ^ <*y*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len T1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len (T2 ^ <*k1*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
len T2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len T2) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(T1 ^ <*y*>) . ((len T1) + 1) is set
(T2 ^ <*k1*>) . ((len T2) + 1) is set
x is Relation-like F1() -valued Function-like () set
x . {} is set
dom x is non empty Tree-like set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom x
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
((dom x),g) is Element of bool (dom x)
bool (dom x) is non empty set
{ (g ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : g ^ <*b1*> in dom x } is set
(F1(),x,g) is Element of F1()
{ (g ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : P1[b1,(F1(),x,g)] } is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,y) is Element of F1()
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len <*y*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,y) is Element of F1()
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len <*y*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len y) + (len <*y*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
((dom Y),y) is Element of bool (dom Y)
bool (dom Y) is non empty set
{ (y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : y ^ <*b1*> in dom Y } is set
{ (y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : P1[b1,(F1(),Y,y)] } is set
Y . g is set
y is set
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*T1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
g ^ <*T1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
len k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len g) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
((dom Y),T2) is Element of bool (dom Y)
{ (T2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : T2 ^ <*b1*> in dom Y } is set
(F1(),Y,T2) is Element of F1()
{ (T2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : P1[b1,(F1(),Y,T2)] } is set
T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*k1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F1(),Y,T2) is Element of F1()
y is set
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*T1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
g ^ <*T1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
y ^ <*T1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
g ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x . (g ^ <*y*>) is set
T1 is set
F3() . (T1,y) is set
[T1,y] is set
{T1,y} is non empty finite set
{T1} is non empty trivial finite 1 -element set
{{T1,y},{T1}} is non empty finite V42() set
F3() . [T1,y] is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
len k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len g) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . (y ^ <*y*>) is set
T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*k1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . T2 is set
F3() . ((Y . T2),k1) is set
[(Y . T2),k1] is set
{(Y . T2),k1} is non empty finite set
{(Y . T2)} is non empty trivial finite 1 -element set
{{(Y . T2),k1},{(Y . T2)}} is non empty finite V42() set
F3() . [(Y . T2),k1] is set
X is set
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is Relation-like F1() -valued Function-like () set
B . {} is set
dom B is non empty Tree-like set
f is set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
((dom B),x) is Element of bool (dom B)
bool (dom B) is non empty set
{ (x ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : x ^ <*b1*> in dom B } is set
(F1(),B,x) is Element of F1()
{ (x ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : P1[b1,(F1(),B,x)] } is set
y is set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*g*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*g*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . (x ^ <*g*>) is set
F3() . (y,g) is set
[y,g] is set
{y,g} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,g},{y}} is non empty finite V42() set
F3() . [y,g] is set
X is Relation-like Function-like set
dom X is set
rng X is set
Y is non empty set
B is set
f is set
X . f is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is Relation-like F1() -valued Function-like () set
D . {} is set
dom D is non empty Tree-like set
B is Relation-like Function-like () set
f is Relation-like Function-like () set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X . D is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X . x is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
g is Relation-like F1() -valued Function-like () set
g . {} is set
dom g is non empty Tree-like set
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is Relation-like F1() -valued Function-like () set
y . {} is set
dom y is non empty Tree-like set
dom B is non empty Tree-like set
dom f is non empty Tree-like set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
len k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . k1 is set
f . k1 is set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
k1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
len T2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . T2 is set
f . T2 is set
Seg k1 is finite k1 -element Element of bool NAT
T2 | (Seg k1) is Relation-like NAT -defined Seg k1 -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
len t1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . t1 is set
f . t1 is set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x is set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
n ^ <*x*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len n) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
rng <*x*> is non empty trivial finite 1 -element set
{x} is non empty trivial finite 1 -element set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
t1 ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
((dom B),t1) is Element of bool (dom B)
bool (dom B) is non empty set
{ (t1 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : t1 ^ <*b1*> in dom B } is set
{ (t1 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : P1[b1,B . t1] } is set
i is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*i*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
t1 ^ <*i*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
t2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom f
((dom f),t2) is Element of bool (dom f)
bool (dom f) is non empty set
{ (t2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : t2 ^ <*b1*> in dom f } is set
f . t2 is set
{ (t2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : P1[b1,f . t2] } is set
g . T2 is set
g . t1 is set
F3() . ((g . t1),x) is set
[(g . t1),x] is set
{(g . t1),x} is non empty finite set
{(g . t1)} is non empty trivial finite 1 -element set
{{(g . t1),x},{(g . t1)}} is non empty finite V42() set
F3() . [(g . t1),x] is set
k1 is set
T2 is set
k2 is set
[T2,k2] is set
{T2,k2} is non empty finite set
{T2} is non empty trivial finite 1 -element set
{{T2,k2},{T2}} is non empty finite V42() set
B . T2 is set
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
len t1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . t1 is set
f . t1 is set
B is set
f is set
D is set
X . D is set
x is set
X . x is set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
union (rng X) is set
B is Relation-like F1() -valued Function-like () set
B . {} is set
dom B is non empty Tree-like set
X . 0 is set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is Relation-like F1() -valued Function-like () set
f . {} is set
dom f is non empty Tree-like set
[{},F2()] is set
{{},F2()} is non empty finite set
{{{},F2()},{{}}} is non empty finite V42() set
x is Relation-like Function-like () set
dom x is non empty Tree-like set
g is set
x . g is set
B . g is set
[g,(x . g)] is set
{g,(x . g)} is non empty finite set
{g} is non empty trivial finite 1 -element set
{{g,(x . g)},{g}} is non empty finite V42() set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom B
((dom B),x) is Element of bool (dom B)
bool (dom B) is non empty set
{ (x ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : x ^ <*b1*> in dom B } is set
(F1(),B,x) is Element of F1()
{ (x ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : P1[b1,(F1(),B,x)] } is set
g is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . g is set
[g,(B . g)] is set
{g,(B . g)} is non empty finite set
{g} is non empty trivial finite 1 -element set
{{g,(B . g)},{g}} is non empty finite V42() set
y is set
T1 is set
X . T1 is set
T2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
k1 is Relation-like F1() -valued Function-like () set
k1 . {} is set
dom k1 is non empty Tree-like set
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom k1
len t1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len x) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom k1
len k2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
((dom k1),k2) is Element of bool (dom k1)
bool (dom k1) is non empty set
{ (k2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : k2 ^ <*b1*> in dom k1 } is set
(F1(),k1,k2) is Element of F1()
{ (k2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : P1[b1,(F1(),k1,k2)] } is set
k1 . x is set
[x,(F1(),B,x)] is set
{x,(F1(),B,x)} is non empty finite set
{x} is functional non empty trivial finite V42() 1 -element set
{{x,(F1(),B,x)},{x}} is non empty finite V42() set
g is set
y is set
X . y is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X . y is set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
T1 is Relation-like F1() -valued Function-like () set
T1 . {} is set
dom T1 is non empty Tree-like set
y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
X . (y + 1) is set
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
T2 is Relation-like F1() -valued Function-like () set
T2 . {} is set
dom T2 is non empty Tree-like set
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom T1
len t1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
T2 . x is set
t2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom T2
len t2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
((dom T2),t2) is Element of bool (dom T2)
bool (dom T2) is non empty set
{ (t2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : t2 ^ <*b1*> in dom T2 } is set
(F1(),T2,t2) is Element of F1()
{ (t2 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : P1[b1,(F1(),T2,t2)] } is set
n is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*n*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . (x ^ <*n*>) is set
F3() . ((F1(),B,x),n) is Element of F1()
[(F1(),B,x),n] is set
{(F1(),B,x),n} is non empty finite set
{(F1(),B,x)} is non empty trivial finite 1 -element set
{{(F1(),B,x),n},{(F1(),B,x)}} is non empty finite V42() set
F3() . [(F1(),B,x),n] is set
T2 . (x ^ <*n*>) is set
X is non empty Tree-like set
Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{ (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : verum } is set
union { (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : verum } is set
f is set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,D) is (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = D } is set
(Y,D) is (Y)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of Y : len b1 = D } is set
{ (Y,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : verum } is set
union { (Y,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : verum } is set
f is set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(Y,D) is (Y)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of Y : len b1 = D } is set
(X,D) is (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = D } is set
TrivialInfiniteTree is non empty non trivial non finite Tree-like set
{ (b1 |-> 0) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : verum } is set
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(TrivialInfiniteTree,Y) is ( TrivialInfiniteTree )
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of TrivialInfiniteTree : len b1 = Y } is set
Y |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite Y -element FinSequence-like FinSubsequence-like Element of Y -tuples_on NAT
Y -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{(Y |-> 0)} is functional non empty trivial finite V42() 1 -element set
D is set
len (Y |-> 0) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of TrivialInfiniteTree
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
g |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite g -element FinSequence-like FinSubsequence-like Element of g -tuples_on NAT
g -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
X is set
Y is set
PFuncs (X,Y) is functional non empty set
bool (PFuncs (X,Y)) is non empty set
B is c=-linear functional Element of bool (PFuncs (X,Y))
union B is set
f is set
x is set
D is functional non empty set
{ (dom b1) where b1 is Relation-like Function-like Element of D : verum } is set
g is Relation-like Function-like Element of D
dom g is set
y is Relation-like Function-like set
dom y is set
rng y is set
x is set
{ (rng b1) where b1 is Relation-like Function-like Element of D : verum } is set
g is Relation-like Function-like Element of D
rng g is set
y is Relation-like Function-like set
dom y is set
rng y is set
f is Relation-like Function-like set
rng f is set
union { (rng b1) where b1 is Relation-like Function-like Element of D : verum } is set
dom f is set
union { (dom b1) where b1 is Relation-like Function-like Element of D : verum } is set
[:X,Y:] is Relation-like set
bool [:X,Y:] is non empty set