REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool NAT 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 Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
{{},1} is non empty finite V37() set
Trees is non empty constituted-Trees set
bool Trees is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of NAT
ProperPrefixes {} is finite set
{{}} is functional non empty trivial finite V37() 1 -element Tree-like set
NAT * is functional non empty FinSequence-membered M8( NAT )
<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding FinSequence of NAT
[:NAT,NAT:] is Relation-like non empty non trivial non finite set
elementary_tree 0 is non empty finite Tree-like set
elementary_tree 1 is non empty finite 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
{{},<*0*>} is functional non empty finite V37() set
elementary_tree 2 is non empty finite Tree-like set
<*1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
{{},<*0*>,<*1*>} is non empty finite set
card {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
[:NAT,NAT:] is Relation-like REAL -defined REAL -valued non empty non trivial non finite Element of bool [:REAL,REAL:]
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is non empty set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
F is non empty Tree-like set
F is non empty set
F is Relation-like F -valued Function-like DecoratedTree-like set
proj1 F is non empty Tree-like set
((proj1 F)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
F . ((proj1 F)) is Element of F
F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*F*> ^ A is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*F*> ^ A) . 1 is set
G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*F*> ^ G is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*F*> ^ A) ^ G is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
((<*F*> ^ A) ^ G) . 1 is set
A ^ G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*F*> ^ (A ^ G) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(<*F*> ^ (A ^ G)) . 1 is set
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*F*> ^ A is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(<*F*> ^ A) . 1 is set
G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*F*> ^ G is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
<*F*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*F*> ^ A is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
F is non empty Tree-like set
A is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
<*A*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
{} ^ <*G*> is Relation-like NAT -defined Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like set
{} + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F ^ <*A*> is Relation-like NAT -defined NAT -valued Function-like non empty 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
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F ^ F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F ^ A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
PFuncs ((NAT *),[:NAT,NAT:]) is set
F is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like set
rng F is Relation-like NAT -defined NAT -valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
proj1 F is non empty Tree-like set
F is non empty Tree-like set
F is non empty Tree-like set
A is non empty Tree-like set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
F with-replacement (G,F) is non empty Tree-like set
F with-replacement (G,A) is non empty Tree-like set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
G ^ A 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
G ^ B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
G ^ A 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
G ^ B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F is non empty set
F is Relation-like F -valued Function-like DecoratedTree-like set
proj1 F is non empty Tree-like set
A is Relation-like F -valued Function-like DecoratedTree-like set
G is Relation-like F -valued Function-like DecoratedTree-like set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
F with-replacement (A,A) is Relation-like Function-like DecoratedTree-like set
F with-replacement (A,G) is Relation-like Function-like DecoratedTree-like set
proj1 (F with-replacement (A,A)) is non empty Tree-like set
proj1 A is non empty Tree-like set
(proj1 F) with-replacement (A,(proj1 A)) is non empty Tree-like set
proj1 G is non empty Tree-like set
(proj1 F) with-replacement (A,(proj1 G)) is non empty Tree-like set
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
A . k2 is set
G . k2 is set
A ^ k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F with-replacement (A,A)) . (A ^ k2) is set
(F with-replacement (A,G)) . (A ^ k2) is set
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
A ^ A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
G . A1 is set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
A ^ G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
A . G is set
proj1 (F with-replacement (A,G)) is non empty Tree-like set
F is non empty Tree-like set
F is non empty Tree-like set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F with-replacement (A,F) is non empty Tree-like set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F with-replacement (A,F)
succ A is Element of bool (F with-replacement (A,F))
bool (F with-replacement (A,F)) is non empty set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
succ B is Element of bool F
bool F is non empty set
k1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B ^ k1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal set
dom k1 is finite Element of bool NAT
len B is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
(len B) + k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
dom A is finite Element of bool NAT
A . ((len B) + k2) is set
rng A is finite Element of bool NAT
k1 . k2 is set
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
A1 is set
{ (A ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : A ^ <*b1*> in F with-replacement (A,F) } is set
G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
A ^ <*G*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{ (B ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : B ^ <*b1*> in F } is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
A ^ a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
A ^ a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B ^ <*G*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
k2 ^ a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B ^ (k2 ^ a) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len a is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
len k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(len k2) + (len a) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
len <*G*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
{ (B ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : B ^ <*b1*> in F } is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{ (B ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : B ^ <*b1*> in F } is set
G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
B ^ <*G*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A ^ <*G*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes <*G*> is finite set
{ (A ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : A ^ <*b1*> in F with-replacement (A,F) } is set
F is non empty Tree-like set
F is non empty Tree-like set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F with-replacement (A,F) is non empty Tree-like set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F with-replacement (A,F)
succ A is Element of bool (F with-replacement (A,F))
bool (F with-replacement (A,F)) is non empty set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
succ B is Element of bool F
bool F is non empty set
k1 is set
{ (A ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : A ^ <*b1*> in F with-replacement (A,F) } is set
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
A ^ <*k2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A1 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
A ^ G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{ (B ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : B ^ <*b1*> in F } is set
{ (B ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : B ^ <*b1*> in F } is set
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
B ^ <*k2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A ^ <*k2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
{ (A ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : A ^ <*b1*> in F with-replacement (A,F) } is set
F is non empty Tree-like set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F is non empty Tree-like set
F with-replacement (A,F) is non empty Tree-like set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F with-replacement (A,F)
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
A ^ A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
succ G is Element of bool (F with-replacement (A,F))
bool (F with-replacement (A,F)) is non empty set
succ A is Element of bool F
bool F is non empty set
F is non empty Tree-like set
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F | F is non empty Tree-like set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
succ G is Element of bool F
bool F is non empty set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F | F
F ^ A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
succ A is Element of bool (F | F)
bool (F | F) is non empty set
B is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
G ^ <*B*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A ^ <*B*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F ^ (A ^ <*B*>) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B is set
{ (G ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : G ^ <*b1*> in F } is set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
G ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
G ^ <*k2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A ^ <*k2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B is Relation-like Function-like set
proj1 B is set
k1 is set
proj2 B is set
k2 is set
B . k2 is set
{ (G ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : G ^ <*b1*> in F } is set
A1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
<*A1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
G ^ <*A1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A ^ <*A1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
{ (A ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : A ^ <*b1*> in F | F } is set
{ (A ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : A ^ <*b1*> in F | F } is set
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
A ^ <*k2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
G ^ <*k2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
{ (G ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : G ^ <*b1*> in F } is set
B . (G ^ <*k2*>) is set
k1 is set
k2 is set
B . k1 is set
B . k2 is set
A1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
<*A1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
G ^ <*A1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
G ^ <*G*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A ^ <*G*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A ^ <*A1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F is non empty finite Tree-like set
(F) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
branchdeg (F) is set
card F is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
succ (F) is finite Element of bool F
bool F is non empty finite V37() set
card (succ (F)) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F is set
{(F)} is functional non empty trivial finite V37() 1 -element Element of bool F
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
A is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
<*A*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element 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
<*A*> ^ G is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
{} ^ <*A*> is Relation-like NAT -defined Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like set
{} + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
bool [:NAT,NAT:] is non empty non trivial non finite set
{<*0*>} is functional non empty trivial finite V37() 1 -element Element of bool (bool [:NAT,NAT:])
bool (bool [:NAT,NAT:]) is non empty non trivial non finite set
F is non empty finite Tree-like set
(F) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
branchdeg (F) is set
succ (F) is finite Element of bool F
bool F is non empty finite V37() set
card (succ (F)) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F is set
{F} is non empty trivial finite 1 -element set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
{ ((F) ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : (F) ^ <*b1*> in F } is set
G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
(F) ^ <*G*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
{<*0*>,<*1*>} is functional non empty finite V37() Element of bool (bool [:NAT,NAT:])
F is non empty finite Tree-like set
(F) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
branchdeg (F) is set
succ (F) is finite Element of bool F
bool F is non empty finite V37() set
card (succ (F)) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F is set
A is set
{F,A} is non empty finite set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
{ ((F) ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : (F) ^ <*b1*> in F } is set
A is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
<*A*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
(F) ^ <*A*> 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 NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
(F) ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F) ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F) ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F is non empty Tree-like set
(F) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
F | F is non empty Tree-like set
{ (F ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : F ^ b1 in F } is set
G is set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F ^ A 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 ^ B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
G is Relation-like Function-like set
proj1 G is set
G is Relation-like Function-like set
proj1 G is set
A is set
proj2 G is set
B is set
G . B is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT *
F ^ k2 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 Element of NAT *
F ^ B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
G . B is set
A is set
B is set
G . A is set
G . B is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F ^ k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F ^ k2 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 NAT *
F ^ G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F is non empty finite Tree-like set
(F) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
card F is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
F | F is non empty finite Tree-like set
card (F | F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
{ (F ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : F ^ b1 in F } is set
G is finite set
{(F)} is functional non empty trivial finite V37() 1 -element Element of bool F
bool F is non empty finite V37() set
G \/ {(F)} is non empty finite set
B is set
A is finite set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT *
F ^ k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
card A is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
card G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
(card G) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
(card (F | F)) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F is non empty finite Tree-like set
(F) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
succ (F) is finite Element of bool F
bool F is non empty finite V37() set
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
{F} is functional non empty trivial finite V37() 1 -element Element of bool F
F | F is non empty finite Tree-like set
(elementary_tree 1) with-replacement (<*0*>,(F | F)) is non empty Tree-like set
card (succ (F)) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
branchdeg (F) is set
G is set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*k1*> ^ B is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F) ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (elementary_tree 1) with-replacement (<*0*>,(F | F))
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (elementary_tree 1) with-replacement (<*0*>,(F | F))
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ B is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (elementary_tree 1) with-replacement (<*0*>,(F | F))
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
[:(proj1 F),(proj2 F):] is Relation-like set
F is non empty set
A is Relation-like F -valued Function-like finite DecoratedTree-like set
proj1 A is non empty finite Tree-like set
((proj1 A)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A
succ ((proj1 A)) is finite Element of bool (proj1 A)
bool (proj1 A) is non empty finite V37() set
(F,A) is Element of F
A . ((proj1 A)) is Element of F
(elementary_tree 1) --> (F,A) is Relation-like elementary_tree 1 -defined F -valued Function-like V30( elementary_tree 1,F) finite DecoratedTree-like Element of bool [:(elementary_tree 1),F:]
[:(elementary_tree 1),F:] is Relation-like non empty set
bool [:(elementary_tree 1),F:] is non empty set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A
{G} is functional non empty trivial finite V37() 1 -element Element of bool (proj1 A)
A | G is Relation-like F -valued Function-like DecoratedTree-like set
((elementary_tree 1) --> (F,A)) with-replacement (<*0*>,(A | G)) is Relation-like Function-like DecoratedTree-like set
dom ((elementary_tree 1) --> (F,A)) is non empty finite Tree-like Element of bool (elementary_tree 1)
bool (elementary_tree 1) is non empty finite V37() set
proj1 (A | G) is non empty Tree-like set
(proj1 A) | G is non empty finite Tree-like set
card (succ ((proj1 A))) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
branchdeg ((proj1 A)) is set
proj1 (((elementary_tree 1) --> (F,A)) with-replacement (<*0*>,(A | G))) is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(((elementary_tree 1) --> (F,A)) with-replacement (<*0*>,(A | G))) . B is set
A . B is set
(dom ((elementary_tree 1) --> (F,A))) with-replacement (<*0*>,(proj1 (A | G))) is non empty Tree-like set
((elementary_tree 1) --> (F,A)) . B is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ k1 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A | G) . k1 is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ k1 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A | G) . k1 is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ k1 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ k2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A | G) . k2 is set
(elementary_tree 1) with-replacement (<*0*>,((proj1 A) | G)) is non empty Tree-like set
F is non empty Tree-like set
(F) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
succ (F) is Element of bool F
bool F is non empty set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
{A,G} is functional non empty finite V37() Element of bool F
F | A is non empty Tree-like set
(elementary_tree 2) with-replacement (<*0*>,(F | A)) is non empty Tree-like set
F | G is non empty Tree-like set
((elementary_tree 2) with-replacement (<*0*>,(F | A))) with-replacement (<*1*>,(F | G)) is non empty Tree-like set
B 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 V28() V29() 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
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*k2*> ^ k1 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F) ^ <*k2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ A1 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 FinSequence of NAT
<*0*> ^ k1 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 FinSequence of NAT
<*1*> ^ k1 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 FinSequence of NAT
<*1*> ^ k1 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F is non empty set
A is Relation-like F -valued Function-like DecoratedTree-like set
proj1 A is non empty Tree-like set
((proj1 A)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A
succ ((proj1 A)) is Element of bool (proj1 A)
bool (proj1 A) is non empty set
(F,A) is Element of F
A . ((proj1 A)) is Element of F
(elementary_tree 2) --> (F,A) is Relation-like elementary_tree 2 -defined F -valued Function-like V30( elementary_tree 2,F) finite DecoratedTree-like Element of bool [:(elementary_tree 2),F:]
[:(elementary_tree 2),F:] is Relation-like non empty set
bool [:(elementary_tree 2),F:] is non empty set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A
{G,A} is functional non empty finite V37() Element of bool (proj1 A)
A | G is Relation-like F -valued Function-like DecoratedTree-like set
((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G)) is Relation-like Function-like DecoratedTree-like set
A | A is Relation-like F -valued Function-like DecoratedTree-like set
(((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G))) with-replacement (<*1*>,(A | A)) is Relation-like Function-like DecoratedTree-like set
proj1 (A | A) is non empty Tree-like set
(proj1 A) | A is non empty Tree-like set
proj1 (A | G) is non empty Tree-like set
(proj1 A) | G is non empty Tree-like set
dom ((elementary_tree 2) --> (F,A)) is non empty finite Tree-like Element of bool (elementary_tree 2)
bool (elementary_tree 2) is non empty finite V37() set
proj1 (((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G))) is non empty Tree-like set
(dom ((elementary_tree 2) --> (F,A))) with-replacement (<*0*>,(proj1 (A | G))) is non empty Tree-like set
proj1 ((((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G))) with-replacement (<*1*>,(A | A))) is non empty Tree-like set
(proj1 (((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G)))) with-replacement (<*1*>,(proj1 (A | A))) is non empty Tree-like set
(elementary_tree 2) with-replacement (<*0*>,((proj1 A) | G)) is non empty Tree-like set
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
((((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G))) with-replacement (<*1*>,(A | A))) . A1 is set
A . A1 is set
(((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G))) . A1 is set
((elementary_tree 2) --> (F,A)) . A1 is set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ G is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A | A) . G is set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ G is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A | G) . G is set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ G is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A | A) . G is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ k is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A | G) . k is set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ G is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A | A) . G is set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ G is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ k is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A | A) . k is set
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ a is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A | G) . a is set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ G is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ k is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A | A) . k is set
{3} is non empty trivial finite V37() 1 -element Element of bool NAT
[:{3},NAT:] is Relation-like NAT -defined REAL -valued non empty non trivial non finite Element of bool [:NAT,REAL:]
[:NAT,REAL:] is Relation-like set
bool [:NAT,REAL:] is non empty set
() is set
{0,1,2} is non empty finite Element of bool NAT
[:{0,1,2},NAT:] is Relation-like NAT -defined REAL -valued non empty non trivial non finite Element of bool [:NAT,REAL:]
() is set
F is set
F is set
A is set
[F,A] is V22() set
{F,A} is non empty finite set
{F} is non empty trivial finite 1 -element set
{{F,A},{F}} is non empty finite V37() set
F is non empty finite Tree-like set
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F
branchdeg F is set
succ F is finite Element of bool F
bool F is non empty finite V37() set
card (succ F) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[0,0] is V22() Element of [:NAT,NAT:]
{0,0} is functional non empty finite V37() set
{0} is functional non empty trivial finite V37() 1 -element Tree-like set
{{0,0},{0}} is non empty finite V37() set
[1,0] is V22() Element of [:NAT,NAT:]
{1,0} is non empty finite V37() set
{1} is non empty trivial finite V37() 1 -element set
{{1,0},{1}} is non empty finite V37() set
[1,1] is V22() Element of [:NAT,NAT:]
{1,1} is non empty finite V37() set
{{1,1},{1}} is non empty finite V37() set
[2,0] is V22() Element of [:NAT,NAT:]
{2,0} is non empty finite V37() set
{2} is non empty trivial finite V37() 1 -element set
{{2,0},{2}} is non empty finite V37() set
A is set
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
proj1 G is non empty finite Tree-like set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),A) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . B is Element of [:NAT,NAT:]
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),k1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . k1 is Element of [:NAT,NAT:]
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),k2) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . k2 is Element of [:NAT,NAT:]
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
proj1 A is non empty finite Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A
((proj1 A),B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A
((proj1 A),k1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . k1 is Element of [:NAT,NAT:]
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A
((proj1 A),k2) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . k2 is Element of [:NAT,NAT:]
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A
((proj1 A),A1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . A1 is Element of [:NAT,NAT:]
G is Relation-like Function-like DecoratedTree-like set
proj1 G is non empty Tree-like set
proj2 G is set
A is set
B is set
G . B is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
G . k1 is set
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
proj1 B is non empty finite Tree-like set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
((proj1 B),k1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
B . k1 is Element of [:NAT,NAT:]
succ k1 is finite Element of bool (proj1 B)
bool (proj1 B) is non empty finite V37() set
the Element of succ k1 is Element of succ k1
{ (k1 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : k1 ^ <*b1*> in proj1 B } is set
A1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
<*A1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
k1 ^ <*A1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B is non empty set
k1 is set
k1 is functional non empty constituted-DTrees DTree-set of [:NAT,NAT:]
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
proj1 A1 is non empty finite Tree-like set
k2 is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A1
((proj1 A1),G) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A1
((proj1 A1),k) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A1 . k is Element of [:NAT,NAT:]
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A1
((proj1 A1),a) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A1 . a is Element of [:NAT,NAT:]
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A1
((proj1 A1),v) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A1 . v is Element of [:NAT,NAT:]
s is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
proj1 s is non empty finite Tree-like set
F is functional non empty constituted-DTrees DTree-set of [:NAT,NAT:]
F is functional non empty constituted-DTrees DTree-set of [:NAT,NAT:]
A is set
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
proj1 G is non empty finite Tree-like set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),A) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . B is Element of [:NAT,NAT:]
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),k1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . k1 is Element of [:NAT,NAT:]
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),k2) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . k2 is Element of [:NAT,NAT:]
A is set
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
proj1 G is non empty finite Tree-like set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),A) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . B is Element of [:NAT,NAT:]
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),k1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . k1 is Element of [:NAT,NAT:]
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),k2) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . k2 is Element of [:NAT,NAT:]
() is functional non empty constituted-DTrees DTree-set of [:NAT,NAT:]
F is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like Element of ()
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 F is non empty finite Tree-like set
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
F | F is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like set
proj1 (F | F) is non empty Tree-like set
(proj1 F) | F is non empty finite Tree-like set
G is non empty finite Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of G
F ^ B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (proj1 F) | F
succ k2 is finite Element of bool ((proj1 F) | F)
bool ((proj1 F) | F) is non empty finite V37() set
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
succ A1 is finite Element of bool (proj1 F)
bool (proj1 F) is non empty finite V37() set
succ B is finite Element of bool G
bool G is non empty finite V37() set
card (succ B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
card (succ A1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
(G,B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
((proj1 F),A1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
A . B is set
F . A1 is Element of [:NAT,NAT:]
F . A1 is Element of [:NAT,NAT:]
G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,G] is V22() Element of [:NAT,NAT:]
{3,G} is non empty finite V37() set
{3} is non empty trivial finite V37() 1 -element set
{{3,G},{3}} is non empty finite V37() set
G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,G] is V22() Element of [:NAT,NAT:]
{3,G} is non empty finite V37() set
{3} is non empty trivial finite V37() 1 -element set
{{3,G},{3}} is non empty finite V37() set
k is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,k] is V22() Element of [:NAT,NAT:]
{3,k} is non empty finite V37() set
{{3,k},{3}} is non empty finite V37() set
k is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,k] is V22() Element of [:NAT,NAT:]
{3,k} is non empty finite V37() set
{{3,k},{3}} is non empty finite V37() set
F . A1 is Element of [:NAT,NAT:]
F . A1 is Element of [:NAT,NAT:]
F . A1 is Element of [:NAT,NAT:]
F . A1 is Element of [:NAT,NAT:]
F . A1 is Element of [:NAT,NAT:]
F is Element of ()
F `1 is set
F is non empty set
A is Element of F
G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[A,G] is V22() Element of [:F,NAT:]
[:F,NAT:] is Relation-like non empty non trivial non finite set
{A,G} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,G},{A}} is non empty finite V37() set
F is non empty set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F is Relation-like F -valued Function-like DecoratedTree-like set
proj1 F is non empty Tree-like set
A is Relation-like F -valued Function-like DecoratedTree-like set
F with-replacement (G,A) is Relation-like Function-like DecoratedTree-like set
proj2 (F with-replacement (G,A)) is set
B is set
proj1 (F with-replacement (G,A)) is non empty Tree-like set
k1 is set
(F with-replacement (G,A)) . k1 is set
proj1 A is non empty Tree-like set
(proj1 F) with-replacement (G,(proj1 A)) is non empty Tree-like set
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F with-replacement (G,A)) . k2 is set
F . k2 is set
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
G ^ A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
F . A1 is Element of F
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F with-replacement (G,A)) . k2 is set
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
G ^ A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
A . A1 is set
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
G ^ A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
A . A1 is set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A
A . G is Element of F
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(F with-replacement (G,A)) . k2 is set
F . k2 is set
(elementary_tree 1) --> [1,0] is Relation-like elementary_tree 1 -defined [:NAT,NAT:] -valued Function-like V30( elementary_tree 1,[:NAT,NAT:]) finite DecoratedTree-like Element of bool [:(elementary_tree 1),[:NAT,NAT:]:]
[:(elementary_tree 1),[:NAT,NAT:]:] is Relation-like non empty non trivial non finite set
bool [:(elementary_tree 1),[:NAT,NAT:]:] is non empty non trivial non finite set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
dom ((elementary_tree 1) --> [1,0]) is non empty finite Tree-like Element of bool (elementary_tree 1)
bool (elementary_tree 1) is non empty finite V37() set
([:NAT,NAT:],((elementary_tree 1) --> [1,0]),F,<*0*>) is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like set
proj1 (((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,F)) is non empty Tree-like set
proj1 F is non empty finite Tree-like set
(dom ((elementary_tree 1) --> [1,0])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of elementary_tree 1
(elementary_tree 1) with-replacement (F,(proj1 F)) is non empty finite Tree-like set
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
proj1 G is non empty finite Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G
((proj1 G),B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . B is Element of [:NAT,NAT:]
((elementary_tree 1) --> [1,0]) . B is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ k1 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
k2 is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom ((elementary_tree 1) --> [1,0])
succ k1 is finite Element of bool (dom ((elementary_tree 1) --> [1,0]))
bool (dom ((elementary_tree 1) --> [1,0])) is non empty finite V37() set
{ (k1 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : k1 ^ <*b1*> in dom ((elementary_tree 1) --> [1,0]) } is set
A1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
<*A1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
k1 ^ <*A1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
k1 ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite