REAL is set
NAT is V6() V7() V8() non empty non trivial non finite V33() V34() countable denumerable Element of bool REAL
bool REAL is set
NAT is V6() V7() V8() non empty non trivial non finite V33() V34() countable denumerable set
bool NAT is non trivial non finite set
bool NAT is non trivial non finite set
{} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional finite finite-yielding V32() V33() V35( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() Cardinal-yielding countable V154() ext-real V158() set
the Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional finite finite-yielding V32() V33() V35( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() Cardinal-yielding countable V154() ext-real V158() set is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional finite finite-yielding V32() V33() V35( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() Cardinal-yielding countable V154() ext-real V158() set
1 is V6() V7() V8() V12() non empty finite V33() countable V154() ext-real V158() Element of NAT
{{},1} is non empty finite V32() countable set
Trees is non empty constituted-Trees set
bool Trees is set
FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees
K314() is non empty V112() L13()
the carrier of K314() is non empty set
FinTrees the carrier of K314() is non empty functional constituted-DTrees DTree-set of the carrier of K314()
K313(K314()) is functional constituted-DTrees Element of bool (FinTrees the carrier of K314())
bool (FinTrees the carrier of K314()) is set
[:K313(K314()),NAT:] is Relation-like set
bool [:K313(K314()),NAT:] is set
[:NAT,K313(K314()):] is Relation-like set
bool [:NAT,K313(K314()):] is set
K404() is set
2 is V6() V7() V8() V12() non empty finite V33() countable V154() ext-real V158() Element of NAT
K123(2,K404()) is M8(K404())
[:K123(2,K404()),K404():] is Relation-like set
bool [:K123(2,K404()),K404():] is set
3 is V6() V7() V8() V12() non empty finite V33() countable V154() ext-real V158() Element of NAT
K123(3,K404()) is M8(K404())
[:K123(3,K404()),K404():] is Relation-like set
bool [:K123(3,K404()),K404():] is set
K425() is Relation-like K123(2,K404()) -defined K404() -valued Function-like V25(K123(2,K404()),K404()) Element of bool [:K123(2,K404()),K404():]
0 is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional finite finite-yielding V32() V33() V35( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() Cardinal-yielding countable V154() ext-real V158() Element of NAT
<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional finite finite-yielding V32() V33() V35( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() Cardinal-yielding countable V154() ext-real V158() FinSequence of NAT
elementary_tree 0 is non empty Tree-like set
height (elementary_tree 0) is V6() V7() V8() V12() finite V33() countable V154() ext-real V158() Element of NAT
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
V is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total Variables of A
K334(S,V) is non empty V112() V116() V117() V118() L13()
the carrier of K334(S,V) is non empty set
FinTrees the carrier of K334(S,V) is non empty functional constituted-DTrees DTree-set of the carrier of K334(S,V)
S -Terms V is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(S,V))
bool (FinTrees the carrier of K334(S,V)) is set
the Sorts of A \/ V is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
K334(S,( the Sorts of A \/ V)) is non empty V112() V116() V117() V118() L13()
the carrier of K334(S,( the Sorts of A \/ V)) is non empty set
FinTrees the carrier of K334(S,( the Sorts of A \/ V)) is non empty functional constituted-DTrees DTree-set of the carrier of K334(S,( the Sorts of A \/ V))
S -Terms ( the Sorts of A \/ V) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(S,( the Sorts of A \/ V)))
bool (FinTrees the carrier of K334(S,( the Sorts of A \/ V))) is set
X is Element of the carrier of S
V . X is non empty set
G is Element of V . X
[G,X] is pair set
{G,X} is non empty finite countable set
{G} is non empty trivial finite V35(1) countable set
{{G,X},{G}} is non empty finite V32() countable set
root-tree [G,X] is Relation-like trivial Function-like constant finite DecoratedTree-like finite-order finite-branching countable set
C is Relation-like the carrier of K334(S,V) -valued Function-like finite DecoratedTree-like finite-order finite-branching countable M26( the carrier of K334(S,V), FinTrees the carrier of K334(S,V),S -Terms V)
the_sort_of C is Element of the carrier of S
f is Relation-like the carrier of K334(S,( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching countable M26( the carrier of K334(S,( the Sorts of A \/ V)), FinTrees the carrier of K334(S,( the Sorts of A \/ V)),S -Terms ( the Sorts of A \/ V))
the_sort_of f is Element of the carrier of S
the carrier' of S is non empty set
X is Element of the carrier' of S
Sym (X,V) is Element of K316(K334(S,V))
K316(K334(S,V)) is non empty Element of bool the carrier of K334(S,V)
bool the carrier of K334(S,V) is set
[X, the carrier of S] is pair set
{X, the carrier of S} is non empty finite countable set
{X} is non empty trivial finite V35(1) countable set
{{X, the carrier of S},{X}} is non empty finite V32() countable set
G is Relation-like NAT -defined FinTrees the carrier of K334(S,V) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Function-yielding V54() countable ArgumentSeq of Sym (X,V)
proj2 G is finite countable set
[X, the carrier of S] -tree G is Relation-like Function-like DecoratedTree-like set
C is Relation-like the carrier of K334(S,V) -valued Function-like finite DecoratedTree-like finite-order finite-branching countable M26( the carrier of K334(S,V), FinTrees the carrier of K334(S,V),S -Terms V)
the_sort_of C is Element of the carrier of S
f is Relation-like the carrier of K334(S,( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching countable M26( the carrier of K334(S,( the Sorts of A \/ V)), FinTrees the carrier of K334(S,( the Sorts of A \/ V)),S -Terms ( the Sorts of A \/ V))
the_sort_of f is Element of the carrier of S
C . {} is set
the_result_sort_of X is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V25( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S . X is Element of the carrier of S
G is Relation-like the carrier of K334(S,( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching countable M26( the carrier of K334(S,( the Sorts of A \/ V)), FinTrees the carrier of K334(S,( the Sorts of A \/ V)),S -Terms ( the Sorts of A \/ V))
X is Relation-like the carrier of K334(S,V) -valued Function-like finite DecoratedTree-like finite-order finite-branching countable M26( the carrier of K334(S,V), FinTrees the carrier of K334(S,V),S -Terms V)
the_sort_of G is Element of the carrier of S
the_sort_of X is Element of the carrier of S
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
S -Terms A is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(S,A))
K334(S,A) is non empty V112() V116() V117() V118() L13()
the carrier of K334(S,A) is non empty set
FinTrees the carrier of K334(S,A) is non empty functional constituted-DTrees DTree-set of the carrier of K334(S,A)
bool (FinTrees the carrier of K334(S,A)) is set
bool (S -Terms A) is set
V is non empty functional constituted-DTrees Element of bool (S -Terms A)
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
S -Terms A is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(S,A))
K334(S,A) is non empty V112() V116() V117() V118() L13()
the carrier of K334(S,A) is non empty set
FinTrees the carrier of K334(S,A) is non empty functional constituted-DTrees DTree-set of the carrier of K334(S,A)
bool (FinTrees the carrier of K334(S,A)) is set
bool (S -Terms A) is set
V is non empty functional constituted-DTrees Element of bool (S -Terms A)
(S,A,V) is non empty V68() strict V153() ManySortedSign
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
the ResultSort of (S,A,V) is Relation-like the carrier' of (S,A,V) -defined the carrier of (S,A,V) -valued Function-like V25( the carrier' of (S,A,V), the carrier of (S,A,V)) Element of bool [: the carrier' of (S,A,V), the carrier of (S,A,V):]
the carrier' of (S,A,V) is set
the carrier of (S,A,V) is non empty set
[: the carrier' of (S,A,V), the carrier of (S,A,V):] is Relation-like set
bool [: the carrier' of (S,A,V), the carrier of (S,A,V):] is set
id the carrier' of (S,A,V) is Relation-like the carrier' of (S,A,V) -defined the carrier' of (S,A,V) -valued Function-like one-to-one total Element of bool [: the carrier' of (S,A,V), the carrier' of (S,A,V):]
[: the carrier' of (S,A,V), the carrier' of (S,A,V):] is Relation-like set
bool [: the carrier' of (S,A,V), the carrier' of (S,A,V):] is set
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
S -Terms A is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(S,A))
K334(S,A) is non empty V112() V116() V117() V118() L13()
the carrier of K334(S,A) is non empty set
FinTrees the carrier of K334(S,A) is non empty functional constituted-DTrees DTree-set of the carrier of K334(S,A)
bool (FinTrees the carrier of K334(S,A)) is set
bool (S -Terms A) is set
V is non empty functional constituted-DTrees Element of bool (S -Terms A)
C is non empty non void V68() V153() ManySortedSign
the carrier of C is non empty set
f is Relation-like non-empty non empty-yielding the carrier of C -defined non empty Function-like total set
C -Terms f is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(C,f))
K334(C,f) is non empty V112() V116() V117() V118() L13()
the carrier of K334(C,f) is non empty set
FinTrees the carrier of K334(C,f) is non empty functional constituted-DTrees DTree-set of the carrier of K334(C,f)
bool (FinTrees the carrier of K334(C,f)) is set
bool (C -Terms f) is set
(S,A,V) is non empty V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
X is Relation-like Function-like DecoratedTree-like Element of V
G is Relation-like Function-like DecoratedTree-like Element of V
G . {} is set
g is non empty functional constituted-DTrees Element of bool (C -Terms f)
the carrier' of C is non empty set
{ the carrier of C} is non empty trivial finite V35(1) countable set
[: the carrier' of C,{ the carrier of C}:] is Relation-like set
(C,f,g) is non empty V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees g is non empty functional constituted-DTrees set
[: the carrier' of C,{ the carrier of C}:] -Subtrees g is functional constituted-DTrees Element of bool (Subtrees g)
bool (Subtrees g) is set
[: the carrier' of C,{ the carrier of C}:] -ImmediateSubtrees g is Relation-like [: the carrier' of C,{ the carrier of C}:] -Subtrees g -defined (Subtrees g) * -valued Function-like V25([: the carrier' of C,{ the carrier of C}:] -Subtrees g,(Subtrees g) * ) Function-yielding V54() Element of bool [:([: the carrier' of C,{ the carrier of C}:] -Subtrees g),((Subtrees g) *):]
(Subtrees g) * is non empty functional FinSequence-membered M8( Subtrees g)
[:([: the carrier' of C,{ the carrier of C}:] -Subtrees g),((Subtrees g) *):] is Relation-like set
bool [:([: the carrier' of C,{ the carrier of C}:] -Subtrees g),((Subtrees g) *):] is set
incl ([: the carrier' of C,{ the carrier of C}:] -Subtrees g) is Relation-like [: the carrier' of C,{ the carrier of C}:] -Subtrees g -defined Subtrees g -valued [: the carrier' of C,{ the carrier of C}:] -Subtrees g -valued Function-like one-to-one V25([: the carrier' of C,{ the carrier of C}:] -Subtrees g, Subtrees g) Function-yielding V54() Element of bool [:([: the carrier' of C,{ the carrier of C}:] -Subtrees g),(Subtrees g):]
[:([: the carrier' of C,{ the carrier of C}:] -Subtrees g),(Subtrees g):] is Relation-like set
bool [:([: the carrier' of C,{ the carrier of C}:] -Subtrees g),(Subtrees g):] is set
ManySortedSign(# (Subtrees g),([: the carrier' of C,{ the carrier of C}:] -Subtrees g),([: the carrier' of C,{ the carrier of C}:] -ImmediateSubtrees g),(incl ([: the carrier' of C,{ the carrier of C}:] -Subtrees g)) #) is non empty V68() strict V153() ManySortedSign
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
S -Terms A is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(S,A))
K334(S,A) is non empty V112() V116() V117() V118() L13()
the carrier of K334(S,A) is non empty set
FinTrees the carrier of K334(S,A) is non empty functional constituted-DTrees DTree-set of the carrier of K334(S,A)
bool (FinTrees the carrier of K334(S,A)) is set
bool (S -Terms A) is set
V is non empty functional constituted-DTrees Element of bool (S -Terms A)
(S,A,V) is non empty V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
X is Relation-like the carrier of K334(S,A) -valued Function-like finite DecoratedTree-like finite-order finite-branching countable CompoundTerm of S,A
X . {} is set
X is Relation-like Function-like DecoratedTree-like Element of V
X . {} is set
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
V is non empty functional constituted-DTrees SetWithCompoundTerm of S,A
(S,A,V) is non empty V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
S -Terms A is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(S,A))
K334(S,A) is non empty V112() V116() V117() V118() L13()
the carrier of K334(S,A) is non empty set
FinTrees the carrier of K334(S,A) is non empty functional constituted-DTrees DTree-set of the carrier of K334(S,A)
bool (FinTrees the carrier of K334(S,A)) is set
bool (S -Terms A) is set
V is non empty functional constituted-DTrees Element of bool (S -Terms A)
(S,A,V) is non empty V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
the carrier of (S,A,V) is non empty set
the carrier' of (S,A,V) is set
G is Element of the carrier of (S,A,V)
C is Relation-like Function-like DecoratedTree-like Element of V
proj1 C is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of proj1 C
C | f is Relation-like the carrier of K334(S,A) -valued Function-like finite DecoratedTree-like finite-order finite-branching countable M26( the carrier of K334(S,A), FinTrees the carrier of K334(S,A),S -Terms A)
G is set
C is Relation-like Function-like DecoratedTree-like Element of V
proj1 C is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of proj1 C
C | f is Relation-like the carrier of K334(S,A) -valued Function-like finite DecoratedTree-like finite-order finite-branching countable M26( the carrier of K334(S,A), FinTrees the carrier of K334(S,A),S -Terms A)
Leaves (proj1 C) is Element of bool (proj1 C)
bool (proj1 C) is set
C . f is Element of the carrier of K334(S,A)
proj1 (C | f) is non empty finite Tree-like finite-order finite-branching countable set
(proj1 C) | f is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of proj1 (C | f)
f ^ f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT
g is Relation-like the carrier of K334(S,A) -valued Function-like finite DecoratedTree-like finite-order finite-branching countable M26( the carrier of K334(S,A), FinTrees the carrier of K334(S,A),S -Terms A)
g . f is set
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
S -Terms A is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(S,A))
K334(S,A) is non empty V112() V116() V117() V118() L13()
the carrier of K334(S,A) is non empty set
FinTrees the carrier of K334(S,A) is non empty functional constituted-DTrees DTree-set of the carrier of K334(S,A)
bool (FinTrees the carrier of K334(S,A)) is set
bool (S -Terms A) is set
V is non empty functional constituted-DTrees Element of bool (S -Terms A)
(S,A,V) is non empty V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
the carrier of (S,A,V) is non empty set
the carrier' of (S,A,V) is set
X is Element of the carrier of (S,A,V)
C is Relation-like Function-like DecoratedTree-like Element of V
proj1 C is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of proj1 C
C | f is Relation-like the carrier of K334(S,A) -valued Function-like finite DecoratedTree-like finite-order finite-branching countable M26( the carrier of K334(S,A), FinTrees the carrier of K334(S,A),S -Terms A)
g is Relation-like the carrier of K334(S,A) -valued Function-like finite DecoratedTree-like finite-order finite-branching countable CompoundTerm of S,A
g . {} is set
f ^ (<*> NAT) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT
(proj1 C) | f is non empty Tree-like set
C . f is Element of the carrier of K334(S,A)
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
V is non empty functional constituted-DTrees SetWithCompoundTerm of S,A
(S,A,V) is non empty non void V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
the carrier' of (S,A,V) is non empty set
X is Element of the carrier' of (S,A,V)
the_arity_of X is Relation-like NAT -defined the carrier of (S,A,V) -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of (S,A,V) *
the carrier of (S,A,V) is non empty set
the carrier of (S,A,V) * is non empty functional FinSequence-membered M8( the carrier of (S,A,V))
the Arity of (S,A,V) is Relation-like the carrier' of (S,A,V) -defined the carrier of (S,A,V) * -valued Function-like V25( the carrier' of (S,A,V), the carrier of (S,A,V) * ) Function-yielding V54() Element of bool [: the carrier' of (S,A,V),( the carrier of (S,A,V) *):]
[: the carrier' of (S,A,V),( the carrier of (S,A,V) *):] is Relation-like set
bool [: the carrier' of (S,A,V),( the carrier of (S,A,V) *):] is set
the Arity of (S,A,V) . X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of (S,A,V) *
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
S -Terms A is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(S,A))
K334(S,A) is non empty V112() V116() V117() V118() L13()
the carrier of K334(S,A) is non empty set
FinTrees the carrier of K334(S,A) is non empty functional constituted-DTrees DTree-set of the carrier of K334(S,A)
bool (FinTrees the carrier of K334(S,A)) is set
bool (S -Terms A) is set
V is non empty functional constituted-DTrees Element of bool (S -Terms A)
(S,A,V) is non empty V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
the carrier of (S,A,V) is non empty set
X is Element of the carrier of (S,A,V)
G is Element of the carrier of (S,A,V)
C is Element of the carrier of (S,A,V)
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
S -Terms A is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(S,A))
K334(S,A) is non empty V112() V116() V117() V118() L13()
the carrier of K334(S,A) is non empty set
FinTrees the carrier of K334(S,A) is non empty functional constituted-DTrees DTree-set of the carrier of K334(S,A)
bool (FinTrees the carrier of K334(S,A)) is set
bool (S -Terms A) is set
V is non empty functional constituted-DTrees Element of bool (S -Terms A)
(S,A,V) is non empty V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
the carrier of (S,A,V) is non empty set
X is Relation-like Function-like finite countable Element of the carrier of (S,A,V)
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
V is non empty functional constituted-DTrees SetWithCompoundTerm of S,A
(S,A,V) is non empty non void V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
the carrier' of (S,A,V) is non empty set
X is Element of the carrier' of (S,A,V)
G is Element of the carrier' of (S,A,V)
C is Element of the carrier' of (S,A,V)
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
V is non empty functional constituted-DTrees SetWithCompoundTerm of S,A
(S,A,V) is non empty non void V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
the carrier' of (S,A,V) is non empty set
X is Relation-like Function-like finite countable Element of the carrier' of (S,A,V)
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
S -Terms A is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(S,A))
K334(S,A) is non empty V112() V116() V117() V118() L13()
the carrier of K334(S,A) is non empty set
FinTrees the carrier of K334(S,A) is non empty functional constituted-DTrees DTree-set of the carrier of K334(S,A)
bool (FinTrees the carrier of K334(S,A)) is set
bool (S -Terms A) is set
V is non empty functional constituted-DTrees Element of bool (S -Terms A)
(S,A,V) is non empty V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees V is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees V is functional constituted-DTrees Element of bool (Subtrees V)
bool (Subtrees V) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined (Subtrees V) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V,(Subtrees V) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):]
(Subtrees V) * is non empty functional FinSequence-membered M8( Subtrees V)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),((Subtrees V) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined Subtrees V -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees V, Subtrees V) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),(Subtrees V):] is set
ManySortedSign(# (Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) #) is non empty V68() strict V153() ManySortedSign
the Arity of (S,A,V) is Relation-like the carrier' of (S,A,V) -defined the carrier of (S,A,V) * -valued Function-like V25( the carrier' of (S,A,V), the carrier of (S,A,V) * ) Function-yielding V54() Element of bool [: the carrier' of (S,A,V),( the carrier of (S,A,V) *):]
the carrier' of (S,A,V) is set
the carrier of (S,A,V) is non empty set
the carrier of (S,A,V) * is non empty functional FinSequence-membered M8( the carrier of (S,A,V))
[: the carrier' of (S,A,V),( the carrier of (S,A,V) *):] is Relation-like set
bool [: the carrier' of (S,A,V),( the carrier of (S,A,V) *):] is set
X is non empty functional constituted-DTrees Element of bool (S -Terms A)
(S,A,X) is non empty V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees X is non empty functional constituted-DTrees set
[: the carrier' of S,{ the carrier of S}:] -Subtrees X is functional constituted-DTrees Element of bool (Subtrees X)
bool (Subtrees X) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees X -defined (Subtrees X) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees X,(Subtrees X) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees X),((Subtrees X) *):]
(Subtrees X) * is non empty functional FinSequence-membered M8( Subtrees X)
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees X),((Subtrees X) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees X),((Subtrees X) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees X) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees X -defined Subtrees X -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees X -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees X, Subtrees X) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees X),(Subtrees X):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees X),(Subtrees X):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees X),(Subtrees X):] is set
ManySortedSign(# (Subtrees X),([: the carrier' of S,{ the carrier of S}:] -Subtrees X),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees X)) #) is non empty V68() strict V153() ManySortedSign
the Arity of (S,A,X) is Relation-like the carrier' of (S,A,X) -defined the carrier of (S,A,X) * -valued Function-like V25( the carrier' of (S,A,X), the carrier of (S,A,X) * ) Function-yielding V54() Element of bool [: the carrier' of (S,A,X),( the carrier of (S,A,X) *):]
the carrier' of (S,A,X) is set
the carrier of (S,A,X) is non empty set
the carrier of (S,A,X) * is non empty functional FinSequence-membered M8( the carrier of (S,A,X))
[: the carrier' of (S,A,X),( the carrier of (S,A,X) *):] is Relation-like set
bool [: the carrier' of (S,A,X),( the carrier of (S,A,X) *):] is set
the ResultSort of (S,A,V) is Relation-like the carrier' of (S,A,V) -defined the carrier of (S,A,V) -valued Function-like V25( the carrier' of (S,A,V), the carrier of (S,A,V)) Element of bool [: the carrier' of (S,A,V), the carrier of (S,A,V):]
[: the carrier' of (S,A,V), the carrier of (S,A,V):] is Relation-like set
bool [: the carrier' of (S,A,V), the carrier of (S,A,V):] is set
the ResultSort of (S,A,X) is Relation-like the carrier' of (S,A,X) -defined the carrier of (S,A,X) -valued Function-like V25( the carrier' of (S,A,X), the carrier of (S,A,X)) Element of bool [: the carrier' of (S,A,X), the carrier of (S,A,X):]
[: the carrier' of (S,A,X), the carrier of (S,A,X):] is Relation-like set
bool [: the carrier' of (S,A,X), the carrier of (S,A,X):] is set
proj1 ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V) is set
id ([: the carrier' of S,{ the carrier of S}:] -Subtrees V) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees V -defined [: the carrier' of S,{ the carrier of S}:] -Subtrees V -valued Function-like one-to-one total Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees V),([: the carrier' of S,{ the carrier of S}:] -Subtrees V):] is set
proj1 (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees V)) is set
proj1 ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X) is set
id ([: the carrier' of S,{ the carrier of S}:] -Subtrees X) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees X -defined [: the carrier' of S,{ the carrier of S}:] -Subtrees X -valued Function-like one-to-one total Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees X),([: the carrier' of S,{ the carrier of S}:] -Subtrees X):]
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees X),([: the carrier' of S,{ the carrier of S}:] -Subtrees X):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees X),([: the carrier' of S,{ the carrier of S}:] -Subtrees X):] is set
proj1 (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees X)) is set
C is set
proj1 the Arity of (S,A,V) is set
proj1 the Arity of (S,A,X) is set
(proj1 the Arity of (S,A,V)) /\ (proj1 the Arity of (S,A,X)) is set
([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees V) . C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the Arity of (S,A,V) . C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the Arity of (S,A,X) . C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
t is Relation-like Function-like DecoratedTree-like Element of V
t9 is Relation-like Function-like DecoratedTree-like Element of X
f is Relation-like Function-like DecoratedTree-like Element of Subtrees V
f . {} is set
g is Relation-like NAT -defined Subtrees V -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Function-yielding V54() countable FinSequence of Subtrees V
(f . {}) -tree g is Relation-like Function-like DecoratedTree-like set
f is Relation-like NAT -defined Subtrees X -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Function-yielding V54() countable FinSequence of Subtrees X
(f . {}) -tree f is Relation-like Function-like DecoratedTree-like set
C is set
proj1 the ResultSort of (S,A,V) is set
proj1 the ResultSort of (S,A,X) is set
(proj1 the ResultSort of (S,A,V)) /\ (proj1 the ResultSort of (S,A,X)) is set
the ResultSort of (S,A,V) . C is set
the ResultSort of (S,A,X) . C is set
S is functional constituted-DTrees set
A is functional constituted-DTrees set
S \/ A is set
S is non empty functional constituted-DTrees set
A is non empty functional constituted-DTrees set
S \/ A is non empty functional constituted-DTrees set
Subtrees (S \/ A) is non empty functional constituted-DTrees set
Subtrees S is non empty functional constituted-DTrees set
Subtrees A is non empty functional constituted-DTrees set
(Subtrees S) \/ (Subtrees A) is non empty functional constituted-DTrees set
V is set
X is Relation-like Function-like DecoratedTree-like Element of S \/ A
proj1 X is non empty Tree-like set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of proj1 X
X | G is Relation-like Function-like DecoratedTree-like set
V is set
X is Relation-like Function-like DecoratedTree-like Element of S
proj1 X is non empty Tree-like set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of proj1 X
X | G is Relation-like Function-like DecoratedTree-like set
X is Relation-like Function-like DecoratedTree-like Element of A
proj1 X is non empty Tree-like set
G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of proj1 X
X | G is Relation-like Function-like DecoratedTree-like set
S is non empty functional constituted-DTrees set
A is non empty functional constituted-DTrees set
S \/ A is non empty functional constituted-DTrees set
V is set
V -Subtrees (S \/ A) is functional constituted-DTrees Element of bool (Subtrees (S \/ A))
Subtrees (S \/ A) is non empty functional constituted-DTrees set
bool (Subtrees (S \/ A)) is set
V -Subtrees S is functional constituted-DTrees Element of bool (Subtrees S)
Subtrees S is non empty functional constituted-DTrees set
bool (Subtrees S) is set
V -Subtrees A is functional constituted-DTrees Element of bool (Subtrees A)
Subtrees A is non empty functional constituted-DTrees set
bool (Subtrees A) is set
(V -Subtrees S) \/ (V -Subtrees A) is functional constituted-DTrees set
X is set
G is Relation-like Function-like DecoratedTree-like Element of S \/ A
proj1 G is non empty Tree-like set
C is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of proj1 G
G | C is Relation-like Function-like DecoratedTree-like set
Leaves (proj1 G) is Element of bool (proj1 G)
bool (proj1 G) is set
G . C is set
X is set
G is Relation-like Function-like DecoratedTree-like Element of S
proj1 G is non empty Tree-like set
C is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of proj1 G
G | C is Relation-like Function-like DecoratedTree-like set
Leaves (proj1 G) is Element of bool (proj1 G)
bool (proj1 G) is set
G . C is set
G is Relation-like Function-like DecoratedTree-like Element of A
proj1 G is non empty Tree-like set
C is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of proj1 G
G | C is Relation-like Function-like DecoratedTree-like set
Leaves (proj1 G) is Element of bool (proj1 G)
bool (proj1 G) is set
G . C is set
S is non empty functional constituted-DTrees set
A is non empty functional constituted-DTrees set
S \/ A is non empty functional constituted-DTrees set
V is Relation-like Function-like DecoratedTree-like Element of S \/ A
V is set
V -ImmediateSubtrees (S \/ A) is Relation-like V -Subtrees (S \/ A) -defined (Subtrees (S \/ A)) * -valued Function-like V25(V -Subtrees (S \/ A),(Subtrees (S \/ A)) * ) Function-yielding V54() Element of bool [:(V -Subtrees (S \/ A)),((Subtrees (S \/ A)) *):]
V -Subtrees (S \/ A) is functional constituted-DTrees Element of bool (Subtrees (S \/ A))
Subtrees (S \/ A) is non empty functional constituted-DTrees set
bool (Subtrees (S \/ A)) is set
(Subtrees (S \/ A)) * is non empty functional FinSequence-membered M8( Subtrees (S \/ A))
[:(V -Subtrees (S \/ A)),((Subtrees (S \/ A)) *):] is Relation-like set
bool [:(V -Subtrees (S \/ A)),((Subtrees (S \/ A)) *):] is set
V -ImmediateSubtrees S is Relation-like V -Subtrees S -defined (Subtrees S) * -valued Function-like V25(V -Subtrees S,(Subtrees S) * ) Function-yielding V54() Element of bool [:(V -Subtrees S),((Subtrees S) *):]
V -Subtrees S is functional constituted-DTrees Element of bool (Subtrees S)
Subtrees S is non empty functional constituted-DTrees set
bool (Subtrees S) is set
(Subtrees S) * is non empty functional FinSequence-membered M8( Subtrees S)
[:(V -Subtrees S),((Subtrees S) *):] is Relation-like set
bool [:(V -Subtrees S),((Subtrees S) *):] is set
V -ImmediateSubtrees A is Relation-like V -Subtrees A -defined (Subtrees A) * -valued Function-like V25(V -Subtrees A,(Subtrees A) * ) Function-yielding V54() Element of bool [:(V -Subtrees A),((Subtrees A) *):]
V -Subtrees A is functional constituted-DTrees Element of bool (Subtrees A)
Subtrees A is non empty functional constituted-DTrees set
bool (Subtrees A) is set
(Subtrees A) * is non empty functional FinSequence-membered M8( Subtrees A)
[:(V -Subtrees A),((Subtrees A) *):] is Relation-like set
bool [:(V -Subtrees A),((Subtrees A) *):] is set
(V -ImmediateSubtrees S) +* (V -ImmediateSubtrees A) is Relation-like Function-like set
proj1 (V -ImmediateSubtrees (S \/ A)) is set
proj1 (V -ImmediateSubtrees S) is set
proj1 (V -ImmediateSubtrees A) is set
(V -Subtrees S) \/ (V -Subtrees A) is functional constituted-DTrees set
g is set
(proj1 (V -ImmediateSubtrees S)) \/ (proj1 (V -ImmediateSubtrees A)) is set
(V -ImmediateSubtrees (S \/ A)) . g is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
(V -ImmediateSubtrees A) . g is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
f is Relation-like Function-like DecoratedTree-like Element of Subtrees (S \/ A)
f . {} is set
t is Relation-like NAT -defined Subtrees (S \/ A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Function-yielding V54() countable FinSequence of Subtrees (S \/ A)
(f . {}) -tree t is Relation-like Function-like DecoratedTree-like set
t9 is Relation-like NAT -defined Subtrees A -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Function-yielding V54() countable FinSequence of Subtrees A
(f . {}) -tree t9 is Relation-like Function-like DecoratedTree-like set
(V -ImmediateSubtrees S) . g is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
t9 is Relation-like NAT -defined Subtrees S -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Function-yielding V54() countable FinSequence of Subtrees S
(f . {}) -tree t9 is Relation-like Function-like DecoratedTree-like set
S is non empty non void V68() V153() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
S -Terms A is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of K334(S,A))
K334(S,A) is non empty V112() V116() V117() V118() L13()
the carrier of K334(S,A) is non empty set
FinTrees the carrier of K334(S,A) is non empty functional constituted-DTrees DTree-set of the carrier of K334(S,A)
bool (FinTrees the carrier of K334(S,A)) is set
bool (S -Terms A) is set
V is non empty functional constituted-DTrees Element of bool (S -Terms A)
X is non empty functional constituted-DTrees Element of bool (S -Terms A)
V \/ X is non empty functional constituted-DTrees Element of bool (S -Terms A)
(S,A,(V \/ X)) is non empty V68() strict Circuit-like unsplit V153() ManySortedSign
Subtrees (V \/ X) is non empty functional constituted-DTrees set
the carrier' of S is non empty set
{ the carrier of S} is non empty trivial finite V35(1) countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[: the carrier' of S,{ the carrier of S}:] -Subtrees (V \/ X) is functional constituted-DTrees Element of bool (Subtrees (V \/ X))
bool (Subtrees (V \/ X)) is set
[: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees (V \/ X) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees (V \/ X) -defined (Subtrees (V \/ X)) * -valued Function-like V25([: the carrier' of S,{ the carrier of S}:] -Subtrees (V \/ X),(Subtrees (V \/ X)) * ) Function-yielding V54() Element of bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees (V \/ X)),((Subtrees (V \/ X)) *):]
(Subtrees (V \/ X)) * is non empty functional FinSequence-membered M8( Subtrees (V \/ X))
[:([: the carrier' of S,{ the carrier of S}:] -Subtrees (V \/ X)),((Subtrees (V \/ X)) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] -Subtrees (V \/ X)),((Subtrees (V \/ X)) *):] is set
incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees (V \/ X)) is Relation-like [: the carrier' of S,{ the carrier of S}:] -Subtrees (V \/ X) -defined Subtrees (V \/ X) -valued [: the carrier' of S,{ the carrier of S}:] -Subtrees (V \/ X) -valued Function-like one-to-one V25([: the carrier' of S,{ the carrier of S}:] -Subtrees (V \/ X), Subtrees (V \/ X)) Function-yielding V54() Element of bool [:([: the carrier' of