:: AOFA_000 semantic presentation

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 )

{ b

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

{ b

{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

{ H

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,b

A is Relation-like Function-like set

dom A is set

S is set

(A,S) is set

{ ((iter (A,b

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,b

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,b

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,b

(A,S) is set

{ ((iter (A,b

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,b

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,b

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,b

f . C is set

P . C is set

(A,C) is set

{ ((iter (A,b

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,b

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,b

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,b

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,b

f . C is set

T . C is set

P . C is set

(A,C) is set

{ ((iter (A,b

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,b

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,b

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,b

(A,T) is set

{ ((iter (A,b

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,b

f . I is Element of A

I is Element of A

(S,I) is set

{ ((iter (S,b

(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,b

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

{ b

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