:: 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

bool is non empty set
bool () is non empty 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

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 ()
bool () is non empty set
is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set
K635() is set

{ } is set
[:(),K635():] is Relation-like set
bool [:(),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

{ } is set
[:(),K635():] is Relation-like set
bool [:(),K635():] is non empty set

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

is non empty non trivial Relation-like non finite 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

K469(0) is non empty V239() set
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 . C is set
Union T is set
proj2 T is set
union () is set
proj1 T is set

Union T is set
proj2 T is set
union () is set
C is set
T . C 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 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

[: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

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

Union () is non empty set
proj2 () is non empty with_non-empty_elements set
union (proj2 ()) is set
[: the carrier' of C,{ the carrier of C}:] \/ (Union ()) is non empty set
REL T is Relation-like [: the carrier' of C,{ the carrier of C}:] \/ (Union ()) -defined ([: the carrier' of C,{ the carrier of C}:] \/ (Union ())) * -valued Element of bool [:([: the carrier' of C,{ the carrier of C}:] \/ (Union ())),(([: the carrier' of C,{ the carrier of C}:] \/ (Union ())) *):]
([: the carrier' of C,{ the carrier of C}:] \/ (Union ())) * is non empty functional FinSequence-membered FinSequenceSet of [: the carrier' of C,{ the carrier of C}:] \/ (Union ())
[:([: the carrier' of C,{ the carrier of C}:] \/ (Union ())),(([: the carrier' of C,{ the carrier of C}:] \/ (Union ())) *):] is non empty Relation-like set
bool [:([: the carrier' of C,{ the carrier of C}:] \/ (Union ())),(([: the carrier' of C,{ the carrier of C}:] \/ (Union ())) *):] is non empty set
DTConstrStr(# ([: the carrier' of C,{ the carrier of C}:] \/ (Union ())),(REL T) #) is non empty strict DTConstrStr
the carrier of () is non empty set
FinTrees the carrier of () is non empty functional constituted-DTrees DTree-set of the carrier of ()
C -Terms T is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of ())
bool (FinTrees the carrier of ()) is non empty set
f1 is non empty Relation-like the carrier of () -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 --> 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,():]
[: the carrier of C,():] is non empty non trivial Relation-like non finite set
bool [: the carrier of C,():] is non empty non trivial non finite set
T \/ ( the carrier of C --> ) 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 --> )) 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 --> )) 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 --> ))) is non empty set
proj2 (coprod (T \/ ( the carrier of C --> ))) is non empty with_non-empty_elements set
union (proj2 (coprod (T \/ ( the carrier of C --> )))) is set
[: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> )))) is non empty set
REL (T \/ ( the carrier of C --> )) is Relation-like [: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> )))) -defined ([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))) * -valued Element of bool [:([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))),(([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))) *):]
([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))) * 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,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))),(([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))) *):] 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,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))) *):] is non empty set
DTConstrStr(# ([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))),(REL (T \/ ( the carrier of C --> ))) #) is non empty strict DTConstrStr
the carrier of (DTConMSA (T \/ ( the carrier of C --> ))) is non empty set
FinTrees the carrier of (DTConMSA (T \/ ( the carrier of C --> ))) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA (T \/ ( the carrier of C --> )))
C -Terms (T \/ ( the carrier of C --> )) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA (T \/ ( the carrier of C --> ))))
bool (FinTrees the carrier of (DTConMSA (T \/ ( the carrier of C --> )))) 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

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

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

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

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 --> 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,():]
[: the carrier of C,():] is non empty non trivial Relation-like non finite set
bool [: the carrier of C,():] 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 --> ) 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 --> )) 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 --> )) 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 --> ))) is non empty set
proj2 (coprod (T \/ ( the carrier of C --> ))) is non empty with_non-empty_elements set
union (proj2 (coprod (T \/ ( the carrier of C --> )))) is set
[: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> )))) is non empty set
REL (T \/ ( the carrier of C --> )) is Relation-like [: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> )))) -defined ([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))) * -valued Element of bool [:([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))),(([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))) *):]
([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))) * 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,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))),(([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))) *):] 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,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))) *):] is non empty set
DTConstrStr(# ([: the carrier' of C,{ the carrier of C}:] \/ (Union (coprod (T \/ ( the carrier of C --> ))))),(REL (T \/ ( the carrier of C --> ))) #) is non empty strict DTConstrStr
the carrier of (DTConMSA (T \/ ( the carrier of C --> ))) is non empty set
FinTrees the carrier of (DTConMSA (T \/ ( the carrier of C --> ))) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA (T \/ ( the carrier of C --> )))
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 --> )) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA (T \/ ( the carrier of C --> ))))
bool (FinTrees the carrier of (DTConMSA (T \/ ( the carrier of C --> )))) is non empty set
a is Element of the carrier of C
(T \/ ( the carrier of C --> )) . a is non empty set
[:((T \/ ( the carrier of C --> )) . a), the carrier of C:] is non empty Relation-like set
b is Element of (T \/ ( the carrier of C --> )) . a
[b,a] is pair non empty Element of [:((T \/ ( the carrier of C --> )) . 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 --> )) . a), the carrier of C:] -valued Function-like DecoratedTree-like Element of FinTrees [:((T \/ ( the carrier of C --> )) . a), the carrier of C:]
FinTrees [:((T \/ ( the carrier of C --> )) . a), the carrier of C:] is non empty functional constituted-DTrees DTree-set of [:((T \/ ( the carrier of C --> )) . 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 --> )) . a -defined the carrier of C -valued Element of bool [:((T \/ ( the carrier of C --> )) . a), the carrier of C:]
bool [:((T \/ ( the carrier of C --> )) . 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 --> ))) is Element of NonTerminals (DTConMSA (T \/ ( the carrier of C --> )))
NonTerminals (DTConMSA (T \/ ( the carrier of C --> ))) is non empty Element of bool the carrier of (DTConMSA (T \/ ( the carrier of C --> )))
bool the carrier of (DTConMSA (T \/ ( the carrier of C --> ))) is non empty set
{ b1 where b1 is Element of the carrier of (DTConMSA (T \/ ( the carrier of C --> ))) : 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 --> ))) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V115() DTree-yielding ArgumentSeq of Sym (a,(T \/ ( the carrier of C --> )))
rng b is functional finite constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA (T \/ ( the carrier of C --> ))))
[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 --> ))) is non empty Relation-like the carrier of C -defined Function-like total ManySortedSubset of the Sorts of (FreeMSA (T \/ ( the carrier of C --> )))
FreeMSA (T \/ ( the carrier of C --> )) is strict non-empty V172(C) MSAlgebra over C
FreeSort (T \/ ( the carrier of C --> )) 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 --> )) 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 --> ))) #), the ResultSort of C * (FreeSort (T \/ ( 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 * 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 --> ))) # 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 --> ))) #) 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 --> ))) is Relation-like non-empty the carrier' of C -defined Function-like set
MSAlgebra(# (FreeSort (T \/ ( the carrier of C --> ))),(FreeOper (T \/ ( the carrier of C --> ))) #) is strict MSAlgebra over C
the Sorts of (FreeMSA (T \/ ( the carrier of C --> ))) 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 --> )))) -tree b is non empty Relation-like the carrier of (DTConMSA (T \/ ( the carrier of C --> ))) -valued Function-like finite DecoratedTree-like Element of C -Terms (T \/ ( the carrier of C --> ))
the_sort_of ((Sym (a,(T \/ ( the carrier of C --> )))) -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 --> )))) is set
proj2 (C -Terms (T,(T \/ ( the carrier of C --> )))) is non empty set
union (proj2 (C -Terms (T,(T \/ ( the carrier of C --> ))))) is set

len () 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 --> ))) -valued Function-like finite DecoratedTree-like Element of C -Terms (T \/ ( the carrier of C --> ))
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

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

[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 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

len () 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 --> ))) is Element of NonTerminals (DTConMSA (T \/ ( the carrier of C --> )))
NonTerminals (DTConMSA (T \/ ( the carrier of C --> ))) is non empty Element of bool the carrier of (DTConMSA (T \/ ( the carrier of C --> )))
bool the carrier of (DTConMSA (T \/ ( the carrier of C --> ))) is non empty set
{ b1 where b1 is Element of the carrier of (DTConMSA (T \/ ( the carrier of C --> ))) : 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

bool (Rank ()) is non empty set
{ b1 where b1 is Element of bool (Rank ()) : ( 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 ()) : ( 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 ())
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 ())
f2 is set
f2 /\ (Rank ()) is set
a is Element of bool (Rank ())
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
(()) 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 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

proj1 C is set
C . 0 is set

Union T is set
proj2 T is non empty set
union () is set

Union f1 is set
proj2 f1 is non empty set
union (proj2 f1) is set
f1 . 0 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
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

Union f1 is set
proj2 f1 is non empty set
union (proj2 f1) is set
f1 . 0 is 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 . 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

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 + 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 + 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

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 . 0 is set
T is finite Element of bool ()
Union C is set
proj2 C is non empty set
union () 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

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

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

Union C is set
proj2 C is non empty set
union () 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

[(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

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

Union C is set
proj2 C is non empty set
union () 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

Union C is set
proj2 C is non empty set
union () 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

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

C is set
(C) is set

Rank (succ (succ ())) 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

bool () is non empty set
C is finite Element of bool ()

proj1 T is set
proj2 T is set
f1 is set
f2 is set
T . f2 is set

f1 is non empty finite V315() V316() V317() V318() V319() V320() V322() V323() V324() V325() V326() Element of bool 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
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

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

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

Union C is set
proj2 C is non empty set
union () 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

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

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

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

is pair non empty set
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
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 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