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
{ <*b1*> where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not 0 <= b1 } is set
{{}} is functional non empty trivial V43(1) Tree-like 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
<*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
{ <*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
<*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
{ <*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
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
{ <*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
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
{ <*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
<*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
{ <*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
(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
{ b1 where b1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : ( 1 <= b1 & b1 <= D2 ) } is set
(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
{ <*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
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
{ <*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 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
{ 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)) --> (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
{ <*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
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
{ <*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 ((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