:: TREES_4 semantic presentation

REAL is set
NAT is non empty V28() V29() V30() V36() V41() V42() Element of bool REAL
bool REAL is non empty set
1 is non empty ext-real positive V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
[:1,1:] is Relation-like non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is Relation-like non empty set
bool [:[:1,1:],1:] is non empty set
NAT is non empty V28() V29() V30() V36() V41() V42() set
bool NAT is non empty V36() set
bool NAT is non empty V36() set

{{},1} is non empty set
Trees is non empty constituted-Trees set
bool Trees is non empty set
2 is non empty ext-real positive V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
3 is non empty ext-real positive V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

elementary_tree 0 is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not 0 <= b1 } is set

{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not 0 <= b1 } \/ is non empty set
elementary_tree 1 is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not 1 <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not 1 <= b1 } \/ is non empty set

[1,0] is set
{1,0} is non empty set
{1} is non empty trivial V43(1) set
{{1,0},{1}} is non empty set

tree {} is non empty V36() Tree-like set
^ is non empty V36() Tree-like set
D1 is set
D2 is set

dom d1 is Element of bool NAT
d1 . D2 is set
rng d1 is set

dom D1 is non empty Tree-like set
dom D2 is non empty Tree-like set
d1 is set
D1 . d1 is set
D2 . d1 is set

D1 . d1 is set
D2 . d1 is set

D1 . d2 is set
D2 . d2 is set
D1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
elementary_tree D1 is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D1 <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D1 <= b1 } \/ is non empty set
D2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
elementary_tree D2 is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D2 <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D2 <= b1 } \/ is non empty set

[1,D2] is set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set

<*D2*> . 1 is set
d1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,d1] is set
{1,d1} is non empty set
{{1,d1},{1}} is non empty set

D1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
elementary_tree D1 is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D1 <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D1 <= b1 } \/ is non empty set
D2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
elementary_tree D2 is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D2 <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D2 <= b1 } \/ is non empty set
D1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D1 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

len D2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
dom D2 is Element of bool NAT
D2 . (D1 + 1) is set
rng D2 is set
0 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 is set

len d1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D1 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d1 . (D1 + 1) is set
rng d1 is set
D1 is set

{D1} is non empty trivial V43(1) set
[:,{D1}:] is Relation-like non empty set
bool [:,{D1}:] is non empty set
D1 is non empty set
D2 is Element of D1

{D2} is non empty trivial V43(1) set
[:,{D2}:] is Relation-like non empty set
bool [:,{D2}:] is non empty set

[:,D1:] is Relation-like non empty set
bool [:,D1:] is non empty set
dom ( --> D2) is non empty Tree-like set
D1 is set

{D1} is non empty trivial V43(1) set
[:,{D1}:] is Relation-like non empty set
bool [:,{D1}:] is non empty set
dom (D1) is non empty Tree-like set
(D1) . {} is set
D1 is set

{D1} is non empty trivial V43(1) set
[:,{D1}:] is Relation-like non empty set
bool [:,{D1}:] is non empty set
D2 is set

{D2} is non empty trivial V43(1) set
[:,{D2}:] is Relation-like non empty set
bool [:,{D2}:] is non empty set
(D1) . {} is set

dom D1 is non empty Tree-like set
D1 . {} is set

{(D1 . {})} is non empty trivial V43(1) set
[:,{(D1 . {})}:] is Relation-like non empty set
bool [:,{(D1 . {})}:] is non empty set
D2 is set
D1 . D2 is set
D1 is set

{D1} is non empty trivial V43(1) set
[:,{D1}:] is Relation-like non empty set
bool [:,{D1}:] is non empty set
[{},D1] is set
{{},D1} is non empty set
{{{},D1},} is non empty set

[:,{D1}:] is Relation-like non empty set

len D2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
elementary_tree (len D2) is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len D2 <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len D2 <= b1 } \/ is non empty set
D1 is set
d1 is set

p2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,p2] is set
{1,p2} is non empty set
{{1,p2},{1}} is non empty set

p2 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 . (p2 + 1) is set
y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,y] is set
{1,y} is non empty set
{{1,y},{1}} is non empty set

x is set
y + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 . (y + 1) is set
x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set

p2 is set
x + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 . (x + 1) is set
y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,y] is set
{1,y} is non empty set
{{1,y},{1}} is non empty set

dom d1 is set

dom d2 is non empty Tree-like set
d2 . {} is set
p is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set

p + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 . (p + 1) is set
p is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set

d2 . <*p*> is set
p + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 . (p + 1) is set
p2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,p2] is set
{1,p2} is non empty set
{{1,p2},{1}} is non empty set

p2 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 . (p2 + 1) is set
<*p*> . 1 is set

dom d1 is non empty Tree-like set
d1 . {} is set

dom d2 is non empty Tree-like set
d2 . {} is set
p is set

x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set

d1 . p is set
x + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 . (x + 1) is set
d2 . p is set
x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set

D1 is set
D2 is set

(D1,d1) . {} is set
dom (D1,d1) is non empty Tree-like set
len d1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
elementary_tree (len d1) is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b1 } \/ is non empty set
dom (D2,d2) is non empty Tree-like set
len d2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
elementary_tree (len d2) is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d2 <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d2 <= b1 } \/ is non empty set
p is ext-real V27() V28() V29() V30() V34() V35() V36() V41() set
p2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() set
1 + p2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d1 . p is set

[1,p2] is set
{1,p2} is non empty set
{{1,p2},{1}} is non empty set

(D1,d1) . <*p2*> is set
d2 . p is set
D1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,D1] is set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set

D2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
elementary_tree D2 is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D2 <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D2 <= b1 } \/ is non empty set
() | <*D1*> is non empty Tree-like set

Seg D2 is V36() V43(D2) Element of bool NAT
{ b1 where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : ( 1 <= b1 & b1 <= D2 ) } is set

is non empty trivial V43(1) set
[:(Seg D2),:] is Relation-like set
bool [:(Seg D2),:] is non empty set
tree (D2 |-> ) is non empty V36() Tree-like set
1 + D1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D1 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
len (D2 |-> ) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
(tree (D2 |-> )) | <*D1*> is non empty Tree-like set
(D2 |-> ) . (D1 + 1) is set
D1 is set
D2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,D2] is set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set

D2 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

len d1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

d1 . (D2 + 1) is set
((d1 . (D2 + 1))) is Relation-like Function-like DecoratedTree-like set
--> (d1 . (D2 + 1)) is Relation-like elementary_tree 0 -defined {(d1 . (D2 + 1))} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{(d1 . (D2 + 1))}) DecoratedTree-like Element of bool [:,{(d1 . (D2 + 1))}:]
{(d1 . (D2 + 1))} is non empty trivial V43(1) set
[:,{(d1 . (D2 + 1))}:] is Relation-like non empty set
bool [:,{(d1 . (D2 + 1))}:] is non empty set
dom (D1,d1) is non empty Tree-like set
(dom (D1,d1)) | <*D2*> is non empty Tree-like set
(D1,d1) . <*D2*> is set
elementary_tree (len d1) is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b1 } \/ is non empty set
(elementary_tree (len d1)) | <*D2*> is non empty Tree-like set
dom ((D1,d1) | <*D2*>) is non empty Tree-like set

((D1,d1) | <*D2*>) . d2 is set
(D1,d1) . (<*D2*> ^ d2) is set

D1 is set
len D2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

dom (doms D2) is set
dom D2 is Element of bool NAT

tree d1 is non empty Tree-like set
d2 is set

x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set

x + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

D2 .. ((x + 1),y) is set

K80(K149(D2),(x + 1),y) is set
y is set
p2 is set
y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,y] is set
{1,y} is non empty set
{{1,y},{1}} is non empty set

x is set
y + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 .. ((y + 1),y) is set
K80(K149(D2),(y + 1),y) is set

dom d2 is set

dom p is non empty Tree-like set
p . {} is set
len d1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
p2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,p2] is set
{1,p2} is non empty set
{{1,p2},{1}} is non empty set

p2 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 . (p2 + 1) is set

dom x is non empty Tree-like set
d1 . (p2 + 1) is set
(dom p) | <*p2*> is non empty Tree-like set
dom (p | <*p2*>) is non empty Tree-like set

p . (<*p2*> ^ y) is set
y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,y] is set
{1,y} is non empty set
{{1,y},{1}} is non empty set

y + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 .. ((y + 1),T) is set

K80(K149(D2),(y + 1),T) is set
(<*p2*> ^ y) . 1 is set
(<*y*> ^ T) . 1 is set
x . y is set
(p | <*p2*>) . y is set

dom d1 is non empty Tree-like set
d1 . {} is set

dom d2 is non empty Tree-like set
d2 . {} is set

tree (doms p) is non empty Tree-like set

tree (doms p2) is non empty Tree-like set

y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,y] is set
{1,y} is non empty set
{{1,y},{1}} is non empty set

len (doms p) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

y + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 . (y + 1) is set

(dom d1) | <*y*> is non empty Tree-like set
d1 . x is set
(d1 | <*y*>) . y is set
d2 . x is set
D1 is set

[1,D2] is set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set

D1 is set

[1,D2] is set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set

[1,d1] is set
{1,d1} is non empty set
{{1,d1},{1}} is non empty set

1 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
(D1,<*D2,d1*>) is Relation-like Function-like DecoratedTree-like set
D1 is set

dom (D1,D2) is non empty Tree-like set

tree (doms D2) is non empty Tree-like set

tree (doms d1) is non empty Tree-like set
D1 is set
D2 is set

dom (D2,d1) is non empty Tree-like set
len d1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

tree (doms d1) is non empty Tree-like set
len (doms d1) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

d2 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
(doms d1) . (d2 + 1) is set

[1,d2] is set
{1,d2} is non empty set
{{1,d2},{1}} is non empty set

dom d1 is Element of bool NAT
d1 . (d2 + 1) is set

dom y is non empty Tree-like set

x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
x + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d1 . (x + 1) is set

[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set

dom p is non empty Tree-like set
d2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d2 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d1 . (d2 + 1) is set

[1,d2] is set
{1,d2} is non empty set
{{1,d2},{1}} is non empty set

y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
y + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
(doms d1) . (y + 1) is set

[1,y] is set
{1,y} is non empty set
{{1,y},{1}} is non empty set

dom p is non empty Tree-like set

dom T is non empty Tree-like set
d2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d2 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d1 . (d2 + 1) is set

[1,d2] is set
{1,d2} is non empty set
{{1,d2},{1}} is non empty set

x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

x + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
(doms d1) . (x + 1) is set

[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set

y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
y + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d1 . (y + 1) is set

[1,y] is set
{1,y} is non empty set
{{1,y},{1}} is non empty set

D1 is set

len D2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

d1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d1 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
D2 . (d1 + 1) is set

[1,d1] is set
{1,d1} is non empty set
{{1,d1},{1}} is non empty set

dom d2 is non empty Tree-like set

(D1,D2) . (<*d1*> ^ p) is set
d2 . p is set
dom (D1,D2) is non empty Tree-like set
(dom (D1,D2)) | <*d1*> is non empty Tree-like set

((D1,D2) | <*d1*>) . p is set
D1 is set

[1,D2] is set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set

dom (D1,D2) is non empty Tree-like set
dom D2 is non empty Tree-like set
^ (dom D2) is non empty Tree-like set
dom (D1,<*D2*>) is non empty Tree-like set

tree (doms <*D2*>) is non empty Tree-like set

[1,(dom D2)] is set
{1,(dom D2)} is non empty set
{{1,(dom D2)},{1}} is non empty set
{[1,(dom D2)]} is Relation-like Function-like constant non empty trivial V43(1) set
D1 is set

(D1,D2,d1) is Relation-like Function-like DecoratedTree-like set

[1,D2] is set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set

[1,d1] is set
{1,d1} is non empty set
{{1,d1},{1}} is non empty set

(D1,<*D2,d1*>) is Relation-like Function-like DecoratedTree-like set
dom (D1,D2,d1) is non empty Tree-like set
dom D2 is non empty Tree-like set
dom d1 is non empty Tree-like set
tree ((dom D2),(dom d1)) is non empty Tree-like set
dom (D1,<*D2,d1*>) is non empty Tree-like set

tree (doms <*D2,d1*>) is non empty Tree-like set

[1,(dom D2)] is set
{1,(dom D2)} is non empty set
{{1,(dom D2)},{1}} is non empty set
{[1,(dom D2)]} is Relation-like Function-like constant non empty trivial V43(1) set

[1,(dom d1)] is set
{1,(dom d1)} is non empty set
{{1,(dom d1)},{1}} is non empty set
{[1,(dom d1)]} is Relation-like Function-like constant non empty trivial V43(1) set

D1 is set
D2 is set

(D1,d1) . {} is set
dom (D1,d1) is non empty Tree-like set

tree (doms d1) is non empty Tree-like set
dom (D2,d2) is non empty Tree-like set

tree (doms d2) is non empty Tree-like set
dom d1 is Element of bool NAT
dom (doms d1) is Element of bool NAT
dom (doms d2) is Element of bool NAT
dom d2 is Element of bool NAT
len d1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
len d2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
p is ext-real V27() V28() V29() V30() V34() V35() V36() V41() set
p2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() set
1 + p2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d1 . p is set

[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set

d2 . p is set
D1 is set

{D1} is non empty trivial V43(1) set
[:,{D1}:] is Relation-like non empty set
bool [:,{D1}:] is non empty set
D2 is set

(D1) . {} is set
dom (D2,d1) is non empty Tree-like set
len d1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
elementary_tree (len d1) is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b1 } \/ is non empty set
D1 is set

{D1} is non empty trivial V43(1) set
[:,{D1}:] is Relation-like non empty set
bool [:,{D1}:] is non empty set
D2 is set

(D1) . {} is set
dom (D2,d1) is non empty Tree-like set

tree (doms d2) is non empty Tree-like set

dom (doms d1) is set
dom d1 is Element of bool NAT
D1 is set
D2 is set

len d1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
dom d1 is Element of bool NAT

len d2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
(D1,d1) . {} is set

Seg (len d1) is V36() V43( len d1) Element of bool NAT
{ b1 where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : ( 1 <= b1 & b1 <= len d1 ) } is set
(Seg (len d1)) --> is Relation-like non-empty NAT -defined Seg (len d1) -defined Seg (len d1) -defined -valued Function-like constant V14( Seg (len d1)) V14( Seg (len d1)) V18( Seg (len d1),) V36() FinSequence-like FinSubsequence-like Element of bool [:(Seg (len d1)),:]
is non empty trivial V43(1) set
[:(Seg (len d1)),:] is Relation-like set
bool [:(Seg (len d1)),:] is non empty set
tree ((len d1) |-> ) is non empty V36() Tree-like set
elementary_tree (len d1) is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b1 } \/ is non empty set
dom (D1,d1) is non empty Tree-like set

tree (doms p) is non empty Tree-like set
len (doms p) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
p2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d2 . p2 is set
d1 . p2 is set
((d1 . p2)) is Relation-like Function-like DecoratedTree-like set
--> (d1 . p2) is Relation-like elementary_tree 0 -defined {(d1 . p2)} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{(d1 . p2)}) DecoratedTree-like Element of bool [:,{(d1 . p2)}:]
{(d1 . p2)} is non empty trivial V43(1) set
[:,{(d1 . p2)}:] is Relation-like non empty set
bool [:,{(d1 . p2)}:] is non empty set
x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() set
1 + x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,y] is set
{1,y} is non empty set
{{1,y},{1}} is non empty set

D1 is set

dom (D1,D2) is non empty Tree-like set
d1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

[1,d1] is set
{1,d1} is non empty set
{{1,d1},{1}} is non empty set

d1 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

(D1,D2) . (<*d1*> ^ d2) is set
D2 .. ((d1 + 1),d2) is set

K80(K149(D2),(d1 + 1),d2) is set

tree (doms D2) is non empty Tree-like set
len (doms D2) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
len D2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

(dom (D1,D2)) | <*d1*> is non empty Tree-like set

dom ((D1,D2) | <*d1*>) is non empty Tree-like set
((D1,D2) | <*d1*>) . p is set
dom D2 is Element of bool NAT
D2 . (d1 + 1) is set
D1 is set

{D1} is non empty trivial V43(1) set
[:,{D1}:] is Relation-like non empty set
bool [:,{D1}:] is non empty set

dom (D1,{}) is non empty Tree-like set
D2 is set
(D1,{}) . D2 is set
dom (D1,{}) is non empty Tree-like set

tree (doms D2) is non empty Tree-like set
d1 is set

(D1,D2) . d1 is set
D1 is set

{D1} is non empty trivial V43(1) set
[:(),{D1}:] is Relation-like non empty set
bool [:(),{D1}:] is non empty set
D2 is set

[1,D2] is set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set

{D2} is non empty trivial V43(1) set
[:,{D2}:] is Relation-like non empty set
bool [:,{D2}:] is non empty set

dom (D1,<*D2*>) is non empty Tree-like set
len <*D2*> is non empty ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
elementary_tree (len <*D2*>) is non empty V36() Tree-like set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len <*D2*> <= b1 } is set
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len <*D2*> <= b1 } \/ is non empty set
dom (D2) is non empty Tree-like set
dom (() --> D1) is non empty Tree-like set
dom ((() --> D1) with-replacement (,(D2))) is non empty Tree-like set
() with-replacement (,) is non empty Tree-like set
d2 is set
<*D2*> . 1 is set
(D1,<*D2*>) . {} is set
((() --> D1) with-replacement (,(D2))) . {} is set
(() --> D1) . {} is set
(D1,<*D2*>) . is set
0 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
<*D2*> . (0 + 1) is set
((() --> D1) with-replacement (,(D2))) . is set
(D2) . {} is set
((() --> D1) with-replacement (,(D2))) . d2 is set
(D1,<*D2*>) . d2 is set
D1 is set

{D1} is non empty trivial V43(1) set
[:(),{D1}:] is Relation-like non empty set
bool [:(),{D1}:] is non empty set

[1,D2] is set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set

dom D2 is non empty Tree-like set
() with-replacement (,(dom D2)) is non empty Tree-like set
dom (D1,<*D2*>) is non empty Tree-like set

tree (doms <*D2*>) is non empty Tree-like set

[1,(dom D2)] is set
{1,(dom D2)} is non empty set
{{1,(dom D2)},{1}} is non empty set
{[1,(dom D2)]} is Relation-like Function-like constant non empty trivial V43(1) set
tree <*(dom D2)*> is non empty Tree-like set
^ (dom D2) is non empty Tree-like set
dom (() --> D1) is non empty Tree-like set

dom ((() --> D1) with-replacement (,D2)) is non empty Tree-like set
x is set

((() --> D1) with-replacement (,D2)) . {} is set
(() --> D1) . p is set
(D1,<*D2*>) . {} is set

((() --> D1) with-replacement (,D2)) . y is set
D2 . T is set
len <*D2*> is non empty ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
0 + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
<*D2*> . (0 + 1) is set

(() with-replacement (,(dom D2))) | p2 is non empty Tree-like set
(D1,<*D2*>) . y is set
((() --> D1) with-replacement (,D2)) . x is set
(D1,<*D2*>) . x is set