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

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V28() V29() V30() V32() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding 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

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V28() V29() V30() V32() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of NAT

doms {} is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

rngs {} is Relation-like Function-like 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 ext-real V27() V28() V29() V30() V32() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding FinSequence of NAT

[:NAT,NAT:] is Relation-like non empty V36() set

elementary_tree 0 is non empty V36() Tree-like set

{ <*b

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

{ <*b

elementary_tree 1 is non empty V36() Tree-like set

{ <*b

{ <*b

<*0*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[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

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

{{},<*0*>} is functional non empty set

FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees

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

^ (elementary_tree 0) is non empty V36() Tree-like set

D1 is set

D2 is set

d1 is Relation-like NAT -defined D1 -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of D1

dom d1 is Element of bool NAT

d1 . D2 is set

rng d1 is set

D1 is Relation-like Function-like DecoratedTree-like set

D2 is Relation-like Function-like DecoratedTree-like 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 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1

D1 . d1 is set

D2 . d1 is set

d2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1

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

{ <*b

{ <*b

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

{ <*b

{ <*b

<*D2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,D2] is set

{1,D2} is non empty set

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

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

<*D2*> . 1 is set

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

<*d1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,d1] is set

{1,d1} is non empty set

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

{[1,d1]} is Relation-like Function-like constant non empty trivial V43(1) 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

{ <*b

{ <*b

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

{ <*b

{ <*b

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 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

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

d1 is Relation-like NAT -defined D2 -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of D2

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

(elementary_tree 0) --> D1 is Relation-like elementary_tree 0 -defined {D1} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{D1}) DecoratedTree-like Element of bool [:(elementary_tree 0),{D1}:]

{D1} is non empty trivial V43(1) set

[:(elementary_tree 0),{D1}:] is Relation-like non empty set

bool [:(elementary_tree 0),{D1}:] is non empty set

D1 is non empty set

D2 is Element of D1

(D2) is Relation-like Function-like DecoratedTree-like set

(elementary_tree 0) --> D2 is Relation-like elementary_tree 0 -defined D1 -valued {D2} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{D2}) DecoratedTree-like Element of bool [:(elementary_tree 0),{D2}:]

{D2} is non empty trivial V43(1) set

[:(elementary_tree 0),{D2}:] is Relation-like non empty set

bool [:(elementary_tree 0),{D2}:] is non empty set

FinTrees D1 is functional non empty constituted-DTrees DTree-set of D1

(elementary_tree 0) --> D2 is Relation-like elementary_tree 0 -defined D1 -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,D1) DecoratedTree-like Element of bool [:(elementary_tree 0),D1:]

[:(elementary_tree 0),D1:] is Relation-like non empty set

bool [:(elementary_tree 0),D1:] is non empty set

dom ((elementary_tree 0) --> D2) is non empty Tree-like set

D1 is set

(D1) is Relation-like Function-like DecoratedTree-like set

(elementary_tree 0) --> D1 is Relation-like elementary_tree 0 -defined {D1} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{D1}) DecoratedTree-like Element of bool [:(elementary_tree 0),{D1}:]

{D1} is non empty trivial V43(1) set

[:(elementary_tree 0),{D1}:] is Relation-like non empty set

bool [:(elementary_tree 0),{D1}:] is non empty set

dom (D1) is non empty Tree-like set

(D1) . {} is set

D1 is set

(D1) is Relation-like Function-like DecoratedTree-like set

(elementary_tree 0) --> D1 is Relation-like elementary_tree 0 -defined {D1} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{D1}) DecoratedTree-like Element of bool [:(elementary_tree 0),{D1}:]

{D1} is non empty trivial V43(1) set

[:(elementary_tree 0),{D1}:] is Relation-like non empty set

bool [:(elementary_tree 0),{D1}:] is non empty set

D2 is set

(D2) is Relation-like Function-like DecoratedTree-like set

(elementary_tree 0) --> D2 is Relation-like elementary_tree 0 -defined {D2} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{D2}) DecoratedTree-like Element of bool [:(elementary_tree 0),{D2}:]

{D2} is non empty trivial V43(1) set

[:(elementary_tree 0),{D2}:] is Relation-like non empty set

bool [:(elementary_tree 0),{D2}:] is non empty set

(D1) . {} is set

D1 is Relation-like Function-like DecoratedTree-like set

dom D1 is non empty Tree-like set

D1 . {} is set

((D1 . {})) is Relation-like Function-like DecoratedTree-like set

(elementary_tree 0) --> (D1 . {}) is Relation-like elementary_tree 0 -defined {(D1 . {})} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{(D1 . {})}) DecoratedTree-like Element of bool [:(elementary_tree 0),{(D1 . {})}:]

{(D1 . {})} is non empty trivial V43(1) set

[:(elementary_tree 0),{(D1 . {})}:] is Relation-like non empty set

bool [:(elementary_tree 0),{(D1 . {})}:] is non empty set

D2 is set

D1 . D2 is set

D1 is set

(D1) is Relation-like Function-like DecoratedTree-like set

(elementary_tree 0) --> D1 is Relation-like elementary_tree 0 -defined {D1} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{D1}) DecoratedTree-like Element of bool [:(elementary_tree 0),{D1}:]

{D1} is non empty trivial V43(1) set

[:(elementary_tree 0),{D1}:] is Relation-like non empty set

bool [:(elementary_tree 0),{D1}:] is non empty set

[{},D1] is set

{{},D1} is non empty set

{{{},D1},{{}}} is non empty set

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

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

D2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-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

{ <*b

{ <*b

D1 is set

d1 is set

d2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of elementary_tree (len D2)

p is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

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

<*p2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,p2] is set

{1,p2} is non empty set

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

{[1,p2]} is Relation-like Function-like constant non empty trivial V43(1) 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

<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,y] is set

{1,y} is non empty set

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

{[1,y]} is Relation-like Function-like constant non empty trivial V43(1) 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

<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,x] is set

{1,x} is non empty set

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

{[1,x]} is Relation-like Function-like constant non empty trivial V43(1) 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

<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,y] is set

{1,y} is non empty set

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

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

d1 is Relation-like Function-like set

dom d1 is set

d2 is Relation-like Function-like DecoratedTree-like 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

<*p*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,p] is set

{1,p} is non empty set

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

{[1,p]} is Relation-like Function-like constant non empty trivial V43(1) 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

<*p*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,p] is set

{1,p} is non empty set

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

{[1,p]} is Relation-like Function-like constant non empty trivial V43(1) 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

<*p2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,p2] is set

{1,p2} is non empty set

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

{[1,p2]} is Relation-like Function-like constant non empty trivial V43(1) 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

d1 is Relation-like Function-like DecoratedTree-like set

dom d1 is non empty Tree-like set

d1 . {} is set

d2 is Relation-like Function-like DecoratedTree-like set

dom d2 is non empty Tree-like set

d2 . {} is set

p is set

p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of elementary_tree (len D2)

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

<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,x] is set

{1,x} is non empty set

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

{[1,x]} is Relation-like Function-like constant non empty trivial V43(1) 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

<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,x] is set

{1,x} is non empty set

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

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

D1 is set

D2 is set

d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

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

d2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

(D2,d2) is Relation-like Function-like DecoratedTree-like 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

{ <*b

{ <*b

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

{ <*b

{ <*b

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

<*p2*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like set

[1,p2] is set

{1,p2} is non empty set

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

{[1,p2]} is Relation-like Function-like constant non empty trivial V43(1) 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

<*D1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,D1] is set

{1,D1} is non empty set

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

{[1,D1]} is Relation-like Function-like constant non empty trivial V43(1) 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

{ <*b

{ <*b

(elementary_tree D2) | <*D1*> is non empty Tree-like set

D2 |-> (elementary_tree 0) is Relation-like NAT -defined Function-like V36() V43(D2) FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding set

Seg D2 is V36() V43(D2) Element of bool NAT

{ b

(Seg D2) --> (elementary_tree 0) is Relation-like non-empty NAT -defined Seg D2 -defined Seg D2 -defined {(elementary_tree 0)} -valued Function-like constant V14( Seg D2) V14( Seg D2) V18( Seg D2,{(elementary_tree 0)}) V36() FinSequence-like FinSubsequence-like Element of bool [:(Seg D2),{(elementary_tree 0)}:]

{(elementary_tree 0)} is non empty trivial V43(1) set

[:(Seg D2),{(elementary_tree 0)}:] is Relation-like set

bool [:(Seg D2),{(elementary_tree 0)}:] is non empty set

tree (D2 |-> (elementary_tree 0)) 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 |-> (elementary_tree 0)) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT

(tree (D2 |-> (elementary_tree 0))) | <*D1*> is non empty Tree-like set

(D2 |-> (elementary_tree 0)) . (D1 + 1) is set

D1 is set

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

<*D2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,D2] is set

{1,D2} is non empty set

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

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

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

d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

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

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

(D1,d1) | <*D2*> is Relation-like Function-like DecoratedTree-like set

d1 . (D2 + 1) is set

((d1 . (D2 + 1))) is Relation-like Function-like DecoratedTree-like set

(elementary_tree 0) --> (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 [:(elementary_tree 0),{(d1 . (D2 + 1))}:]

{(d1 . (D2 + 1))} is non empty trivial V43(1) set

[:(elementary_tree 0),{(d1 . (D2 + 1))}:] is Relation-like non empty set

bool [:(elementary_tree 0),{(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

{ <*b

{ <*b

(elementary_tree (len d1)) | <*D2*> is non empty Tree-like set

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

d2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of (dom (D1,d1)) | <*D2*>

<*D2*> ^ d2 is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT

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

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

D2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

D1 is set

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

doms D2 is Relation-like Function-like set

dom (doms D2) is set

dom D2 is Element of bool NAT

d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

tree d1 is non empty Tree-like set

d2 is set

p is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of tree d1

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

<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,x] is set

{1,x} is non empty set

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

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

p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

<*x*> ^ p2 is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT

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

y is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

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

K149(D2) is Relation-like Function-like 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

<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,y] is set

{1,y} is non empty set

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

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

y is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

<*y*> ^ y is Relation-like NAT -defined Function-like non empty V36() FinSequence-like FinSubsequence-like 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

d2 is Relation-like Function-like set

dom d2 is set

p is Relation-like Function-like DecoratedTree-like 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

<*p2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,p2] is set

{1,p2} is non empty set

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

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

p | <*p2*> is Relation-like Function-like DecoratedTree-like set

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

D2 . (p2 + 1) is set

x is Relation-like Function-like DecoratedTree-like 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

y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

<*p2*> ^ y is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT

p . (<*p2*> ^ y) is set

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

<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,y] is set

{1,y} is non empty set

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

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

T is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

<*y*> ^ T is Relation-like NAT -defined Function-like non empty V36() FinSequence-like FinSubsequence-like set

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

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

K149(D2) is Relation-like Function-like 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

d1 is Relation-like Function-like DecoratedTree-like set

dom d1 is non empty Tree-like set

d1 . {} is set

d2 is Relation-like Function-like DecoratedTree-like set

dom d2 is non empty Tree-like set

d2 . {} is set

p is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like DTree-yielding set

doms p is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

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

p2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like DTree-yielding set

doms p2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

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

x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

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

<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,y] is set

{1,y} is non empty set

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

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

y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

<*y*> ^ y is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT

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

d1 | <*y*> is Relation-like Function-like DecoratedTree-like set

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

D2 . (y + 1) is set

d2 | <*y*> is Relation-like Function-like DecoratedTree-like 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

D2 is Relation-like Function-like DecoratedTree-like set

<*D2*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like DTree-yielding set

[1,D2] is set

{1,D2} is non empty set

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

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

(D1,<*D2*>) is Relation-like Function-like DecoratedTree-like set

D1 is set

D2 is Relation-like Function-like DecoratedTree-like set

d1 is Relation-like Function-like DecoratedTree-like set

<*D2,d1*> is Relation-like NAT -defined Function-like non empty V36() V43(2) FinSequence-like FinSubsequence-like DTree-yielding set

<*D2*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like DTree-yielding set

[1,D2] is set

{1,D2} is non empty set

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

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

<*d1*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like DTree-yielding set

[1,d1] is set

{1,d1} is non empty set

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

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

<*D2*> ^ <*d1*> is Relation-like NAT -defined Function-like non empty V36() V43(1 + 1) FinSequence-like FinSubsequence-like DTree-yielding 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

D2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like DTree-yielding set

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

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

doms D2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

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

d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like DTree-yielding set

doms d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

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

D1 is set

D2 is set

d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like DTree-yielding set

(D2,d1) is Relation-like Function-like DecoratedTree-like 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

doms d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

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

p is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

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

(doms d1) . (d2 + 1) is set

<*d2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,d2] is set

{1,d2} is non empty set

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

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

<*d2*> ^ p is Relation-like NAT -defined Function-like non empty V36() FinSequence-like FinSubsequence-like set

dom d1 is Element of bool NAT

d1 . (d2 + 1) is set

p2 is Relation-like Function-like DecoratedTree-like set

y is Relation-like Function-like DecoratedTree-like set

dom y is non empty Tree-like set

y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom y

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

<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,x] is set

{1,x} is non empty set

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

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

T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom y

<*x*> ^ T is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT

p is Relation-like Function-like DecoratedTree-like 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

<*d2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,d2] is set

{1,d2} is non empty set

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

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

p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom p

<*d2*> ^ p2 is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT

x is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like 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

y is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,y] is set

{1,y} is non empty set

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

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

<*y*> ^ y is Relation-like NAT -defined Function-like non empty V36() FinSequence-like FinSubsequence-like set

p is Relation-like Function-like DecoratedTree-like set

dom p is non empty Tree-like set

T is Relation-like Function-like DecoratedTree-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

<*d2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,d2] is set

{1,d2} is non empty set

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

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

p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom p

<*d2*> ^ p2 is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT

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

y is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

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

(doms d1) . (x + 1) is set

<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,x] is set

{1,x} is non empty set

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

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

<*x*> ^ y is Relation-like NAT -defined Function-like non empty V36() FinSequence-like FinSubsequence-like 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

<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,y] is set

{1,y} is non empty set

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

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

x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom T

<*y*> ^ x is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT

D1 is set

D2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like DTree-yielding set

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

(D1,D2) is Relation-like Function-like DecoratedTree-like 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

D2 . (d1 + 1) is set

<*d1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,d1] is set

{1,d1} is non empty set

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

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

d2 is Relation-like Function-like DecoratedTree-like set

dom d2 is non empty Tree-like set

p is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom d2

<*d1*> ^ p is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT

(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*> is Relation-like Function-like DecoratedTree-like set

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

D1 is set

D2 is Relation-like Function-like DecoratedTree-like set

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

<*D2*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like DTree-yielding set

[1,D2] is set

{1,D2} is non empty set

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

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

(D1,<*D2*>) is Relation-like Function-like DecoratedTree-like 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

doms <*D2*> is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

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

<*(dom D2)*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like Tree-yielding 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

D2 is Relation-like Function-like DecoratedTree-like set

d1 is Relation-like Function-like DecoratedTree-like set

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

<*D2,d1*> is Relation-like NAT -defined Function-like non empty V36() V43(2) FinSequence-like FinSubsequence-like DTree-yielding set

<*D2*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like DTree-yielding set

[1,D2] is set

{1,D2} is non empty set

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

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

<*d1*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like DTree-yielding set

[1,d1] is set

{1,d1} is non empty set

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

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

<*D2*> ^ <*d1*> is Relation-like NAT -defined Function-like non empty V36() V43(1 + 1) FinSequence-like FinSubsequence-like DTree-yielding 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

doms <*D2,d1*> is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

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

<*(dom D2),(dom d1)*> is Relation-like NAT -defined Function-like non empty V36() V43(2) FinSequence-like FinSubsequence-like Tree-yielding set

<*(dom D2)*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like Tree-yielding 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

<*(dom d1)*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like Tree-yielding 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

<*(dom D2)*> ^ <*(dom d1)*> is Relation-like NAT -defined Function-like non empty V36() V43(1 + 1) FinSequence-like FinSubsequence-like Tree-yielding set

D1 is set

D2 is set

d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like DTree-yielding set

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

d2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like DTree-yielding set

(D2,d2) is Relation-like Function-like DecoratedTree-like set

(D1,d1) . {} is set

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

doms d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

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

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

doms d2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding 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

<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,x] is set

{1,x} is non empty set

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

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

(D1,d1) | <*x*> is Relation-like Function-like DecoratedTree-like set

d2 . p is set

D1 is set

(D1) is Relation-like Function-like DecoratedTree-like set

(elementary_tree 0) --> D1 is Relation-like elementary_tree 0 -defined {D1} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{D1}) DecoratedTree-like Element of bool [:(elementary_tree 0),{D1}:]

{D1} is non empty trivial V43(1) set

[:(elementary_tree 0),{D1}:] is Relation-like non empty set

bool [:(elementary_tree 0),{D1}:] is non empty set

D2 is set

d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

(D2,d1) is Relation-like Function-like DecoratedTree-like 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

{ <*b

{ <*b

D1 is set

(D1) is Relation-like Function-like DecoratedTree-like set

(elementary_tree 0) --> D1 is Relation-like elementary_tree 0 -defined {D1} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{D1}) DecoratedTree-like Element of bool [:(elementary_tree 0),{D1}:]

{D1} is non empty trivial V43(1) set

[:(elementary_tree 0),{D1}:] is Relation-like non empty set

bool [:(elementary_tree 0),{D1}:] is non empty set

D2 is set

d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

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

(D1) . {} is set

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

d2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like DTree-yielding set

doms d2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

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

doms d1 is Relation-like Function-like set

dom (doms d1) is set

dom d1 is Element of bool NAT

D1 is set

D2 is set

d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

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

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

dom d1 is Element of bool NAT

d2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

(D2,d2) is Relation-like Function-like DecoratedTree-like set

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

(D1,d1) . {} is set

(len d1) |-> (elementary_tree 0) is Relation-like NAT -defined Function-like V36() V43( len d1) FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding set

Seg (len d1) is V36() V43( len d1) Element of bool NAT

{ b

(Seg (len d1)) --> (elementary_tree 0) is Relation-like non-empty NAT -defined Seg (len d1) -defined Seg (len d1) -defined {(elementary_tree 0)} -valued Function-like constant V14( Seg (len d1)) V14( Seg (len d1)) V18( Seg (len d1),{(elementary_tree 0)}) V36() FinSequence-like FinSubsequence-like Element of bool [:(Seg (len d1)),{(elementary_tree 0)}:]

{(elementary_tree 0)} is non empty trivial V43(1) set

[:(Seg (len d1)),{(elementary_tree 0)}:] is Relation-like set

bool [:(Seg (len d1)),{(elementary_tree 0)}:] is non empty set

tree ((len d1) |-> (elementary_tree 0)) is non empty V36() Tree-like set

elementary_tree (len d1) is non empty V36() Tree-like set

{ <*b

{ <*b

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

p is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like DTree-yielding set

doms p is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding 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

(elementary_tree 0) --> (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 [:(elementary_tree 0),{(d1 . p2)}:]

{(d1 . p2)} is non empty trivial V43(1) set

[:(elementary_tree 0),{(d1 . p2)}:] is Relation-like non empty set

bool [:(elementary_tree 0),{(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

<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,y] is set

{1,y} is non empty set

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

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

(D1,d1) | <*y*> is Relation-like Function-like DecoratedTree-like set

D1 is set

D2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like DTree-yielding set

(D1,D2) is Relation-like Function-like DecoratedTree-like 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

<*d1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT

[1,d1] is set

{1,d1} is non empty set

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

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

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

d2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

<*d1*> ^ d2 is Relation-like NAT -defined Function-like non empty V36() FinSequence-like FinSubsequence-like set

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

D2 .. ((d1 + 1),d2) is set

K149(D2) is Relation-like Function-like set

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

doms D2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding 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

p is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

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

(D1,D2) | <*d1*> is Relation-like Function-like DecoratedTree-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 Relation-like Function-like DecoratedTree-like set

(D1) is Relation-like Function-like DecoratedTree-like set

(elementary_tree 0) --> D1 is Relation-like elementary_tree 0 -defined {D1} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{D1}) DecoratedTree-like Element of bool [:(elementary_tree 0),{D1}:]

{D1} is non empty trivial V43(1) set

[:(elementary_tree 0),{D1}:] is Relation-like non empty set

bool [:(elementary_tree 0),{D1}:] is non empty set

(D1,{}) is Relation-like Function-like DecoratedTree-like set

len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V28() V29() V30() V32() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of NAT

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

D2 is set

(D1,{}) . D2 is set

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

D2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like DTree-yielding set

doms D2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

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

d1 is set

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

(D1,D2) . d1 is set

D1 is set

(elementary_tree 1) --> D1 is Relation-like elementary_tree 1 -defined {D1} -valued Function-like constant non empty V14( elementary_tree 1) V18( elementary_tree 1,{D1}) DecoratedTree-like Element of bool [:(elementary_tree 1),{D1}:]

{D1} is non empty trivial V43(1) set

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

bool [:(elementary_tree 1),{D1}:] is non empty set

D2 is set

<*D2*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like set

[1,D2] is set

{1,D2} is non empty set

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

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

(D1,<*D2*>) is Relation-like Function-like DecoratedTree-like set

(D2) is Relation-like Function-like DecoratedTree-like set

(elementary_tree 0) --> D2 is Relation-like elementary_tree 0 -defined {D2} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{D2}) DecoratedTree-like Element of bool [:(elementary_tree 0),{D2}:]

{D2} is non empty trivial V43(1) set

[:(elementary_tree 0),{D2}:] is Relation-like non empty set

bool [:(elementary_tree 0),{D2}:] is non empty set

((elementary_tree 1) --> D1) with-replacement (<*0*>,(D2)) is Relation-like Function-like DecoratedTree-like 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

{ <*b

{ <*b

dom (D2) is non empty Tree-like set

dom ((elementary_tree 1) --> D1) is non empty Tree-like set

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

(elementary_tree 1) with-replacement (<*0*>,(elementary_tree 0)) is non empty Tree-like set

d2 is set

<*D2*> . 1 is set

(D1,<*D2*>) . {} is set

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

((elementary_tree 1) --> D1) . {} is set

(D1,<*D2*>) . <*0*> is set

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

<*D2*> . (0 + 1) is set

(((elementary_tree 1) --> D1) with-replacement (<*0*>,(D2))) . <*0*> is set

(D2) . {} is set

(((elementary_tree 1) --> D1) with-replacement (<*0*>,(D2))) . d2 is set

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

D1 is set

(elementary_tree 1) --> D1 is Relation-like elementary_tree 1 -defined {D1} -valued Function-like constant non empty V14( elementary_tree 1) V18( elementary_tree 1,{D1}) DecoratedTree-like Element of bool [:(elementary_tree 1),{D1}:]

{D1} is non empty trivial V43(1) set

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

bool [:(elementary_tree 1),{D1}:] is non empty set

D2 is Relation-like Function-like DecoratedTree-like set

<*D2*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like DTree-yielding set

[1,D2] is set

{1,D2} is non empty set

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

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

(D1,<*D2*>) is Relation-like Function-like DecoratedTree-like set

((elementary_tree 1) --> D1) with-replacement (<*0*>,D2) is Relation-like Function-like DecoratedTree-like set

dom D2 is non empty Tree-like set

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

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

doms <*D2*> is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set

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

<*(dom D2)*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like Tree-yielding 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 ((elementary_tree 1) --> D1) is non empty Tree-like set

p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of elementary_tree 1

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

x is set

y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of (elementary_tree 1) with-replacement (<*0*>,(dom D2))

p is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of elementary_tree 1

p2 ^ p is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

p2 ^ y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

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

((elementary_tree 1) --> D1) . p is set

(D1,<*D2*>) . {} is set

y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

<*0*> ^ y is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT

T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2

p2 ^ T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

(((elementary_tree 1) --> D1) with-replacement (<*0*>,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

(D1,<*D2*>) | p2 is Relation-like Function-like DecoratedTree-like set

((elementary_tree 1) with-replacement (<*0*>,(dom D2))) | p2 is non empty Tree-like set

(D1,<*D2*>) . y is set

(((elementary_tree 1) --> D1) with-replacement (<*0*>,D2)) . x is set

(D1,<*D2*>) . x is set

y is Relation-like NAT -defined NAT -valued