:: 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₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not 0 <= b₁ } is set
{{}} is functional non empty trivial V43(1) Tree-like set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not 0 <= b₁ } \/ {{}} is non empty set
elementary_tree 1 is non empty V36() Tree-like set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not 1 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not 1 <= b₁ } \/ {{}} 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
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D1 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D1 <= b₁ } \/ {{}} 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
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D2 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D2 <= b₁ } \/ {{}} 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
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D1 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D1 <= b₁ } \/ {{}} 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
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D2 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D2 <= b₁ } \/ {{}} 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
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len D2 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len D2 <= b₁ } \/ {{}} 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
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b₁ } \/ {{}} 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
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d2 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d2 <= b₁ } \/ {{}} 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
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D2 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not D2 <= b₁ } \/ {{}} 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
{ b₁ where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : ( 1 <= b₁ & b₁ <= 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
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b₁ } \/ {{}} 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
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b₁ } \/ {{}} 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
{ b₁ where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : ( 1 <= b₁ & b₁ <= 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
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b₁ } \/ {{}} 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
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len <*D2*> <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len <*D2*> <= b₁ } \/ {{}} 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 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
D1 is non empty set
D2 is Element of D1
d1 is Relation-like NAT -defined D1 -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of D1
(D2,d1) is Relation-like Function-like DecoratedTree-like set
rng (D2,d1) is set
p is set
dom (D2,d1) is non empty Tree-like set
p2 is set
(D2,d1) . p2 is 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₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b₁ } is set
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len d1 <= b₁ } \/ {{}} is non empty set
(D2,d1) . {} is set
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom (D2,d1)
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
(D2,d1) . x is set
y + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d1 . (y + 1) is set
rng d1 is set
D1 is non empty set
D2 is functional non empty constituted-DTrees DTree-set of D1
d1 is Element of D1
d2 is Relation-like NAT -defined D2 -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of D2
(d1,d2) is Relation-like Function-like DecoratedTree-like set
rng (d1,d2) is set
p2 is set
dom (d1,d2) is non empty Tree-like set
x is set
(d1,d2) . x 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
(tree (doms d2)) -level 1 is Level of tree (doms d2)
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of tree (doms d2) : len b₁ = 1 } is set
len (doms d2) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
{ <*b₁*> where b₁ is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : not len (doms d2) <= b₁ } is set
(d1,d2) . {} is set
len d2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom (d1,d2)
T is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
<*T*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
[1,T] is set
{1,T} is non empty set
{{1,T},{1}} is non empty set
{[1,T]} 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
<*T*> ^ y is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT
len <*T*> is non empty ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
(dom (d1,d2)) | <*T*> is non empty Tree-like set
(dom (d1,d2)) -level 1 is Level of dom (d1,d2)
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom (d1,d2) : len b₁ = 1 } is set
(d1,d2) | <*T*> is Relation-like Function-like DecoratedTree-like set
dom ((d1,d2) | <*T*>) is non empty Tree-like 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
<*T*> . 1 is set
<*x*> . 1 is set
T + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
d2 . (T + 1) is Relation-like Function-like set
rng d2 is set
a is Relation-like D1 -valued Function-like DecoratedTree-like Element of D2
a . y is set
rng a is set
D1 is non empty set
D2 is Element of D1
d1 is Relation-like D1 -valued Function-like DecoratedTree-like set
(D2,d1) is Relation-like Function-like DecoratedTree-like 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 Function-like DecoratedTree-like set
Trees D1 is functional non empty constituted-DTrees DTree-set of D1
(Trees D1) * is functional non empty FinSequence-membered FinSequenceSet of Trees D1
d2 is Relation-like D1 -valued Function-like DecoratedTree-like Element of Trees D1
<*d2*> is Relation-like NAT -defined Trees D1 -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of Trees D1
[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,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
(D2,<*d2*>) is Relation-like Function-like DecoratedTree-like set
p is Relation-like NAT -defined Trees D1 -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding Element of (Trees D1) *
(D2,p) is Relation-like D1 -valued Function-like DecoratedTree-like set
D1 is non empty set
D2 is Element of D1
d1 is Relation-like D1 -valued Function-like DecoratedTree-like set
d2 is Relation-like D1 -valued Function-like DecoratedTree-like set
(D2,d1,d2) is Relation-like Function-like DecoratedTree-like set
<*d1,d2*> is Relation-like NAT -defined Function-like non empty V36() V43(2) FinSequence-like FinSubsequence-like DTree-yielding 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*> 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 NAT -defined Function-like non empty V36() V43(1 + 1) FinSequence-like FinSubsequence-like DTree-yielding set
(D2,<*d1,d2*>) is Relation-like Function-like DecoratedTree-like set
Trees D1 is functional non empty constituted-DTrees DTree-set of D1
p is Relation-like D1 -valued Function-like DecoratedTree-like Element of Trees D1
p2 is Relation-like D1 -valued Function-like DecoratedTree-like Element of Trees D1
<*p,p2*> is Relation-like NAT -defined Function-like non empty V36() V43(2) FinSequence-like FinSubsequence-like DTree-yielding set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like DTree-yielding set
[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
<*p2*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like DTree-yielding 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
<*p*> ^ <*p2*> is Relation-like NAT -defined Function-like non empty V36() V43(1 + 1) FinSequence-like FinSubsequence-like DTree-yielding set
<*p*> is Relation-like NAT -defined Trees D1 -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of Trees D1
<*p2*> is Relation-like NAT -defined Trees D1 -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of Trees D1
<*p*> ^ <*p2*> is Relation-like NAT -defined Trees D1 -valued Function-like non empty V36() V43(1 + 1) FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of Trees D1
(Trees D1) * is functional non empty FinSequence-membered FinSequenceSet of Trees D1
(D2,p,p2) is Relation-like Function-like DecoratedTree-like set
(D2,<*p,p2*>) is Relation-like Function-like DecoratedTree-like set
x is Relation-like NAT -defined Trees D1 -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding Element of (Trees D1) *
(D2,x) is Relation-like D1 -valued Function-like DecoratedTree-like set
D1 is non empty set
FinTrees D1 is functional non empty constituted-DTrees DTree-set of D1
D2 is Relation-like NAT -defined FinTrees D1 -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of FinTrees D1
doms D2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set
dom (doms D2) is Element of bool NAT
dom D2 is Element of bool NAT
rng D2 is set
d1 is set
rng (doms D2) is set
d2 is set
(doms D2) . d2 is set
D2 . d2 is Relation-like Function-like set
p is Relation-like Function-like DecoratedTree-like set
dom p is non empty Tree-like set
D1 is non empty set
FinTrees D1 is functional non empty constituted-DTrees DTree-set of D1
D2 is Element of D1
d1 is Relation-like NAT -defined FinTrees D1 -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of FinTrees D1
(D2,d1) is Relation-like D1 -valued Function-like DecoratedTree-like set
dom (D2,d1) is non empty Tree-like set
(D1,d1) is Relation-like NAT -defined FinTrees -valued Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding FinSequence of FinTrees
tree (D1,d1) is non empty V36() Tree-like set
D1 is non empty set
bool D1 is non empty set
D2 is Element of bool D1
d1 is Relation-like NAT -defined D2 -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of D2
rng d1 is set
D1 is functional non empty constituted-DTrees set
bool D1 is non empty set
D2 is functional constituted-DTrees Element of bool D1
d1 is Relation-like NAT -defined D1 -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() (D1,D2)
F₁() is non empty Tree-like set
F₂() is non empty Tree-like set
D1 is set
the Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of F₁() is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of F₁()
d1 is non empty set
d2 is set
d2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes d2 is V36() set
p is set
p2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
p2 ^ x is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
y 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
y ^ y is Relation-like NAT -defined NAT -valued Function-like 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 F₁()
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of F₂()
T ^ x is Relation-like NAT -defined NAT -valued Function-like 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 F₁()
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of F₂()
T ^ x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
len y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
len T is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
a is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
y ^ a is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
a is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
T ^ a is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
n ^ y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
T ^ (n ^ y) is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
d2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
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 Relation-like NAT -defined NAT -valued Function-like non empty 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
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 NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of F₁()
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of F₂()
x ^ y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ {} is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
y is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
T is set
<*T*> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like set
[1,T] is set
{1,T} is non empty set
{{1,T},{1}} is non empty set
{[1,T]} is Relation-like Function-like constant non empty trivial V43(1) set
y ^ <*T*> is Relation-like NAT -defined Function-like non empty V36() FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
(x ^ x) ^ <*T*> is Relation-like NAT -defined Function-like non empty V36() FinSequence-like FinSubsequence-like set
len d2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
(len d2) + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
(d2 ^ <*p*>) . ((len d2) + 1) is set
len (x ^ x) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
(len (x ^ x)) + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
((x ^ x) ^ <*T*>) . ((len (x ^ x)) + 1) is set
len <*p*> is non empty ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
len <*T*> is non empty ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
len (d2 ^ <*p*>) is non empty ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
(len d2) + (len <*p*>) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
len ((x ^ x) ^ <*T*>) is non empty ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
(len (x ^ x)) + (len <*T*>) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
x ^ <*p2*> is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ (x ^ <*p2*>) is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT
d2 is non empty Tree-like set
p is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of F₁()
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of F₂()
p2 ^ x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of F₁()
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of F₂()
p2 ^ x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
D1 is Relation-like Function-like DecoratedTree-like set
dom D1 is non empty Tree-like set
D2 is Relation-like Function-like DecoratedTree-like set
dom D2 is non empty Tree-like set
Leaves (dom D1) is Element of bool (dom D1)
bool (dom D1) is non empty set
d1 is set
d2 is non empty Tree-like set
p is set
D1 . p is set
p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of d2
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . x is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
x ^ y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
D2 . y is set
T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
T ^ x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
D1 . T is set
y is set
D2 . x is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
y ^ y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
x is set
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . x is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
x ^ y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
y is set
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
a is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
x ^ a is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
D1 . x is set
T is set
D2 . a is set
p is Relation-like Function-like set
dom p is set
p2 is Relation-like Function-like DecoratedTree-like set
dom p2 is non empty Tree-like set
x is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like 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 V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . y is set
T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
y ^ T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . x is set
p2 . x is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
y ^ y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
D1 . y is set
D2 . y is set
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . x is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
x ^ y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
p2 . (x ^ y) is set
D2 . y is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
y ^ T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
D1 . y is set
D2 . T is set
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
n is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ n is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
a is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
q is non empty Tree-like set
Leaves q is Element of bool q
bool q is non empty set
len x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
len a is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
T is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
x ^ T is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
T is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
a ^ T is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d2 is Relation-like Function-like DecoratedTree-like set
dom d2 is non empty Tree-like set
p is Relation-like Function-like DecoratedTree-like set
dom p is non empty Tree-like set
p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . x is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
x ^ y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . x is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
x ^ y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
x is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom d2
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . y is set
p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
y ^ p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
d2 . (y ^ p2) is set
D2 . p2 is set
d2 . x is set
p . x is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . y is set
d2 . y is set
d2 . x is set
p . x is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . y is set
d2 . x is set
p . x is set
d2 . x is set
p . x is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom d2
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . y is set
T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
y ^ T 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 Element of dom D1
D1 . y is set
T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
y ^ T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
d2 . x is set
D2 . T is set
p . x is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom d2
D1 is non empty set
D2 is Relation-like D1 -valued Function-like DecoratedTree-like set
d1 is Relation-like D1 -valued Function-like DecoratedTree-like set
d2 is set
(D2,d1,d2) is Relation-like Function-like DecoratedTree-like set
rng (D2,d1,d2) is set
p is set
dom (D2,d1,d2) is non empty Tree-like set
p2 is set
(D2,d1,d2) . p2 is set
dom d1 is non empty Tree-like set
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom (D2,d1,d2)
dom D2 is non empty Tree-like set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
Leaves (dom D2) is Element of bool (dom D2)
bool (dom D2) is non empty set
D2 . y is Element of D1
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom d1
y ^ y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
(D2,d1,d2) . (y ^ y) is set
d1 . y is Element of D1
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
Leaves (dom D2) is Element of bool (dom D2)
bool (dom D2) is non empty set
D2 . y is Element of D1
(D2,d1,d2) . y is set
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
Leaves (dom D2) is Element of bool (dom D2)
bool (dom D2) is non empty set
D2 . y is Element of D1
dom D2 is non empty Tree-like set
Leaves (dom D2) is Element of bool (dom D2)
bool (dom D2) is non empty set
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom (D2,d1,d2)
y is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
D2 . y is Element of D1
T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom d1
y ^ T 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 Element of dom D2
D2 . y is Element of D1
T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom d1
y ^ T is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
(D2,d1,d2) . x is set
d1 . T is Element of D1
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom (D2,d1,d2)
dom D2 is non empty Tree-like set
Leaves (dom D2) is Element of bool (dom D2)
bool (dom D2) is non empty set
D1 is Relation-like Function-like DecoratedTree-like set
rng D1 is set
Leaves D1 is set
dom D1 is non empty Tree-like set
Leaves (dom D1) is Element of bool (dom D1)
bool (dom D1) is non empty set
D1 .: (Leaves (dom D1)) is set
D2 is Relation-like Function-like DecoratedTree-like set
d1 is set
(D1,D2,d1) is Relation-like Function-like DecoratedTree-like set
dom (D1,D2,d1) is non empty Tree-like set
d2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
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 D1
D1 . p is set
p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
p ^ p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
p is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . p is set
p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D2
p ^ p2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
d2 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom (D1,D2,d1)
(D1,D2,d1) . d2 is set
D1 . d2 is set
p is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom D1
D1 . p is set
D1 is non empty set
D2 is non empty set
[:D1,D2:] is Relation-like non empty set
d1 is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like set
d1 `1 is Relation-like D1 -valued Function-like DecoratedTree-like set
dom (d1 `1) is non empty Tree-like set
dom d1 is non empty Tree-like set
d1 `2 is Relation-like D2 -valued Function-like DecoratedTree-like set
dom (d1 `2) is non empty Tree-like set
pr1 (D1,D2) is Relation-like [:D1,D2:] -defined D1 -valued Function-like V18([:D1,D2:],D1) Element of bool [:[:D1,D2:],D1:]
[:[:D1,D2:],D1:] is Relation-like non empty set
bool [:[:D1,D2:],D1:] is non empty set
d1 * (pr1 (D1,D2)) is Relation-like D1 -valued Function-like DecoratedTree-like set
pr2 (D1,D2) is Relation-like [:D1,D2:] -defined D2 -valued Function-like V18([:D1,D2:],D2) Element of bool [:[:D1,D2:],D2:]
[:[:D1,D2:],D2:] is Relation-like non empty set
bool [:[:D1,D2:],D2:] is non empty set
d1 * (pr2 (D1,D2)) is Relation-like D2 -valued Function-like DecoratedTree-like set
rng d1 is set
dom (pr1 (D1,D2)) is Relation-like set
dom (pr2 (D1,D2)) is Relation-like set
D1 is non empty set
D2 is non empty set
[:D1,D2:] is Relation-like non empty set
d1 is Element of D1
(D1,d1) is Relation-like D1 -valued Function-like DecoratedTree-like Element of FinTrees D1
FinTrees D1 is functional non empty constituted-DTrees DTree-set of D1
(elementary_tree 0) --> d1 is Relation-like elementary_tree 0 -defined D1 -valued {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 Element of D2
[d1,d2] is Element of [:D1,D2:]
{d1,d2} is non empty set
{{d1,d2},{d1}} is non empty set
([:D1,D2:],[d1,d2]) is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of FinTrees [:D1,D2:]
FinTrees [:D1,D2:] is functional non empty constituted-DTrees DTree-set of [:D1,D2:]
(elementary_tree 0) --> [d1,d2] is Relation-like elementary_tree 0 -defined [:D1,D2:] -valued {[d1,d2]} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{[d1,d2]}) DecoratedTree-like Element of bool [:(elementary_tree 0),{[d1,d2]}:]
{[d1,d2]} is Relation-like Function-like constant non empty trivial V43(1) set
[:(elementary_tree 0),{[d1,d2]}:] is Relation-like non empty set
bool [:(elementary_tree 0),{[d1,d2]}:] is non empty set
([:D1,D2:],[d1,d2]) `1 is Relation-like D1 -valued Function-like DecoratedTree-like set
([:D1,D2:],[d1,d2]) `2 is Relation-like D2 -valued Function-like DecoratedTree-like set
(D2,d2) is Relation-like D2 -valued Function-like DecoratedTree-like Element of FinTrees D2
FinTrees D2 is functional non empty constituted-DTrees DTree-set of D2
(elementary_tree 0) --> d2 is Relation-like elementary_tree 0 -defined D2 -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
dom ([:D1,D2:],[d1,d2]) is non empty V36() Tree-like set
dom (([:D1,D2:],[d1,d2]) `1) is non empty Tree-like set
dom (([:D1,D2:],[d1,d2]) `2) is non empty Tree-like set
p is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom ([:D1,D2:],[d1,d2])
([:D1,D2:],[d1,d2]) . p is Element of [:D1,D2:]
[d1,d2] `1 is Element of D1
[d1,d2] `2 is Element of D2
(([:D1,D2:],[d1,d2]) `1) . p is set
(((([:D1,D2:],[d1,d2]) `1) . p)) is Relation-like Function-like DecoratedTree-like set
(elementary_tree 0) --> ((([:D1,D2:],[d1,d2]) `1) . p) is Relation-like elementary_tree 0 -defined {((([:D1,D2:],[d1,d2]) `1) . p)} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{((([:D1,D2:],[d1,d2]) `1) . p)}) DecoratedTree-like Element of bool [:(elementary_tree 0),{((([:D1,D2:],[d1,d2]) `1) . p)}:]
{((([:D1,D2:],[d1,d2]) `1) . p)} is non empty trivial V43(1) set
[:(elementary_tree 0),{((([:D1,D2:],[d1,d2]) `1) . p)}:] is Relation-like non empty set
bool [:(elementary_tree 0),{((([:D1,D2:],[d1,d2]) `1) . p)}:] is non empty set
(([:D1,D2:],[d1,d2]) `2) . p is set
(((([:D1,D2:],[d1,d2]) `2) . p)) is Relation-like Function-like DecoratedTree-like set
(elementary_tree 0) --> ((([:D1,D2:],[d1,d2]) `2) . p) is Relation-like elementary_tree 0 -defined {((([:D1,D2:],[d1,d2]) `2) . p)} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{((([:D1,D2:],[d1,d2]) `2) . p)}) DecoratedTree-like Element of bool [:(elementary_tree 0),{((([:D1,D2:],[d1,d2]) `2) . p)}:]
{((([:D1,D2:],[d1,d2]) `2) . p)} is non empty trivial V43(1) set
[:(elementary_tree 0),{((([:D1,D2:],[d1,d2]) `2) . p)}:] is Relation-like non empty set
bool [:(elementary_tree 0),{((([:D1,D2:],[d1,d2]) `2) . p)}:] 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
(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),(D2):> is Relation-like Function-like DecoratedTree-like set
[D1,D2] is set
{D1,D2} is non empty set
{{D1,D2},{D1}} is non empty set
([D1,D2]) is Relation-like Function-like DecoratedTree-like set
(elementary_tree 0) --> [D1,D2] is Relation-like elementary_tree 0 -defined {[D1,D2]} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{[D1,D2]}) DecoratedTree-like Element of bool [:(elementary_tree 0),{[D1,D2]}:]
{[D1,D2]} is Relation-like Function-like constant non empty trivial V43(1) set
[:(elementary_tree 0),{[D1,D2]}:] is Relation-like non empty set
bool [:(elementary_tree 0),{[D1,D2]}:] is non empty set
[:{D1},{D2}:] is Relation-like non empty set
d1 is Element of {D1}
d2 is Element of {D2}
[d1,d2] is Element of [:{D1},{D2}:]
{d1,d2} is non empty set
{d1} is non empty trivial V43(1) set
{{d1,d2},{d1}} is non empty set
([:{D1},{D2}:],[d1,d2]) is Relation-like [:{D1},{D2}:] -valued Function-like DecoratedTree-like Element of FinTrees [:{D1},{D2}:]
FinTrees [:{D1},{D2}:] is functional non empty constituted-DTrees DTree-set of [:{D1},{D2}:]
(elementary_tree 0) --> [d1,d2] is Relation-like elementary_tree 0 -defined [:{D1},{D2}:] -valued {[d1,d2]} -valued Function-like constant non empty V14( elementary_tree 0) V18( elementary_tree 0,{[d1,d2]}) DecoratedTree-like Element of bool [:(elementary_tree 0),{[d1,d2]}:]
{[d1,d2]} is Relation-like Function-like constant non empty trivial V43(1) set
[:(elementary_tree 0),{[d1,d2]}:] is Relation-like non empty set
bool [:(elementary_tree 0),{[d1,d2]}:] is non empty set
([:{D1},{D2}:],[d1,d2]) `1 is Relation-like {D1} -valued Function-like DecoratedTree-like set
([:{D1},{D2}:],[d1,d2]) `2 is Relation-like {D2} -valued Function-like DecoratedTree-like set
D1 is non empty set
D2 is non empty set
[:D1,D2:] is Relation-like non empty set
d1 is Element of D1
d2 is Element of D2
[d1,d2] is Element of [:D1,D2:]
{d1,d2} is non empty set
{d1} is non empty trivial V43(1) set
{{d1,d2},{d1}} is non empty set
p is functional non empty constituted-DTrees DTree-set of [:D1,D2:]
p2 is functional non empty constituted-DTrees DTree-set of D1
x is Relation-like NAT -defined p -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of p
dom x is Element of bool NAT
([d1,d2],x) is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like set
([d1,d2],x) `1 is Relation-like D1 -valued Function-like DecoratedTree-like set
y is Relation-like NAT -defined p2 -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of p2
dom y is Element of bool NAT
(d1,y) is Relation-like D1 -valued Function-like DecoratedTree-like set
doms x is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set
len (doms x) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
len x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
doms y is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set
len (doms y) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
len y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
dom (doms x) is Element of bool NAT
dom (doms y) is Element of bool NAT
x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() set
x . x is Relation-like Function-like set
y . x is Relation-like Function-like set
a is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of p
a `1 is Relation-like D1 -valued Function-like DecoratedTree-like set
(doms x) . x is set
dom a is non empty Tree-like set
(doms y) . x is set
dom (a `1) is non empty Tree-like set
dom (([d1,d2],x) `1) is non empty Tree-like set
dom ([d1,d2],x) is non empty Tree-like set
tree (doms x) is non empty Tree-like set
dom (d1,y) is non empty Tree-like set
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom (([d1,d2],x) `1)
(([d1,d2],x) `1) . x is set
(d1,y) . x is set
(([d1,d2],x) `1) . x is Element of D1
a is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom ([d1,d2],x)
([d1,d2],x) . a is Element of [:D1,D2:]
(([d1,d2],x) . a) `1 is Element of D1
([d1,d2],x) . x is set
T is Relation-like Function-like DecoratedTree-like set
dom T is non empty Tree-like set
n is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
n + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
x . (n + 1) is Relation-like Function-like set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is Relation-like Function-like constant non empty trivial V43(1) set
q is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom T
<*n*> ^ q is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT
T is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of p
T `1 is Relation-like D1 -valued Function-like DecoratedTree-like set
dom (T `1) is non empty Tree-like set
y . (n + 1) is Relation-like Function-like set
q is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom (T `1)
T . q is set
(d1,y) . a is set
(T `1) . q is Element of D1
D1 is non empty set
D2 is non empty set
[:D1,D2:] is Relation-like non empty set
d1 is Element of D1
d2 is Element of D2
[d1,d2] is Element of [:D1,D2:]
{d1,d2} is non empty set
{d1} is non empty trivial V43(1) set
{{d1,d2},{d1}} is non empty set
p is functional non empty constituted-DTrees DTree-set of [:D1,D2:]
p2 is functional non empty constituted-DTrees DTree-set of D2
x is Relation-like NAT -defined p -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of p
dom x is Element of bool NAT
([d1,d2],x) is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like set
([d1,d2],x) `2 is Relation-like D2 -valued Function-like DecoratedTree-like set
y is Relation-like NAT -defined p2 -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of p2
dom y is Element of bool NAT
(d2,y) is Relation-like D2 -valued Function-like DecoratedTree-like set
doms x is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set
len (doms x) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
len x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
doms y is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like Tree-yielding set
len (doms y) is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
len y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
dom (doms x) is Element of bool NAT
dom (doms y) is Element of bool NAT
x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() set
x . x is Relation-like Function-like set
y . x is Relation-like Function-like set
a is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of p
a `2 is Relation-like D2 -valued Function-like DecoratedTree-like set
(doms x) . x is set
dom a is non empty Tree-like set
(doms y) . x is set
dom (a `2) is non empty Tree-like set
dom (([d1,d2],x) `2) is non empty Tree-like set
dom ([d1,d2],x) is non empty Tree-like set
tree (doms x) is non empty Tree-like set
dom (d2,y) is non empty Tree-like set
x is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom (([d1,d2],x) `2)
(([d1,d2],x) `2) . x is set
(d2,y) . x is set
(([d1,d2],x) `2) . x is Element of D2
a is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom ([d1,d2],x)
([d1,d2],x) . a is Element of [:D1,D2:]
(([d1,d2],x) . a) `2 is Element of D2
([d1,d2],x) . x is set
T is Relation-like Function-like DecoratedTree-like set
dom T is non empty Tree-like set
n is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
n + 1 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
x . (n + 1) is Relation-like Function-like set
<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of NAT
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is Relation-like Function-like constant non empty trivial V43(1) set
q is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom T
<*n*> ^ q is Relation-like NAT -defined NAT -valued Function-like non empty V36() FinSequence-like FinSubsequence-like FinSequence of NAT
T is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of p
T `2 is Relation-like D2 -valued Function-like DecoratedTree-like set
dom (T `2) is non empty Tree-like set
y . (n + 1) is Relation-like Function-like set
q is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like Element of dom (T `2)
T . q is set
(d2,y) . a is set
(T `2) . q is Element of D2
D1 is non empty set
Trees D1 is functional non empty constituted-DTrees DTree-set of D1
D2 is non empty set
[:D1,D2:] is Relation-like non empty set
d1 is Element of D1
d2 is Element of D2
[d1,d2] is Element of [:D1,D2:]
{d1,d2} is non empty set
{d1} is non empty trivial V43(1) set
{{d1,d2},{d1}} is non empty set
p is functional non empty constituted-DTrees DTree-set of [:D1,D2:]
p2 is Relation-like NAT -defined p -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of p
dom p2 is Element of bool NAT
([d1,d2],p2) is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like set
([d1,d2],p2) `1 is Relation-like D1 -valued Function-like DecoratedTree-like set
len p2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
Seg (len p2) is V36() V43( len p2) Element of bool NAT
{ b<sub>1</sub> where b<sub>1</sub> is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= len p2 ) } is set
x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() set
p2 . x is Relation-like Function-like set
y is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of p
y `1 is Relation-like D1 -valued Function-like DecoratedTree-like set
y is Relation-like D1 -valued Function-like DecoratedTree-like Element of Trees D1
x is Relation-like NAT -defined Trees D1 -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of Trees D1
dom x is Element of bool NAT
(d1,x) is Relation-like D1 -valued Function-like DecoratedTree-like set
y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
p2 . y is Relation-like Function-like set
x . y is Relation-like Function-like set
y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
p2 . y is Relation-like Function-like set
x . y is Relation-like Function-like set
y is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like set
y `1 is Relation-like D1 -valued Function-like DecoratedTree-like set
T is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of p
T `1 is Relation-like D1 -valued Function-like DecoratedTree-like set
D1 is non empty set
D2 is non empty set
[:D1,D2:] is Relation-like non empty set
Trees D2 is functional non empty constituted-DTrees DTree-set of D2
d1 is Element of D1
d2 is Element of D2
[d1,d2] is Element of [:D1,D2:]
{d1,d2} is non empty set
{d1} is non empty trivial V43(1) set
{{d1,d2},{d1}} is non empty set
p is functional non empty constituted-DTrees DTree-set of [:D1,D2:]
p2 is Relation-like NAT -defined p -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of p
dom p2 is Element of bool NAT
([d1,d2],p2) is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like set
([d1,d2],p2) `2 is Relation-like D2 -valued Function-like DecoratedTree-like set
len p2 is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
Seg (len p2) is V36() V43( len p2) Element of bool NAT
{ b<sub>1</sub> where b<sub>1</sub> is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= len p2 ) } is set
x is ext-real V27() V28() V29() V30() V34() V35() V36() V41() set
p2 . x is Relation-like Function-like set
y is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of p
y `2 is Relation-like D2 -valued Function-like DecoratedTree-like set
y is Relation-like D2 -valued Function-like DecoratedTree-like Element of Trees D2
x is Relation-like NAT -defined Trees D2 -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of Trees D2
dom x is Element of bool NAT
(d2,x) is Relation-like D2 -valued Function-like DecoratedTree-like set
y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
p2 . y is Relation-like Function-like set
x . y is Relation-like Function-like set
y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
p2 . y is Relation-like Function-like set
x . y is Relation-like Function-like set
y is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like set
y `2 is Relation-like D2 -valued Function-like DecoratedTree-like set
T is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of p
T `2 is Relation-like D2 -valued Function-like DecoratedTree-like set
D1 is non empty set
FinTrees D1 is functional non empty constituted-DTrees DTree-set of D1
D2 is non empty set
[:D1,D2:] is Relation-like non empty set
FinTrees [:D1,D2:] is functional non empty constituted-DTrees DTree-set of [:D1,D2:]
d1 is Element of D1
d2 is Element of D2
[d1,d2] is Element of [:D1,D2:]
{d1,d2} is non empty set
{d1} is non empty trivial V43(1) set
{{d1,d2},{d1}} is non empty set
p is Relation-like NAT -defined FinTrees [:D1,D2:] -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of FinTrees [:D1,D2:]
dom p is Element of bool NAT
([:D1,D2:],[d1,d2],p) is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of FinTrees [:D1,D2:]
([:D1,D2:],[d1,d2],p) `1 is Relation-like D1 -valued Function-like DecoratedTree-like set
Trees D1 is functional non empty constituted-DTrees DTree-set of D1
p2 is Relation-like NAT -defined Trees D1 -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of Trees D1
dom p2 is Element of bool NAT
(d1,p2) is Relation-like D1 -valued Function-like DecoratedTree-like set
rng p2 is set
x is set
y is set
p2 . y is Relation-like Function-like set
y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
p . y is Relation-like Function-like set
p2 . y is Relation-like Function-like set
T is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of FinTrees [:D1,D2:]
T `1 is Relation-like D1 -valued Function-like DecoratedTree-like set
dom (T `1) is non empty Tree-like set
dom T is non empty V36() Tree-like set
D1 is non empty set
D2 is non empty set
[:D1,D2:] is Relation-like non empty set
FinTrees [:D1,D2:] is functional non empty constituted-DTrees DTree-set of [:D1,D2:]
FinTrees D2 is functional non empty constituted-DTrees DTree-set of D2
d1 is Element of D1
d2 is Element of D2
[d1,d2] is Element of [:D1,D2:]
{d1,d2} is non empty set
{d1} is non empty trivial V43(1) set
{{d1,d2},{d1}} is non empty set
p is Relation-like NAT -defined FinTrees [:D1,D2:] -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of FinTrees [:D1,D2:]
dom p is Element of bool NAT
([:D1,D2:],[d1,d2],p) is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of FinTrees [:D1,D2:]
([:D1,D2:],[d1,d2],p) `2 is Relation-like D2 -valued Function-like DecoratedTree-like set
Trees D2 is functional non empty constituted-DTrees DTree-set of D2
p2 is Relation-like NAT -defined Trees D2 -valued Function-like V36() FinSequence-like FinSubsequence-like Function-yielding V48() DTree-yielding FinSequence of Trees D2
dom p2 is Element of bool NAT
(d2,p2) is Relation-like D2 -valued Function-like DecoratedTree-like set
rng p2 is set
x is set
y is set
p2 . y is Relation-like Function-like set
y is ext-real V27() V28() V29() V30() V34() V35() V36() V41() Element of NAT
p . y is Relation-like Function-like set
p2 . y is Relation-like Function-like set
T is Relation-like [:D1,D2:] -valued Function-like DecoratedTree-like Element of FinTrees [:D1,D2:]
T `2 is Relation-like D2 -valued Function-like DecoratedTree-like set
dom (T `2) is non empty Tree-like set
dom T is non empty V36() Tree-like set