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()
{ b1 where b1 is Relation-like NAT -defined K635() -valued Function-like finite FinSequence-like FinSubsequence-like Element of K635() * : len b1 = 2 } is set
[:(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()
{ b1 where b1 is Relation-like NAT -defined K635() -valued Function-like finite FinSequence-like FinSubsequence-like Element of K635() * : len b1 = 3 } is set
[:(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
{ b1 where b1 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 <= b1 & b1 <= 1 ) } is set
{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
{ b1 where b1 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 <= b1 & b1 <= 2 ) } is set
{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
{ b1 where b1 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 <= b1 & b1 <= len f2 ) } is set
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
{ b1 where b1 is Element of the carrier of (DTConMSA (T \/ ( the carrier of C --> {0}))) : ex b2 being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set st b1 ==> b2 } is set
[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
{ b1 where b1 is Element of the carrier of (DTConMSA (T \/ ( the carrier of C --> {0}))) : ex b2 being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set st b1 ==> b2 } is set
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
{ b1 where b1 is Element of bool (Rank (the_rank_of C)) : ( C c= b1 & ( for b2, b3 being set holds
( not [b2,b3] in b1 or b2 c= b1 ) ) ) } is set
meet { b1 where b1 is Element of bool (Rank (the_rank_of C)) : ( C c= b1 & ( for b2, b3 being set holds
( not [b2,b3] in b1 or b2 c= b1 ) ) ) } is set
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
{ (b1) where b1 is Element of C : verum } is set
union { (b1) where b1 is Element of C : verum } is set
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
F1() is set
{ F2(b1) where b1 is Element of F1() : P1[b1] } is set
union { F2(b1) where b1 is Element of F1() : P1[b1] } is set
((union { F2(b1) where b1 is Element of F1() : P1[b1] } )) is set
{ (F2(b1)) where b1 is Element of F1() : P1[b1] } is set
union { (F2(b1)) where b1 is Element of F1() : P1[b1] } is set
f1 is set
f2 is set
(f2) is set
x is Element of F1()
F2(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 F1()
F2(a) is set
(F2(a)) is set
f1 is set
f2 is set
x is Element of F1()
F2(x) is set
(F2(x)) is set
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
{ (b1) where b1 is Element of {C,T} : verum } is set
union {C,T} is set
union { (b1) where b1 is Element of {C,T} : verum } is set
{(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
{ [(b1),b2] where b1 is Element of bool a2, b2 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 : b1 is finite } is set
{ [{},b1] where b1 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 : verum } is set
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
{ [(b1),b2] where b1 is Element of bool (f1 . f2), b2 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 : b1 is finite } is set
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
{ [(b1),b2] where b1 is Element of bool (C . T), b2 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 : b1 is finite } is set
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
{ [(b1),b2] where b1 is Element of bool (C . f2), b2 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 : b1 is finite } is set
bool (C . T) is non empty set
{ [(b1),b2] where b1 is Element of bool (C . T), b2 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 : b1 is finite } is set
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
{ [(b1),b2] where b1 is Element of bool (f1 . f2), b2 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 : b1 is finite } is set
dom f1 is non empty V315() V316() V317() V318() V319() V320() V322() V324() Element of bool NAT
{ [(b1),b2] where b1 is Element of bool (), b2 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 : b1 is finite } 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
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
{ [(b1),b2] where b1 is Element of bool (C . f1), b2 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 : b1 is finite } is set
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
{ [(b1),b2] where b1 is Element of bool (C . T), b2 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 : b1 is finite } 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 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
{ (b1) where b1 is Element of proj2 C : verum } is set
union { (b1) where b1 is Element of proj2 C : verum } is set
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
{ [(b1),b2] where b1 is Element of bool (C . x), b2 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 : b1 is finite } is set
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