:: TREES_3 semantic presentation

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

{ <*b

{{}} is functional non empty trivial finite V40() V43(1) Tree-like set

{ <*b

elementary_tree 1 is non empty finite Tree-like set

{ <*b

{ <*b

<*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

{ <*b

{ <*b

<*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

{ b

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

{ b

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

{ (b

union { (b

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

{ b

x1 is non empty Tree-like set

x1 -level 1 is Level of x1

{ b

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)

{ b

len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

{ <*b

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)

{ b

len p is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

{ <*b

(x1) -level 1 is Level of (x1)

{ b

len x1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

{ <*b

x2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

{ <*b

k is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

{ <*b

<*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

{ <*b

{ <*b

(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

{ <*b

{ <*b

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()