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 FinSequence-like FinSubsequence-like FinSequence of NAT
{ (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
succ B is finite Element of bool (proj1 G)
bool (proj1 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
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
F . 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
F . k1 is set
succ B is finite Element of bool (proj1 G)
bool (proj1 G) is non empty finite V37() set
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
succ k2 is finite Element of bool (proj1 F)
bool (proj1 F) 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 k2) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
((proj1 F),k2) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F . k2 is Element of [:NAT,NAT:]
A1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,A1] is V22() Element of [:NAT,NAT:]
{3,A1} is non empty finite V37() set
{3} is non empty trivial finite V37() 1 -element set
{{3,A1},{3}} is non empty finite V37() set
((elementary_tree 1) --> [1,0]) . B is set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,k1] is V22() Element of [:NAT,NAT:]
{3,k1} is non empty finite V37() set
{3} is non empty trivial finite V37() 1 -element set
{{3,k1},{3}} is non empty finite V37() set
(elementary_tree 1) --> [1,1] 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:]:]
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
dom ((elementary_tree 1) --> [1,1]) is non empty finite Tree-like Element of bool (elementary_tree 1)
bool (elementary_tree 1) is non empty finite V37() set
proj1 (((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,F)) is non empty Tree-like set
proj1 F is non empty finite Tree-like set
(dom ((elementary_tree 1) --> [1,1])) 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
([:NAT,NAT:],((elementary_tree 1) --> [1,1]),F,<*0*>) is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-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,1]) . 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,1])
succ k1 is finite Element of bool (dom ((elementary_tree 1) --> [1,1]))
bool (dom ((elementary_tree 1) --> [1,1])) 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,1]) } 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 FinSequence-like FinSubsequence-like FinSequence of NAT
{ (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,1]) } is set
succ B is finite Element of bool (proj1 G)
bool (proj1 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
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
F . 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
F . k1 is set
succ B is finite Element of bool (proj1 G)
bool (proj1 G) is non empty finite V37() set
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
succ k2 is finite Element of bool (proj1 F)
bool (proj1 F) 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 k2) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
((proj1 F),k2) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F . k2 is Element of [:NAT,NAT:]
A1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,A1] is V22() Element of [:NAT,NAT:]
{3,A1} is non empty finite V37() set
{3} is non empty trivial finite V37() 1 -element set
{{3,A1},{3}} is non empty finite V37() set
((elementary_tree 1) --> [1,1]) . B is set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,k1] is V22() Element of [:NAT,NAT:]
{3,k1} is non empty finite V37() set
{3} is non empty trivial finite V37() 1 -element set
{{3,k1},{3}} is non empty finite V37() set
(elementary_tree 2) --> [2,0] is Relation-like elementary_tree 2 -defined [:NAT,NAT:] -valued Function-like V30( elementary_tree 2,[:NAT,NAT:]) finite DecoratedTree-like Element of bool [:(elementary_tree 2),[:NAT,NAT:]:]
[:(elementary_tree 2),[:NAT,NAT:]:] is Relation-like non empty non trivial non finite set
bool [:(elementary_tree 2),[: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 2) --> [2,0]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) with-replacement (<*1*>,F) is Relation-like Function-like DecoratedTree-like set
proj1 F is non empty finite Tree-like set
proj1 F is non empty finite Tree-like set
dom ((elementary_tree 2) --> [2,0]) is non empty finite Tree-like Element of bool (elementary_tree 2)
bool (elementary_tree 2) is non empty finite V37() set
([:NAT,NAT:],((elementary_tree 2) --> [2,0]),F,<*0*>) is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like set
k2 is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like set
proj1 k2 is non empty Tree-like set
(dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of elementary_tree 2
k1 is non empty finite Tree-like set
(elementary_tree 2) with-replacement (A,k1) is non empty finite Tree-like set
A1 is non empty finite Tree-like set
proj1 ((((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) with-replacement (<*1*>,F)) is non empty Tree-like set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of A1
B is non empty finite Tree-like set
A1 with-replacement (G,B) is non empty finite Tree-like set
([:NAT,NAT:],k2,F,<*1*>) is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like set
k is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
proj1 k is non empty finite Tree-like set
(proj1 k2) with-replacement (<*1*>,(proj1 F)) is non empty Tree-like set
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 k
((proj1 k),v) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k . v is Element of [:NAT,NAT:]
k2 . v is set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ s is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
((elementary_tree 2) --> [2,0]) . v is set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ s is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
succ v is finite Element of bool (proj1 k)
bool (proj1 k) is non empty finite V37() set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom ((elementary_tree 2) --> [2,0])
succ s is finite Element of bool (dom ((elementary_tree 2) --> [2,0]))
bool (dom ((elementary_tree 2) --> [2,0])) is non empty finite V37() set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 k2
succ s is Element of bool (proj1 k2)
bool (proj1 k2) is non empty set
s is set
{ (s ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : s ^ <*b1*> in dom ((elementary_tree 2) --> [2,0]) } is set
v9 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
<*v9*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
s ^ <*v9*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
s ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
{ (s ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : s ^ <*b1*> in dom ((elementary_tree 2) --> [2,0]) } is set
s ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
{ (s ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : s ^ <*b1*> in dom ((elementary_tree 2) --> [2,0]) } is set
s ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
s ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
card (succ v) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ s is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F . s is set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ s is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F . s is set
succ v is finite Element of bool (proj1 k)
bool (proj1 k) is non empty finite V37() set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
succ s is finite Element of bool (proj1 F)
bool (proj1 F) is non empty finite V37() set
v9 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 k2
succ v9 is Element of bool (proj1 k2)
bool (proj1 k2) is non empty set
card (succ v) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
card (succ s) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
((proj1 F),s) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F . s is Element of [:NAT,NAT:]
v9 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,v9] is V22() Element of [:NAT,NAT:]
{3,v9} is non empty finite V37() set
{3} is non empty trivial finite V37() 1 -element set
{{3,v9},{3}} is non empty finite V37() set
((elementary_tree 2) --> [2,0]) . v is set
s is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,s] is V22() Element of [:NAT,NAT:]
{3,s} is non empty finite V37() set
{3} is non empty trivial finite V37() 1 -element set
{{3,s},{3}} is non empty finite V37() set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ s is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F . s is set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ s is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F . s is set
succ v is finite Element of bool (proj1 k)
bool (proj1 k) is non empty finite V37() set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
succ s is finite Element of bool (proj1 F)
bool (proj1 F) is non empty finite V37() set
card (succ v) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
card (succ s) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
((proj1 F),s) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F . s is Element of [:NAT,NAT:]
v9 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,v9] is V22() Element of [:NAT,NAT:]
{3,v9} is non empty finite V37() set
{3} is non empty trivial finite V37() 1 -element set
{{3,v9},{3}} is non empty finite V37() set
k2 . v is set
s is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,s] is V22() Element of [:NAT,NAT:]
{3,s} is non empty finite V37() set
{3} is non empty trivial finite V37() 1 -element set
{{3,s},{3}} is non empty finite V37() 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
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) with-replacement (<*1*>,F) is Relation-like Function-like DecoratedTree-like set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(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
((F)) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,(F)) is Relation-like Function-like DecoratedTree-like 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
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(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
((F),(F)) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,(F)) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,(F))) with-replacement (<*1*>,(F)) is Relation-like Function-like DecoratedTree-like set
(((F),(F))) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,((F),(F))) is Relation-like Function-like DecoratedTree-like set
(F,(F)) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) with-replacement (<*1*>,(F)) is Relation-like Function-like DecoratedTree-like set
((F,(F))) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,(F,(F))) is Relation-like Function-like DecoratedTree-like set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
[3,F] is V22() Element of [:NAT,NAT:]
{3,F} is non empty finite V37() set
{3} is non empty trivial finite V37() 1 -element set
{{3,F},{3}} is non empty finite V37() set
(elementary_tree 0) --> [3,F] is Relation-like elementary_tree 0 -defined [:NAT,NAT:] -valued Function-like V30( elementary_tree 0,[:NAT,NAT:]) finite DecoratedTree-like Element of bool [:(elementary_tree 0),[:NAT,NAT:]:]
[:(elementary_tree 0),[:NAT,NAT:]:] is Relation-like non empty non trivial non finite set
bool [:(elementary_tree 0),[:NAT,NAT:]:] is non empty non trivial non finite set
dom ((elementary_tree 0) --> [3,F]) is non empty finite Tree-like Element of bool (elementary_tree 0)
bool (elementary_tree 0) is non empty finite V37() set
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
proj1 A is non empty finite Tree-like set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A
((proj1 A),G) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . G is Element of [:NAT,NAT:]
succ G is finite Element of bool (proj1 A)
bool (proj1 A) is non empty finite V37() set
the Element of succ G is Element of succ G
{ (G ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : G ^ <*b1*> in proj1 A } is 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
(elementary_tree 0) --> [0,0] is Relation-like elementary_tree 0 -defined [:NAT,NAT:] -valued Function-like V30( elementary_tree 0,[:NAT,NAT:]) finite DecoratedTree-like Element of bool [:(elementary_tree 0),[:NAT,NAT:]:]
[:(elementary_tree 0),[:NAT,NAT:]:] is Relation-like non empty non trivial non finite set
bool [:(elementary_tree 0),[:NAT,NAT:]:] is non empty non trivial non finite set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set
proj1 F 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 F
((proj1 F),A) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F . A is Element of [:NAT,NAT:]
succ A is finite Element of bool (proj1 F)
bool (proj1 F) is non empty finite V37() set
the Element of succ A is Element of succ A
{ (A ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : A ^ <*b1*> in proj1 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
A ^ <*A*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F is Element of ()
(elementary_tree 0) --> F is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
[:(elementary_tree 0),():] is Relation-like non empty set
bool [:(elementary_tree 0),():] is non empty 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 Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> F is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F is Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> F is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
(F) . {} is 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,F] is V22() Element of [:NAT,NAT:]
{F,F} is non empty finite V37() set
{F} is non empty trivial finite V37() 1 -element set
{{F,F},{F}} is non empty finite V37() set
(elementary_tree 1) --> [F,F] 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:]:]
dom ((elementary_tree 1) --> [F,F]) is non empty finite Tree-like Element of bool (elementary_tree 1)
bool (elementary_tree 1) is non empty finite V37() set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(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
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(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
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
dom ((elementary_tree 1) --> [1,1]) is non empty finite Tree-like Element of bool (elementary_tree 1)
bool (elementary_tree 1) is non empty finite V37() set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F,F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) with-replacement (<*1*>,F) is Relation-like Function-like DecoratedTree-like set
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A,G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,G) is Relation-like Function-like DecoratedTree-like set
dom ((elementary_tree 2) --> [2,0]) 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) --> [2,0]) with-replacement (<*0*>,A)) is non empty Tree-like set
proj1 A is non empty finite Tree-like set
(dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(proj1 A)) is non empty Tree-like set
proj1 F is non empty finite Tree-like set
(dom ((elementary_tree 2) --> [2,0])) with-replacement (<*1*>,(proj1 F)) is non empty Tree-like set
proj1 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) is non empty Tree-like set
proj1 F is non empty finite Tree-like set
(dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
proj1 (F,F) is non empty finite Tree-like set
(proj1 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F))) with-replacement (<*1*>,(proj1 F)) is non empty Tree-like set
proj1 (A,G) is non empty finite Tree-like set
proj1 G is non empty finite Tree-like set
(proj1 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A))) with-replacement (<*1*>,(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
<*1*> ^ 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
<*1*> ^ 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
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F . k2 is set
G . k2 is set
<*1*> ^ k2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A,G) . (<*1*> ^ k2) is set
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
G . A1 is set
(F,F) . (<*1*> ^ k2) 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
F . G is set
((dom ((elementary_tree 2) --> [2,0])) with-replacement (<*1*>,(proj1 F))) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
((dom ((elementary_tree 2) --> [2,0])) with-replacement (<*1*>,(proj1 F))) with-replacement (<*0*>,(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 . k2 is set
A . k2 is set
<*0*> ^ k2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) . (<*0*> ^ k2) is set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) . (<*0*> ^ k2) is set
(F,F) . (<*0*> ^ k2) is set
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
F . A1 is set
(A,F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,F) is Relation-like Function-like DecoratedTree-like set
(A,F) . (<*0*> ^ k2) is set
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ A1 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F . A1 is set
(A,G) . (<*0*> ^ k2) is set
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
G . A1 is set
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ A1 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
A . A1 is set
() is Relation-like [:NAT,NAT:] -valued Function-like finite 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
card (proj1 F) is non empty 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 proj1 F
succ A is finite Element of bool (proj1 F)
bool (proj1 F) is non empty finite V37() set
the Element of succ A is Element of succ A
{ (A ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT : A ^ <*b1*> in proj1 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
A ^ <*A*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
((proj1 F),A) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F . A is Element of [:NAT,NAT:]
G is set
F . G is set
F . A 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
B is set
F . B is set
A is Element of ()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> A is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F . A is Element of [:NAT,NAT:]
G is Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> G is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
((proj1 F)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
((proj1 F),((proj1 F))) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
succ ((proj1 F)) is finite Element of bool (proj1 F)
bool (proj1 F) is non empty finite V37() set
card (succ ((proj1 F))) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G is set
{G} 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 proj1 F
(F,A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
F . ((proj1 F)) is Element of [:NAT,NAT:]
([:NAT,NAT:],F) is Element of [:NAT,NAT:]
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,B) is Relation-like Function-like DecoratedTree-like set
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,B) is Relation-like Function-like DecoratedTree-like set
F . ((proj1 F)) is Element of [:NAT,NAT:]
([:NAT,NAT:],F) is Element of [:NAT,NAT:]
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,B) is Relation-like Function-like DecoratedTree-like set
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,B) is Relation-like Function-like DecoratedTree-like set
F . ((proj1 F)) is Element of [:NAT,NAT:]
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,B) is Relation-like Function-like DecoratedTree-like set
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,B) is Relation-like Function-like DecoratedTree-like set
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,B) is Relation-like Function-like DecoratedTree-like set
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,B) is Relation-like Function-like DecoratedTree-like set
succ ((proj1 F)) is finite Element of bool (proj1 F)
bool (proj1 F) is non empty finite V37() set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
(F,G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
(F,A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
([:NAT,NAT:],F) is Element of [:NAT,NAT:]
F . ((proj1 F)) is Element of [:NAT,NAT:]
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
k1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(B,k1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) with-replacement (<*1*>,k1) is Relation-like Function-like DecoratedTree-like set
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is Relation-like Function-like DecoratedTree-like set
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
k1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(B,k1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) with-replacement (<*1*>,k1) is Relation-like Function-like DecoratedTree-like set
k2 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k2) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,k2) is Relation-like Function-like DecoratedTree-like set
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A1) is Relation-like Function-like DecoratedTree-like set
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
k is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G,k) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,G)) with-replacement (<*1*>,k) is Relation-like Function-like DecoratedTree-like set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(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
proj1 (F) is non empty finite Tree-like set
card (proj1 (F)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
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
(dom ((elementary_tree 1) --> [1,0])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
G 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 Element of proj1 (F)
A ^ G 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
(proj1 (F)) | A is non empty finite Tree-like set
((proj1 (F))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (F)
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
proj1 (F) is non empty finite Tree-like set
card (proj1 (F)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
dom ((elementary_tree 1) --> [1,1]) is non empty finite Tree-like Element of bool (elementary_tree 1)
bool (elementary_tree 1) is non empty finite V37() set
(dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
G 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 Element of proj1 (F)
A ^ G 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
(proj1 (F)) | A is non empty finite Tree-like set
((proj1 (F))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (F)
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F,F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) with-replacement (<*1*>,F) is Relation-like Function-like DecoratedTree-like set
proj1 (F,F) is non empty finite Tree-like set
card (proj1 (F,F)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
dom ((elementary_tree 2) --> [2,0]) 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) --> [2,0]) with-replacement (<*0*>,F)) is non empty Tree-like set
(dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
(proj1 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F))) with-replacement (<*1*>,(proj1 F)) is non empty Tree-like set
k1 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 proj1 (F,F)
B ^ 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
<*1*> ^ k2 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
B ^ k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(proj1 (F,F)) | B is non empty finite Tree-like set
k1 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 Element of proj1 (F,F)
A ^ 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
<*1*> ^ k2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(proj1 (F,F)) | A is non empty finite Tree-like set
((proj1 (F,F))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (F,F)
[3,0] is V22() Element of [:NAT,NAT:]
{3,0} is non empty finite V37() set
{3} is non empty trivial finite V37() 1 -element set
{{3,0},{3}} is non empty finite V37() set
F is Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> F is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
(()) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,()) is Relation-like Function-like DecoratedTree-like set
(()) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,()) is Relation-like Function-like DecoratedTree-like set
((),()) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,()) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,())) with-replacement (<*1*>,()) is Relation-like Function-like DecoratedTree-like set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
((proj1 F)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
((proj1 F),((proj1 F))) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A is Element of ()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> A is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
succ ((proj1 F)) is finite Element of bool (proj1 F)
bool (proj1 F) is non empty finite V37() set
([:NAT,NAT:],F) is Element of [:NAT,NAT:]
F . ((proj1 F)) is Element of [:NAT,NAT:]
(elementary_tree 1) --> ([:NAT,NAT:],F) 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
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
(F,A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> ([:NAT,NAT:],F)) with-replacement (<*0*>,(F,A)) is Relation-like Function-like DecoratedTree-like set
proj1 (F,A) is non empty finite Tree-like set
(proj1 F) | A is non empty finite Tree-like set
card (proj1 (F,A)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
((F,A)) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,(F,A)) is Relation-like Function-like DecoratedTree-like set
proj1 (F,A) is non empty finite Tree-like set
(proj1 F) | A is non empty finite Tree-like set
card (proj1 (F,A)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
((F,A)) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,(F,A)) is Relation-like Function-like DecoratedTree-like set
succ ((proj1 F)) is finite Element of bool (proj1 F)
bool (proj1 F) is non empty finite V37() set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
(F,A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 (F,A) is non empty finite Tree-like set
(proj1 F) | A is non empty finite Tree-like set
card (proj1 (F,A)) is non empty 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 F
(F,B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 (F,B) is non empty finite Tree-like set
(proj1 F) | B is non empty finite Tree-like set
card (proj1 (F,B)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
([:NAT,NAT:],F) is Element of [:NAT,NAT:]
F . ((proj1 F)) is Element of [:NAT,NAT:]
(elementary_tree 2) --> ([:NAT,NAT:],F) is Relation-like elementary_tree 2 -defined [:NAT,NAT:] -valued Function-like V30( elementary_tree 2,[:NAT,NAT:]) finite DecoratedTree-like Element of bool [:(elementary_tree 2),[:NAT,NAT:]:]
[:(elementary_tree 2),[:NAT,NAT:]:] is Relation-like non empty non trivial non finite set
bool [:(elementary_tree 2),[:NAT,NAT:]:] is non empty non trivial non finite set
((elementary_tree 2) --> ([:NAT,NAT:],F)) with-replacement (<*0*>,(F,A)) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> ([:NAT,NAT:],F)) with-replacement (<*0*>,(F,A))) with-replacement (<*1*>,(F,B)) is Relation-like Function-like DecoratedTree-like set
((F,A),(F,B)) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,(F,A)) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,(F,A))) with-replacement (<*1*>,(F,B)) is Relation-like Function-like DecoratedTree-like set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(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
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F,F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) with-replacement (<*1*>,F) is Relation-like Function-like DecoratedTree-like set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
F is Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> F is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F is Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> F is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is Relation-like Function-like DecoratedTree-like set
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A,B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is Relation-like Function-like DecoratedTree-like set
F is Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> F is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(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
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F,A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) with-replacement (<*1*>,A) is Relation-like Function-like DecoratedTree-like set
proj1 (F) is non empty finite Tree-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
proj1 (F) is non empty finite Tree-like set
proj1 F is non empty finite Tree-like set
(elementary_tree 1) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
dom ((elementary_tree 1) --> [1,1]) is non empty finite Tree-like Element of bool (elementary_tree 1)
proj1 (F) is non empty finite Tree-like set
dom ((elementary_tree 2) --> [2,0]) 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) --> [2,0]) with-replacement (<*0*>,F)) is non empty Tree-like set
(dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
proj1 (F,A) is non empty finite Tree-like set
proj1 A is non empty finite Tree-like set
(proj1 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F))) with-replacement (<*1*>,(proj1 A)) is non empty Tree-like set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(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
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F,A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) with-replacement (<*1*>,A) is Relation-like Function-like DecoratedTree-like set
proj1 (F) is non empty finite Tree-like set
proj1 (F) is non empty finite Tree-like set
proj1 F is non empty finite Tree-like set
k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (F)
(F) . k2 is set
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ A1 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F . A1 is 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
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
dom ((elementary_tree 1) --> [1,1]) is non empty finite Tree-like Element of bool (elementary_tree 1)
(dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
((elementary_tree 1) --> [1,1]) . k2 is set
((elementary_tree 1) --> [1,0]) . k2 is set
(F) . k2 is Element of [:NAT,NAT:]
A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ A1 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
F . A1 is set
dom ((elementary_tree 2) --> [2,0]) 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) --> [2,0]) with-replacement (<*0*>,F)) is non empty Tree-like set
(dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
proj1 (F,A) is non empty finite Tree-like set
proj1 A is non empty finite Tree-like set
(proj1 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F))) with-replacement (<*1*>,(proj1 A)) is non empty Tree-like 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
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F,A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) with-replacement (<*1*>,A) is Relation-like Function-like DecoratedTree-like set
dom ((elementary_tree 2) --> [2,0]) 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) --> [2,0]) with-replacement (<*0*>,F)) is non empty Tree-like set
proj1 F is non empty finite Tree-like set
(dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
proj1 (F,A) is non empty finite Tree-like set
proj1 A is non empty finite Tree-like set
(proj1 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F))) with-replacement (<*1*>,(proj1 A)) is non empty Tree-like set
dom ((elementary_tree 1) --> [1,1]) is non empty finite Tree-like Element of bool (elementary_tree 1)
bool (elementary_tree 1) is non empty finite V37() set
proj1 (F) is non empty finite Tree-like set
proj1 F is non empty finite Tree-like set
(dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
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
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(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
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(F,F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F)) with-replacement (<*1*>,F) is Relation-like Function-like DecoratedTree-like set
proj1 () is non empty finite Tree-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
proj1 (F) is non empty finite 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
dom ((elementary_tree 1) --> [1,1]) is non empty finite Tree-like Element of bool (elementary_tree 1)
proj1 (F) is non empty finite Tree-like set
(dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
dom ((elementary_tree 2) --> [2,0]) 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) --> [2,0]) with-replacement (<*0*>,F)) is non empty Tree-like set
(dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set
proj1 (F,F) is non empty finite Tree-like set
proj1 F is non empty finite Tree-like set
(proj1 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,F))) with-replacement (<*1*>,(proj1 F)) is non empty Tree-like set
F is Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> F is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
rng (F) is Relation-like NAT -defined NAT -valued finite Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
{F} is non empty trivial finite 1 -element Element of bool ()
bool () is non empty set
rng () is Relation-like NAT -defined NAT -valued finite Element of bool [:NAT,NAT:]
{[0,0]} is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element Element of bool [:NAT,NAT:]
F is Element of ()
(F) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> F is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(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
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is Relation-like Function-like DecoratedTree-like set
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G,A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,G)) with-replacement (<*1*>,A) is Relation-like Function-like DecoratedTree-like set
F1() is non empty set
[:(),F1():] is Relation-like non empty set
bool [:(),F1():] is non empty set
F2() is Element of F1()
F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A is non empty finite Tree-like set
card (proj1 A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F . A is Element of F1()
G is Element of F1()
A is Element of ()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> A is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(A) is Element of F1()
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,B) is Relation-like Function-like DecoratedTree-like set
F . B is Element of F1()
F4((F . B)) is Element of F1()
k1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,k1) is Relation-like Function-like DecoratedTree-like set
F . k1 is Element of F1()
F5((F . k1)) is Element of F1()
k2 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k2,A1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,k2) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,k2)) with-replacement (<*1*>,A1) is Relation-like Function-like DecoratedTree-like set
F . k2 is Element of F1()
F . A1 is Element of F1()
F6((F . k2),(F . A1)) is Element of F1()
G is Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> G is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
G is Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> G is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(G) is Element of F1()
A is Element of F1()
B is Element of ()
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> B is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(B) is Element of F1()
k1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,k1) is Relation-like Function-like DecoratedTree-like set
F . k1 is Element of F1()
F4((F . k1)) is Element of F1()
k2 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k2) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,k2) is Relation-like Function-like DecoratedTree-like set
F . k2 is Element of F1()
F5((F . k2)) is Element of F1()
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A1,G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) with-replacement (<*1*>,G) is Relation-like Function-like DecoratedTree-like set
F . A1 is Element of F1()
F . G is Element of F1()
F6((F . A1),(F . G)) is Element of F1()
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
F . G is Element of F1()
F4((F . G)) is Element of F1()
A is Element of F1()
B is Element of ()
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> B is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(B) is Element of F1()
k1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,k1) is Relation-like Function-like DecoratedTree-like set
F . k1 is Element of F1()
F4((F . k1)) is Element of F1()
k2 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k2) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,k2) is Relation-like Function-like DecoratedTree-like set
F . k2 is Element of F1()
F5((F . k2)) is Element of F1()
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A1,G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) with-replacement (<*1*>,G) is Relation-like Function-like DecoratedTree-like set
F . A1 is Element of F1()
F . G is Element of F1()
F6((F . A1),(F . G)) is Element of F1()
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
F . G is Element of F1()
F5((F . G)) is Element of F1()
A is Element of F1()
B is Element of ()
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> B is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(B) is Element of F1()
k1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,k1) is Relation-like Function-like DecoratedTree-like set
F . k1 is Element of F1()
F4((F . k1)) is Element of F1()
k2 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k2) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,k2) is Relation-like Function-like DecoratedTree-like set
F . k2 is Element of F1()
F5((F . k2)) is Element of F1()
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A1,G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) with-replacement (<*1*>,G) is Relation-like Function-like DecoratedTree-like set
F . A1 is Element of F1()
F . G is Element of F1()
F6((F . A1),(F . G)) is Element of F1()
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G,A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,G)) with-replacement (<*1*>,A) is Relation-like Function-like DecoratedTree-like set
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G,A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,G)) with-replacement (<*1*>,A) is Relation-like Function-like DecoratedTree-like set
F . G is Element of F1()
F . A is Element of F1()
F6((F . G),(F . A)) is Element of F1()
k1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
k2 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k1,k2) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,k1) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,k1)) with-replacement (<*1*>,k2) is Relation-like Function-like DecoratedTree-like set
B is Element of F1()
F . k1 is Element of F1()
F . k2 is Element of F1()
F6((F . k1),(F . k2)) is Element of F1()
k1 is Element of ()
(k1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> k1 is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(k1) is Element of F1()
k2 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k2) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,k2) is Relation-like Function-like DecoratedTree-like set
F . k2 is Element of F1()
F4((F . k2)) is Element of F1()
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A1) is Relation-like Function-like DecoratedTree-like set
F . A1 is Element of F1()
F5((F . A1)) is Element of F1()
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
k is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G,k) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,G)) with-replacement (<*1*>,k) is Relation-like Function-like DecoratedTree-like set
F . G is Element of F1()
F . k is Element of F1()
F6((F . G),(F . k)) is Element of F1()
A is Element of F1()
B is Element of ()
(B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> B is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
k1 is Element of F1()
k2 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k2) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,k2) is Relation-like Function-like DecoratedTree-like set
A1 is Element of F1()
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
k is Element of F1()
a is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
v is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(a,v) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,a) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,a)) with-replacement (<*1*>,v) is Relation-like Function-like DecoratedTree-like set
s is Element of F1()
A is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
G is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A is non empty finite Tree-like set
card (proj1 A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . A is Element of F1()
F . A is Element of F1()
k1 is Element of ()
(k1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> k1 is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(k1) is Element of F1()
F . A is Element of F1()
k1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,k1) is Relation-like Function-like DecoratedTree-like set
G . k1 is Element of F1()
F4((G . k1)) is Element of F1()
proj1 k1 is non empty finite Tree-like set
card (proj1 k1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F . k1 is Element of F1()
F . A is Element of F1()
k1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,k1) is Relation-like Function-like DecoratedTree-like set
G . k1 is Element of F1()
F5((G . k1)) is Element of F1()
proj1 k1 is non empty finite Tree-like set
card (proj1 k1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F . k1 is Element of F1()
F . A is Element of F1()
k1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
G . k1 is Element of F1()
k2 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k1,k2) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,k1) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,k1)) with-replacement (<*1*>,k2) is Relation-like Function-like DecoratedTree-like set
G . k2 is Element of F1()
F6((G . k1),(G . k2)) is Element of F1()
proj1 k1 is non empty finite Tree-like set
card (proj1 k1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F . k1 is Element of F1()
proj1 k2 is non empty finite Tree-like set
card (proj1 k2) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
F . k2 is Element of F1()
F . A is Element of F1()
the Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():] is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
the Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():] . F is Element of F1()
A is Element of ()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> A is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(A) is Element of F1()
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,G) is Relation-like Function-like DecoratedTree-like set
the Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():] . G is Element of F1()
F4(( the Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():] . G)) is Element of F1()
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is Relation-like Function-like DecoratedTree-like set
the Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():] . A is Element of F1()
F5(( the Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():] . A)) is Element of F1()
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
k1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(B,k1) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) with-replacement (<*1*>,k1) is Relation-like Function-like DecoratedTree-like set
the Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():] . B is Element of F1()
the Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():] . k1 is Element of F1()
F6(( the Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():] . B),( the Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():] . k1)) is Element of F1()
F is set
F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 F is non empty finite Tree-like set
card (proj1 F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
A . F is set
G is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
G . F is Element of F1()
A is Element of ()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> A is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
proj1 (A) is non empty finite Tree-like set
card (proj1 (A)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . (A) is Element of F1()
G . (A) is Element of F1()
F3(A) is Element of F1()
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A is non empty finite Tree-like set
card (proj1 A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . A is Element of F1()
G . A is Element of F1()
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 B is non empty finite Tree-like set
card (proj1 B) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . B is Element of F1()
G . B is Element of F1()
(A,B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is Relation-like Function-like DecoratedTree-like set
proj1 (A,B) is non empty finite Tree-like set
card (proj1 (A,B)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . (A,B) is Element of F1()
G . (A,B) is Element of F1()
F6((G . A),(G . B)) is Element of F1()
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A is non empty finite Tree-like set
card (proj1 A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . A is Element of F1()
G . A is Element of F1()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is Relation-like Function-like DecoratedTree-like set
proj1 (A) is non empty finite Tree-like set
card (proj1 (A)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . (A) is Element of F1()
G . (A) is Element of F1()
F5((G . A)) is Element of F1()
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A is non empty finite Tree-like set
card (proj1 A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . A is Element of F1()
G . A is Element of F1()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is Relation-like Function-like DecoratedTree-like set
proj1 (A) is non empty finite Tree-like set
card (proj1 (A)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . (A) is Element of F1()
G . (A) is Element of F1()
F4((G . A)) is Element of F1()
proj1 () is non empty finite Tree-like set
card (proj1 ()) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A . () is Element of F1()
G . () is Element of F1()
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
F is set
A is set
F . A is set
G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 G is non empty finite Tree-like set
card (proj1 G) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
A . G is Element of F1()
F is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
F . () is Element of F1()
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A is non empty finite Tree-like set
card (proj1 A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
G . () is Element of F1()
A is Element of ()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> A is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F . (A) is Element of F1()
F3(A) is Element of F1()
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 B is non empty finite Tree-like set
card (proj1 B) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k1 is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
k1 . (A) is Element of F1()
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is Relation-like Function-like DecoratedTree-like set
F . (A) is Element of F1()
F . A is Element of F1()
F4((F . A)) is Element of F1()
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 B is non empty finite Tree-like set
card (proj1 B) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k1 is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
proj1 (A) is non empty finite Tree-like set
card (proj1 (A)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A1 is non empty finite Tree-like set
card (proj1 A1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k1 . A1 is Element of F1()
G is Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> G is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(G) is Element of F1()
k is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,k) is Relation-like Function-like DecoratedTree-like set
k1 . k is Element of F1()
F4((k1 . k)) is Element of F1()
a is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(a) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,a) is Relation-like Function-like DecoratedTree-like set
k1 . a is Element of F1()
F5((k1 . a)) is Element of F1()
v is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
s is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(v,s) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,v) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,v)) with-replacement (<*1*>,s) is Relation-like Function-like DecoratedTree-like set
k1 . v is Element of F1()
k1 . s is Element of F1()
F6((k1 . v),(k1 . s)) is Element of F1()
proj1 A is non empty finite Tree-like set
card (proj1 A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A1 is non empty finite Tree-like set
card (proj1 A1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k1 . A1 is Element of F1()
G is Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> G is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(G) is Element of F1()
k is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,k) is Relation-like Function-like DecoratedTree-like set
k1 . k is Element of F1()
F4((k1 . k)) is Element of F1()
a is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(a) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,a) is Relation-like Function-like DecoratedTree-like set
k1 . a is Element of F1()
F5((k1 . a)) is Element of F1()
v is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
s is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(v,s) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,v) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,v)) with-replacement (<*1*>,s) is Relation-like Function-like DecoratedTree-like set
k1 . v is Element of F1()
k1 . s is Element of F1()
F6((k1 . v),(k1 . s)) is Element of F1()
k1 . A is Element of F1()
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A1 is non empty finite Tree-like set
card (proj1 A1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k1 . (A) is Element of F1()
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is Relation-like Function-like DecoratedTree-like set
F . (A) is Element of F1()
F . A is Element of F1()
F5((F . A)) is Element of F1()
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 B is non empty finite Tree-like set
card (proj1 B) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k1 is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
proj1 (A) is non empty finite Tree-like set
card (proj1 (A)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A1 is non empty finite Tree-like set
card (proj1 A1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k1 . A1 is Element of F1()
G is Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> G is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(G) is Element of F1()
k is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,k) is Relation-like Function-like DecoratedTree-like set
k1 . k is Element of F1()
F4((k1 . k)) is Element of F1()
a is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(a) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,a) is Relation-like Function-like DecoratedTree-like set
k1 . a is Element of F1()
F5((k1 . a)) is Element of F1()
v is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
s is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(v,s) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,v) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,v)) with-replacement (<*1*>,s) is Relation-like Function-like DecoratedTree-like set
k1 . v is Element of F1()
k1 . s is Element of F1()
F6((k1 . v),(k1 . s)) is Element of F1()
proj1 A is non empty finite Tree-like set
card (proj1 A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A1 is non empty finite Tree-like set
card (proj1 A1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k1 . A1 is Element of F1()
G is Element of ()
(G) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> G is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(G) is Element of F1()
k is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(k) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,k) is Relation-like Function-like DecoratedTree-like set
k1 . k is Element of F1()
F4((k1 . k)) is Element of F1()
a is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(a) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,a) is Relation-like Function-like DecoratedTree-like set
k1 . a is Element of F1()
F5((k1 . a)) is Element of F1()
v is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
s is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(v,s) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,v) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,v)) with-replacement (<*1*>,s) is Relation-like Function-like DecoratedTree-like set
k1 . v is Element of F1()
k1 . s is Element of F1()
F6((k1 . v),(k1 . s)) is Element of F1()
k1 . A is Element of F1()
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A1 is non empty finite Tree-like set
card (proj1 A1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k1 . (A) is Element of F1()
A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(A,B) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is Relation-like Function-like DecoratedTree-like set
F . (A,B) is Element of F1()
F . A is Element of F1()
F . B is Element of F1()
F6((F . A),(F . B)) is Element of F1()
proj1 A is non empty finite Tree-like set
card (proj1 A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
proj1 B is non empty finite Tree-like set
card (proj1 B) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 A1 is non empty finite Tree-like set
card (proj1 A1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G is Relation-like () -defined F1() -valued Function-like V30((),F1()) Element of bool [:(),F1():]
proj1 (A,B) is non empty finite Tree-like set
card (proj1 (A,B)) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k 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 Element of ()
proj1 a is non empty finite Tree-like set
card (proj1 a) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . a is Element of F1()
v is Element of ()
(v) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> v is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(v) is Element of F1()
s is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(s) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,s) is Relation-like Function-like DecoratedTree-like set
G . s is Element of F1()
F4((G . s)) is Element of F1()
s is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(s) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,s) is Relation-like Function-like DecoratedTree-like set
G . s is Element of F1()
F5((G . s)) is Element of F1()
v9 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
c17 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(v9,c17) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,v9) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,v9)) with-replacement (<*1*>,c17) is Relation-like Function-like DecoratedTree-like set
G . v9 is Element of F1()
G . c17 is Element of F1()
F6((G . v9),(G . c17)) is Element of F1()
k is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 k is non empty finite Tree-like set
card (proj1 k) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . k is Element of F1()
a is Element of ()
(a) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> a is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(a) is Element of F1()
v is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(v) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,v) is Relation-like Function-like DecoratedTree-like set
G . v is Element of F1()
F4((G . v)) is Element of F1()
s is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(s) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,s) is Relation-like Function-like DecoratedTree-like set
G . s is Element of F1()
F5((G . s)) is Element of F1()
s is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
v9 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(s,v9) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,s) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,s)) with-replacement (<*1*>,v9) is Relation-like Function-like DecoratedTree-like set
G . s is Element of F1()
G . v9 is Element of F1()
F6((G . s),(G . v9)) is Element of F1()
G . A is Element of F1()
k is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 k is non empty finite Tree-like set
card (proj1 k) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
k is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 k is non empty finite Tree-like set
card (proj1 k) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . k is Element of F1()
a is Element of ()
(a) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(elementary_tree 0) --> a is Relation-like elementary_tree 0 -defined () -valued Function-like V30( elementary_tree 0,()) finite DecoratedTree-like Element of bool [:(elementary_tree 0),():]
F3(a) is Element of F1()
v is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(v) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,v) is Relation-like Function-like DecoratedTree-like set
G . v is Element of F1()
F4((G . v)) is Element of F1()
s is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(s) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,s) is Relation-like Function-like DecoratedTree-like set
G . s is Element of F1()
F5((G . s)) is Element of F1()
s is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
v9 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
(s,v9) is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,s) is Relation-like Function-like DecoratedTree-like set
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,s)) with-replacement (<*1*>,v9) is Relation-like Function-like DecoratedTree-like set
G . s is Element of F1()
G . v9 is Element of F1()
F6((G . s),(G . v9)) is Element of F1()
G . B is Element of F1()
k is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()
proj1 k is non empty finite Tree-like set
card (proj1 k) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT
G . (A,B) is Element of F1()