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

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

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

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

is Relation-like non empty non trivial non finite 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

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

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

K89({},,<*1*>) is non empty finite set
p is V24() V25() V26() V30() V31() ext-real 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
x1 . p is set

(x1 ^ x2) . p is set
dom x1 is finite Element of bool NAT
bool () is non empty set
{ b1 where b1 is functional FinSequence-membered Element of bool () : b1 is non empty Tree-like set } is set
x1 is set

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

{} 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

p is set
p is set
p is non empty set

bool [:,p:] is non empty set
the Element of p is Element of p

{( --> the Element of p)} is functional non empty trivial finite V40() V43(1) Element of bool ()
bool () 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

{} 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)

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

dom n is set
rng n is set
k is functional non empty () set
n is set

dom n is set
rng n is set
[:p,x1:] is Relation-like non empty set
bool [:p,x1:] is non empty set

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

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)

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

k is set
k is functional non empty () (p)

dom n is non empty Tree-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

dom n is non empty Tree-like set
k is 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

rng p is 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

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

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

rng (p ^ x1) is finite set
rng p is finite set
rng x1 is finite set
(rng p) \/ (rng x1) is finite set

rng (p ^ x1) is finite set
rng p is finite set
rng x1 is finite set
(rng p) \/ (rng x1) is finite 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 non empty trivial finite V43(1) set
rng <*p*> is non empty trivial finite V43(1) set
p is 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 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 non empty finite set
rng <*p,x1*> is non empty finite set
p is set
x1 is 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 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

Seg x1 is finite V43(x1) Element of bool NAT

{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

Seg x1 is finite V43(x1) Element of bool NAT

{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

Seg x1 is finite V43(x1) Element of bool NAT

{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

rng p is set
p is non empty () set

x2 is set
rng x1 is finite set
rng x1 is finite () Element of bool p
bool p is non empty set

p is non empty () () set

x2 is set
rng x1 is finite set
rng x1 is finite () () Element of bool p
bool p is non empty set

p is functional non empty () set

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 non empty Tree-like set

x1 is non empty Tree-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 is non empty finite Tree-like set

x1 is non empty finite Tree-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 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

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

dom x2 is non empty Tree-like set

dom (doms p) is set

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

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

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

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

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

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

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

(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

(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

p is non empty set
x1 is non empty set
[:p,x1:] is Relation-like non empty set

dom x2 is non empty Tree-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

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

(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

(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

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

(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

x2 is set

x1 is set

x2 is set

k is set

x1 is set

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

p is non empty finite Tree-like set

p is non empty finite Tree-like set

x2 is non empty Tree-like set
p with-replacement (x1,x2) is non empty Tree-like set

p is non empty finite Tree-like set

p is non empty Tree-like set

p is non empty Tree-like set
p -level 1 is Level of p
{ } is set
x1 is non empty Tree-like set
x1 -level 1 is Level of x1
{ } is set
x2 is set

n is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element 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

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

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

p with-replacement (x2,x1) is non empty Tree-like set
k is set

dom p is non empty Tree-like set

x1 . {} is 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

x1 . k is set

dom p is non empty Tree-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

x1 . n is set

dom p is non empty Tree-like set

dom x1 is non empty Tree-like set

(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

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

(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 non empty Tree-like set
n is non empty Tree-like set
k \/ n is non empty Tree-like set

(k \/ n) | n is non empty Tree-like set
n | n is non empty Tree-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

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

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

q is 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

bool is non empty non trivial non finite set
rng r is finite set
k .: (Seg r) is finite Element of bool NAT

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

dom <*s*> is non empty trivial finite V43(1) Element of bool NAT

n . 1 is set
k . 1 is set

n 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() Element of NAT

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

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

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

{} + 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

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

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

(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

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

q is non empty Tree-like set

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

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

x1 is non empty Tree-like set
x2 is non empty Tree-like set
p is non empty Tree-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 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 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

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
x1 . (k + 1) is set

(<*p*> ^ x2) . 1 is set
(<*k*> ^ n) . 1 is set

(p) is non empty Tree-like set
(p) -level 1 is Level of (p)
{ } 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

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

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

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

x2 is 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

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

(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

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

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

(<*x2*> ^ n) . 1 is set
(<*n*> ^ q) . 1 is set

(p) is non empty Tree-like set

(x1) is non empty Tree-like set
(p) -level 1 is Level of (p)
{ } 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)
{ } 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*> . 1 is set
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() 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

(p) | <*n*> is non empty Tree-like set
x1 . x2 is set

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

k is non empty Tree-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) + () 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 + 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

(<*(len x1)*> ^ p) . 1 is set
(<*n*> ^ n) . 1 is set
({}) 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

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 V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element 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

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

(()) is non empty Tree-like set

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

k + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
() . (k + 1) is set

Seg p is finite V43(p) Element of bool NAT

is non empty trivial finite V40() V43(1) set

bool [:(Seg p),:] is non empty finite V40()