REAL is complex-membered ext-real-membered real-membered V107() V146() V147() V149() set
NAT is non empty non trivial ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V107() V144() V146() Element of bool REAL
bool REAL is non empty set
ExtREAL is ext-real-membered V149() set
[:NAT,ExtREAL:] is Relation-like V92() set
bool [:NAT,ExtREAL:] is non empty set
bool ExtREAL is non empty set
omega is non empty non trivial ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V107() V144() V146() set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is complex-membered V107() set
RAT is complex-membered ext-real-membered real-membered rational-membered V107() set
INT is complex-membered ext-real-membered real-membered rational-membered integer-membered V107() set
{} is empty ordinal natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V22() finite finite-yielding V44() cardinal {} -element Function-yielding FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() ext-real non positive non negative with_common_domain V91() V92() V93() to-naturals complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V107() FuncSeq-like V146() V147() V148() V149() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V188() set
the empty ordinal natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V22() finite finite-yielding V44() cardinal {} -element Function-yielding FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() ext-real non positive non negative with_common_domain V91() V92() V93() to-naturals complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V107() FuncSeq-like V146() V147() V148() V149() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V188() set is empty ordinal natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V22() finite finite-yielding V44() cardinal {} -element Function-yielding FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() ext-real non positive non negative with_common_domain V91() V92() V93() to-naturals complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V107() FuncSeq-like V146() V147() V148() V149() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V188() set
1 is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
{{},1} is non empty finite V44() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() V188() set
K395() is non empty set
0 is empty ordinal natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V22() finite finite-yielding V44() cardinal {} -element Function-yielding FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() ext-real non positive non negative with_common_domain V89() V90() V91() V92() V93() to-naturals complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V107() FuncSeq-like V146() V147() V148() V149() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V188() Element of NAT
{0,1} is non empty finite V44() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() V188() set
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
HFuncs NAT is non empty M21(NAT * , NAT )
K345((NAT *),NAT) is M21(NAT * , NAT )
{ b1 where b1 is Relation-like NAT * -defined NAT -valued Function-like M22(NAT * , NAT ,K345((NAT *),NAT)) : b1 is homogeneous } is set
bool (HFuncs NAT) is non empty set
bool (HFuncs NAT) is non empty Element of bool (bool (HFuncs NAT))
bool (bool (HFuncs NAT)) is non empty set
[:NAT,(bool (HFuncs NAT)):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool (HFuncs NAT)):] is non empty non trivial non finite set
2 is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
K481() is L10()
the carrier of K481() is 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 RAT -valued INT -valued non finite V91() V92() V93() to-naturals 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
2 -tuples_on K395() is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of K395()
[:(2 -tuples_on K395()),K395():] is non empty Relation-like set
bool [:(2 -tuples_on K395()),K395():] is non empty set
3 is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
3 -tuples_on K395() is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of K395()
[:(3 -tuples_on K395()),K395():] is non empty Relation-like set
bool [:(3 -tuples_on K395()),K395():] is non empty set
K671() is non empty Relation-like 2 -tuples_on K395() -defined K395() -valued Function-like total quasi_total V114() Element of bool [:(2 -tuples_on K395()),K395():]
[:NAT,REAL:] is Relation-like V91() V92() V93() set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
bool RAT is non empty set
[:1,1:] is non empty Relation-like RAT -valued INT -valued finite V91() V92() V93() to-naturals set
bool [:1,1:] is non empty finite V44() set
[:[:1,1:],1:] is non empty Relation-like RAT -valued INT -valued finite V91() V92() V93() to-naturals set
bool [:[:1,1:],1:] is non empty finite V44() set
dom {} is empty ordinal natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V22() finite finite-yielding V44() cardinal {} -element Function-yielding FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() ext-real non positive non negative with_common_domain V91() V92() V93() to-naturals complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V107() FuncSeq-like V146() V147() V148() V149() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V188() set
rng {} is empty trivial ordinal natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V22() with_non-empty_elements finite finite-yielding V44() cardinal {} -element Function-yielding FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() ext-real non positive non negative with_common_domain V91() V92() V93() to-naturals V95() V96() V97() V98() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V107() FuncSeq-like V146() V147() V148() V149() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V188() set
{{}} is non empty trivial functional finite V44() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Tree-like V188() set
4 is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
Seg 4 is non empty finite 4 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of bool NAT
{ b1 where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : ( 1 <= b1 & b1 <= 4 ) } is set
{1,2,3,4} is non empty finite set
card {} is empty ordinal natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V22() finite finite-yielding V44() cardinal {} -element Function-yielding FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() ext-real non positive non negative with_common_domain V91() V92() V93() to-naturals complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V107() FuncSeq-like V146() V147() V148() V149() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V188() set
+infty is non empty V80() ext-real positive non negative set
-infty is non empty V80() ext-real non positive negative set
A is Relation-like Function-like set
dom A is set
S is Relation-like Function-like set
dom S is set
T is Relation-like Function-like set
rng T is set
T * A is Relation-like Function-like set
T * S is Relation-like Function-like set
f is set
dom (T * A) is set
dom T is set
dom (T * S) is set
P is set
(T * A) . P is set
T . P is set
A . (T . P) is set
(T * S) . P is set
S . (T . P) is set
A is non empty set
S is non empty set
<*A,S*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*A*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,A] is non empty V22() set
{1,A} is non empty finite set
{1} is non empty trivial finite V44() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() V188() set
{{1,A},{1}} is non empty finite V44() set
{[1,A]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*S*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,S] is non empty V22() set
{1,S} is non empty finite set
{{1,S},{1}} is non empty finite V44() set
{[1,S]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*A*> ^ <*S*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
rng <*A,S*> is non empty finite set
{A,S} is non empty finite set
A is Relation-like non-empty NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
S is Relation-like non-empty NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
A ^ S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (A ^ S) is finite set
rng A is with_non-empty_elements finite set
rng S is with_non-empty_elements finite set
(rng A) \/ (rng S) is finite set
A is set
S is non empty set
T is functional FinSequence-membered FinSequenceSet of A
f is Element of S
T --> f is set
A * is non empty functional FinSequence-membered FinSequenceSet of A
[:(A *),S:] is non empty Relation-like set
bool [:(A *),S:] is non empty set
T --> f is Relation-like T -defined S -valued Function-like total quasi_total Element of bool [:T,S:]
[:T,S:] is Relation-like set
bool [:T,S:] is non empty set
dom (T --> f) is functional FinSequence-membered Element of bool T
bool T is non empty set
rng (T --> f) is Element of bool S
bool S is non empty set
{f} is non empty trivial finite 1 -element set
A is non empty set
A * is non empty functional FinSequence-membered FinSequenceSet of A
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
T is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
T -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
S is Element of A
(A,A,(T -tuples_on A),S) is Relation-like A * -defined A -valued Function-like Element of bool [:(A *),A:]
dom (A,A,(T -tuples_on A),S) is functional FinSequence-membered Element of bool (A *)
bool (A *) is non empty set
f is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
f -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
C is non empty Relation-like A * -defined A -valued Function-like homogeneous Element of bool [:(A *),A:]
arity C is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
I is Relation-like A * -defined A -valued Function-like Element of bool [:(A *),A:]
A is non empty set
S is Element of A
T is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
T -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
(A,A,(T -tuples_on A),S) is non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total Element of bool [:(A *),A:]
A * is non empty functional FinSequence-membered FinSequenceSet of A
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
arity (A,A,(T -tuples_on A),S) is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
dom (A,A,(T -tuples_on A),S) is non empty functional FinSequence-membered with_common_domain Element of bool (A *)
bool (A *) is non empty set
f is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
f -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
A is non empty set
T is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
T -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
S is Element of A
(A,A,(T -tuples_on A),S) is non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total Element of bool [:(A *),A:]
A * is non empty functional FinSequence-membered FinSequenceSet of A
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
arity (A,A,(T -tuples_on A),S) is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
A is non empty set
A * is non empty functional FinSequence-membered FinSequenceSet of A
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
T is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
T -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
S is Element of A
(A,A,(T -tuples_on A),S) is non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total Element of bool [:(A *),A:]
f is Relation-like A * -defined A -valued Function-like homogeneous Element of bool [:(A *),A:]
A is non empty set
A * is non empty functional FinSequence-membered FinSequenceSet of A
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
the Element of A is Element of A
2 -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
[:(2 -tuples_on A),A:] is non empty Relation-like set
bool [:(2 -tuples_on A),A:] is non empty set
T is non empty Relation-like 2 -tuples_on A -defined A -valued Function-like total quasi_total Element of bool [:(2 -tuples_on A),A:]
T is non empty Relation-like 2 -tuples_on A -defined A -valued Function-like total quasi_total Element of bool [:(2 -tuples_on A),A:]
rng T is non empty Element of bool A
bool A is non empty set
dom T is non empty functional FinSequence-membered Element of bool (2 -tuples_on A)
bool (2 -tuples_on A) is non empty set
f is non empty Relation-like A * -defined A -valued Function-like homogeneous Element of bool [:(A *),A:]
arity f is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
P is non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total Element of bool [:(A *),A:]
arity P is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
C is set
I is set
<*C,I*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*C*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,C] is non empty V22() set
{1,C} is non empty finite set
{{1,C},{1}} is non empty finite V44() set
{[1,C]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*I*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,I] is non empty V22() set
{1,I} is non empty finite set
{{1,I},{1}} is non empty finite V44() set
{[1,I]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*C*> ^ <*I*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
dom P is non empty functional FinSequence-membered with_common_domain Element of bool (A *)
bool (A *) is non empty set
s is set
<*I,s*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*s*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,s] is non empty V22() set
{1,s} is non empty finite set
{{1,s},{1}} is non empty finite V44() set
{[1,s]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*I*> ^ <*s*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
P . <*C,I*> is set
<*(P . <*C,I*>),s*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*(P . <*C,I*>)*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,(P . <*C,I*>)] is non empty V22() set
{1,(P . <*C,I*>)} is non empty finite set
{{1,(P . <*C,I*>)},{1}} is non empty finite V44() set
{[1,(P . <*C,I*>)]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*(P . <*C,I*>)*> ^ <*s*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
P . <*I,s*> is set
<*C,(P . <*I,s*>)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*(P . <*I,s*>)*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,(P . <*I,s*>)] is non empty V22() set
{1,(P . <*I,s*>)} is non empty finite set
{{1,(P . <*I,s*>)},{1}} is non empty finite V44() set
{[1,(P . <*I,s*>)]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*C*> ^ <*(P . <*I,s*>)*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
IFEQ (C, the Element of A,I,C) is set
IFEQ (I, the Element of A,s,I) is set
IFEQ (C, the Element of A,(IFEQ (I, the Element of A,s,I)),C) is set
IFEQ (C, the Element of A,s,C) is set
P . <*(P . <*C,I*>),s*> is set
r is Element of A
i is Element of A
IFEQ (r, the Element of A,i,r) is Element of A
s is Element of A
<*(IFEQ (r, the Element of A,i,r)),s*> is non empty Relation-like NAT -defined A -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like FinSequence of A
<*(IFEQ (r, the Element of A,i,r))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,(IFEQ (r, the Element of A,i,r))] is non empty V22() set
{1,(IFEQ (r, the Element of A,i,r))} is non empty finite set
{{1,(IFEQ (r, the Element of A,i,r))},{1}} is non empty finite V44() set
{[1,(IFEQ (r, the Element of A,i,r))]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*s*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,s] is non empty V22() set
{1,s} is non empty finite set
{{1,s},{1}} is non empty finite V44() set
{[1,s]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*(IFEQ (r, the Element of A,i,r))*> ^ <*s*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
P . <*(IFEQ (r, the Element of A,i,r)),s*> is set
IFEQ ((IFEQ (C, the Element of A,I,C)), the Element of A,s,(IFEQ (C, the Element of A,I,C))) is set
IFEQ (i, the Element of A,s,i) is Element of A
<*r,(IFEQ (i, the Element of A,s,i))*> is non empty Relation-like NAT -defined A -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like FinSequence of A
<*r*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,r] is non empty V22() set
{1,r} is non empty finite set
{{1,r},{1}} is non empty finite V44() set
{[1,r]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*(IFEQ (i, the Element of A,s,i))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,(IFEQ (i, the Element of A,s,i))] is non empty V22() set
{1,(IFEQ (i, the Element of A,s,i))} is non empty finite set
{{1,(IFEQ (i, the Element of A,s,i))},{1}} is non empty finite V44() set
{[1,(IFEQ (i, the Element of A,s,i))]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*r*> ^ <*(IFEQ (i, the Element of A,s,i))*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
P . <*r,(IFEQ (i, the Element of A,s,i))*> is set
P . <*C,(P . <*I,s*>)*> is set
C is set
I is set
<*C,I*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*C*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,C] is non empty V22() set
{1,C} is non empty finite set
{{1,C},{1}} is non empty finite V44() set
{[1,C]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*I*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,I] is non empty V22() set
{1,I} is non empty finite set
{{1,I},{1}} is non empty finite V44() set
{[1,I]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*C*> ^ <*I*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
dom P is non empty functional FinSequence-membered with_common_domain set
<*I,C*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*I*> ^ <*C*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<* the Element of A,C*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<* the Element of A*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1, the Element of A] is non empty V22() set
{1, the Element of A} is non empty finite set
{{1, the Element of A},{1}} is non empty finite V44() set
{[1, the Element of A]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<* the Element of A*> ^ <*C*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
P . <* the Element of A,C*> is set
<*C, the Element of A*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*C*> ^ <* the Element of A*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
P . <*C, the Element of A*> is set
s is Element of A
<* the Element of A,s*> is non empty Relation-like NAT -defined A -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like FinSequence of A
<*s*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,s] is non empty V22() set
{1,s} is non empty finite set
{{1,s},{1}} is non empty finite V44() set
{[1,s]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<* the Element of A*> ^ <*s*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
IFEQ ( the Element of A, the Element of A,s, the Element of A) is Element of A
<*s, the Element of A*> is non empty Relation-like NAT -defined A -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like FinSequence of A
<*s*> ^ <* the Element of A*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
IFEQ (s, the Element of A, the Element of A,s) is Element of A
the Element of A is Element of A
0 -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
(A,A,(0 -tuples_on A), the Element of A) is non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total 0 -ary Element of bool [:(A *),A:]
arity (A,A,(0 -tuples_on A), the Element of A) is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
the Element of A is Element of A
3 -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
(A,A,(3 -tuples_on A), the Element of A) is non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total 3 -ary Element of bool [:(A *),A:]
arity (A,A,(3 -tuples_on A), the Element of A) is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
A is non empty set
FinTrees A is non empty functional constituted-DTrees DTree-set of A
S is Relation-like NAT -defined FinTrees A -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees A
rng S is functional finite constituted-DTrees Element of bool (FinTrees A)
bool (FinTrees A) is non empty set
f is set
T is set
T -tree S is Relation-like Function-like DecoratedTree-like set
P is Relation-like A -valued Function-like DecoratedTree-like Element of FinTrees A
dom P is non empty finite Tree-like set
C is non empty finite Tree-like set
{ H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V91() V92() V93() to-naturals Element of C : S1[b1] } is set
the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V91() V92() V93() to-naturals Element of C is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V91() V92() V93() to-naturals Element of C
len the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V91() V92() V93() to-naturals Element of C is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
I is finite set
r is set
i is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V91() V92() V93() to-naturals Element of C
len i is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
r is non empty finite complex-membered ext-real-membered real-membered V144() V145() V146() V147() V148() set
max r is V79() V80() ext-real set
i is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V91() V92() V93() to-naturals Element of C
len i is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
dom S is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of bool NAT
s is set
S . s is Relation-like Function-like set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
r is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
1 + r is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
len S is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
<*r*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like V189() set
[1,r] is non empty V22() set
{1,r} is non empty finite V44() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() V188() set
{{1,r},{1}} is non empty finite V44() set
{[1,r]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*r*> ^ i is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (T -tree S) is non empty Tree-like set
len (<*r*> ^ i) is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
1 + (len i) is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
S is Relation-like Function-like set
A is Relation-like Function-like set
T is set
A | T is Relation-like Function-like set
S +* (A | T) is Relation-like Function-like set
A is Relation-like Function-like set
dom A is set
S is Relation-like Function-like set
T is set
f is set
(A,S,f) is Relation-like Function-like set
A | f is Relation-like Function-like set
S +* (A | f) is Relation-like Function-like set
(A,S,f) . T is set
A . T is set
dom (A | f) is set
(dom A) /\ f is set
(A | f) . T is set
S is Relation-like Function-like set
dom S is set
A is Relation-like Function-like set
T is set
f is set
(A,S,f) is Relation-like Function-like set
A | f is Relation-like Function-like set
S +* (A | f) is Relation-like Function-like set
(A,S,f) . T is set
S . T is set
dom A is set
(dom A) /\ f is set
dom (A | f) is set
A is non empty set
S is non empty set
Funcs (A,S) is non empty functional FUNCTION_DOMAIN of A,S
T is Relation-like A -defined S -valued Function-like total quasi_total Element of Funcs (A,S)
f is Relation-like A -defined S -valued Function-like total quasi_total Element of Funcs (A,S)
P is set
(T,f,P) is Relation-like Function-like set
T | P is Relation-like P -defined A -defined S -valued Function-like set
f +* (T | P) is Relation-like Function-like set
dom f is Element of bool A
bool A is non empty set
T | P is Relation-like A -defined P -defined A -defined S -valued Function-like Element of bool [:A,S:]
[:A,S:] is non empty Relation-like set
bool [:A,S:] is non empty set
dom (T | P) is Element of bool A
(dom f) \/ (dom (T | P)) is Element of bool A
dom (T,f,P) is set
rng (T,f,P) is set
rng f is Element of bool S
bool S is non empty set
rng (T | P) is Element of bool S
(rng f) \/ (rng (T | P)) is Element of bool S
A is non empty set
S is non empty set
Funcs (A,S) is non empty functional FUNCTION_DOMAIN of A,S
T is non empty set
Funcs (S,T) is non empty functional FUNCTION_DOMAIN of S,T
f is Relation-like A -defined S -valued Function-like total quasi_total Element of Funcs (A,S)
P is Relation-like S -defined T -valued Function-like total quasi_total Element of Funcs (S,T)
f * P is Relation-like A -defined T -valued Function-like set
Funcs (A,T) is non empty functional FUNCTION_DOMAIN of A,T
P * f is non empty Relation-like A -defined T -valued Function-like total quasi_total Element of bool [:A,T:]
[:A,T:] is non empty Relation-like set
bool [:A,T:] is non empty set
A is Relation-like Function-like set
S is set
{ ((iter (A,b1)) . S) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : S in dom (iter (A,b1)) } is set
A is Relation-like Function-like set
dom A is set
S is set
(A,S) is set
{ ((iter (A,b1)) . S) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : S in dom (iter (A,b1)) } is set
rng A is set
(dom A) \/ (rng A) is set
iter (A,0) is Relation-like Function-like set
field A is set
id (field A) is Relation-like field A -defined field A -valued Function-like one-to-one total quasi_total Element of bool [:(field A),(field A):]
[:(field A),(field A):] is Relation-like set
bool [:(field A),(field A):] is non empty set
(iter (A,0)) . S is set
dom (iter (A,0)) is set
A is Relation-like Function-like set
rng A is set
dom A is set
T is set
S is set
(A,S) is set
{ ((iter (A,b1)) . S) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : S in dom (iter (A,b1)) } is set
A . T is set
f is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
iter (A,f) is Relation-like Function-like set
(iter (A,f)) . S is set
dom (iter (A,f)) is set
f + 1 is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
iter (A,(f + 1)) is Relation-like Function-like set
(iter (A,f)) * A is Relation-like Function-like set
(iter (A,(f + 1))) . S is set
rng (iter (A,f)) is set
field A is set
(dom A) \/ (rng A) is set
dom (iter (A,(f + 1))) is set
A is Relation-like Function-like set
dom A is set
S is set
A . S is set
(A,S) is set
{ ((iter (A,b1)) . S) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : S in dom (iter (A,b1)) } is set
iter (A,1) is Relation-like Function-like set
A is Relation-like Function-like set
dom A is set
S is set
A . S is set
(A,(A . S)) is set
{ ((iter (A,b1)) . (A . S)) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : A . S in dom (iter (A,b1)) } is set
(A,S) is set
{ ((iter (A,b1)) . S) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : S in dom (iter (A,b1)) } is set
T is set
f is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
iter (A,f) is Relation-like Function-like set
(iter (A,f)) . (A . S) is set
dom (iter (A,f)) is set
f + 1 is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
iter (A,(f + 1)) is Relation-like Function-like set
A * (iter (A,f)) is Relation-like Function-like set
(iter (A,(f + 1))) . S is set
dom (iter (A,(f + 1))) is set
A is Relation-like Function-like set
rng A is set
dom A is set
field A is set
(dom A) \/ (rng A) is set
iter (A,0) is Relation-like Function-like set
id (dom A) is Relation-like dom A -defined dom A -valued Function-like one-to-one total quasi_total Element of bool [:(dom A),(dom A):]
[:(dom A),(dom A):] is Relation-like set
bool [:(dom A),(dom A):] is non empty set
dom (iter (A,0)) is set
f is set
f is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
iter (A,f) is Relation-like Function-like set
dom (iter (A,f)) is set
f + 1 is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
iter (A,(f + 1)) is Relation-like Function-like set
dom (iter (A,(f + 1))) is set
P is set
(iter (A,f)) . P is set
rng (iter (A,f)) is set
(iter (A,f)) * A is Relation-like Function-like set
S is set
T is set
f is set
P is set
(dom A) \ f is Element of bool (dom A)
bool (dom A) is non empty set
P is set
(A,P) is set
{ ((iter (A,b1)) . P) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : P in dom (iter (A,b1)) } is set
C is set
I is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
iter (A,I) is Relation-like Function-like set
(iter (A,I)) . P is set
dom (iter (A,I)) is set
I is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,I) is Relation-like Function-like set
(iter (A,I)) . P is set
s is set
r is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,r) is Relation-like Function-like set
(iter (A,r)) . P is set
P is Relation-like Function-like set
dom P is set
f --> T is Relation-like f -defined {T} -valued Function-like total quasi_total Element of bool [:f,{T}:]
{T} is non empty trivial finite 1 -element set
[:f,{T}:] is Relation-like set
bool [:f,{T}:] is non empty set
(f --> T) +* P is Relation-like Function-like set
C is Relation-like Function-like set
dom C is set
dom (f --> T) is Element of bool f
bool f is non empty set
f \/ ((dom A) \ f) is set
I is set
(A,I) is set
{ ((iter (A,b1)) . I) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : I in dom (iter (A,b1)) } is set
C . I is set
(f --> T) . I is set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,s) is Relation-like Function-like set
(iter (A,s)) . I is set
dom (iter (A,s)) is set
P . I is set
r is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,r) is Relation-like Function-like set
(iter (A,r)) . I is set
f is Relation-like Function-like set
dom f is set
P is Relation-like Function-like set
dom P is set
C is set
(A,C) is set
{ ((iter (A,b1)) . C) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : C in dom (iter (A,b1)) } is set
f . C is set
P . C is set
(A,C) is set
{ ((iter (A,b1)) . C) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : C in dom (iter (A,b1)) } is set
I is set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
iter (A,s) is Relation-like Function-like set
(iter (A,s)) . C is set
dom (iter (A,s)) is set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,s) is Relation-like Function-like set
(iter (A,s)) . C is set
r is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,r) is Relation-like Function-like set
(iter (A,r)) . C is set
f . C is set
P . C is set
(A,C) is set
{ ((iter (A,b1)) . C) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : C in dom (iter (A,b1)) } is set
A is Relation-like Function-like set
rng A is set
dom A is set
field A is set
(dom A) \/ (rng A) is set
iter (A,0) is Relation-like Function-like set
id (dom A) is Relation-like dom A -defined dom A -valued Function-like one-to-one total quasi_total Element of bool [:(dom A),(dom A):]
[:(dom A),(dom A):] is Relation-like set
bool [:(dom A),(dom A):] is non empty set
dom (iter (A,0)) is set
f is set
f is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
iter (A,f) is Relation-like Function-like set
dom (iter (A,f)) is set
f + 1 is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
iter (A,(f + 1)) is Relation-like Function-like set
dom (iter (A,(f + 1))) is set
P is set
(iter (A,f)) . P is set
rng (iter (A,f)) is set
(iter (A,f)) * A is Relation-like Function-like set
S is set
T is Relation-like Function-like set
f is set
P is set
(dom A) \ f is Element of bool (dom A)
bool (dom A) is non empty set
P is set
(A,P) is set
{ ((iter (A,b1)) . P) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : P in dom (iter (A,b1)) } is set
C is set
I is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
iter (A,I) is Relation-like Function-like set
(iter (A,I)) . P is set
dom (iter (A,I)) is set
I is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,I) is Relation-like Function-like set
(iter (A,I)) . P is set
s is set
r is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,r) is Relation-like Function-like set
(iter (A,r)) . P is set
P is Relation-like Function-like set
dom P is set
f --> 0 is Relation-like f -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V91() V92() V93() to-naturals Element of bool [:f,NAT:]
[:f,NAT:] is Relation-like RAT -valued INT -valued V91() V92() V93() to-naturals set
bool [:f,NAT:] is non empty set
T | f is Relation-like Function-like set
(f --> 0) +* (T | f) is Relation-like Function-like set
((f --> 0) +* (T | f)) +* P is Relation-like Function-like set
C is Relation-like Function-like set
dom C is set
dom (f --> 0) is Element of bool f
bool f is non empty set
dom ((f --> 0) +* (T | f)) is set
dom (T | f) is set
f \/ (dom (T | f)) is set
f \/ ((dom A) \ f) is set
I is set
(A,I) is set
{ ((iter (A,b1)) . I) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : I in dom (iter (A,b1)) } is set
C . I is set
T . I is set
((f --> 0) +* (T | f)) . I is set
(T | f) . I is set
(f --> 0) . I is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
dom T is set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,s) is Relation-like Function-like set
(iter (A,s)) . I is set
r is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
iter (A,r) is Relation-like Function-like set
dom (iter (A,r)) is set
P . I is set
i is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,i) is Relation-like Function-like set
(iter (A,i)) . I is set
f is Relation-like Function-like set
dom f is set
P is Relation-like Function-like set
dom P is set
C is set
(A,C) is set
{ ((iter (A,b1)) . C) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : C in dom (iter (A,b1)) } is set
f . C is set
T . C is set
P . C is set
(A,C) is set
{ ((iter (A,b1)) . C) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : C in dom (iter (A,b1)) } is set
I is set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
iter (A,s) is Relation-like Function-like set
(iter (A,s)) . C is set
dom (iter (A,s)) is set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,s) is Relation-like Function-like set
(iter (A,s)) . C is set
r is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,r) is Relation-like Function-like set
(iter (A,r)) . C is set
f . C is set
P . C is set
(A,C) is set
{ ((iter (A,b1)) . C) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : C in dom (iter (A,b1)) } is set
A is Relation-like Function-like set
rng A is set
dom A is set
S is Relation-like Function-like set
T is set
(A,T) is set
{ ((iter (A,b1)) . T) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : T in dom (iter (A,b1)) } is set
f is set
(A,f,S) is Relation-like Function-like set
(A,f,S) . T is set
P is set
C is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
iter (A,C) is Relation-like Function-like set
(iter (A,C)) . T is set
dom (iter (A,C)) is set
C is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,C) is Relation-like Function-like set
(iter (A,C)) . T is set
I is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,I) is Relation-like Function-like set
(iter (A,I)) . T is set
I is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,I) is Relation-like Function-like set
(iter (A,I)) . T is set
A is Relation-like Function-like set
rng A is set
dom A is set
S is Relation-like Function-like set
A * S is Relation-like Function-like set
T is set
f is set
(A,f,S) is Relation-like Function-like set
(A,f,S) . T is set
A . T is set
(A,f,S) . (A . T) is set
(A,(A . T)) is set
{ ((iter (A,b1)) . (A . T)) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : A . T in dom (iter (A,b1)) } is set
(A,T) is set
{ ((iter (A,b1)) . T) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : T in dom (iter (A,b1)) } is set
S . (A . T) is set
S . T is set
P is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,P) is Relation-like Function-like set
(iter (A,P)) . T is set
field A is set
(dom A) \/ (rng A) is set
iter (A,0) is Relation-like Function-like set
id (dom A) is Relation-like dom A -defined dom A -valued Function-like one-to-one total quasi_total Element of bool [:(dom A),(dom A):]
[:(dom A),(dom A):] is Relation-like set
bool [:(dom A),(dom A):] is non empty set
0 + 1 is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
C is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
1 + C is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
iter (A,C) is Relation-like Function-like set
A * (iter (A,C)) is Relation-like Function-like set
(iter (A,C)) . (A . T) is set
I is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
I + 1 is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
iter (A,(I + 1)) is Relation-like Function-like set
iter (A,I) is Relation-like Function-like set
A * (iter (A,I)) is Relation-like Function-like set
(iter (A,(I + 1))) . T is set
(iter (A,I)) . (A . T) is set
A is Relation-like Function-like set
rng A is set
dom A is set
S is Relation-like Function-like set
T is set
f is set
(A,f,S) is Relation-like Function-like set
(A,f,S) . T is set
field A is set
(dom A) \/ (rng A) is set
iter (A,0) is Relation-like Function-like set
id (dom A) is Relation-like dom A -defined dom A -valued Function-like one-to-one total quasi_total Element of bool [:(dom A),(dom A):]
[:(dom A),(dom A):] is Relation-like set
bool [:(dom A),(dom A):] is non empty set
(iter (A,0)) . T is set
P is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (A,P) is Relation-like Function-like set
(iter (A,P)) . T is set
A is non empty set
Funcs (A,A) is non empty functional FUNCTION_DOMAIN of A,A
S is Relation-like A -defined A -valued Function-like total quasi_total Element of Funcs (A,A)
T is set
f is Relation-like A -defined A -valued Function-like total quasi_total Element of Funcs (A,A)
(S,T,f) is Relation-like Function-like set
dom S is Element of bool A
bool A is non empty set
rng S is Element of bool A
dom (S,T,f) is set
rng (S,T,f) is set
P is set
C is set
(S,T,f) . C is set
I is Element of A
(S,I) is set
{ ((iter (S,b1)) . I) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : I in dom (iter (S,b1)) } is set
f . I is Element of A
I is Element of A
(S,I) is set
{ ((iter (S,b1)) . I) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : I in dom (iter (S,b1)) } is set
(S,T,f) . I is set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
iter (S,s) is Relation-like Function-like set
(iter (S,s)) . I is set
dom (iter (S,s)) is set
rng (iter (S,s)) is set
I is Element of A
(S,I) is set
{ ((iter (S,b1)) . I) where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : I in dom (iter (S,b1)) } is set
A is non empty set
S is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V91() V92() V93() to-naturals FinSequence of NAT
dom S is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of bool NAT
len S is non empty ordinal natural V22() finite cardinal V79() V80() ext-real positive non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of NAT
Seg (len S) is non empty finite len S -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V145() V146() V147() V148() Element of bool NAT
{ b1 where b1 is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT : ( 1 <= b1 & b1 <= len S ) } is set
the Element of A is Element of A
f is set
P is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
S . P is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
C is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
C -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
(A,A,(C -tuples_on A), the Element of A) is non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total C -ary Element of bool [:(A *),A:]
A * is non empty functional FinSequence-membered FinSequenceSet of A
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
f is Relation-like Function-like set
dom f is set
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng P is finite set
A * is non empty functional FinSequence-membered FinSequenceSet of A
PFuncs ((A *),A) is set
C is set
dom P is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of bool NAT
I is set
P . I is set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
r is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
S . s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
r -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
(A,A,(r -tuples_on A), the Element of A) is non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total r -ary Element of bool [:(A *),A:]
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
dom (A,A,(r -tuples_on A), the Element of A) is non empty functional FinSequence-membered with_common_domain Element of bool (A *)
bool (A *) is non empty set
rng (A,A,(r -tuples_on A), the Element of A) is non empty Element of bool A
bool A is non empty set
{ the Element of A} is non empty trivial finite 1 -element set
C is Relation-like NAT -defined PFuncs ((A *),A) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs ((A *),A)
UAStr(# A,C #) is non empty strict UAStr
the carrier of UAStr(# A,C #) is non empty set
the carrier of UAStr(# A,C #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# A,C #)
[:( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #):] is non empty Relation-like set
bool [:( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #):] is non empty set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
the charact of UAStr(# A,C #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #))
PFuncs (( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #)) is set
dom the charact of UAStr(# A,C #) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of bool NAT
the charact of UAStr(# A,C #) . s is set
r is Relation-like the carrier of UAStr(# A,C #) * -defined the carrier of UAStr(# A,C #) -valued Function-like Element of bool [:( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #):]
i is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
S . i is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
s -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
(A,A,(s -tuples_on A), the Element of A) is non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total s -ary Element of bool [:(A *),A:]
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
the charact of UAStr(# A,C #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #))
the carrier of UAStr(# A,C #) is non empty set
the carrier of UAStr(# A,C #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# A,C #)
PFuncs (( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #)) is set
rng the charact of UAStr(# A,C #) is finite Element of bool (PFuncs (( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #)))
bool (PFuncs (( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #))) is non empty set
dom C is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of bool NAT
s is set
C . s is set
r is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
i is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
S . r is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
i -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
(A,A,(i -tuples_on A), the Element of A) is non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total i -ary Element of bool [:(A *),A:]
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
the carrier of UAStr(# A,C #) is non empty set
the carrier of UAStr(# A,C #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# A,C #)
[:( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #):] is non empty Relation-like set
bool [:( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #):] is non empty set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
the charact of UAStr(# A,C #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #))
PFuncs (( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #)) is set
dom the charact of UAStr(# A,C #) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of bool NAT
the charact of UAStr(# A,C #) . s is set
r is Relation-like the carrier of UAStr(# A,C #) * -defined the carrier of UAStr(# A,C #) -valued Function-like Element of bool [:( the carrier of UAStr(# A,C #) *), the carrier of UAStr(# A,C #):]
i is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
s is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
S . i is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
s -tuples_on A is non empty functional FinSequence-membered with_common_domain product-like FinSequenceSet of A
(A,A,(s -tuples_on A), the Element of A) is non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total s -ary Element of bool [:(A *),A:]
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
s is non empty partial quasi_total non-empty UAStr
the carrier of s is non empty set
signature s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V91() V92() V93() to-naturals FinSequence of NAT
len C is ordinal natural V22() finite cardinal V79() V80() ext-real non negative V89() V90() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() Element of NAT
r is ordinal natural V22() finite cardinal V79() V80() ext-real non negative set
the carrier of s * is non empty functional FinSequence-membered FinSequenceSet of the carrier of s
[:( the carrier of s *), the carrier of s:] is non empty Relation-like set
bool [:( the carrier of s *), the carrier of s:] is non empty set
i is non empty Relation-like the carrier of s * -defined the carrier of s -valued Function-like homogeneous Element of bool [:( the carrier of s *), the carrier of s:]
the charact of s is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of s