:: ABCMIZ_1 semantic presentation

REAL is V315() V316() V317() V321() V324() V325() V327() set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V315() V316() V317() V318() V319() V320() V321() V322() V324() 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 V315() V316() V317() V318() V319() V320() V321() V322() V324() set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

1 is non pair non empty epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real positive V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() V328() V329() Element of NAT

2 is non pair non empty epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real positive V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() V328() V329() Element of NAT

[:NAT,REAL:] is Relation-like set

bool [:NAT,REAL:] is non empty set

bool (bool REAL) is non empty set

{} is non pair empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V100() V103() V106() Function-yielding V115() ext-real constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding non with_pair V315() V316() V317() V318() V319() V320() V321() V324() V325() V326() V327() V328() set

the non pair empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V100() V103() V106() Function-yielding V115() ext-real constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding non with_pair V315() V316() V317() V318() V319() V320() V321() V324() V325() V326() V327() V328() set is non pair empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V100() V103() V106() Function-yielding V115() ext-real constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding non with_pair V315() V316() V317() V318() V319() V320() V321() V324() V325() V326() V327() V328() set

{{},1} is non empty finite V38() non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

Trees is non empty constituted-Trees set

bool Trees is non empty set

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

PeanoNat is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of PeanoNat is non empty set

FinTrees the carrier of PeanoNat is non empty functional constituted-DTrees DTree-set of the carrier of PeanoNat

TS PeanoNat is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of PeanoNat)

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

[:(TS PeanoNat),NAT:] is non empty non trivial Relation-like non finite set

bool [:(TS PeanoNat),NAT:] is non empty non trivial non finite set

[:NAT,(TS PeanoNat):] is non empty non trivial Relation-like non finite set

bool [:NAT,(TS PeanoNat):] is non empty non trivial non finite set

K635() is set

2 -tuples_on K635() is functional FinSequence-membered FinSequenceSet of K635()

K635() * is non empty functional FinSequence-membered FinSequenceSet of K635()

{ b

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

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

3 is non pair non empty epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real positive V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() V328() V329() Element of NAT

3 -tuples_on K635() is functional FinSequence-membered FinSequenceSet of K635()

{ b

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

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

K664() is Relation-like 2 -tuples_on K635() -defined K635() -valued Function-like quasi_total Element of bool [:(2 -tuples_on K635()),K635():]

COMPLEX is V315() V321() set

RAT is V315() V316() V317() V318() V321() set

INT is V315() V316() V317() V318() V319() V321() set

0 is non pair empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V100() V103() V106() Function-yielding V115() ext-real constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding non with_pair V315() V316() V317() V318() V319() V320() V321() V324() V325() V326() V327() V328() V329() Element of NAT

<*> NAT is non pair empty proper Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V100() V103() V106() Function-yielding V115() ext-real constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding non with_pair V315() V316() V317() V318() V319() V320() V321() V324() V325() V326() V327() V328() FinSequence of NAT

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

union {} is non pair epsilon-transitive epsilon-connected ordinal natural V32() finite cardinal ext-real V328() set

Seg 1 is non empty trivial finite 1 -element V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() Element of bool NAT

{ b

{1} is non empty trivial finite V38() 1 -element non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

Seg 2 is non empty finite 2 -element V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() Element of bool NAT

{ b

{1,2} is non empty finite V38() non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

Rank {} is epsilon-transitive set

K469(0) is non empty V239() set

{0} is non empty trivial functional finite V38() 1 -element non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() Element of bool NAT

C is set

T is Relation-like Function-like set

T . C is set

Union T is set

proj2 T is set

union (proj2 T) is set

proj1 T is set

T is Relation-like Function-like set

Union T is set

proj2 T is set

union (proj2 T) is set

C is set

T . C is set

C is Relation-like Function-like set

T is set

f1 is set

[T,f1] is pair non empty set

{T,f1} is non empty finite set

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

{{T,f1},{T}} is non empty finite V38() set

f2 is set

x is set

[f2,x] is pair non empty set

{f2,x} is non empty finite set

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

{{f2,x},{f2}} is non empty finite V38() set

a is set

b is set

[a,b] is pair non empty set

{a,b} is non empty finite set

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

{{a,b},{a}} is non empty finite V38() set

C is set

id C is Relation-like C -defined C -valued Function-like one-to-one total V99() V101() V102() V106() V350() Element of bool [:C,C:]

[:C,C:] is Relation-like set

bool [:C,C:] is non empty set

T is set

(id C) .: T is Element of bool C

bool C is non empty set

f1 is set

f2 is set

[f2,f1] is pair non empty set

{f2,f1} is non empty finite set

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

{{f2,f1},{f2}} is non empty finite V38() set

C is non empty non void V58() V259() ManySortedSign

the carrier of C is non empty set

T is non empty Relation-like non-empty non empty-yielding the carrier of C -defined Function-like total set

DTConMSA T is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier' of C is non empty set

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

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

coprod T is non empty Relation-like non-empty non empty-yielding the carrier of C -defined Function-like total set

Union (coprod T) is non empty set

proj2 (coprod T) is non empty with_non-empty_elements set

union (proj2 (coprod T)) is set

[: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod T)) is non empty set

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

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

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

bool [:([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod T))),(([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod T))) *):] is non empty set

DTConstrStr(# ([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod T))),(REL T) #) is non empty strict DTConstrStr

the carrier of (DTConMSA T) is non empty set

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

C -Terms T is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA T))

bool (FinTrees the carrier of (DTConMSA T)) is non empty set

f1 is non empty Relation-like the carrier of (DTConMSA T) -valued Function-like finite DecoratedTree-like Element of C -Terms T

f2 is set

x is set

[f2,x] is pair non empty set

{f2,x} is non empty finite set

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

{{f2,x},{f2}} is non empty finite V38() set

f1 . {} is set

a is Element of the carrier of C

T . a is non empty set

b is Element of T . a

[b,a] is pair non empty Element of [:(T . a), the carrier of C:]

[:(T . a), the carrier of C:] is non empty Relation-like set

{b,a} is non empty finite set

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

{{b,a},{b}} is non empty finite V38() set

{{}} is non empty trivial functional finite V38() 1 -element non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{},(f1 . {})} is non empty finite set

a is Element of the carrier of C

T . a is non empty set

b is Element of T . a

[b,a] is pair non empty Element of [:(T . a), the carrier of C:]

[:(T . a), the carrier of C:] is non empty Relation-like set

{b,a} is non empty finite set

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

{{b,a},{b}} is non empty finite V38() set

i is set

pi1 is set

[i,pi1] is pair non empty set

{i,pi1} is non empty finite set

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

{{i,pi1},{i}} is non empty finite V38() set

[{},(f1 . {})] is pair non empty set

{{{},(f1 . {})},{{}}} is non empty finite V38() set

proj1 f1 is non empty finite V239() set

C is non empty non void V58() V259() ManySortedSign

the carrier of C is non empty set

T is non empty Relation-like non empty-yielding the carrier of C -defined Function-like total set

Free (C,T) is strict non empty MSAlgebra over C

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

Union the Sorts of (Free (C,T)) is non empty set

proj2 the Sorts of (Free (C,T)) is non empty set

union (proj2 the Sorts of (Free (C,T))) is set

f1 is non empty Relation-like Function-like finite DecoratedTree-like Element of Union the Sorts of (Free (C,T))

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

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

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

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

DTConMSA (T \/ ( the carrier of C --> {0})) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier' of C is non empty set

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

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

coprod (T \/ ( the carrier of C --> {0})) is non empty Relation-like non-empty non empty-yielding the carrier of C -defined Function-like total set

Union (coprod (T \/ ( the carrier of C --> {0}))) is non empty set

proj2 (coprod (T \/ ( the carrier of C --> {0}))) is non empty with_non-empty_elements set

union (proj2 (coprod (T \/ ( the carrier of C --> {0})))) is set

[: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> {0})))) is non empty set

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

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

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

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

DTConstrStr(# ([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> {0}))))),(REL (T \/ ( the carrier of C --> {0}))) #) is non empty strict DTConstrStr

the carrier of (DTConMSA (T \/ ( the carrier of C --> {0}))) is non empty set

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

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

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

C is set

f1 is set

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

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

T is set

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

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

f2 is Relation-like NAT -defined {f1} -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of {f1}

dom f2 is finite V315() V316() V317() V318() V319() V320() V324() V325() V326() Element of bool NAT

len f2 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

Seg (len f2) is finite len f2 -element V315() V316() V317() V318() V319() V320() V324() V325() V326() Element of bool NAT

{ b

x is Relation-like NAT -defined {f1} -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of {f1}

dom x is finite V315() V316() V317() V318() V319() V320() V324() V325() V326() Element of bool NAT

a is non pair epsilon-transitive epsilon-connected ordinal natural V32() finite cardinal ext-real V328() set

f2 . a is set

rng f2 is trivial finite Element of bool {f1}

bool {f1} is non empty finite V38() set

x . a is set

rng x is trivial finite Element of bool {f1}

C is non empty non void V58() V259() ManySortedSign

C is non empty non void V58() V259() ManySortedSign

the carrier of C is non empty set

T is non empty Relation-like non empty-yielding the carrier of C -defined Function-like total set

Free (C,T) is strict non empty MSAlgebra over C

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

Union the Sorts of (Free (C,T)) is non empty set

proj2 the Sorts of (Free (C,T)) is non empty set

union (proj2 the Sorts of (Free (C,T))) is set

f1 is Relation-like NAT -defined Union the Sorts of (Free (C,T)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Union the Sorts of (Free (C,T))

f2 is set

proj2 f1 is finite set

rng f1 is finite Element of bool (Union the Sorts of (Free (C,T)))

bool (Union the Sorts of (Free (C,T))) is non empty set

C is non empty non void V58() V259() ManySortedSign

the carrier of C is non empty set

the carrier' of C is non empty set

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

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

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

T is non empty Relation-like non empty-yielding the carrier of C -defined Function-like total set

Free (C,T) is strict non empty MSAlgebra over C

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

Union the Sorts of (Free (C,T)) is non empty set

proj2 the Sorts of (Free (C,T)) is non empty set

union (proj2 the Sorts of (Free (C,T))) is set

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

DTConMSA (T \/ ( the carrier of C --> {0})) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

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

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

coprod (T \/ ( the carrier of C --> {0})) is non empty Relation-like non-empty non empty-yielding the carrier of C -defined Function-like total set

Union (coprod (T \/ ( the carrier of C --> {0}))) is non empty set

proj2 (coprod (T \/ ( the carrier of C --> {0}))) is non empty with_non-empty_elements set

union (proj2 (coprod (T \/ ( the carrier of C --> {0})))) is set

[: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> {0})))) is non empty set

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

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

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

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

DTConstrStr(# ([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> {0}))))),(REL (T \/ ( the carrier of C --> {0}))) #) is non empty strict DTConstrStr

the carrier of (DTConMSA (T \/ ( the carrier of C --> {0}))) is non empty set

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

f1 is non pair non empty Relation-like Function-like finite DecoratedTree-like Element of Union the Sorts of (Free (C,T))

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

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

a is Element of the carrier of C

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

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

b is Element of (T \/ ( the carrier of C --> {0})) . a

[b,a] is pair non empty Element of [:((T \/ ( the carrier of C --> {0})) . a), the carrier of C:]

{b,a} is non empty finite set

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

{{b,a},{b}} is non empty finite V38() set

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

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

proj1 (root-tree [b,a]) is non empty finite V239() set

(root-tree [b,a]) . {} is set

rng (root-tree [b,a]) is non empty Relation-like (T \/ ( the carrier of C --> {0})) . a -defined the carrier of C -valued Element of bool [:((T \/ ( the carrier of C --> {0})) . a), the carrier of C:]

bool [:((T \/ ( the carrier of C --> {0})) . a), the carrier of C:] is non empty set

T . a is set

a is Element of the carrier' of C

Sym (a,(T \/ ( the carrier of C --> {0}))) is Element of NonTerminals (DTConMSA (T \/ ( the carrier of C --> {0})))

NonTerminals (DTConMSA (T \/ ( the carrier of C --> {0}))) is non empty Element of bool the carrier of (DTConMSA (T \/ ( the carrier of C --> {0})))

bool the carrier of (DTConMSA (T \/ ( the carrier of C --> {0}))) is non empty set

{ b

[a, the carrier of C] is pair non empty set

{a, the carrier of C} is non empty finite set

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

{{a, the carrier of C},{a}} is non empty finite V38() set

b is Relation-like NAT -defined FinTrees the carrier of (DTConMSA (T \/ ( the carrier of C --> {0}))) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V115() DTree-yielding ArgumentSeq of Sym (a,(T \/ ( the carrier of C --> {0})))

rng b is functional finite constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA (T \/ ( the carrier of C --> {0}))))

[a, the carrier of C] -tree b is non empty Relation-like Function-like DecoratedTree-like set

dom the Sorts of (Free (C,T)) is non empty Element of bool the carrier of C

bool the carrier of C is non empty set

pi1 is set

the Sorts of (Free (C,T)) . pi1 is set

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

FreeMSA (T \/ ( the carrier of C --> {0})) is strict non-empty V172(C) MSAlgebra over C

FreeSort (T \/ ( the carrier of C --> {0})) is non empty Relation-like non-empty non empty-yielding the carrier of C -defined Function-like total V159() set

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

the Arity of C is Relation-like the carrier' of C -defined the carrier of C * -valued Function-like quasi_total Function-yielding V115() Element of bool [: the carrier' of C,( the carrier of C *):]

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

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

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

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

the Arity of C * ((FreeSort (T \/ ( the carrier of C --> {0}))) #) is Relation-like non-empty the carrier' of C -defined Function-like set

the ResultSort of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

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

the ResultSort of C * (FreeSort (T \/ ( the carrier of C --> {0}))) is Relation-like non-empty the carrier' of C -defined Function-like set

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

the Sorts of (FreeMSA (T \/ ( the carrier of C --> {0}))) is non empty Relation-like non-empty non empty-yielding the carrier of C -defined Function-like total V159() set

(Sym (a,(T \/ ( the carrier of C --> {0})))) -tree b is non empty Relation-like the carrier of (DTConMSA (T \/ ( the carrier of C --> {0}))) -valued Function-like finite DecoratedTree-like Element of C -Terms (T \/ ( the carrier of C --> {0}))

the_sort_of ((Sym (a,(T \/ ( the carrier of C --> {0})))) -tree b) is Element of the carrier of C

the_result_sort_of a is Element of the carrier of C

the ResultSort of C . a is Element of the carrier of C

z is Element of the carrier of C

Union (C -Terms (T,(T \/ ( the carrier of C --> {0})))) is set

proj2 (C -Terms (T,(T \/ ( the carrier of C --> {0})))) is non empty set

union (proj2 (C -Terms (T,(T \/ ( the carrier of C --> {0}))))) is set

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

the Arity of C . a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of C *

len (the_arity_of a) is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

len b is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

x is non empty Relation-like the carrier of (DTConMSA (T \/ ( the carrier of C --> {0}))) -valued Function-like finite DecoratedTree-like Element of C -Terms (T \/ ( the carrier of C --> {0}))

b is set

a is Element of the carrier of C

[b,a] is pair non empty set

{b,a} is non empty finite set

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

{{b,a},{b}} is non empty finite V38() set

root-tree [b,a] is non empty Relation-like Function-like DecoratedTree-like set

T . a is set

i is Element of the carrier' of C

[i, the carrier of C] is pair non empty set

{i, the carrier of C} is non empty finite set

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

{{i, the carrier of C},{i}} is non empty finite V38() set

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

[i, the carrier of C] -tree pi1 is non empty Relation-like Function-like DecoratedTree-like set

len pi1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

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

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

the Arity of C is Relation-like the carrier' of C -defined the carrier of C * -valued Function-like quasi_total Function-yielding V115() Element of bool [: the carrier' of C,( the carrier of C *):]

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

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

the Arity of C . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of C *

len (the_arity_of i) is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

Sym (i,(T \/ ( the carrier of C --> {0}))) is Element of NonTerminals (DTConMSA (T \/ ( the carrier of C --> {0})))

NonTerminals (DTConMSA (T \/ ( the carrier of C --> {0}))) is non empty Element of bool the carrier of (DTConMSA (T \/ ( the carrier of C --> {0})))

bool the carrier of (DTConMSA (T \/ ( the carrier of C --> {0}))) is non empty set

{ b

C is set

T is set

f1 is set

the_rank_of C is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of C) is epsilon-transitive set

bool (Rank (the_rank_of C)) is non empty set

{ b

( not [b

meet { b

( not [b

f1 is set

f2 is set

x is set

[f2,x] is pair non empty set

{f2,x} is non empty finite set

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

{{f2,x},{f2}} is non empty finite V38() set

f2 is set

x is set

a is Element of bool (Rank (the_rank_of C))

f2 is set

x is set

[f2,x] is pair non empty set

{f2,x} is non empty finite set

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

{{f2,x},{f2}} is non empty finite V38() set

a is set

b is set

i is Element of bool (Rank (the_rank_of C))

f2 is set

f2 /\ (Rank (the_rank_of C)) is set

a is Element of bool (Rank (the_rank_of C))

b is set

i is set

[b,i] is pair non empty set

{b,i} is non empty finite set

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

{{b,i},{b}} is non empty finite V38() set

f1 is set

T is set

f2 is set

x is set

[f2,x] is pair non empty set

{f2,x} is non empty finite set

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

{{f2,x},{f2}} is non empty finite V38() set

a is set

({}) is set

C is set

T is set

[C,T] is pair non empty set

{C,T} is non empty finite set

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

{{C,T},{C}} is non empty finite V38() set

C is set

C is set

T is set

(C) is set

(T) is set

f1 is set

f2 is set

[f1,f2] is pair non empty set

{f1,f2} is non empty finite set

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

{{f1,f2},{f1}} is non empty finite V38() set

C is set

union C is set

((union C)) is set

{ (b

union { (b

f1 is set

f2 is set

x is Element of C

(x) is set

f1 is set

f2 is set

[f1,f2] is pair non empty set

{f1,f2} is non empty finite set

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

{{f1,f2},{f1}} is non empty finite V38() set

x is set

a is Element of C

(a) is set

f1 is set

f2 is set

x is Element of C

(x) is set

F

{ F

union { F

((union { F

{ (F

union { (F

f1 is set

f2 is set

(f2) is set

x is Element of F

F

f1 is set

f2 is set

[f1,f2] is pair non empty set

{f1,f2} is non empty finite set

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

{{f1,f2},{f1}} is non empty finite V38() set

x is set

a is Element of F

F

(F

f1 is set

f2 is set

x is Element of F

F

(F

C is set

(C) is set

T is set

C \/ T is set

((C \/ T)) is set

(T) is set

(C) \/ (T) is set

{C,T} is non empty finite set

{ (b

union {C,T} is set

union { (b

{(C),(T)} is non empty finite set

f2 is set

x is Element of {C,T}

(x) is set

f2 is set

C is non empty set

meet C is set

((meet C)) is set

f1 is set

f2 is set

[f1,f2] is pair non empty set

{f1,f2} is non empty finite set

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

{{f1,f2},{f1}} is non empty finite V38() set

x is set

(x) is set

C is set

(C) is set

T is set

(T) is set

(C) /\ (T) is set

(((C) /\ (T))) is set

f2 is set

x is set

[f2,x] is pair non empty set

{f2,x} is non empty finite set

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

{{f2,x},{f2}} is non empty finite V38() set

C is non pair empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V100() V103() V106() Function-yielding V115() ext-real constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding non with_pair V315() V316() V317() V318() V319() V320() V321() V324() V325() V326() V327() V328() set

(C) is set

{ [(b

{ [{},b

C is Relation-like Function-like set

proj1 C is set

C . 0 is set

T is non empty Relation-like NAT -defined Function-like total set

Union T is set

proj2 T is non empty set

union (proj2 T) is set

f1 is non empty Relation-like NAT -defined Function-like total set

Union f1 is set

proj2 f1 is non empty set

union (proj2 f1) is set

f1 . 0 is set

f2 is non pair epsilon-transitive epsilon-connected ordinal natural V32() finite cardinal ext-real V328() set

f2 + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

f1 . (f2 + 1) is set

f1 . f2 is set

bool (f1 . f2) is non empty set

{ [(b

C is set

T is set

f1 is non empty Relation-like NAT -defined Function-like total set

Union f1 is set

proj2 f1 is non empty set

union (proj2 f1) is set

f1 . 0 is set

f2 is non empty Relation-like NAT -defined Function-like total set

Union f2 is set

proj2 f2 is non empty set

union (proj2 f2) is set

f2 . 0 is set

dom f1 is non empty V315() V316() V317() V318() V319() V320() V322() V324() Element of bool NAT

dom f2 is non empty V315() V316() V317() V318() V319() V320() V322() V324() Element of bool NAT

() is set

C is non empty Relation-like NAT -defined Function-like total set

C . 0 is set

T is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . T is set

T + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . (T + 1) is set

bool (C . T) is non empty set

{ [(b

f1 is set

f2 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

[{},f2] is pair non empty set

{{},f2} is non empty finite V38() non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{}} is non empty trivial functional finite V38() 1 -element non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{{},f2},{{}}} is non empty finite V38() set

T is non pair epsilon-transitive epsilon-connected ordinal natural V32() finite cardinal ext-real V328() set

C . T is set

T is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . T is set

T + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . (T + 1) is set

f1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() finite cardinal ext-real V328() set

f1 + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

f1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() finite cardinal ext-real V328() set

f1 + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

f2 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . f2 is set

bool (C . f2) is non empty set

{ [(b

bool (C . T) is non empty set

{ [(b

x is set

a is Element of bool (C . f2)

(a) is set

b is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

[(a),b] is pair non empty set

{(a),b} is non empty finite set

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

{{(a),b},{(a)}} is non empty finite V38() set

f1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() finite cardinal ext-real V328() set

C . f1 is set

T is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

f1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . T is set

C . f1 is set

bool () is non empty set

C is non empty Relation-like NAT -defined Function-like total set

C . 0 is set

T is finite Element of bool ()

Union C is set

proj2 C is non empty set

union (proj2 C) is set

f1 is set

f2 is set

dom C is non empty V315() V316() V317() V318() V319() V320() V322() V324() Element of bool NAT

x is set

C . x is set

a is set

C . a is set

f1 is Relation-like Function-like set

proj1 f1 is set

proj2 f1 is set

f2 is non empty finite V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() Element of bool NAT

sup f2 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V328() V329() set

x is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . x is set

a is set

f1 . a is set

b is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . b is set

C is non empty Relation-like NAT -defined Function-like total set

Union C is set

proj2 C is non empty set

union (proj2 C) is set

C . 0 is set

dom C is non empty V315() V316() V317() V318() V319() V320() V322() V324() Element of bool NAT

C is finite Element of bool ()

(C) is set

T is non pair epsilon-transitive epsilon-connected ordinal natural V32() finite cardinal ext-real V328() set

[(C),T] is pair non empty set

{(C),T} is non empty finite set

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

{{(C),T},{(C)}} is non empty finite V38() set

f1 is non empty Relation-like NAT -defined Function-like total set

Union f1 is set

proj2 f1 is non empty set

union (proj2 f1) is set

f1 . 0 is set

f2 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

f1 . f2 is set

f2 + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

f1 . (f2 + 1) is set

bool (f1 . f2) is non empty set

{ [(b

dom f1 is non empty V315() V316() V317() V318() V319() V320() V322() V324() Element of bool NAT

{ [(b

C is non empty Relation-like NAT -defined Function-like total set

Union C is set

proj2 C is non empty set

union (proj2 C) is set

C . 0 is set

dom C is non empty V315() V316() V317() V318() V319() V320() V322() V324() Element of bool NAT

f1 is set

f2 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

[{},f2] is pair non empty set

{{},f2} is non empty finite V38() non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{}} is non empty trivial functional finite V38() 1 -element non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{{},f2},{{}}} is non empty finite V38() set

f1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . f1 is set

f1 + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . (f1 + 1) is set

bool (C . f1) is non empty set

{ [(b

f2 is set

x is Element of bool (C . f1)

(x) is set

a is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

[(x),a] is pair non empty set

{(x),a} is non empty finite set

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

{{(x),a},{(x)}} is non empty finite V38() set

f1 is set

f2 is set

C . f2 is set

f1 is set

f2 is Element of bool ()

(f2) is set

x is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

[(f2),x] is pair non empty set

{(f2),x} is non empty finite set

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

{{(f2),x},{(f2)}} is non empty finite V38() set

(()) is set

C is non empty Relation-like NAT -defined Function-like total set

Union C is set

proj2 C is non empty set

union (proj2 C) is set

C . 0 is set

T is set

f1 is set

[T,f1] is pair non empty set

{T,f1} is non empty finite set

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

{{T,f1},{T}} is non empty finite V38() set

f2 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

[{},f2] is pair non empty set

{{},f2} is non empty finite V38() non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{}} is non empty trivial functional finite V38() 1 -element non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{{},f2},{{}}} is non empty finite V38() set

((C . 0)) is set

T is non pair epsilon-transitive epsilon-connected ordinal natural V32() finite cardinal ext-real V328() set

C . T is set

((C . T)) is set

T + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . (T + 1) is set

bool (C . T) is non empty set

{ [(b

f2 is set

x is set

[f2,x] is pair non empty set

{f2,x} is non empty finite set

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

{{f2,x},{f2}} is non empty finite V38() set

a is Element of bool (C . T)

(a) is set

b is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

[(a),b] is pair non empty set

{(a),b} is non empty finite set

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

{{(a),b},{(a)}} is non empty finite V38() set

f1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . f1 is set

f1 + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . (f1 + 1) is set

((C . (T + 1))) is set

{ (b

union { (b

T is set

f1 is set

f2 is Element of proj2 C

(f2) is set

dom C is non empty V315() V316() V317() V318() V319() V320() V322() V324() Element of bool NAT

x is set

C . x is set

a is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . a is set

((C . a)) is set

C is set

the_rank_of C is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of C) is epsilon-transitive set

C is set

(C) is set

the_rank_of (C) is epsilon-transitive epsilon-connected ordinal set

the_rank_of C is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of C) is epsilon-transitive set

succ (the_rank_of C) is non empty epsilon-transitive epsilon-connected ordinal set

succ (succ (the_rank_of C)) is non empty epsilon-transitive epsilon-connected ordinal set

Rank (succ (succ (the_rank_of C))) is epsilon-transitive set

f1 is set

f2 is set

[f1,f2] is pair non empty set

{f1,f2} is non empty finite set

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

{{f1,f2},{f1}} is non empty finite V38() set

Rank omega is epsilon-transitive set

bool (Rank omega) is non empty set

C is finite Element of bool (Rank omega)

T is Relation-like Function-like set

proj1 T is set

proj2 T is set

f1 is set

f2 is set

T . f2 is set

the_rank_of f2 is epsilon-transitive epsilon-connected ordinal set

the_rank_of C is epsilon-transitive epsilon-connected ordinal set

f1 is non empty finite V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() Element of bool NAT

sup f1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V328() V329() set

f2 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

1 + f2 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

Rank (1 + f2) is epsilon-transitive set

a is set

T . a is set

the_rank_of a is epsilon-transitive epsilon-connected ordinal set

b is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

succ f2 is non pair non empty epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() V328() V329() Element of omega

the_rank_of C is epsilon-transitive epsilon-connected ordinal set

succ (1 + f2) is non pair non empty epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() V328() V329() Element of omega

(1 + f2) + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C is non empty Relation-like NAT -defined Function-like total set

Union C is set

proj2 C is non empty set

union (proj2 C) is set

C . 0 is set

T is set

dom C is non empty V315() V316() V317() V318() V319() V320() V322() V324() Element of bool NAT

f1 is set

C . f1 is set

x is set

a is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

[{},a] is pair non empty set

{{},a} is non empty finite V38() non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{}} is non empty trivial functional finite V38() 1 -element non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{{},a},{{}}} is non empty finite V38() set

a + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

succ a is non pair non empty epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() V328() V329() Element of omega

the_rank_of {} is epsilon-transitive epsilon-connected ordinal set

the_rank_of a is epsilon-transitive epsilon-connected ordinal set

Rank (a + 1) is epsilon-transitive set

succ (a + 1) is non pair non empty epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() V328() V329() Element of omega

succ (succ (a + 1)) is non pair non empty epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() V328() V329() Element of omega

Rank (succ (succ (a + 1))) is epsilon-transitive set

x is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . x is set

x + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . (x + 1) is set

bool (C . x) is non empty set

{ [(b

a is set

b is Element of bool (C . x)

(b) is set

i is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

[(b),i] is pair non empty set

{(b),i} is non empty finite set

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

{{(b),i},{(b)}} is non empty finite V38() set

the_rank_of b is epsilon-transitive epsilon-connected ordinal set

pi1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

i \/ pi1 is finite V315() V316() V317() V318() V319() V320() V324() V325() V326() set

the_rank_of (b) is epsilon-transitive epsilon-connected ordinal set

the_rank_of i is epsilon-transitive epsilon-connected ordinal set

z is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

succ z is non pair non empty epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() V328() V329() Element of omega

z + 1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

Rank (z + 1) is epsilon-transitive set

succ (z + 1) is non pair non empty epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() V328() V329() Element of omega

succ (succ (z + 1)) is non pair non empty epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() V328() V329() Element of omega

Rank (succ (succ (z + 1))) is epsilon-transitive set

f2 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

C . f2 is set

C is finite Element of bool ()

(C) is set

the_rank_of C is epsilon-transitive epsilon-connected ordinal set

the_rank_of (C) is epsilon-transitive epsilon-connected ordinal set

[{},0] is pair non empty set

{{},0} is non empty functional finite V38() non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{}} is non empty trivial functional finite V38() 1 -element non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{{},0},{{}}} is non empty finite V38() set

C is Element of ()

C `1 is set

T is Element of bool ()

(T) is set

f1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

[(T),f1] is pair non empty set

{(T),f1} is non empty finite set

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

{{(T),f1},{(T)}} is non empty finite V38() set

C is Element of ()

C `1 is finite set

T is Element of bool ()

(T) is set

f1 is non pair epsilon-transitive epsilon-connected ordinal natural V32() V33() finite cardinal ext-real V315() V316() V317() V318() V319() V320() V324() V325() V326() V328() V329() Element of NAT

[(T),f1] is pair non empty set

{(T),f1} is non empty finite set

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

{{(T),f1},{(T)}} is non empty finite V38() set

C is non pair epsilon-transitive epsilon-connected ordinal natural V32() finite cardinal ext-real V328() set

[{},C] is pair non empty set

{{},C} is non empty finite V38() non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{}} is non empty trivial functional finite V38() 1 -element non with_pair V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() set

{{{},C},{{}}} is non empty finite V38() set

C is non