:: CIRCTRM1 semantic presentation

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