REAL is set
NAT is non empty non trivial V24() V25() V26() non finite V41() V42() Element of bool REAL
bool REAL is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
{{},1} is non empty finite V40() set
COMPLEX is set
NAT is non empty non trivial V24() V25() V26() non finite V41() V42() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
2 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
3 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
Seg 1 is non empty trivial finite V43(1) Element of bool NAT
{1} is non empty trivial finite V40() V43(1) set
Seg 2 is non empty finite V43(2) Element of bool NAT
{1,2} is non empty finite V40() set
ProperPrefixes {} is finite set
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty proper V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered 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
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not 0 <= b1 } is set
{{}} is functional non empty trivial finite V40() V43(1) Tree-like set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not 0 <= b1 } \/ {{}} is non empty set
elementary_tree 1 is non empty finite Tree-like set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not 1 <= b1 } is set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not 1 <= b1 } \/ {{}} is non empty set
<*0*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
{{},<*0*>} is functional non empty finite V40() set
elementary_tree 2 is non empty finite Tree-like set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not 2 <= b1 } is set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not 2 <= b1 } \/ {{}} is non empty set
<*1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
K89({},<*0*>,<*1*>) is non empty finite set
p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 . p is set
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x1 ^ x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(x1 ^ x2) . p is set
dom x1 is finite Element of bool NAT
bool (NAT *) is non empty set
{ b1 where b1 is functional FinSequence-membered Element of bool (NAT *) : b1 is non empty Tree-like set } is set
x1 is set
x2 is functional FinSequence-membered Element of bool (NAT *)
x2 is non empty Tree-like set
p is set
x1 is set
() is set
the non empty Tree-like set is non empty Tree-like set
bool () is non empty set
{ b1 where b1 is Element of () : b1 is non empty finite Tree-like set } is set
x1 is set
x2 is Element of ()
x1 is Element of bool ()
x2 is set
k is Element of ()
k is non empty finite Tree-like set
p is Element of bool ()
x1 is Element of bool ()
() is Element of bool ()
the non empty finite Tree-like set is non empty finite Tree-like set
p is set
x1 is set
x1 is set
p is set
x1 is set
x1 is set
p is set
x1 is set
p \/ x1 is set
x2 is set
x2 is set
x2 is set
p is set
x1 is set
p \+\ x1 is set
p \ x1 is set
x1 \ p is set
(p \ x1) \/ (x1 \ p) is set
x2 is set
p is set
x1 is set
p /\ x1 is set
x1 /\ p is set
p \ x1 is Element of bool p
bool p is non empty set
x2 is set
x2 is set
p is set
x1 is set
p \/ x1 is set
x2 is set
x2 is set
x2 is set
p is set
x1 is set
p \+\ x1 is set
p \ x1 is set
x1 \ p is set
(p \ x1) \/ (x1 \ p) is set
x2 is set
p is set
x1 is set
p /\ x1 is set
x1 /\ p is set
p \ x1 is Element of bool p
bool p is non empty set
x2 is set
x2 is set
p is set
x1 is set
p \/ x1 is set
x2 is set
x2 is set
x2 is set
p is set
x1 is set
p \+\ x1 is set
p \ x1 is set
x1 \ p is set
(p \ x1) \/ (x1 \ p) is set
x2 is set
p is set
x1 is set
p /\ x1 is set
x1 /\ p is set
p \ x1 is Element of bool p
bool p is non empty set
x2 is set
x2 is set
p is set
x1 is set
x1 is set
x1 is set
p is set
{p} is non empty trivial finite V43(1) set
x1 is set
p is set
{p} is non empty trivial finite V43(1) set
x1 is set
p is set
{p} is non empty trivial finite V43(1) set
x1 is set
p is set
x1 is set
{p,x1} is non empty finite set
x2 is set
p is set
x1 is set
{p,x1} is non empty finite set
x2 is set
p is set
x1 is set
{p,x1} is non empty finite set
x2 is set
p is set
x1 is set
x2 is set
p is set
x1 is set
x2 is set
p is set
x1 is set
x2 is set
the non empty finite Tree-like set is non empty finite Tree-like set
{ the non empty finite Tree-like set } is non empty trivial finite V40() V43(1) set
the Relation-like Function-like DecoratedTree-like set is Relation-like Function-like DecoratedTree-like set
{ the Relation-like Function-like DecoratedTree-like set } is functional non empty trivial finite V43(1) set
p is set
x1 is set
p is () set
bool p is non empty set
x1 is Element of bool p
x2 is set
p is () () set
bool p is non empty set
x1 is () Element of bool p
x2 is set
p is () set
bool p is non empty set
x1 is Element of bool p
x2 is set
p is non empty () set
x1 is Element of p
x2 is Element of p
p is non empty () () set
x1 is non empty Tree-like Element of p
p is set
x1 is set
p is functional non empty () set
x1 is Relation-like Function-like Element of p
p is set
p is set
p is non empty set
[:(elementary_tree 0),p:] is Relation-like non empty set
bool [:(elementary_tree 0),p:] is non empty set
the Element of p is Element of p
(elementary_tree 0) --> the Element of p is Relation-like elementary_tree 0 -defined p -valued Function-like non empty total quasi_total finite DecoratedTree-like Element of bool [:(elementary_tree 0),p:]
{((elementary_tree 0) --> the Element of p)} is functional non empty trivial finite V40() V43(1) Element of bool (bool [:(elementary_tree 0),p:])
bool (bool [:(elementary_tree 0),p:]) is non empty set
x1 is set
p is non empty set
x1 is non empty (p)
x2 is set
p is non empty set
the Relation-like p -valued Function-like DecoratedTree-like set is Relation-like p -valued Function-like DecoratedTree-like set
{ the Relation-like p -valued Function-like DecoratedTree-like set } is functional non empty trivial finite V43(1) set
x2 is set
x2 is functional non empty () set
k is set
k is functional non empty () (p)
p is non empty set
x1 is functional non empty () (p)
x2 is Relation-like Function-like DecoratedTree-like Element of x1
p is non empty Tree-like set
x1 is non empty set
Funcs (p,x1) is functional non empty set
Funcs (p,x1) is functional non empty FUNCTION_DOMAIN of p,x1
k is set
n is Relation-like Function-like set
dom n is set
rng n is set
k is functional non empty () set
n is set
n is Relation-like Function-like set
dom n is set
rng n is set
[:p,x1:] is Relation-like non empty set
bool [:p,x1:] is non empty set
the Relation-like p -defined x1 -valued Function-like non empty total quasi_total Element of bool [:p,x1:] is Relation-like p -defined x1 -valued Function-like non empty total quasi_total Element of bool [:p,x1:]
dom the Relation-like p -defined x1 -valued Function-like non empty total quasi_total Element of bool [:p,x1:] is non empty Element of bool p
bool p is non empty set
rng the Relation-like p -defined x1 -valued Function-like non empty total quasi_total Element of bool [:p,x1:] is non empty Element of bool x1
bool x1 is non empty set
n is functional non empty () (x1)
p is non empty Tree-like set
x1 is non empty set
[:p,x1:] is Relation-like non empty set
bool [:p,x1:] is non empty set
x2 is Relation-like p -defined x1 -valued Function-like non empty total quasi_total Element of bool [:p,x1:]
dom x2 is non empty Element of bool p
bool p is non empty set
p is non empty set
{ (b1,p) where b1 is non empty Tree-like Element of () : verum } is set
union { (b1,p) where b1 is non empty Tree-like Element of () : verum } is set
the non empty Tree-like Element of () is non empty Tree-like Element of ()
the Element of p is Element of p
the non empty Tree-like Element of () --> the Element of p is Relation-like the non empty Tree-like Element of () -defined p -valued Function-like non empty total quasi_total DecoratedTree-like Element of bool [: the non empty Tree-like Element of (),p:]
[: the non empty Tree-like Element of (),p:] is Relation-like non empty set
bool [: the non empty Tree-like Element of (),p:] is non empty set
( the non empty Tree-like Element of (),p) is functional non empty () (p)
n is set
n is set
q is non empty Tree-like Element of ()
(q,p) is functional non empty () (p)
n is functional non empty () set
n is set
q is set
q is non empty Tree-like Element of ()
(q,p) is functional non empty () (p)
n is functional non empty () (p)
q is Relation-like p -valued Function-like DecoratedTree-like set
dom q is non empty Tree-like set
rng q is Element of bool p
bool p is non empty set
q is non empty Tree-like Element of ()
(q,p) is functional non empty () (p)
x1 is functional non empty () (p)
x2 is functional non empty () (p)
k is set
k is set
p is non empty set
(p) is functional non empty () (p)
p is non empty set
(p) is functional non empty () (p)
x1 is set
the Relation-like p -valued Function-like finite DecoratedTree-like set is Relation-like p -valued Function-like finite DecoratedTree-like set
dom the Relation-like p -valued Function-like finite DecoratedTree-like set is non empty finite Tree-like set
k is set
k is functional non empty () (p)
n is Relation-like p -valued Function-like DecoratedTree-like set
dom n is non empty Tree-like set
n is Relation-like p -valued Function-like DecoratedTree-like set
dom n is non empty Tree-like set
x1 is functional non empty () (p)
x2 is functional non empty () (p)
k is set
n is Relation-like p -valued Function-like DecoratedTree-like set
dom n is non empty Tree-like set
k is set
n is Relation-like p -valued Function-like DecoratedTree-like set
dom n is non empty Tree-like set
p is non empty set
(p) is functional non empty () (p)
(p) is functional non empty () (p)
x1 is set
p is Relation-like Function-like set
rng p is set
p is Relation-like Function-like set
dom p is set
rng p is set
x1 is set
p . x1 is set
x1 is set
rng p is set
x2 is set
p . x2 is set
p is Relation-like Function-like set
dom p is set
rng p is set
x1 is set
p . x1 is set
x1 is set
rng p is set
x2 is set
p . x2 is set
p is Relation-like Function-like set
dom p is set
rng p is set
x1 is set
p . x1 is set
x1 is set
rng p is set
x2 is set
p . x2 is set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p ^ x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (p ^ x1) is finite set
rng p is finite set
rng x1 is finite set
(rng p) \/ (rng x1) is finite set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p ^ x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (p ^ x1) is finite set
rng p is finite set
rng x1 is finite set
(rng p) \/ (rng x1) is finite set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p ^ x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (p ^ x1) is finite set
rng p is finite set
rng x1 is finite set
(rng p) \/ (rng x1) is finite set
p is set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like set
{p} is non empty trivial finite V43(1) set
rng <*p*> is non empty trivial finite V43(1) set
p is set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like set
{p} is non empty trivial finite V43(1) set
rng <*p*> is non empty trivial finite V43(1) set
p is set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like set
{p} is non empty trivial finite V43(1) set
rng <*p*> is non empty trivial finite V43(1) set
p is set
x1 is set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like set
{p,x1} is non empty finite set
rng <*p,x1*> is non empty finite set
p is set
x1 is set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like set
{p,x1} is non empty finite set
rng <*p,x1*> is non empty finite set
p is set
x1 is set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like set
{p,x1} is non empty finite set
rng <*p,x1*> is non empty finite set
p is set
x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 |-> p is Relation-like NAT -defined Function-like finite V43(x1) FinSequence-like FinSubsequence-like set
Seg x1 is finite V43(x1) Element of bool NAT
(Seg x1) --> p is Relation-like Seg x1 -defined {p} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg x1),{p}:]
{p} is non empty trivial finite V43(1) set
[:(Seg x1),{p}:] is Relation-like finite set
bool [:(Seg x1),{p}:] is non empty finite V40() set
rng (x1 |-> p) is finite set
p is set
x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 |-> p is Relation-like NAT -defined Function-like finite V43(x1) FinSequence-like FinSubsequence-like set
Seg x1 is finite V43(x1) Element of bool NAT
(Seg x1) --> p is Relation-like Seg x1 -defined {p} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg x1),{p}:]
{p} is non empty trivial finite V43(1) set
[:(Seg x1),{p}:] is Relation-like finite set
bool [:(Seg x1),{p}:] is non empty finite V40() set
rng (x1 |-> p) is finite set
p is set
x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 |-> p is Relation-like NAT -defined Function-like finite V43(x1) FinSequence-like FinSubsequence-like set
Seg x1 is finite V43(x1) Element of bool NAT
(Seg x1) --> p is Relation-like Seg x1 -defined {p} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg x1),{p}:]
{p} is non empty trivial finite V43(1) set
[:(Seg x1),{p}:] is Relation-like finite set
bool [:(Seg x1),{p}:] is non empty finite V40() set
rng (x1 |-> p) is finite set
the non empty finite Tree-like set is non empty finite Tree-like set
<* the non empty finite Tree-like set *> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like set
the Relation-like Function-like DecoratedTree-like set is Relation-like Function-like DecoratedTree-like set
<* the Relation-like Function-like DecoratedTree-like set *> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like set
the Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () () set is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () () set
the Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
p is Relation-like Function-like set
rng p is set
p is non empty () set
x1 is Relation-like NAT -defined p -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of p
x2 is set
rng x1 is finite set
rng x1 is finite () Element of bool p
bool p is non empty set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
p ^ x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p is non empty () () set
x1 is Relation-like NAT -defined p -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of p
x2 is set
rng x1 is finite set
rng x1 is finite () () Element of bool p
bool p is non empty set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () () set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () () set
p ^ x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
p is functional non empty () set
x1 is Relation-like NAT -defined p -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of p
x2 is set
rng x1 is finite set
rng x1 is functional finite () Element of bool p
bool p is non empty set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
p ^ x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like set
x1 is non empty Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like set
p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 is non empty Tree-like set
p |-> x1 is Relation-like NAT -defined Function-like finite V43(p) FinSequence-like FinSubsequence-like set
0 |-> x1 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered () () () () () () set
p is non empty finite Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
x1 is non empty finite Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 is non empty finite Tree-like set
p |-> x1 is Relation-like NAT -defined Function-like finite V43(p) FinSequence-like FinSubsequence-like () set
0 |-> x1 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered () () () () () () set
p is Relation-like Function-like DecoratedTree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like set
x1 is Relation-like Function-like DecoratedTree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like set
p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 is Relation-like Function-like DecoratedTree-like set
p |-> x1 is Relation-like NAT -defined Function-like finite V43(p) FinSequence-like FinSubsequence-like set
0 |-> x1 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered () () () () () () set
p is Relation-like Function-like () set
doms p is Relation-like Function-like set
dom (doms p) is set
dom p is set
rng p is set
SubFuncs (rng p) is set
p " (SubFuncs (rng p)) is set
x1 is set
p . x1 is set
x1 is set
p . x1 is set
(doms p) . x1 is set
x2 is Relation-like Function-like DecoratedTree-like set
dom x2 is non empty Tree-like set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
doms p is Relation-like Function-like set
dom (doms p) is set
dom p is finite Element of bool NAT
len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len p) is finite V43( len p) Element of bool NAT
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
doms p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
len (doms p) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom p is finite Element of bool NAT
dom (doms p) is finite Element of bool NAT
Seg (len p) is finite V43( len p) Element of bool NAT
p is non empty set
x1 is Relation-like p -valued Function-like DecoratedTree-like set
dom x1 is non empty Tree-like set
[:(dom x1),p:] is Relation-like non empty set
bool [:(dom x1),p:] is non empty set
rng x1 is Element of bool p
bool p is non empty set
p is Relation-like Function-like DecoratedTree-like set
x1 is Relation-like Function-like DecoratedTree-like set
<:p,x1:> is Relation-like Function-like set
dom <:p,x1:> is set
dom p is non empty Tree-like set
dom x1 is non empty Tree-like set
(dom p) /\ (dom x1) is non empty Tree-like set
p is non empty set
x1 is non empty set
[:p,x1:] is Relation-like non empty set
x2 is Relation-like p -valued Function-like DecoratedTree-like set
k is Relation-like x1 -valued Function-like DecoratedTree-like set
<:x2,k:> is Relation-like Function-like DecoratedTree-like set
rng <:x2,k:> is set
rng x2 is Element of bool p
bool p is non empty set
rng k is Element of bool x1
bool x1 is non empty set
[:(rng x2),(rng k):] is Relation-like set
p is non empty set
x1 is non empty set
[:p,x1:] is Relation-like non empty set
bool [:p,x1:] is non empty set
x2 is Relation-like p -valued Function-like DecoratedTree-like set
k is Relation-like p -defined x1 -valued Function-like non empty total quasi_total Element of bool [:p,x1:]
x2 * k is Relation-like x1 -valued Function-like set
dom x2 is non empty Tree-like set
[:(dom x2),p:] is Relation-like non empty set
bool [:(dom x2),p:] is non empty set
[:(dom x2),x1:] is Relation-like non empty set
bool [:(dom x2),x1:] is non empty set
n is Relation-like dom x2 -defined p -valued Function-like non empty total quasi_total DecoratedTree-like Element of bool [:(dom x2),p:]
k * n is Relation-like dom x2 -defined x1 -valued Function-like non empty total quasi_total DecoratedTree-like Element of bool [:(dom x2),x1:]
n is Relation-like dom x2 -defined x1 -valued Function-like non empty total quasi_total DecoratedTree-like Element of bool [:(dom x2),x1:]
rng n is non empty Element of bool x1
bool x1 is non empty set
p is non empty set
x1 is non empty set
pr1 (p,x1) is Relation-like Function-like set
[:p,x1:] is Relation-like non empty set
[:[:p,x1:],p:] is Relation-like non empty set
bool [:[:p,x1:],p:] is non empty set
pr1 (p,x1) is Relation-like [:p,x1:] -defined p -valued Function-like non empty total quasi_total Element of bool [:[:p,x1:],p:]
pr2 (p,x1) is Relation-like Function-like set
[:[:p,x1:],x1:] is Relation-like non empty set
bool [:[:p,x1:],x1:] is non empty set
pr2 (p,x1) is Relation-like [:p,x1:] -defined x1 -valued Function-like non empty total quasi_total Element of bool [:[:p,x1:],x1:]
p is non empty set
x1 is non empty set
[:p,x1:] is Relation-like non empty set
x2 is Relation-like [:p,x1:] -valued Function-like DecoratedTree-like set
(p,x1) is Relation-like [:p,x1:] -defined p -valued Function-like non empty total quasi_total Element of bool [:[:p,x1:],p:]
[:[:p,x1:],p:] is Relation-like non empty set
bool [:[:p,x1:],p:] is non empty set
x2 * (p,x1) is Relation-like p -valued Function-like DecoratedTree-like set
(p,x1) is Relation-like [:p,x1:] -defined x1 -valued Function-like non empty total quasi_total Element of bool [:[:p,x1:],x1:]
[:[:p,x1:],x1:] is Relation-like non empty set
bool [:[:p,x1:],x1:] is non empty set
x2 * (p,x1) is Relation-like x1 -valued Function-like DecoratedTree-like set
p is non empty set
x1 is non empty set
[:p,x1:] is Relation-like non empty set
x2 is Relation-like [:p,x1:] -valued Function-like DecoratedTree-like set
dom x2 is non empty Tree-like set
(p,x1,x2) is Relation-like p -valued Function-like DecoratedTree-like set
(p,x1) is Relation-like [:p,x1:] -defined p -valued Function-like non empty total quasi_total Element of bool [:[:p,x1:],p:]
[:[:p,x1:],p:] is Relation-like non empty set
bool [:[:p,x1:],p:] is non empty set
x2 * (p,x1) is Relation-like p -valued Function-like DecoratedTree-like set
(p,x1,x2) is Relation-like x1 -valued Function-like DecoratedTree-like set
(p,x1) is Relation-like [:p,x1:] -defined x1 -valued Function-like non empty total quasi_total Element of bool [:[:p,x1:],x1:]
[:[:p,x1:],x1:] is Relation-like non empty set
bool [:[:p,x1:],x1:] is non empty set
x2 * (p,x1) is Relation-like x1 -valued Function-like DecoratedTree-like set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom x2
x2 . k is Element of [:p,x1:]
(x2 . k) `1 is Element of p
(p,x1,x2) . k is set
(p,x1,x2) . k is set
(x2 . k) `2 is Element of x1
dom (p,x1) is Relation-like p -defined x1 -valued non empty Element of bool [:p,x1:]
bool [:p,x1:] is non empty set
dom (p,x1) is Relation-like p -defined x1 -valued non empty Element of bool [:p,x1:]
rng x2 is Relation-like p -defined x1 -valued Element of bool [:p,x1:]
dom (p,x1,x2) is non empty Tree-like set
dom (p,x1,x2) is non empty Tree-like set
[((x2 . k) `1),((x2 . k) `2)] is Element of [:p,x1:]
{((x2 . k) `1),((x2 . k) `2)} is non empty finite set
{((x2 . k) `1)} is non empty trivial finite V43(1) set
{{((x2 . k) `1),((x2 . k) `2)},{((x2 . k) `1)}} is non empty finite V40() set
(p,x1) . (((x2 . k) `1),((x2 . k) `2)) is Element of p
[((x2 . k) `1),((x2 . k) `2)] is set
(p,x1) . [((x2 . k) `1),((x2 . k) `2)] is set
(p,x1) . (((x2 . k) `1),((x2 . k) `2)) is Element of x1
(p,x1) . [((x2 . k) `1),((x2 . k) `2)] is set
p is non empty set
x1 is non empty set
[:p,x1:] is Relation-like non empty set
x2 is Relation-like [:p,x1:] -valued Function-like DecoratedTree-like set
(p,x1,x2) is Relation-like p -valued Function-like DecoratedTree-like set
(p,x1) is Relation-like [:p,x1:] -defined p -valued Function-like non empty total quasi_total Element of bool [:[:p,x1:],p:]
[:[:p,x1:],p:] is Relation-like non empty set
bool [:[:p,x1:],p:] is non empty set
x2 * (p,x1) is Relation-like p -valued Function-like DecoratedTree-like set
(p,x1,x2) is Relation-like x1 -valued Function-like DecoratedTree-like set
(p,x1) is Relation-like [:p,x1:] -defined x1 -valued Function-like non empty total quasi_total Element of bool [:[:p,x1:],x1:]
[:[:p,x1:],x1:] is Relation-like non empty set
bool [:[:p,x1:],x1:] is non empty set
x2 * (p,x1) is Relation-like x1 -valued Function-like DecoratedTree-like set
<:(p,x1,x2),(p,x1,x2):> is Relation-like [:p,x1:] -valued Function-like DecoratedTree-like set
dom (p,x1) is Relation-like p -defined x1 -valued non empty Element of bool [:p,x1:]
bool [:p,x1:] is non empty set
dom (p,x1) is Relation-like p -defined x1 -valued non empty Element of bool [:p,x1:]
rng x2 is Relation-like p -defined x1 -valued Element of bool [:p,x1:]
dom (p,x1,x2) is non empty Tree-like set
dom x2 is non empty Tree-like set
dom (p,x1,x2) is non empty Tree-like set
dom <:(p,x1,x2),(p,x1,x2):> is non empty Tree-like set
k is set
<:(p,x1,x2),(p,x1,x2):> . k is set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom x2
(p,x1,x2) . n is set
(p,x1,x2) . n is set
[((p,x1,x2) . n),((p,x1,x2) . n)] is set
{((p,x1,x2) . n),((p,x1,x2) . n)} is non empty finite set
{((p,x1,x2) . n)} is non empty trivial finite V43(1) set
{{((p,x1,x2) . n),((p,x1,x2) . n)},{((p,x1,x2) . n)}} is non empty finite V40() set
x2 . n is Element of [:p,x1:]
(x2 . n) `1 is Element of p
[((x2 . n) `1),((p,x1,x2) . n)] is set
{((x2 . n) `1),((p,x1,x2) . n)} is non empty finite set
{((x2 . n) `1)} is non empty trivial finite V43(1) set
{{((x2 . n) `1),((p,x1,x2) . n)},{((x2 . n) `1)}} is non empty finite V40() set
(x2 . n) `2 is Element of x1
[((x2 . n) `1),((x2 . n) `2)] is Element of [:p,x1:]
{((x2 . n) `1),((x2 . n) `2)} is non empty finite set
{{((x2 . n) `1),((x2 . n) `2)},{((x2 . n) `1)}} is non empty finite V40() set
x2 . k is set
p is non empty finite Tree-like set
Leaves p is finite Element of bool p
bool p is non empty finite V40() set
x1 is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
x2 is set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
x1 is set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
x2 is set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
k is set
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
x1 is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
p is non empty Tree-like set
bool p is non empty set
x1 is non empty Element of bool p
x2 is Element of x1
p is non empty finite Tree-like set
Leaves p is non empty finite Element of bool p
bool p is non empty finite V40() set
x1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Leaf of p
p is non empty finite Tree-like set
x1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
p is non empty finite Tree-like set
x1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (p)
x2 is non empty Tree-like set
p with-replacement (x1,x2) is non empty Tree-like set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p with-replacement (x1,x2)
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x1 ^ n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x1 ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p is non empty finite Tree-like set
x1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
p is non empty Tree-like set
x1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ( elementary_tree 0) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ( elementary_tree 0)
p is non empty Tree-like set
p -level 1 is Level of p
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p : len b1 = 1 } is set
x1 is non empty Tree-like set
x1 -level 1 is Level of x1
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of x1 : len b1 = 1 } is set
x2 is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ n is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
len <*n*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
q is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*q*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
p | q is non empty Tree-like set
p | <*q*> is non empty Tree-like set
x1 | <*q*> is non empty Tree-like set
p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom x1 is finite Element of bool NAT
x1 . (p + 1) is set
rng x1 is finite set
0 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p is non empty Tree-like set
Leaves p is Element of bool p
bool p is non empty set
x1 is non empty Tree-like set
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
p with-replacement (x2,x1) is non empty Tree-like set
k is set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p
p is Relation-like Function-like DecoratedTree-like set
dom p is non empty Tree-like set
x1 is Relation-like Function-like DecoratedTree-like set
x1 . {} is set
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom p
p with-replacement (x2,x1) is Relation-like Function-like DecoratedTree-like set
(p with-replacement (x2,x1)) . x2 is set
dom x1 is non empty Tree-like set
(dom p) with-replacement (x2,(dom x1)) is non empty Tree-like set
x2 ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x2 ^ k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x1 . k is set
p is Relation-like Function-like DecoratedTree-like set
dom p is non empty Tree-like set
x1 is Relation-like Function-like DecoratedTree-like set
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom p
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom p
p with-replacement (x2,x1) is Relation-like Function-like DecoratedTree-like set
(p with-replacement (x2,x1)) . k is set
p . k is set
dom x1 is non empty Tree-like set
(dom p) with-replacement (x2,(dom x1)) is non empty Tree-like set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x2 ^ n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x1 . n is set
p is Relation-like Function-like DecoratedTree-like set
dom p is non empty Tree-like set
x1 is Relation-like Function-like DecoratedTree-like set
dom x1 is non empty Tree-like set
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom p
p with-replacement (x2,x1) is Relation-like Function-like DecoratedTree-like set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom x1
x2 ^ k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(p with-replacement (x2,x1)) . (x2 ^ k) is set
x1 . k is set
(dom p) with-replacement (x2,(dom x1)) is non empty Tree-like set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x2 ^ n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x1 . n is set
p is non empty Tree-like set
x1 is non empty Tree-like set
p \/ x1 is non empty Tree-like set
p is non empty Tree-like set
x1 is non empty Tree-like set
p \/ x1 is non empty Tree-like set
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of p \/ x1
(p \/ x1) | x2 is non empty Tree-like set
p | x2 is non empty Tree-like set
x1 | x2 is non empty Tree-like set
(p | x2) \/ (x1 | x2) is non empty Tree-like set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x2 ^ k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x2 ^ k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k is non empty Tree-like set
n is non empty Tree-like set
k \/ n is non empty Tree-like set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of k \/ n
(k \/ n) | n is non empty Tree-like set
n | n is non empty Tree-like set
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
n ^ q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
n ^ q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 is set
rng p is finite set
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
k + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (k + 1) is set
x2 is non empty set
k is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes k is finite set
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (n + 1) is set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
q is set
r is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
r is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg r is finite V43(r) Element of bool NAT
k | (Seg r) is Relation-like NAT -defined Seg r -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
rng r is finite set
k .: (Seg r) is finite Element of bool NAT
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
s is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*s*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*s*> ^ s is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom <*s*> is non empty trivial finite V43(1) Element of bool NAT
dom n is finite Element of bool NAT
n . 1 is set
k . 1 is set
q is Relation-like NAT -defined NAT -valued Function-like 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
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
k ^ <*n*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
k ^ <*n*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
q is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (q + 1) is set
<*q*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*q*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*n*> . 1 is set
(<*q*> ^ q) . 1 is set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (n + 1) is set
<*n*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
{} ^ <*n*> is Relation-like NAT -defined Function-like non empty finite V43({} + 1) FinSequence-like FinSubsequence-like set
{} + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
q is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*q*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*q*> ^ q is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
r is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
r is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
r + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (r + 1) is set
<*r*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*r*> ^ r is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
q ^ <*n*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*q*> ^ (q ^ <*n*>) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
q ^ <*n*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*q*> ^ (q ^ <*n*>) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(k ^ <*n*>) . 1 is set
q + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (q + 1) is set
k is non empty Tree-like set
n is set
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (n + 1) is set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
q is non empty Tree-like set
r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of q
<*n*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (n + 1) is set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
x1 is non empty Tree-like set
x2 is non empty Tree-like set
p is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
(<*p*>) is non empty Tree-like set
p is non empty Tree-like set
x1 is non empty Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*p,x1*>) is non empty Tree-like set
p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*p*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
p + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(x1) is non empty Tree-like set
len x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 . (p + 1) is set
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*p*> ^ x2 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x1 . (k + 1) is set
<*k*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*k*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(<*p*> ^ x2) . 1 is set
(<*k*> ^ n) . 1 is set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(p) is non empty Tree-like set
(p) -level 1 is Level of (p)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (p) : len b1 = 1 } is set
len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not len p <= b1 } is set
rng p is finite set
x2 is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (p)
len k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
k . 1 is set
<*(k . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like set
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (n + 1) is set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
x2 is set
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*k*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
k + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (k + 1) is set
<*k*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (p)
len n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*x2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(p) | <*x2*> is non empty Tree-like set
x2 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (x2 + 1) is set
k is non empty Tree-like set
<*x2*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*x2*> ^ n is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (n + 1) is set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(<*x2*> ^ n) . 1 is set
(<*n*> ^ q) . 1 is set
<*x2*> ^ n is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
(p) is non empty Tree-like set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
(x1) is non empty Tree-like set
(p) -level 1 is Level of (p)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (p) : len b1 = 1 } is set
len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not len p <= b1 } is set
(x1) -level 1 is Level of (x1)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (x1) : len b1 = 1 } is set
len x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not len x1 <= b1 } is set
x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not x2 <= b1 } is set
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not k <= b1 } is set
<*x2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*x2*> . 1 is set
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
1 + k is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p . x2 is set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(p) | <*n*> is non empty Tree-like set
x1 . x2 is set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
len x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*(len x1)*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*(len x1)*> ^ p is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
k is non empty Tree-like set
<*k*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
x1 ^ <*k*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
(x1 ^ <*k*>) ^ x2 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
(((x1 ^ <*k*>) ^ x2)) is non empty Tree-like set
len ((x1 ^ <*k*>) ^ x2) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len (x1 ^ <*k*>) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len (x1 ^ <*k*>)) + (len x2) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len <*k*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(len x1) + (len <*k*>) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(len x1) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
((len x1) + 1) + (len x2) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(len x1) + (len x2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
((len x1) + (len x2)) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
dom (x1 ^ <*k*>) is non empty finite Element of bool NAT
((x1 ^ <*k*>) ^ x2) . ((len x1) + 1) is set
(x1 ^ <*k*>) . ((len x1) + 1) is set
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
((x1 ^ <*k*>) ^ x2) . (n + 1) is set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(<*(len x1)*> ^ p) . 1 is set
(<*n*> ^ n) . 1 is set
({}) is non empty Tree-like set
p is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered () () () () () () Element of NAT
x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x1 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
{} . (x1 + 1) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered () () () () () () set
<*x1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*x1*> ^ x2 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
elementary_tree (len p) is non empty finite Tree-like set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not len p <= b1 } is set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not len p <= b1 } \/ {{}} is non empty set
(p) is non empty Tree-like set
rng p is finite set
x1 is set
x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*x2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*x2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
x2 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (x2 + 1) is set
k is non empty Tree-like set
<*x2*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
elementary_tree p is non empty finite Tree-like set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not p <= b1 } is set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not p <= b1 } \/ {{}} is non empty set
p |-> (elementary_tree 0) is Relation-like NAT -defined Function-like finite V43(p) FinSequence-like FinSubsequence-like () () set
((p |-> (elementary_tree 0))) is non empty Tree-like set
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len (p |-> (elementary_tree 0)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(p |-> (elementary_tree 0)) . (k + 1) is set
<*k*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*k*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
Seg p is finite V43(p) Element of bool NAT
(Seg p) --> (elementary_tree 0) is Relation-like Seg p -defined {(elementary_tree 0)} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg p),{(elementary_tree 0)}:]
{(elementary_tree 0)} is non empty trivial finite V40() V43(1) set
[:(Seg p),{(elementary_tree 0)}:] is Relation-like finite set
bool [:(Seg p),{(elementary_tree 0)}:] is non empty finite V40() set
rng (p |-> (elementary_tree 0)) is finite set
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(p |-> (elementary_tree 0)) . (k + 1) is set
<*k*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*k*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
p is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
x1 ^ <*p*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
((x1 ^ <*p*>)) is non empty Tree-like set
(x1) is non empty Tree-like set
len x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len x1) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
elementary_tree ((len x1) + 1) is non empty finite Tree-like set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not (len x1) + 1 <= b1 } is set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not (len x1) + 1 <= b1 } \/ {{}} is non empty set
(x1) \/ (elementary_tree ((len x1) + 1)) is non empty Tree-like set
<*(len x1)*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
((x1) \/ (elementary_tree ((len x1) + 1))) with-replacement (<*(len x1)*>,p) is non empty Tree-like set
len <*p*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len (x1 ^ <*p*>) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
q is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(x1 ^ <*p*>) . (q + 1) is set
<*q*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*q*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
dom x1 is finite Element of bool NAT
x1 . (q + 1) is set
r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*q*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
q is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(x1 ^ <*p*>) . (q + 1) is set
<*q*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*q*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*(len x1)*> ^ q is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(x1 ^ <*p*>) . ((len x1) + 1) is set
q is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x1 . (q + 1) is set
<*q*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*q*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
q is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x1 . (q + 1) is set
<*q*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*q*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
dom x1 is finite Element of bool NAT
(x1 ^ <*p*>) . (q + 1) is set
q is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*q*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
q is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*q*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
q + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x1 . (q + 1) is set
rng x1 is finite set
<*q*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*(elementary_tree 0)*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () () set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
p ^ <*(elementary_tree 0)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
((p ^ <*(elementary_tree 0)*>)) is non empty Tree-like set
(p) is non empty Tree-like set
len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len p) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
elementary_tree ((len p) + 1) is non empty finite Tree-like set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not (len p) + 1 <= b1 } is set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not (len p) + 1 <= b1 } \/ {{}} is non empty set
(p) \/ (elementary_tree ((len p) + 1)) is non empty Tree-like set
<*(len p)*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(elementary_tree ((len p) + 1)) | <*(len p)*> is non empty Tree-like set
x1 is set
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (elementary_tree ((len p) + 1)) | <*(len p)*>
<*(len p)*> ^ x2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*k*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
len <*k*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len <*(len p)*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
1 + (len x2) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
1 + 0 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*x1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*x1*> ^ x2 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*(len p)*> . 1 is set
x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x1 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p . (x1 + 1) is set
<*x1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*x1*> ^ x2 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
((p) \/ (elementary_tree ((len p) + 1))) | <*(len p)*> is non empty Tree-like set
((p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,(elementary_tree 0)) is non empty Tree-like set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () set
len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*(len p)*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
x2 is non empty Tree-like set
<*x2*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
p ^ <*x2*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
(p ^ <*x2*>) ^ x1 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
(((p ^ <*x2*>) ^ x1)) is non empty Tree-like set
k is non empty Tree-like set
<*k*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
p ^ <*k*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
(p ^ <*k*>) ^ x1 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
(((p ^ <*k*>) ^ x1)) is non empty Tree-like set
(((p ^ <*k*>) ^ x1)) with-replacement (<*(len p)*>,x2) is non empty Tree-like set
len <*x2*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len <*k*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len (p ^ <*x2*>) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(len p) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len ((p ^ <*x2*>) ^ x1) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len (p ^ <*x2*>)) + (len x1) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len (p ^ <*k*>) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len ((p ^ <*k*>) ^ x1) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(len (p ^ <*k*>)) + (len x1) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
((len p) + 1) + (len x1) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
((p ^ <*k*>) ^ x1) . ((len p) + 1) is set
rng ((p ^ <*k*>) ^ x1) is non empty finite set
<*(len p)*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
((p ^ <*x2*>) ^ x1) . (n + 1) is set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ s is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
dom p is finite Element of bool NAT
dom (p ^ <*k*>) is non empty finite Element of bool NAT
dom (p ^ <*x2*>) is non empty finite Element of bool NAT
(p ^ <*k*>) . (n + 1) is set
p . (n + 1) is set
(p ^ <*x2*>) . (n + 1) is set
((p ^ <*k*>) ^ x1) . (n + 1) is set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ s is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
((len p) + 1) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(n + 1) - ((len p) + 1) is V31() ext-real V35() set
x1 . ((n + 1) - ((len p) + 1)) is set
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
((p ^ <*x2*>) ^ x1) . (n + 1) is set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ s is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(p ^ <*x2*>) . ((len p) + 1) is set
dom (p ^ <*x2*>) is non empty finite Element of bool NAT
((p ^ <*x2*>) ^ x1) . ((len p) + 1) is set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*(len p)*> ^ n is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
((p ^ <*k*>) ^ x1) . (n + 1) is set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ s is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
c14 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*(len p)*> ^ c14 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
1 + n is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*x2*> ^ x1 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
p ^ (<*x2*> ^ x1) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
<*k*> ^ x1 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
p ^ (<*k*> ^ x1) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
((p ^ <*x2*>) ^ x1) . (n + 1) is set
p . (n + 1) is set
(n + 1) - ((len p) + 1) is V31() ext-real V35() set
x1 . ((n + 1) - ((len p) + 1)) is set
p is non empty Tree-like set
(p) is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
(<*p*>) is non empty Tree-like set
(elementary_tree 1) with-replacement (<*0*>,p) is non empty Tree-like set
x1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*p*> . 1 is set
len <*p*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
0 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x2 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p*> . (x2 + 1) is set
<*x2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*x2*> ^ k is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*x2*> ^ n is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x1 ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ x2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
p is non empty Tree-like set
x1 is non empty Tree-like set
(p,x1) is non empty Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*p,x1*>) is non empty Tree-like set
(elementary_tree 2) with-replacement (<*0*>,p) is non empty Tree-like set
((elementary_tree 2) with-replacement (<*0*>,p)) with-replacement (<*1*>,x1) is non empty Tree-like set
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*p,x1*> . 1 is set
<*p,x1*> . 2 is set
len <*p,x1*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
1 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
0 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p,x1*> . (k + 1) is set
<*k*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*k*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ n is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*k*> ^ n is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x2 ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
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
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () () set
(p) is non empty Tree-like set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () () set
len x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(x1) is non empty Tree-like set
x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () () set
len x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(x2) is non empty Tree-like set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is set
<*n*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like set
k ^ <*n*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len <*n*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () () set
len n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len n) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(n) is non empty Tree-like set
elementary_tree (x1 + 1) is non empty finite Tree-like set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not x1 + 1 <= b1 } is set
{ <*b1*> where b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT : not x1 + 1 <= b1 } \/ {{}} is non empty set
(n) \/ (elementary_tree (x1 + 1)) is non empty Tree-like set
<*x1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
q is non empty finite Tree-like set
r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of q
q is non empty finite Tree-like set
q with-replacement (r,q) is non empty finite Tree-like set
len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p is non empty finite Tree-like set
(p) is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () () set
(<*p*>) is non empty finite Tree-like set
p is non empty finite Tree-like set
x1 is non empty finite Tree-like set
(p,x1) is non empty Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () () set
(<*p,x1*>) is non empty finite Tree-like set
p is non empty Tree-like set
(p) is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
(<*p*>) is non empty Tree-like set
x1 is set
len <*p*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p*> . 1 is set
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p*> . (k + 1) is set
<*k*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*k*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
0 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
0 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ k is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
p is non empty Tree-like set
(p) is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
(<*p*>) is non empty Tree-like set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ x1 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len <*p*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x2 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p*> . (x2 + 1) is set
<*x2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*x2*> ^ k is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(<*0*> ^ x1) . 1 is set
(<*x2*> ^ k) . 1 is set
p is non empty Tree-like set
(p) is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
(<*p*>) is non empty Tree-like set
x1 is set
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of elementary_tree 1
<*0*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
p is non empty Tree-like set
x1 is non empty Tree-like set
(p) is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
(<*p*>) is non empty Tree-like set
(x1) is non empty Tree-like set
<*x1*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
(<*x1*>) is non empty Tree-like set
x2 is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (p)
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
p is non empty Tree-like set
(p) is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
(<*p*>) is non empty Tree-like set
x1 is non empty Tree-like set
(x1) is non empty Tree-like set
<*x1*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
(<*x1*>) is non empty Tree-like set
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ x2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
p is non empty Tree-like set
(p) is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
(<*p*>) is non empty Tree-like set
(p) | <*0*> is non empty Tree-like set
len <*p*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p*> . 1 is set
0 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p is non empty Tree-like set
(p) is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
(<*p*>) is non empty Tree-like set
x1 is non empty Tree-like set
(p) with-replacement (<*0*>,x1) is non empty Tree-like set
(x1) is non empty Tree-like set
<*x1*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
(<*x1*>) is non empty Tree-like set
len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered () () () () () () Element of NAT
{} ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V43({} + 1) FinSequence-like FinSubsequence-like () set
{} + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
{} ^ <*x1*> is Relation-like NAT -defined Function-like non empty finite V43({} + 1) FinSequence-like FinSubsequence-like () set
<*p*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
<*x1*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
((elementary_tree 0)) is non empty finite Tree-like set
(<*(elementary_tree 0)*>) is non empty finite Tree-like set
1 |-> (elementary_tree 0) is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () () set
((1 |-> (elementary_tree 0))) is non empty finite Tree-like set
p is non empty Tree-like set
x1 is non empty Tree-like set
(p,x1) is non empty Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*p,x1*>) is non empty Tree-like set
x2 is set
len <*p,x1*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p,x1*> . 1 is set
<*p,x1*> . 2 is set
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p,x1*> . (n + 1) is set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
1 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
0 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*1*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
q is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(<*0*> ^ q) . 1 is set
q + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p,x1*> . (q + 1) is set
<*q*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*q*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
q is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p,x1*> . (q + 1) is set
<*q*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*q*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
p is non empty Tree-like set
x1 is non empty Tree-like set
(p,x1) is non empty Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*p,x1*>) is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
<*x1*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
<*p*> ^ <*x1*> is Relation-like NAT -defined Function-like non empty finite V43(1 + 1) FinSequence-like FinSubsequence-like () set
1 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
{} ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V43({} + 1) FinSequence-like FinSubsequence-like () set
{} + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered () () () () () () Element of NAT
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ x2 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ k is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
x1 is non empty Tree-like set
p is non empty Tree-like set
(p,x1) is non empty Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*p,x1*>) is non empty Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
<*x1*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
<*p*> ^ <*x1*> is Relation-like NAT -defined Function-like non empty finite V43(1 + 1) FinSequence-like FinSubsequence-like () set
1 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
len <*p*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p,x1*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ x2 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ k is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
p is non empty Tree-like set
x1 is non empty Tree-like set
(p,x1) is non empty Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*p,x1*>) is non empty Tree-like set
x2 is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of elementary_tree 2
<*0*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*1*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
p is non empty Tree-like set
x2 is non empty Tree-like set
x1 is non empty Tree-like set
k is non empty Tree-like set
(p,x1) is non empty Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*p,x1*>) is non empty Tree-like set
(x2,k) is non empty Tree-like set
<*x2,k*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*x2,k*>) is non empty Tree-like set
n is set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (p,x1)
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ q is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
p is non empty Tree-like set
x1 is non empty Tree-like set
(p,x1) is non empty Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*p,x1*>) is non empty Tree-like set
x2 is non empty Tree-like set
k is non empty Tree-like set
(x2,k) is non empty Tree-like set
<*x2,k*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*x2,k*>) is non empty Tree-like set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ n is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
p is non empty Tree-like set
x1 is non empty Tree-like set
(p,x1) is non empty Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*p,x1*>) is non empty Tree-like set
(p,x1) | <*0*> is non empty Tree-like set
(p,x1) | <*1*> is non empty Tree-like set
len <*p,x1*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p,x1*> . 1 is set
<*p,x1*> . 2 is set
0 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
1 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x1 is non empty Tree-like set
x2 is non empty Tree-like set
(x1,x2) is non empty Tree-like set
<*x1,x2*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*x1,x2*>) is non empty Tree-like set
p is non empty Tree-like set
(x1,x2) with-replacement (<*0*>,p) is non empty Tree-like set
(p,x2) is non empty Tree-like set
<*p,x2*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*p,x2*>) is non empty Tree-like set
(x1,x2) with-replacement (<*1*>,p) is non empty Tree-like set
(x1,p) is non empty Tree-like set
<*x1,p*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () set
(<*x1,p*>) is non empty Tree-like set
len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered () () () () () () Element of NAT
<*x1*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
{} ^ <*x1*> is Relation-like NAT -defined Function-like non empty finite V43({} + 1) FinSequence-like FinSubsequence-like () set
{} + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
{} ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V43({} + 1) FinSequence-like FinSubsequence-like () set
<*x1,x2*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
<*x1,p*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like () set
len <*x1*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*x2*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () set
<*x1*> ^ <*x2*> is Relation-like NAT -defined Function-like non empty finite V43(1 + 1) FinSequence-like FinSubsequence-like () set
1 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
<*x1*> ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V43(1 + 1) FinSequence-like FinSubsequence-like () set
<*p*> ^ <*x2*> is Relation-like NAT -defined Function-like non empty finite V43(1 + 1) FinSequence-like FinSubsequence-like () set
((elementary_tree 0),(elementary_tree 0)) is non empty finite Tree-like set
<*(elementary_tree 0),(elementary_tree 0)*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () () set
(<*(elementary_tree 0),(elementary_tree 0)*>) is non empty finite Tree-like set
2 |-> (elementary_tree 0) is Relation-like NAT -defined Function-like finite V43(2) FinSequence-like FinSubsequence-like () () set
((2 |-> (elementary_tree 0))) is non empty finite Tree-like set
p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () () set
rng x1 is finite set
(x1) is non empty finite Tree-like set
height (x1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered () () () () () () Element of NAT
len x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x1 . (k + 1) is set
<*k*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*k*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len q is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is non empty finite Tree-like set
height n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len <*k*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
1 + (len q) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
x1 . (k + 1) is set
<*k*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*k*> ^ n is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () () set
rng p is finite set
(p) is non empty finite Tree-like set
height (p) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 is non empty finite Tree-like set
height x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom p is finite Element of bool NAT
x2 is set
p . x2 is set
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
1 + n is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*n*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(p) | <*n*> is non empty Tree-like set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like () () set
rng p is finite set
(p) is non empty finite Tree-like set
height (p) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
x1 is non empty finite Tree-like set
height x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(height x1) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
p is non empty finite Tree-like set
(p) is non empty finite Tree-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like () () set
(<*p*>) is non empty finite Tree-like set
height (p) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
height p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(height p) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
rng <*p*> is non empty trivial finite V43(1) set
{p} is non empty trivial finite V40() V43(1) set
x2 is non empty finite Tree-like set
height x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p is non empty finite Tree-like set
x1 is non empty finite Tree-like set
(p,x1) is non empty finite Tree-like set
<*p,x1*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like () () set
(<*p,x1*>) is non empty finite Tree-like set
height (p,x1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
height p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
height x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
max ((height p),(height x1)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
(max ((height p),(height x1))) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
rng <*p,x1*> is non empty finite set
{p,x1} is non empty finite V40() set
k is non empty finite Tree-like set
height k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p is non empty set
(p) is functional non empty () (p)
x1 is Relation-like p -valued Function-like DecoratedTree-like Element of (p)
dom x1 is non empty Tree-like set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom p is finite Element of bool NAT
len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len p) is finite V43( len p) Element of bool NAT
x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
p . x1 is set
rng p is finite set
x2 is Relation-like Function-like DecoratedTree-like set
x2 . {} is set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom x1 is finite Element of bool NAT
x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p . x2 is set
x1 . x2 is set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom x1 is finite Element of bool NAT
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom x2 is finite Element of bool NAT
k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
x1 . k is set
p . k is set
x2 . k is set
n is Relation-like Function-like DecoratedTree-like set
n . {} is set
n is Relation-like Function-like DecoratedTree-like set
n . {} is set