:: ABCMIZ_A semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

{} is empty trivial Relation-like non-empty empty-yielding NAT -defined non pair Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V105() V106() non with_pair ext-real non negative set

the empty trivial Relation-like non-empty empty-yielding NAT -defined non pair Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V105() V106() non with_pair ext-real non negative set is empty trivial Relation-like non-empty empty-yielding NAT -defined non pair Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V105() V106() non with_pair ext-real non negative set

1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative Element of NAT

{{},1} is non empty finite V32() non with_pair set

Trees is non empty constituted-Trees set

bool Trees is non empty set

COMPLEX is set

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

K422() is non empty V137() L15()

the carrier of K422() is non empty set

FinTrees the carrier of K422() is non empty functional constituted-DTrees DTree-set of the carrier of K422()

K421(K422()) is functional constituted-DTrees Element of bool (FinTrees the carrier of K422())

bool (FinTrees the carrier of K422()) is non empty set

[:K421(K422()),NAT:] is Relation-like set

bool [:K421(K422()),NAT:] is non empty set

[:NAT,K421(K422()):] is Relation-like set

bool [:NAT,K421(K422()):] is non empty set

K488() is set

2 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative Element of NAT

2 -tuples_on K488() is FinSequenceSet of K488()

[:(2 -tuples_on K488()),K488():] is Relation-like set

bool [:(2 -tuples_on K488()),K488():] is non empty set

3 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative Element of NAT

3 -tuples_on K488() is FinSequenceSet of K488()

[:(3 -tuples_on K488()),K488():] is Relation-like set

bool [:(3 -tuples_on K488()),K488():] is non empty set

K524() is Relation-like 2 -tuples_on K488() -defined K488() -valued Function-like V25(2 -tuples_on K488(),K488()) Element of bool [:(2 -tuples_on K488()),K488():]

Vars is non empty set

bool Vars is non empty set

[:Vars,NAT:] is non empty non trivial Relation-like non finite set

bool [:Vars,NAT:] is non empty non trivial non finite set

QuasiLoci is non empty FinSequenceSet of Vars

a_Type is set

0 is empty trivial Relation-like non-empty empty-yielding NAT -defined non pair Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V105() V106() non with_pair ext-real non negative Element of NAT

an_Adj is set

a_Term is set

{a_Type,an_Adj,a_Term} is non empty finite set

[:QuasiLoci,NAT:] is non empty non trivial Relation-like non finite set

VarPoset is non empty V261() V263() V264() V265() L25()

the carrier of VarPoset is non empty set

RAT is set

INT is set

<*> NAT is empty trivial proper Relation-like non-empty empty-yielding NAT -defined NAT -valued non pair Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V105() V106() non with_pair ext-real non negative FinSequence of NAT

[:NAT,NAT:] is non empty non trivial Relation-like non finite set

Seg 1 is non empty trivial finite 1 -element Element of bool NAT

{ b

{1} is non empty trivial finite V32() 1 -element non with_pair set

Seg 2 is non empty finite 2 -element Element of bool NAT

{ b

{1,2} is non empty finite V32() non with_pair set

K179(0) is non empty V39() set

{0} is non empty trivial functional finite V32() 1 -element non with_pair Element of bool NAT

{0,1,2} is non empty finite non with_pair Element of bool NAT

{ [(varcl b

K829(Vars) is empty trivial Relation-like non-empty empty-yielding NAT -defined Vars -valued non pair Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V105() V106() non with_pair ext-real non negative Element of Vars *

Vars * is non empty functional FinSequence-membered FinSequenceSet of Vars

* is set

non_op is set

{*,non_op} is non empty finite set

<*an_Adj,a_Type*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set

<*an_Adj*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

[1,an_Adj] is non empty pair set

{1,an_Adj} is non empty finite set

{{1,an_Adj},{1}} is non empty finite V32() set

{[1,an_Adj]} is non empty trivial Relation-like Function-like constant finite 1 -element set

<*a_Type*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

[1,a_Type] is non empty pair set

{1,a_Type} is non empty finite set

{{1,a_Type},{1}} is non empty finite V32() set

{[1,a_Type]} is non empty trivial Relation-like Function-like constant finite 1 -element set

<*an_Adj*> ^ <*a_Type*> is non empty Relation-like NAT -defined Function-like finite K747(1,1) -element FinSequence-like FinSubsequence-like set

K747(1,1) is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative Element of NAT

{a_Term} is non empty trivial finite 1 -element set

{a_Term} * is non empty functional FinSequence-membered FinSequenceSet of {a_Term}

Constructors is non empty set

Modes is non empty set

{a_Type} is non empty trivial finite 1 -element set

[:{a_Type},[:QuasiLoci,NAT:]:] is non empty non trivial Relation-like non finite set

Attrs is non empty set

{an_Adj} is non empty trivial finite 1 -element set

[:{an_Adj},[:QuasiLoci,NAT:]:] is non empty non trivial Relation-like non finite set

Modes \/ Attrs is non empty set

Funcs is non empty set

[:{a_Term},[:QuasiLoci,NAT:]:] is non empty non trivial Relation-like non finite set

(Modes \/ Attrs) \/ Funcs is non empty set

MaxConstrSign is non empty non void V68() strict V146() constructor initialized with_an_operation_for_each_sort ManySortedSign

{*,non_op} \/ Constructors is non empty set

MC is non empty pair set

MC `1 is set

MC `2 is set

[(MC `1),(MC `2)] is non empty pair set

{(MC `1),(MC `2)} is non empty finite set

{(MC `1)} is non empty trivial finite 1 -element set

{{(MC `1),(MC `2)},{(MC `1)}} is non empty finite V32() set

F

card F

the Element of F

(card F

d is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

f is set

the set is set

x is set

d is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len d is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

d . 1 is set

dom d is finite Element of bool NAT

d . 0 is set

f is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

d . f is set

f + 1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

d . (f + 1) is set

0 + 1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

proj2 d is finite set

f is set

x is set

d . x is set

f is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

x is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

d . x is set

d . f is set

f + 1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

T is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

(f + 1) + T is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

(f + 1) + 0 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

d . ((f + 1) + 0) is set

p is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

(f + 1) + p is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

d . ((f + 1) + p) is set

p + 1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

(f + 1) + (p + 1) is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

d . ((f + 1) + (p + 1)) is set

((f + 1) + p) + 1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

f + p is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

1 + (f + p) is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

Seg ((card F

{ b

card (Seg ((card F

card (proj2 d) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega

f is set

x is set

d . f is set

d . x is set

T is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

p is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

d . T is set

F

bool F

MC is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

l is finite Element of bool F

card l is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega

d is set

f is finite Element of bool F

card f is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega

card F

[#] F

MC is finite Element of bool F

card MC is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega

F

MC is Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like set

proj2 MC is finite set

dom MC is finite Element of bool NAT

l is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

d is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

MC . l is set

MC . d is set

bool F

MC is finite Element of bool F

l is Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like set

proj2 l is finite set

dom l is finite Element of bool NAT

l is non empty finite set

d is set

f is set

d is set

f is set

x is set

d is set

{d} is non empty trivial finite 1 -element set

MC \ {d} is finite Element of bool F

x is Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like set

proj2 x is finite set

dom x is finite Element of bool NAT

<*d*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

[1,d] is non empty pair set

{1,d} is non empty finite set

{{1,d},{1}} is non empty finite V32() set

{[1,d]} is non empty trivial Relation-like Function-like constant finite 1 -element set

proj2 <*d*> is non empty trivial finite 1 -element set

<*d*> ^ x is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len <*d*> is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

T is Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like set

proj2 T is finite set

dom T is finite Element of bool NAT

(proj2 <*d*>) \/ (proj2 x) is non empty finite set

{d} \/ (MC \ {d}) is non empty finite set

p is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

T . p is set

o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

T . o is set

dom <*d*> is non empty trivial finite 1 -element Element of bool NAT

o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

x . o is set

o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

q is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

1 + q is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

q is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set

1 + q is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set

x . o is set

x . q is set

MC is Element of Vars

vars MC is finite Element of bool Vars

varcl (vars MC) is set

l is Element of bool Vars

varcl l is set

d is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

[(varcl l),d] is non empty pair set

{(varcl l),d} is non empty finite set

{(varcl l)} is non empty trivial finite 1 -element set

{{(varcl l),d},{(varcl l)}} is non empty finite V32() set

MC is non empty non void V68() V146() constructor initialized ManySortedSign

MSVars MC is non empty Relation-like non empty-yielding the carrier of MC -defined Function-like total with_missing_variables set

the carrier of MC is non empty set

Free (MC,(MSVars MC)) is strict non-empty non empty MSAlgebra over MC

the Sorts of (Free (MC,(MSVars MC))) is non empty Relation-like the carrier of MC -defined Function-like total set

Union the Sorts of (Free (MC,(MSVars MC))) is non empty set

l is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching Element of Union the Sorts of (Free (MC,(MSVars MC)))

the carrier' of MC is non empty set

QuasiTerms MC is non empty functional constituted-DTrees Element of bool (Union the Sorts of (Free (MC,(MSVars MC))))

bool (Union the Sorts of (Free (MC,(MSVars MC)))) is non empty set

a_Term MC is Element of the carrier of MC

the Sorts of (Free (MC,(MSVars MC))) . (a_Term MC) is set

an_Adj MC is Element of the carrier of MC

non_op MC is OperSymbol of an_Adj MC

a_Type MC is Element of the carrier of MC

ast MC is OperSymbol of a_Type MC

d is Element of Vars

d -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC

[d,a_Term] is non empty pair set

{d,a_Term} is non empty finite set

{d} is non empty trivial finite 1 -element set

{{d,a_Term},{d}} is non empty finite V32() set

root-tree [d,a_Term] is non empty Relation-like Function-like DecoratedTree-like set

f is Element of Vars

f -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC

[f,a_Term] is non empty pair set

{f,a_Term} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,a_Term},{f}} is non empty finite V32() set

root-tree [f,a_Term] is non empty Relation-like Function-like DecoratedTree-like set

T is Relation-like NAT -defined Union the Sorts of (Free (MC,(MSVars MC))) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of QuasiTerms MC

len T is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

x is constructor Element of the carrier' of MC

the_arity_of x is Relation-like NAT -defined the carrier of MC -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *

the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC

the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]

[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set

bool [: the carrier' of MC,( the carrier of MC *):] is non empty set

K122( the carrier' of MC,( the carrier of MC *), the Arity of MC,x) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *

len (the_arity_of x) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

x -trm T is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching compound Element of Union the Sorts of (Free (MC,(MSVars MC)))

p is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching expression of MC, an_Adj MC

(non_op MC) term p is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching compound Element of Union the Sorts of (Free (MC,(MSVars MC)))

o is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching expression of MC, an_Adj MC

o is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching expression of MC, a_Type MC

(ast MC) term (o,o) is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching compound Element of Union the Sorts of (Free (MC,(MSVars MC)))

MC is non empty non void V68() V146() constructor ManySortedSign

the carrier' of MC is non empty set

l is Element of the carrier' of MC

the carrier' of MaxConstrSign is non empty set

MC is Element of the carrier' of MaxConstrSign

MC `1 is set

the_result_sort_of MC is Element of the carrier of MaxConstrSign

the carrier of MaxConstrSign is non empty set

the ResultSort of MaxConstrSign is Relation-like the carrier' of MaxConstrSign -defined the carrier of MaxConstrSign -valued Function-like V25( the carrier' of MaxConstrSign, the carrier of MaxConstrSign) Element of bool [: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:]

[: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:] is non empty Relation-like set

bool [: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:] is non empty set

K122( the carrier' of MaxConstrSign, the carrier of MaxConstrSign, the ResultSort of MaxConstrSign,MC) is Element of the carrier of MaxConstrSign

MC `2 is set

(MC `2) `1 is set

card ((MC `2) `1) is epsilon-transitive epsilon-connected ordinal cardinal set

the_arity_of MC is Relation-like NAT -defined the carrier of MaxConstrSign -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MaxConstrSign *

the carrier of MaxConstrSign * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MaxConstrSign

the Arity of MaxConstrSign is Relation-like the carrier' of MaxConstrSign -defined the carrier of MaxConstrSign * -valued Function-like V25( the carrier' of MaxConstrSign, the carrier of MaxConstrSign * ) Function-yielding V54() Element of bool [: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):]

[: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):] is non empty Relation-like set

bool [: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):] is non empty set

K122( the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *), the Arity of MaxConstrSign,MC) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MaxConstrSign *

len (the_arity_of MC) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

the ResultSort of MaxConstrSign . MC is set

the Arity of MaxConstrSign . MC is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

card ( the Arity of MaxConstrSign . MC) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega

MC is non empty non void V68() V146() constructor initialized () ManySortedSign

the carrier' of MC is non empty set

l is constructor Element of the carrier' of MC

l `2 is set

(l `2) `1 is set

d is Element of Constructors

loci_of d is Relation-like NAT -defined Vars -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Element of QuasiLoci

d `2 is Element of [:QuasiLoci,NAT:]

(d `2) `1 is Relation-like NAT -defined Vars -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Element of QuasiLoci

MC is non empty non void V68() V146() constructor ManySortedSign

l is V146() Subsignature of MC

MC is non empty non void V68() V146() constructor initialized ManySortedSign

l is non empty non void V68() V146() constructor Subsignature of MC

MC is non empty non void V68() V146() constructor () ManySortedSign

l is non empty non void V68() V146() constructor Subsignature of MC

the carrier' of l is non empty set

d is Element of the carrier' of l

d `1 is set

the_result_sort_of d is Element of the carrier of l

the carrier of l is non empty set

the ResultSort of l is Relation-like the carrier' of l -defined the carrier of l -valued Function-like V25( the carrier' of l, the carrier of l) Element of bool [: the carrier' of l, the carrier of l:]

[: the carrier' of l, the carrier of l:] is non empty Relation-like set

bool [: the carrier' of l, the carrier of l:] is non empty set

K122( the carrier' of l, the carrier of l, the ResultSort of l,d) is Element of the carrier of l

d `2 is set

(d `2) `1 is set

card ((d `2) `1) is epsilon-transitive epsilon-connected ordinal cardinal set

the_arity_of d is Relation-like NAT -defined the carrier of l -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of l *

the carrier of l * is non empty functional FinSequence-membered FinSequenceSet of the carrier of l

the Arity of l is Relation-like the carrier' of l -defined the carrier of l * -valued Function-like V25( the carrier' of l, the carrier of l * ) Function-yielding V54() Element of bool [: the carrier' of l,( the carrier of l *):]

[: the carrier' of l,( the carrier of l *):] is non empty Relation-like set

bool [: the carrier' of l,( the carrier of l *):] is non empty set

K122( the carrier' of l,( the carrier of l *), the Arity of l,d) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of l *

len (the_arity_of d) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

the carrier' of MC is non empty set

f is Element of the carrier' of MC

the carrier of MC is non empty set

the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC

the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]

[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set

bool [: the carrier' of MC,( the carrier of MC *):] is non empty set

the Arity of MC | the carrier' of l is Relation-like the carrier' of l -defined the carrier' of MC -defined the carrier of MC * -valued Function-like Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]

the ResultSort of MC is Relation-like the carrier' of MC -defined the carrier of MC -valued Function-like V25( the carrier' of MC, the carrier of MC) Element of bool [: the carrier' of MC, the carrier of MC:]

[: the carrier' of MC, the carrier of MC:] is non empty Relation-like set

bool [: the carrier' of MC, the carrier of MC:] is non empty set

the ResultSort of MC | the carrier' of l is Relation-like the carrier' of l -defined the carrier' of MC -defined the carrier of MC -valued Function-like Element of bool [: the carrier' of MC, the carrier of MC:]

the_result_sort_of f is Element of the carrier of MC

K122( the carrier' of MC, the carrier of MC, the ResultSort of MC,f) is Element of the carrier of MC

the_arity_of f is Relation-like NAT -defined the carrier of MC -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *

K122( the carrier' of MC,( the carrier of MC *), the Arity of MC,f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *

MC is non empty non void V68() V146() constructor () ManySortedSign

the carrier' of MC is non empty set

l is non empty non void V68() V146() constructor () ManySortedSign

the carrier' of l is non empty set

the carrier of MC is non empty set

the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]

the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC

[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set

bool [: the carrier' of MC,( the carrier of MC *):] is non empty set

the ResultSort of MC is Relation-like the carrier' of MC -defined the carrier of MC -valued Function-like V25( the carrier' of MC, the carrier of MC) Element of bool [: the carrier' of MC, the carrier of MC:]

[: the carrier' of MC, the carrier of MC:] is non empty Relation-like set

bool [: the carrier' of MC, the carrier of MC:] is non empty set

ManySortedSign(# the carrier of MC, the carrier' of MC, the Arity of MC, the ResultSort of MC #) is non empty V68() strict V146() ManySortedSign

the carrier of l is non empty set

the Arity of l is Relation-like the carrier' of l -defined the carrier of l * -valued Function-like V25( the carrier' of l, the carrier of l * ) Function-yielding V54() Element of bool [: the carrier' of l,( the carrier of l *):]

the carrier of l * is non empty functional FinSequence-membered FinSequenceSet of the carrier of l

[: the carrier' of l,( the carrier of l *):] is non empty Relation-like set

bool [: the carrier' of l,( the carrier of l *):] is non empty set

the ResultSort of l is Relation-like the carrier' of l -defined the carrier of l -valued Function-like V25( the carrier' of l, the carrier of l) Element of bool [: the carrier' of l, the carrier of l:]

[: the carrier' of l, the carrier of l:] is non empty Relation-like set

bool [: the carrier' of l, the carrier of l:] is non empty set

ManySortedSign(# the carrier of l, the carrier' of l, the Arity of l, the ResultSort of l #) is non empty V68() strict V146() ManySortedSign

d is Element of the carrier' of MC

the Arity of MC . d is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

the Arity of l . d is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Element of the carrier' of l

d `2 is set

(d `2) `1 is set

card ((d `2) `1) is epsilon-transitive epsilon-connected ordinal cardinal set

the_arity_of d is Relation-like NAT -defined the carrier of MC -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *

K122( the carrier' of MC,( the carrier of MC *), the Arity of MC,d) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *

len (the_arity_of d) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

the_arity_of f is Relation-like NAT -defined the carrier of l -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of l *

K122( the carrier' of l,( the carrier of l *), the Arity of l,f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of l *

len (the_arity_of f) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

(len (the_arity_of d)) |-> a_Term is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(len (the_arity_of f)) |-> a_Term is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

the Arity of MC . d is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

the Arity of l . d is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Element of the carrier' of l

d is Element of the carrier' of MC

the ResultSort of MC . d is set

the ResultSort of l . d is set

f is Element of the carrier' of l

the_result_sort_of d is Element of the carrier of MC

K122( the carrier' of MC, the carrier of MC, the ResultSort of MC,d) is Element of the carrier of MC

d `1 is set

the_result_sort_of f is Element of the carrier of l

K122( the carrier' of l, the carrier of l, the ResultSort of l,f) is Element of the carrier of l

the ResultSort of MC . d is set

the ResultSort of l . d is set

f is Element of the carrier' of l

MC is non empty non void V68() V146() constructor ManySortedSign

the carrier' of MaxConstrSign is non empty set

the Arity of MaxConstrSign is Relation-like the carrier' of MaxConstrSign -defined the carrier of MaxConstrSign * -valued Function-like V25( the carrier' of MaxConstrSign, the carrier of MaxConstrSign * ) Function-yielding V54() Element of bool [: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):]

the carrier of MaxConstrSign is non empty set

the carrier of MaxConstrSign * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MaxConstrSign

[: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):] is non empty Relation-like set

bool [: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):] is non empty set

dom the Arity of MaxConstrSign is Element of bool the carrier' of MaxConstrSign

bool the carrier' of MaxConstrSign is non empty set

the ResultSort of MaxConstrSign is Relation-like the carrier' of MaxConstrSign -defined the carrier of MaxConstrSign -valued Function-like V25( the carrier' of MaxConstrSign, the carrier of MaxConstrSign) Element of bool [: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:]

[: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:] is non empty Relation-like set

bool [: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:] is non empty set

dom the ResultSort of MaxConstrSign is Element of bool the carrier' of MaxConstrSign

the carrier' of MC is non empty set

the carrier of MC is non empty set

the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC

the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]

[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set

bool [: the carrier' of MC,( the carrier of MC *):] is non empty set

l is set

d is set

[l,d] is non empty pair set

{l,d} is non empty finite set

{l} is non empty trivial finite 1 -element set

{{l,d},{l}} is non empty finite V32() set

f is Element of the carrier' of MC

the Arity of MC . f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x is Element of the carrier' of MaxConstrSign

the Arity of MaxConstrSign . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x is Element of the carrier' of MaxConstrSign

f `2 is set

(f `2) `1 is set

card ((f `2) `1) is epsilon-transitive epsilon-connected ordinal cardinal set

the_arity_of f is Relation-like NAT -defined the carrier of MC -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *

K122( the carrier' of MC,( the carrier of MC *), the Arity of MC,f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *

len (the_arity_of f) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

card d is epsilon-transitive epsilon-connected ordinal cardinal set

the Arity of MaxConstrSign . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

card ( the Arity of MaxConstrSign . x) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega

the ResultSort of MC is Relation-like the carrier' of MC -defined the carrier of MC -valued Function-like V25( the carrier' of MC, the carrier of MC) Element of bool [: the carrier' of MC, the carrier of MC:]

[: the carrier' of MC, the carrier of MC:] is non empty Relation-like set

bool [: the carrier' of MC, the carrier of MC:] is non empty set

l is set

d is set

[l,d] is non empty pair set

{l,d} is non empty finite set

{l} is non empty trivial finite 1 -element set

{{l,d},{l}} is non empty finite V32() set

f is Element of the carrier' of MC

the ResultSort of MC . f is set

x is Element of the carrier' of MaxConstrSign

the ResultSort of MaxConstrSign . x is set

x is Element of the carrier' of MaxConstrSign

f `1 is set

the_result_sort_of f is Element of the carrier of MC

K122( the carrier' of MC, the carrier of MC, the ResultSort of MC,f) is Element of the carrier of MC

the_result_sort_of x is Element of the carrier of MaxConstrSign

K122( the carrier' of MaxConstrSign, the carrier of MaxConstrSign, the ResultSort of MaxConstrSign,x) is Element of the carrier of MaxConstrSign

the ResultSort of MaxConstrSign . x is set

x is Element of the carrier' of MaxConstrSign

the carrier' of MC is non empty set

l is Element of the carrier' of MC

l `1 is set

the_result_sort_of l is Element of the carrier of MC

the carrier of MC is non empty set

the ResultSort of MC is Relation-like the carrier' of MC -defined the carrier of MC -valued Function-like V25( the carrier' of MC, the carrier of MC) Element of bool [: the carrier' of MC, the carrier of MC:]

[: the carrier' of MC, the carrier of MC:] is non empty Relation-like set

bool [: the carrier' of MC, the carrier of MC:] is non empty set

K122( the carrier' of MC, the carrier of MC, the ResultSort of MC,l) is Element of the carrier of MC

l `2 is set

(l `2) `1 is set

card ((l `2) `1) is epsilon-transitive epsilon-connected ordinal cardinal set

the_arity_of l is Relation-like NAT -defined the carrier of MC -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *

the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC

the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]

[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set

bool [: the carrier' of MC,( the carrier of MC *):] is non empty set

K122( the carrier' of MC,( the carrier of MC *), the Arity of MC,l) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *

len (the_arity_of l) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

d is Element of the carrier' of MaxConstrSign

the ResultSort of MaxConstrSign . d is set

the ResultSort of MaxConstrSign | the carrier' of MC is Relation-like the carrier' of MaxConstrSign -defined the carrier' of MC -defined the carrier' of MaxConstrSign -defined the carrier of MaxConstrSign -valued Function-like Element of bool [: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:]

( the ResultSort of MaxConstrSign | the carrier' of MC) . l is set

the ResultSort of MC . l is set

the Arity of MaxConstrSign . d is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

card ( the Arity of MaxConstrSign . d) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega

the Arity of MaxConstrSign | the carrier' of MC is Relation-like the carrier' of MaxConstrSign -defined the carrier' of MC -defined the carrier' of MaxConstrSign -defined the carrier of MaxConstrSign * -valued Function-like Function-yielding V54() Element of bool [: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):]

( the Arity of MaxConstrSign | the carrier' of MC) . l is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

card (( the Arity of MaxConstrSign | the carrier' of MC) . l) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega

the Arity of MC . l is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

card ( the Arity of MC . l) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega

MC is non empty non void V68() V146() constructor initialized ManySortedSign

a_Term MC is Element of the carrier of MC

the carrier of MC is non empty set

MSVars MC is non empty Relation-like non empty-yielding the carrier of MC -defined Function-like total with_missing_variables set

the Element of Vars is Element of Vars

the Element of Vars -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC

[ the Element of Vars ,a_Term] is non empty pair set

{ the Element of Vars ,a_Term} is non empty finite set

{ the Element of Vars } is non empty trivial finite 1 -element set

{{ the Element of Vars ,a_Term},{ the Element of Vars }} is non empty finite V32() set

root-tree [ the Element of Vars ,a_Term] is non empty Relation-like Function-like DecoratedTree-like set

MC is Element of Vars

l is Element of bool Vars

varcl l is set

d is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

[(varcl l),d] is non empty pair set

{(varcl l),d} is non empty finite set

{(varcl l)} is non empty trivial finite 1 -element set

{{(varcl l),d},{(varcl l)}} is non empty finite V32() set

MC is non empty pair Element of Vars

vars MC is finite Element of bool Vars

MC `1 is finite set

d is Element of bool Vars

varcl d is set

f is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

[(varcl d),f] is non empty pair set

{(varcl d),f} is non empty finite set

{(varcl d)} is non empty trivial finite 1 -element set

{{(varcl d),f},{(varcl d)}} is non empty finite V32() set

l is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

the epsilon-transitive epsilon-connected ordinal Element of l is epsilon-transitive epsilon-connected ordinal Element of l

T is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

MC is set

l is non empty pair Element of Vars

d is Element of bool Vars

varcl d is set

f is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT

[(varcl d),f] is non empty pair set

{(varcl d),f} is non empty finite set

{(varcl d)} is non empty trivial finite 1 -element set

{{(varcl d),f},{(varcl d)}} is non empty finite V32() set

l `2 is set

x is set

T is set

[x,T] is non empty pair set

{x,T} is non empty finite set

{x} is non empty trivial finite 1 -element set

{{x,T},{x}} is non empty finite V32() set

MC is non empty pair Element of Vars

l is non empty pair Element of Vars

MC is non empty non void V68() V146() constructor () ManySortedSign

the carrier' of MC is non empty set

l is set

d is non empty pair Element of Vars

f is Element of the carrier' of MC

MC is non empty non void V68() V146() constructor initialized () ManySortedSign

MSVars MC is non empty Relation-like non empty-yielding the carrier of MC -defined Function-like total with_missing_variables set

the carrier of MC is non empty set

Free (MC,(MSVars MC)) is strict non-empty non empty MSAlgebra over MC

the Sorts of (Free (MC,(MSVars MC))) is non empty Relation-like the carrier of MC -defined Function-like total set

Union the Sorts of (Free (MC,(MSVars MC))) is non empty set

the carrier' of MC is non empty set

l is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching Element of Union the Sorts of (Free (MC,(MSVars MC)))

l . {} is set

the carrier of MC --> {0} is non empty Relation-like non-empty non empty-yielding the carrier of MC -defined the carrier of MC -defined bool NAT -valued Function-like constant total total V25( the carrier of MC, bool NAT) with_missing_variables Element of bool [: the carrier of MC,(bool NAT):]

[: the carrier of MC,(bool NAT):] is non empty non trivial Relation-like non finite set

bool [: the carrier of MC,(bool NAT):] is non empty non trivial non finite set

(MSVars MC) \/ ( the carrier of MC --> {0}) is non empty Relation-like non-empty non empty-yielding the carrier of MC -defined the carrier of MC -defined Function-like total total with_missing_variables set

DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})) is L15()

{ the carrier of MC} is non empty trivial finite 1 -element set

[: the carrier' of MC,{ the carrier of MC}:] is non empty Relation-like set

coprod ((MSVars MC) \/ ( the carrier of MC --> {0})) is Relation-like Function-like set

Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))) is Relation-like set

[: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0})))) is non empty Relation-like set

REL ((MSVars MC) \/ ( the carrier of MC --> {0})) is Relation-like [: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0})))) -defined ([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) * -valued Element of bool [:([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) *):]

([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) * is non empty functional FinSequence-membered FinSequenceSet of [: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))

[:([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) *):] is non empty Relation-like set

bool [:([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) *):] is non empty set

G15(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(REL ((MSVars MC) \/ ( the carrier of MC --> {0})))) is V137() L15()

the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) is set

FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))

MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0})) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))))

bool (FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))) is non empty set

x is non empty Relation-like the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) -valued Function-like finite DecoratedTree-like M31( the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))), FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))),MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0})))

x . {} is set

T is Element of the carrier of MC

((MSVars MC) \/ ( the carrier of MC --> {0})) . T is non empty set

p is Element of ((MSVars MC) \/ ( the carrier of MC --> {0})) . T

[p,T] is non empty pair Element of [:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:]

[:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:] is non empty Relation-like set

{p,T} is non empty finite set

{p} is non empty trivial finite 1 -element set

{{p,T},{p}} is non empty finite V32() set

T is Element of the carrier of MC

((MSVars MC) \/ ( the carrier of MC --> {0})) . T is non empty set

p is Element of ((MSVars MC) \/ ( the carrier of MC --> {0})) . T

[p,T] is non empty pair Element of [:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:]

[:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:] is non empty Relation-like set

{p,T} is non empty finite set

{p} is non empty trivial finite 1 -element set

{{p,T},{p}} is non empty finite V32() set

dom the Sorts of (Free (MC,(MSVars MC))) is non empty Element of bool the carrier of MC

bool the carrier of MC is non empty set

o is set

the Sorts of (Free (MC,(MSVars MC))) . o is set

o is Element of the carrier of MC

root-tree [p,T] is non empty Relation-like [:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:] -valued Function-like DecoratedTree-like Element of FinTrees [:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:]

FinTrees [:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:] is non empty functional constituted-DTrees DTree-set of [:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:]

the_sort_of x is Element of the carrier of MC

MC -Terms ((MSVars MC),((MSVars MC) \/ ( the carrier of MC --> {0}))) is non empty Relation-like the carrier of MC -defined Function-like total ManySortedSubset of the Sorts of (FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))

FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0})) is MSAlgebra over MC

FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0})) is non empty Relation-like the carrier of MC -defined Function-like total set

FreeOper ((MSVars MC) \/ ( the carrier of MC --> {0})) is non empty Relation-like the carrier' of MC -defined Function-like total ManySortedFunction of the Arity of MC * ((FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) #), the ResultSort of MC * (FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0})))

the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]

the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC

[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set

bool [: the carrier' of MC,( the carrier of MC *):] is non empty set

(FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) # is non empty Relation-like the carrier of MC * -defined Function-like total set

the Arity of MC * ((FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) #) is Relation-like the carrier' of MC -defined Function-like set

the ResultSort of MC is Relation-like the carrier' of MC -defined the carrier of MC -valued Function-like V25( the carrier' of MC, the carrier of MC) Element of bool [: the carrier' of MC, the carrier of MC:]

[: the carrier' of MC, the carrier of MC:] is non empty Relation-like set

bool [: the carrier' of MC, the carrier of MC:] is non empty set

the ResultSort of MC * (FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) is Relation-like the carrier' of MC -defined Function-like set

MSAlgebra(# (FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))),(FreeOper ((MSVars MC) \/ ( the carrier of MC --> {0}))) #) is strict MSAlgebra over MC

the Sorts of (FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) is non empty Relation-like the carrier of MC -defined Function-like total set

the Sorts of (Free (MC,(MSVars MC))) . o is set

the Sorts of (FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) . o is set

FreeSort (((MSVars MC) \/ ( the carrier of MC --> {0})),o) is functional constituted-DTrees Element of bool K421((DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))))

K421((DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))))

bool K421((DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))) is non empty set

((MSVars MC) \/ ( the carrier of MC --> {0})) . o is non empty set

{ b

( b

( [b

(MSVars MC) . o is set

q is non empty pair Element of Vars

q -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC

a_Term MC is Element of the carrier of MC

[q,a_Term] is non empty pair set

{q,a_Term} is non empty finite set

{q} is non empty trivial Relation-like finite 1 -element set

{{q,a_Term},{q}} is non empty finite V32() set

root-tree [q,a_Term] is non empty Relation-like Function-like DecoratedTree-like set

x is non empty Relation-like the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) -valued Function-like finite DecoratedTree-like M31( the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))), FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))),MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0})))

x . {} is set

T is set

p is set

[T,p] is non empty pair set

{T,p} is non empty finite set

{T} is non empty trivial finite 1 -element set

{{T,p},{T}} is non empty finite V32() set

o is Element of the carrier' of MC

x is non empty Relation-like the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) -valued Function-like finite DecoratedTree-like M31( the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))), FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))),MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0})))

x . {} is set

MC is non empty non void V68() V146() constructor initialized () ManySortedSign

MSVars MC is non empty Relation-like non empty-yielding the carrier of MC -defined Function-like total with_missing_variables set

the carrier of MC is non empty set

Free (MC,(MSVars MC)) is strict non-empty non empty MSAlgebra over MC

the Sorts of (Free (MC,(MSVars MC))) is non empty Relation-like the carrier of MC -defined Function-like total set

Union the Sorts of (Free (MC,(MSVars MC))) is non empty set

l is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching Element of Union the Sorts of (Free (MC,(MSVars MC)))

l . {} is set

the carrier' of MC is non empty set

d is non empty pair Element of Vars

d -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC

a_Term MC is Element of the carrier of MC

[d,a_Term] is non empty pair set

{d,a_Term} is non empty finite set

{d} is non empty trivial Relation-like finite 1 -element set

{{d,a_Term},{d}} is non empty finite V32() set

root-tree [d,a_Term] is non empty Relation-like Function-like DecoratedTree-like set

f is Element of the carrier' of MC

[f, the carrier of MC] is non empty pair set

{f, the carrier of MC} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f, the carrier of MC},{f}} is non empty finite V32() set

MC is non empty non void V68() V146() constructor initialized ManySortedSign

MSVars MC is non empty Relation-like non empty-yielding the carrier of MC -defined Function-like total with_missing_variables set

the carrier of MC is non empty set

Free (MC,(MSVars MC)) is strict non-empty non empty MSAlgebra over MC

the Sorts of (Free (MC,(MSVars MC))) is non empty Relation-like the carrier of MC -defined Function-like total set

Union the Sorts of (Free (MC,(MSVars MC))) is non empty set

the carrier' of MC is non empty set

l is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching Element of Union the Sorts of (Free (MC,(MSVars MC)))

l . {} is set

d is Element of the carrier' of MC

[d, the carrier of MC] is non empty pair set

{d, the carrier of MC} is non empty finite set

{d} is non empty trivial finite 1 -element set

{{d, the carrier of MC},{d}} is non empty finite V32() set

the_result_sort_of d is Element of the carrier of MC

the ResultSort of MC is Relation-like the carrier' of MC -defined the carrier of MC -valued Function-like V25( the carrier' of MC, the carrier of MC) Element of bool [: the carrier' of MC, the carrier of MC:]

[: the carrier' of MC, the carrier of MC:] is non empty Relation-like set

bool [: the carrier' of MC, the carrier of MC:] is non empty set

K122( the carrier' of MC, the carrier of MC, the ResultSort of MC,d) is Element of the carrier of MC

the carrier of MC --> {0} is non empty Relation-like non-empty non empty-yielding the carrier of MC -defined the carrier of MC -defined bool NAT -valued Function-like constant total total V25( the carrier of MC, bool NAT) with_missing_variables Element of bool [: the carrier of MC,(bool NAT):]

[: the carrier of MC,(bool NAT):] is non empty non trivial Relation-like non finite set

bool [: the carrier of MC,(bool NAT):] is non empty non trivial non finite set

(MSVars MC) \/ ( the carrier of MC --> {0}) is non empty Relation-like non-empty non empty-yielding the carrier of MC -defined the carrier of MC -defined Function-like total total with_missing_variables set

DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})) is L15()

{ the carrier of MC} is non empty trivial finite 1 -element set

[: the carrier' of MC,{ the carrier of MC}:] is non empty Relation-like set

coprod ((MSVars MC) \/ ( the carrier of MC --> {0})) is Relation-like Function-like set

Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))) is Relation-like set

[: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0})))) is non empty Relation-like set

REL ((MSVars MC) \/ ( the carrier of MC --> {0})) is Relation-like [: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0})))) -defined ([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) * -valued Element of bool [:([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) *):]

([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) * is non empty functional FinSequence-membered FinSequenceSet of [: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))

[:([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) *):] is non empty Relation-like set

bool [:([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) *):] is non empty set

G15(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(REL ((MSVars MC) \/ ( the carrier of MC --> {0})))) is V137() L15()

the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) is set

FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))

MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0})) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))))

bool (FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))) is non empty set

T is non empty Relation-like the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) -valued Function-like finite DecoratedTree-like M31( the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))), FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))),MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0})))

variables_in T is non empty Relation-like the carrier of MC -defined Function-like total ManySortedSubset of (MSVars MC) \/ ( the carrier of MC --> {0})

MC variables_in T is non empty Relation-like the carrier of MC -defined Function-like total set

the_sort_of T is Element of the carrier of MC

{ b

MC -Terms ((MSVars MC),((MSVars MC) \/ ( the carrier of MC --> {0}))) is non empty Relation-like the carrier of MC -defined Function-like total ManySortedSubset of the Sorts of (FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))

FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0})) is MSAlgebra over MC

FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0})) is non empty Relation-like the carrier of MC -defined Function-like total set

FreeOper ((MSVars MC) \/ ( the carrier of MC --> {0})) is non empty Relation-like the carrier' of MC -defined Function-like total ManySortedFunction of the Arity of MC * ((FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) #), the ResultSort of MC * (FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0})))

the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]

the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC

[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set

bool [: the carrier' of MC,( the carrier of MC *):] is non empty set

(FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) # is non empty Relation-like the carrier of MC * -defined Function-like total set

the Arity of MC * ((FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) #) is Relation-like the carrier' of MC -defined Function-like set

the ResultSort of MC * (FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) is Relation-like the carrier' of MC -defined Function-like set

MSAlgebra(# (FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))),(FreeOper ((MSVars MC) \/ ( the carrier of MC --> {0}))) #) is strict MSAlgebra over MC

the Sorts of (FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) is non empty Relation-like the carrier of MC -defined Function-like total set

(MC -Terms ((MSVars MC),((MSVars MC) \/ ( the carrier of MC --> {0})))) . (the_sort_of T) is set

the Sorts of (Free (MC,(MSVars MC))) . (the_sort_of T) is set

MC is non empty non void V68() V146() constructor initialized () ManySortedSign

MSVars MC is non empty Relation-like non empty-yielding the carrier of MC -defined Function-like total with_missing_variables set

the carrier of MC is non empty set

Free (MC,(MSVars MC)) is strict non-empty non empty MSAlgebra over MC

the Sorts of (Free (MC,(MSVars MC))) is non empty Relation-like the carrier of MC -defined Function-like total set

Union the Sorts of (Free (MC,(MSVars MC))) is non empty set

a_Type MC is Element of the carrier of MC

an_Adj MC is Element of the carrier of MC

l is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching Element of Union the Sorts of (Free (MC,(MSVars MC)))

l . {} is non empty pair set

(l . {}) `1 is set

d is non empty pair Element of Vars

d -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC

a_Term MC is Element of the carrier of MC

[d,a_Term] is non empty pair set

{d,a_Term} is non empty finite set

{d} is non empty trivial Relation-like finite 1 -element set

{{d,a_Term},{d}} is non empty finite V32() set

root-tree [d,a_Term] is non empty Relation-like Function-like DecoratedTree-like set

d is non empty pair Element of Vars

d -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC

a_Term MC is Element of the carrier of MC

[d,a_Term] is non empty