:: CATALG_1 semantic presentation

REAL is set

NAT is V6() V7() V8() non empty Element of bool REAL

bool REAL is non empty set

NAT is V6() V7() V8() non empty set

bool NAT is non empty set

bool NAT is non empty set

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

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

bool (bool REAL) is non empty set

{} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty V24() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V78() set

the Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty V24() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V78() set is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty V24() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V78() set

1 is V6() V7() V8() V12() non empty Element of NAT

{{},1} is non empty set

K387() is set

bool K387() is non empty set

K388() is Element of bool K387()

K428() is non empty V161() L15()

the carrier of K428() is non empty set

K391( the carrier of K428()) is non empty M36( the carrier of K428())

K427(K428()) is Element of bool K391( the carrier of K428())

bool K391( the carrier of K428()) is non empty set

[:K427(K428()),NAT:] is Relation-like set

bool [:K427(K428()),NAT:] is non empty set

[:NAT,K427(K428()):] is Relation-like set

bool [:NAT,K427(K428()):] is non empty set

2 is V6() V7() V8() V12() non empty Element of NAT

3 is V6() V7() V8() V12() non empty Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty V24() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V78() Element of NAT

Seg 1 is non empty V24() V31(1) Element of bool NAT

{1} is non empty set

Seg 2 is non empty V24() V31(2) Element of bool NAT

{1,2} is non empty set

Seg 3 is non empty V24() V31(3) Element of bool NAT

{1,2,3} is non empty set

product {} is set

{{}} is functional non empty set

C1 is set

F is Relation-like Function-like set

C2 is Relation-like Function-like set

S1 is Relation-like C1 -defined Function-like total set

S2 is set

proj1 S1 is set

S1 . S2 is set

dom S1 is Element of bool C1

bool C1 is non empty set

C2 . S2 is set

F | (C2 . S2) is Relation-like Function-like set

S1 is Relation-like C1 -defined Function-like total Function-yielding V78() set

S2 is Relation-like C1 -defined Function-like total Function-yielding V78() set

A1 is set

S1 . A1 is Relation-like Function-like set

C2 . A1 is set

F | (C2 . A1) is Relation-like Function-like set

S2 . A1 is Relation-like Function-like set

C1 is set

C2 is Relation-like C1 -defined Function-like total set

Union C2 is set

id (Union C2) is Relation-like Union C2 -defined Union C2 -valued Function-like one-to-one total V36( Union C2, Union C2) Element of bool [:(Union C2),(Union C2):]

[:(Union C2),(Union C2):] is Relation-like set

bool [:(Union C2),(Union C2):] is non empty set

(C1,C2,(id (Union C2))) is Relation-like C1 -defined Function-like total Function-yielding V78() set

id C2 is Relation-like C1 -defined Function-like total Function-yielding V78() ManySortedFunction of C2,C2

proj2 C2 is set

union (proj2 C2) is set

S2 is set

dom C2 is Element of bool C1

bool C1 is non empty set

C2 . S2 is set

(C1,C2,(id (Union C2))) . S2 is Relation-like Function-like set

(id (Union C2)) | (C2 . S2) is Relation-like Union C2 -defined C2 . S2 -defined Union C2 -defined Union C2 -valued Function-like Element of bool [:(Union C2),(Union C2):]

(id C2) . S2 is Relation-like Function-like set

id (C2 . S2) is Relation-like C2 . S2 -defined C2 . S2 -valued Function-like one-to-one total V36(C2 . S2,C2 . S2) Element of bool [:(C2 . S2),(C2 . S2):]

[:(C2 . S2),(C2 . S2):] is Relation-like set

bool [:(C2 . S2),(C2 . S2):] is non empty set

C1 is set

C2 is Relation-like C1 -defined Function-like total set

F is Relation-like C1 -defined Function-like total set

S1 is Relation-like Function-like set

(C1,C2,S1) is Relation-like C1 -defined Function-like total Function-yielding V78() set

rngs (C1,C2,S1) is Relation-like C1 -defined Function-like total set

S2 is Relation-like Function-like set

S1 * S2 is Relation-like Function-like set

(C1,C2,(S1 * S2)) is Relation-like C1 -defined Function-like total Function-yielding V78() set

(C1,F,S2) is Relation-like C1 -defined Function-like total Function-yielding V78() set

(C1,F,S2) ** (C1,C2,S1) is Relation-like Function-like Function-yielding V78() set

C1 /\ C1 is set

dom (C1,F,S2) is Element of bool C1

bool C1 is non empty set

dom (C1,C2,S1) is Element of bool C1

proj1 ((C1,F,S2) ** (C1,C2,S1)) is set

A1 is set

(C1,C2,S1) . A1 is Relation-like Function-like set

C2 . A1 is set

S1 | (C2 . A1) is Relation-like Function-like set

(rngs (C1,C2,S1)) . A1 is set

proj2 (S1 | (C2 . A1)) is set

F . A1 is set

(S1 * S2) | (C2 . A1) is Relation-like Function-like set

(S1 | (C2 . A1)) * S2 is Relation-like Function-like set

(F . A1) |` (S1 | (C2 . A1)) is Relation-like Function-like set

S2 | (F . A1) is Relation-like Function-like set

(S1 | (C2 . A1)) * (S2 | (F . A1)) is Relation-like Function-like set

(C1,C2,(S1 * S2)) . A1 is Relation-like Function-like set

(C1,F,S2) . A1 is Relation-like Function-like set

((C1,F,S2) ** (C1,C2,S1)) . A1 is Relation-like Function-like set

dom (C1,C2,(S1 * S2)) is Element of bool C1

C1 is Relation-like Function-like set

proj1 C1 is set

C2 is set

F is Relation-like C2 -defined Function-like total set

S1 is Relation-like C2 -defined Function-like total set

(C2,F,C1) is Relation-like C2 -defined Function-like total Function-yielding V78() set

S2 is set

(C2,F,C1) . S2 is Relation-like Function-like set

F . S2 is set

S1 . S2 is set

[:(F . S2),(S1 . S2):] is Relation-like set

bool [:(F . S2),(S1 . S2):] is non empty set

C1 | (F . S2) is Relation-like Function-like set

C1 .: (F . S2) is set

proj2 ((C2,F,C1) . S2) is set

proj1 ((C2,F,C1) . S2) is set

C1 is set

<*C1*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

C2 is set

<*C2*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

<*C1*> . 1 is set

C1 is non empty feasible feasible ManySortedSign

C1 is non empty feasible feasible ManySortedSign

C2 is MSAlgebra over C1

the Sorts of C2 is Relation-like the carrier of C1 -defined Function-like non empty total set

the carrier of C1 is non empty set

C1 is non empty non void feasible feasible ManySortedSign

the carrier of C1 is non empty set

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

FreeMSA the Relation-like non-empty non empty-yielding the carrier of C1 -defined Function-like non empty total set is strict non-empty disjoint_valued (C1) MSAlgebra over C1

C1 is non empty non void feasible feasible ManySortedSign

C2 is (C1) MSAlgebra over C1

the Sorts of C2 is Relation-like the carrier of C1 -defined Function-like non empty total set

the carrier of C1 is non empty set

the non empty non void feasible feasible ManySortedSign is non empty non void feasible feasible ManySortedSign

the ( the non empty non void feasible feasible ManySortedSign ) MSAlgebra over the non empty non void feasible feasible ManySortedSign is ( the non empty non void feasible feasible ManySortedSign ) MSAlgebra over the non empty non void feasible feasible ManySortedSign

the Sorts of the ( the non empty non void feasible feasible ManySortedSign ) MSAlgebra over the non empty non void feasible feasible ManySortedSign is Relation-like non empty-yielding the carrier of the non empty non void feasible feasible ManySortedSign -defined Function-like non empty total set

the carrier of the non empty non void feasible feasible ManySortedSign is non empty set

{0} is functional non empty set

C1 is set

2 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{0},(2 -tuples_on C1):] is Relation-like set

1 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{1},(1 -tuples_on C1):] is Relation-like set

{2} is non empty set

3 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{2},(3 -tuples_on C1):] is Relation-like set

[:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] is Relation-like set

[:{0},(2 -tuples_on C1):] * is functional non empty FinSequence-membered FinSequenceSet of [:{0},(2 -tuples_on C1):]

C2 is set

C2 `2 is set

C1 * is functional non empty FinSequence-membered FinSequenceSet of C1

{ b

F is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty V24() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V78() set

S1 is Relation-like NAT -defined C1 -valued Function-like V24() FinSequence-like FinSubsequence-like Element of C1 *

len S1 is V6() V7() V8() V12() Element of NAT

S1 . 1 is set

S2 is set

<*S2*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[1,<*S2*>] is V21() set

{1,<*S2*>} is non empty set

{{1,<*S2*>},{1}} is non empty set

A1 is set

<*S2,A1*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*S2,A1*>] is V21() set

{0,<*S2,A1*>} is functional non empty set

{{0,<*S2,A1*>},{0}} is non empty set

A2 is set

<*S2,A1,A2*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set

[2,<*S2,A1,A2*>] is V21() set

{2,<*S2,A1,A2*>} is non empty set

{{2,<*S2,A1,A2*>},{2}} is non empty set

<*A1,A2*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*A1,A2*>] is V21() set

{0,<*A1,A2*>} is functional non empty set

{{0,<*A1,A2*>},{0}} is non empty set

<*[0,<*A1,A2*>],[0,<*S2,A1*>]*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

{S2} is non empty set

rng S1 is Element of bool C1

bool C1 is non empty set

C2 `1 is set

C2 `2 is set

C1 * is functional non empty FinSequence-membered FinSequenceSet of C1

{ b

F is Relation-like NAT -defined C1 -valued Function-like V24() FinSequence-like FinSubsequence-like Element of C1 *

len F is V6() V7() V8() V12() Element of NAT

F . 1 is set

F . 2 is set

F . 3 is set

<*(F . 1),(F . 2),(F . 3)*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set

rng F is Element of bool C1

bool C1 is non empty set

{(F . 1),(F . 2),(F . 3)} is non empty set

<*(F . 2),(F . 3)*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*(F . 2),(F . 3)*>] is V21() set

{0,<*(F . 2),(F . 3)*>} is functional non empty set

{{0,<*(F . 2),(F . 3)*>},{0}} is non empty set

<*(F . 1),(F . 2)*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*(F . 1),(F . 2)*>] is V21() set

{0,<*(F . 1),(F . 2)*>} is functional non empty set

{{0,<*(F . 1),(F . 2)*>},{0}} is non empty set

<*[0,<*(F . 2),(F . 3)*>],[0,<*(F . 1),(F . 2)*>]*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

A2 is non empty set

2 -tuples_on A2 is functional non empty FinSequence-membered FinSequenceSet of A2

[:{0},(2 -tuples_on A2):] is Relation-like non empty set

G is Element of [:{0},(2 -tuples_on A2):]

<*G*> is Relation-like NAT -defined [:{0},(2 -tuples_on A2):] -valued Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like FinSequence of [:{0},(2 -tuples_on A2):]

B1 is Element of [:{0},(2 -tuples_on A2):]

<*B1*> is Relation-like NAT -defined [:{0},(2 -tuples_on A2):] -valued Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like FinSequence of [:{0},(2 -tuples_on A2):]

<*G*> ^ <*B1*> is Relation-like NAT -defined [:{0},(2 -tuples_on A2):] -valued Function-like non empty V24() FinSequence-like FinSubsequence-like FinSequence of [:{0},(2 -tuples_on A2):]

<*(F . 1)*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[1,<*(F . 1)*>] is V21() set

{1,<*(F . 1)*>} is non empty set

{{1,<*(F . 1)*>},{1}} is non empty set

[2,<*(F . 1),(F . 2),(F . 3)*>] is V21() set

{2,<*(F . 1),(F . 2),(F . 3)*>} is non empty set

{{2,<*(F . 1),(F . 2),(F . 3)*>},{2}} is non empty set

C2 `1 is set

C2 is Relation-like Function-like set

proj1 C2 is set

proj2 C2 is set

[:([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),([:{0},(2 -tuples_on C1):] *):] is Relation-like set

bool [:([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),([:{0},(2 -tuples_on C1):] *):] is non empty set

S1 is set

S1 `2 is set

C1 * is functional non empty FinSequence-membered FinSequenceSet of C1

{ b

S2 is Relation-like NAT -defined C1 -valued Function-like V24() FinSequence-like FinSubsequence-like Element of C1 *

len S2 is V6() V7() V8() V12() Element of NAT

S2 . 1 is set

<*(S2 . 1)*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

{(S2 . 1)} is non empty set

rng S2 is Element of bool C1

bool C1 is non empty set

<*(S2 . 1),(S2 . 1)*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*(S2 . 1),(S2 . 1)*>] is V21() set

{0,<*(S2 . 1),(S2 . 1)*>} is functional non empty set

{{0,<*(S2 . 1),(S2 . 1)*>},{0}} is non empty set

G is V21() set

B1 is non empty set

H is Element of B1

<*H,H*> is Relation-like NAT -defined B1 -valued Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like FinSequence of B1

2 -tuples_on B1 is functional non empty FinSequence-membered FinSequenceSet of B1

<*H*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[1,<*H*>] is V21() set

{1,<*H*>} is non empty set

{{1,<*H*>},{1}} is non empty set

<*H,H*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*H,H*>] is V21() set

{0,<*H,H*>} is functional non empty set

{{0,<*H,H*>},{0}} is non empty set

<*H,(S2 . 1),(S2 . 1)*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set

[2,<*H,(S2 . 1),(S2 . 1)*>] is V21() set

{2,<*H,(S2 . 1),(S2 . 1)*>} is non empty set

{{2,<*H,(S2 . 1),(S2 . 1)*>},{2}} is non empty set

<*H,(S2 . 1)*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*H,(S2 . 1)*>] is V21() set

{0,<*H,(S2 . 1)*>} is functional non empty set

{{0,<*H,(S2 . 1)*>},{0}} is non empty set

S1 `1 is set

<*H*> is Relation-like NAT -defined B1 -valued Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like FinSequence of B1

[1,<*H*>] is V21() set

{1,<*H*>} is non empty set

{{1,<*H*>},{1}} is non empty set

[0,<*H,H*>] is V21() set

{0,<*H,H*>} is functional non empty set

{{0,<*H,H*>},{0}} is non empty set

S1 `2 is set

C1 * is functional non empty FinSequence-membered FinSequenceSet of C1

{ b

S2 is Relation-like NAT -defined C1 -valued Function-like V24() FinSequence-like FinSubsequence-like Element of C1 *

len S2 is V6() V7() V8() V12() Element of NAT

S2 . 1 is set

S2 . 2 is set

S2 . 3 is set

<*(S2 . 1),(S2 . 2),(S2 . 3)*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set

rng S2 is Element of bool C1

bool C1 is non empty set

{(S2 . 1),(S2 . 2),(S2 . 3)} is non empty set

<*(S2 . 1),(S2 . 3)*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*(S2 . 1),(S2 . 3)*>] is V21() set

{0,<*(S2 . 1),(S2 . 3)*>} is functional non empty set

{{0,<*(S2 . 1),(S2 . 3)*>},{0}} is non empty set

B1 is V21() set

G is non empty set

2 -tuples_on G is functional non empty FinSequence-membered FinSequenceSet of G

<*(S2 . 1)*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[1,<*(S2 . 1)*>] is V21() set

{1,<*(S2 . 1)*>} is non empty set

{{1,<*(S2 . 1)*>},{1}} is non empty set

<*(S2 . 1),(S2 . 1)*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*(S2 . 1),(S2 . 1)*>] is V21() set

{0,<*(S2 . 1),(S2 . 1)*>} is functional non empty set

{{0,<*(S2 . 1),(S2 . 1)*>},{0}} is non empty set

[2,<*(S2 . 1),(S2 . 2),(S2 . 3)*>] is V21() set

{2,<*(S2 . 1),(S2 . 2),(S2 . 3)*>} is non empty set

{{2,<*(S2 . 1),(S2 . 2),(S2 . 3)*>},{2}} is non empty set

S1 `1 is set

S1 is Relation-like Function-like set

proj1 S1 is set

proj2 S1 is set

[:([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),[:{0},(2 -tuples_on C1):]:] is Relation-like set

bool [:([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),[:{0},(2 -tuples_on C1):]:] is non empty set

F is Relation-like [:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] -defined [:{0},(2 -tuples_on C1):] * -valued Function-like total V36([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):],[:{0},(2 -tuples_on C1):] * ) Function-yielding V78() Element of bool [:([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),([:{0},(2 -tuples_on C1):] *):]

S2 is Relation-like [:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] -defined [:{0},(2 -tuples_on C1):] -valued Function-like V36([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):],[:{0},(2 -tuples_on C1):]) Element of bool [:([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),[:{0},(2 -tuples_on C1):]:]

ManySortedSign(# [:{0},(2 -tuples_on C1):],([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),F,S2 #) is strict ManySortedSign

A1 is strict ManySortedSign

the carrier of A1 is set

the carrier' of A1 is set

the Arity of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 * -valued Function-like total V36( the carrier' of A1, the carrier of A1 * ) Function-yielding V78() Element of bool [: the carrier' of A1,( the carrier of A1 *):]

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

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

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

the ResultSort of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 -valued Function-like V36( the carrier' of A1, the carrier of A1) Element of bool [: the carrier' of A1, the carrier of A1:]

[: the carrier' of A1, the carrier of A1:] is Relation-like set

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

A2 is set

f is non empty set

G is Element of f

<*G*> is Relation-like NAT -defined f -valued Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like FinSequence of f

1 -tuples_on f is functional non empty FinSequence-membered FinSequenceSet of f

<*A2*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[1,<*A2*>] is V21() set

{1,<*A2*>} is non empty set

{{1,<*A2*>},{1}} is non empty set

S2 . [1,<*A2*>] is set

B1 is set

H is set

o is set

<*B1*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[1,<*B1*>] is V21() set

{1,<*B1*>} is non empty set

{{1,<*B1*>},{1}} is non empty set

<*B1,B1*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*B1,B1*>] is V21() set

{0,<*B1,B1*>} is functional non empty set

{{0,<*B1,B1*>},{0}} is non empty set

<*B1,H,o*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set

[2,<*B1,H,o*>] is V21() set

{2,<*B1,H,o*>} is non empty set

{{2,<*B1,H,o*>},{2}} is non empty set

<*B1,o*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*B1,o*>] is V21() set

{0,<*B1,o*>} is functional non empty set

{{0,<*B1,o*>},{0}} is non empty set

F . [1,<*A2*>] is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

the Arity of A1 . [1,<*A2*>] is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

x is set

a is set

b is set

<*x*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[1,<*x*>] is V21() set

{1,<*x*>} is non empty set

{{1,<*x*>},{1}} is non empty set

<*x,a,b*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set

[2,<*x,a,b*>] is V21() set

{2,<*x,a,b*>} is non empty set

{{2,<*x,a,b*>},{2}} is non empty set

<*a,b*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*a,b*>] is V21() set

{0,<*a,b*>} is functional non empty set

{{0,<*a,b*>},{0}} is non empty set

<*x,a*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*x,a*>] is V21() set

{0,<*x,a*>} is functional non empty set

{{0,<*x,a*>},{0}} is non empty set

<*[0,<*a,b*>],[0,<*x,a*>]*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

<*A2*> . 1 is set

<*B1*> . 1 is set

the ResultSort of A1 . [1,<*A2*>] is set

<*A2,A2*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*A2,A2*>] is V21() set

{0,<*A2,A2*>} is functional non empty set

{{0,<*A2,A2*>},{0}} is non empty set

A2 is set

f is set

G is set

<*A2,f,G*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set

[2,<*A2,f,G*>] is V21() set

{2,<*A2,f,G*>} is non empty set

{{2,<*A2,f,G*>},{2}} is non empty set

the Arity of A1 . [2,<*A2,f,G*>] is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

<*f,G*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*f,G*>] is V21() set

{0,<*f,G*>} is functional non empty set

{{0,<*f,G*>},{0}} is non empty set

<*A2,f*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*A2,f*>] is V21() set

{0,<*A2,f*>} is functional non empty set

{{0,<*A2,f*>},{0}} is non empty set

<*[0,<*f,G*>],[0,<*A2,f*>]*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

the ResultSort of A1 . [2,<*A2,f,G*>] is set

<*A2,G*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*A2,G*>] is V21() set

{0,<*A2,G*>} is functional non empty set

{{0,<*A2,G*>},{0}} is non empty set

B1 is non empty set

H is Element of B1

o is Element of B1

x is Element of B1

<*H,o,x*> is Relation-like NAT -defined B1 -valued Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like FinSequence of B1

3 -tuples_on B1 is functional non empty FinSequence-membered FinSequenceSet of B1

F . [2,<*A2,f,G*>] is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

a is set

b is set

c is set

<*a*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[1,<*a*>] is V21() set

{1,<*a*>} is non empty set

{{1,<*a*>},{1}} is non empty set

<*a,b,c*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set

[2,<*a,b,c*>] is V21() set

{2,<*a,b,c*>} is non empty set

{{2,<*a,b,c*>},{2}} is non empty set

<*b,c*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*b,c*>] is V21() set

{0,<*b,c*>} is functional non empty set

{{0,<*b,c*>},{0}} is non empty set

<*a,b*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*a,b*>] is V21() set

{0,<*a,b*>} is functional non empty set

{{0,<*a,b*>},{0}} is non empty set

<*[0,<*b,c*>],[0,<*a,b*>]*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

<*A2*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

<*f*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

<*A2*> ^ <*f*> is Relation-like NAT -defined Function-like non empty V24() FinSequence-like FinSubsequence-like set

<*G*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

(<*A2*> ^ <*f*>) ^ <*G*> is Relation-like NAT -defined Function-like non empty V24() FinSequence-like FinSubsequence-like set

<*b*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

<*a*> ^ <*b*> is Relation-like NAT -defined Function-like non empty V24() FinSequence-like FinSubsequence-like set

<*c*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

(<*a*> ^ <*b*>) ^ <*c*> is Relation-like NAT -defined Function-like non empty V24() FinSequence-like FinSubsequence-like set

S2 . [2,<*A2,f,G*>] is set

g is set

h is set

gh is set

<*g*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[1,<*g*>] is V21() set

{1,<*g*>} is non empty set

{{1,<*g*>},{1}} is non empty set

<*g,g*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*g,g*>] is V21() set

{0,<*g,g*>} is functional non empty set

{{0,<*g,g*>},{0}} is non empty set

<*g,h,gh*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set

[2,<*g,h,gh*>] is V21() set

{2,<*g,h,gh*>} is non empty set

{{2,<*g,h,gh*>},{2}} is non empty set

<*g,gh*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*g,gh*>] is V21() set

{0,<*g,gh*>} is functional non empty set

{{0,<*g,gh*>},{0}} is non empty set

<*A2,f,G*> . 1 is set

<*g,h,gh*> . 1 is set

<*A2,f,G*> . 3 is set

C2 is strict ManySortedSign

the carrier of C2 is set

the carrier' of C2 is set

the Arity of C2 is Relation-like the carrier' of C2 -defined the carrier of C2 * -valued Function-like total V36( the carrier' of C2, the carrier of C2 * ) Function-yielding V78() Element of bool [: the carrier' of C2,( the carrier of C2 *):]

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

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

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

the ResultSort of C2 is Relation-like the carrier' of C2 -defined the carrier of C2 -valued Function-like V36( the carrier' of C2, the carrier of C2) Element of bool [: the carrier' of C2, the carrier of C2:]

[: the carrier' of C2, the carrier of C2:] is Relation-like set

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

F is strict ManySortedSign

the carrier of F is set

the carrier' of F is set

the Arity of F is Relation-like the carrier' of F -defined the carrier of F * -valued Function-like total V36( the carrier' of F, the carrier of F * ) Function-yielding V78() Element of bool [: the carrier' of F,( the carrier of F *):]

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

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

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

the ResultSort of F is Relation-like the carrier' of F -defined the carrier of F -valued Function-like V36( the carrier' of F, the carrier of F) Element of bool [: the carrier' of F, the carrier of F:]

[: the carrier' of F, the carrier of F:] is Relation-like set

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

S1 is set

S1 `1 is set

S1 `2 is set

S2 is set

A1 is set

A2 is set

<*S2,A1,A2*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set

[2,(S1 `2)] is V21() set

{2,(S1 `2)} is non empty set

{{2,(S1 `2)},{2}} is non empty set

the Arity of C2 . [2,(S1 `2)] is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

<*A1,A2*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*A1,A2*>] is V21() set

{0,<*A1,A2*>} is functional non empty set

{{0,<*A1,A2*>},{0}} is non empty set

<*S2,A1*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*S2,A1*>] is V21() set

{0,<*S2,A1*>} is functional non empty set

{{0,<*S2,A1*>},{0}} is non empty set

<*[0,<*A1,A2*>],[0,<*S2,A1*>]*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

the Arity of F . [2,(S1 `2)] is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[1,(S1 `2)] is V21() set

{1,(S1 `2)} is non empty set

{{1,(S1 `2)},{1}} is non empty set

the Arity of C2 . [1,(S1 `2)] is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

the Arity of F . [1,(S1 `2)] is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

S2 is set

<*S2*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

S2 is set

<*S2*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[(S1 `1),(S1 `2)] is V21() set

{(S1 `1),(S1 `2)} is non empty set

{(S1 `1)} is non empty set

{{(S1 `1),(S1 `2)},{(S1 `1)}} is non empty set

the Arity of C2 . S1 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

the Arity of F . S1 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

S1 is set

S1 `1 is set

S1 `2 is set

S2 is set

A1 is set

A2 is set

<*S2,A1,A2*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set

[2,(S1 `2)] is V21() set

{2,(S1 `2)} is non empty set

{{2,(S1 `2)},{2}} is non empty set

the ResultSort of C2 . [2,(S1 `2)] is set

<*S2,A2*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*S2,A2*>] is V21() set

{0,<*S2,A2*>} is functional non empty set

{{0,<*S2,A2*>},{0}} is non empty set

the ResultSort of F . [2,(S1 `2)] is set

S2 is set

<*S2*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[1,(S1 `2)] is V21() set

{1,(S1 `2)} is non empty set

{{1,(S1 `2)},{1}} is non empty set

the ResultSort of C2 . [1,(S1 `2)] is set

<*S2,S2*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*S2,S2*>] is V21() set

{0,<*S2,S2*>} is functional non empty set

{{0,<*S2,S2*>},{0}} is non empty set

the ResultSort of F . [1,(S1 `2)] is set

[(S1 `1),(S1 `2)] is V21() set

{(S1 `1),(S1 `2)} is non empty set

{(S1 `1)} is non empty set

{{(S1 `1),(S1 `2)},{(S1 `1)}} is non empty set

the ResultSort of C2 . S1 is set

the ResultSort of F . S1 is set

dom the Arity of C2 is Element of bool the carrier' of C2

bool the carrier' of C2 is non empty set

dom the Arity of F is Element of bool the carrier' of F

bool the carrier' of F is non empty set

dom the ResultSort of C2 is Element of bool the carrier' of C2

dom the ResultSort of F is Element of bool the carrier' of F

C1 is set

(C1) is strict ManySortedSign

the carrier of (C1) is set

the carrier' of (C1) is set

2 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{0},(2 -tuples_on C1):] is Relation-like set

1 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

3 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{1},(1 -tuples_on C1):] is Relation-like set

[:{2},(3 -tuples_on C1):] is Relation-like set

[:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] is Relation-like set

C1 is non empty set

(C1) is strict feasible ManySortedSign

the carrier of (C1) is set

2 -tuples_on C1 is functional non empty FinSequence-membered FinSequenceSet of C1

[:{0},(2 -tuples_on C1):] is Relation-like non empty set

the carrier' of (C1) is set

1 -tuples_on C1 is functional non empty FinSequence-membered FinSequenceSet of C1

[:{1},(1 -tuples_on C1):] is Relation-like non empty set

3 -tuples_on C1 is functional non empty FinSequence-membered FinSequenceSet of C1

[:{2},(3 -tuples_on C1):] is Relation-like non empty set

[:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] is Relation-like non empty set

C1 is non empty feasible feasible ManySortedSign

the carrier of C1 is non empty set

C2 is set

(C2) is strict feasible ManySortedSign

2 -tuples_on C2 is functional FinSequence-membered FinSequenceSet of C2

[:{0},(2 -tuples_on C2):] is Relation-like set

the Element of the carrier of C1 is Element of the carrier of C1

S1 is set

S2 is set

[S1,S2] is V21() set

{S1,S2} is non empty set

{S1} is non empty set

{{S1,S2},{S1}} is non empty set

C2 * is functional non empty FinSequence-membered FinSequenceSet of C2

{ b

A1 is Relation-like NAT -defined C2 -valued Function-like V24() FinSequence-like FinSubsequence-like Element of C2 *

len A1 is V6() V7() V8() V12() Element of NAT

dom A1 is Element of bool NAT

A1 . 1 is set

rng A1 is Element of bool C2

bool C2 is non empty set

A2 is non empty set

the carrier' of (C2) is set

1 -tuples_on C2 is functional FinSequence-membered FinSequenceSet of C2

[:{1},(1 -tuples_on C2):] is Relation-like set

3 -tuples_on C2 is functional FinSequence-membered FinSequenceSet of C2

[:{2},(3 -tuples_on C2):] is Relation-like set

[:{1},(1 -tuples_on C2):] \/ [:{2},(3 -tuples_on C2):] is Relation-like set

f is Element of A2

<*f*> is Relation-like NAT -defined A2 -valued Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like FinSequence of A2

1 -tuples_on A2 is functional non empty FinSequence-membered FinSequenceSet of A2

the carrier' of C1 is set

({{}}) is non empty non void feasible strict feasible ManySortedSign

C1 is non empty non void feasible strict feasible ManySortedSign

the carrier of C1 is non empty set

2 -tuples_on {{}} is functional non empty FinSequence-membered FinSequenceSet of {{}}

[:{0},(2 -tuples_on {{}}):] is Relation-like non empty set

C1 is set

(C1) is strict feasible ManySortedSign

2 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{0},(2 -tuples_on C1):] is Relation-like set

the carrier of (C1) is set

F is feasible () ManySortedSign

the carrier of F is set

C1 is set

C2 is set

F is feasible (C1)

(C2) is strict feasible ManySortedSign

the carrier of F is set

2 -tuples_on C2 is functional FinSequence-membered FinSequenceSet of C2

[:{0},(2 -tuples_on C2):] is Relation-like set

2 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{0},(2 -tuples_on C1):] is Relation-like set

S1 is set

<*S1,S1*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

S1 is set

<*S1,S1*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

C1 is set

C2 is feasible (C1)

(C1) is strict feasible ManySortedSign

the carrier of C2 is set

2 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{0},(2 -tuples_on C1):] is Relation-like set

C1 is non empty set

C2 is feasible () (C1)

(C1) is non empty non void feasible strict feasible ManySortedSign

the carrier of (C1) is non empty set

the carrier of C2 is set

C1 is set

(C1) is strict feasible ManySortedSign

the carrier of (C1) is set

2 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{0},(2 -tuples_on C1):] is Relation-like set

C1 is set

(C1) is strict feasible ManySortedSign

the carrier of (C1) is set

2 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{0},(2 -tuples_on C1):] is Relation-like set

C1 is ManySortedSign

the carrier of C1 is set

the carrier' of C1 is set

the carrier of C1 \/ the carrier' of C1 is set

proj2 ( the carrier of C1 \/ the carrier' of C1) is set

SubFuncs (proj2 ( the carrier of C1 \/ the carrier' of C1)) is set

union (SubFuncs (proj2 ( the carrier of C1 \/ the carrier' of C1))) is set

proj2 (union (SubFuncs (proj2 ( the carrier of C1 \/ the carrier' of C1)))) is set

F is set

S1 is set

S2 is set

[S2,S1] is V21() set

{S2,S1} is non empty set

{S2} is non empty set

{{S2,S1},{S2}} is non empty set

A1 is set

A2 is Relation-like Function-like set

f is set

[f,A2] is V21() set

{f,A2} is non empty set

{f} is non empty set

{{f,A2},{f}} is non empty set

G is set

B1 is Relation-like Function-like set

[G,B1] is V21() set

{G,B1} is non empty set

{G} is non empty set

{{G,B1},{G}} is non empty set

proj2 B1 is set

S2 is set

A1 is Relation-like Function-like set

[S2,A1] is V21() set

{S2,A1} is non empty set

{S2} is non empty set

{{S2,A1},{S2}} is non empty set

proj2 A1 is set

A2 is set

[A2,S1] is V21() set

{A2,S1} is non empty set

{A2} is non empty set

{{A2,S1},{A2}} is non empty set

C1 is set

(C1) is strict feasible () (C1)

((C1)) is set

the carrier' of (C1) is set

1 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{1},(1 -tuples_on C1):] is Relation-like set

3 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{2},(3 -tuples_on C1):] is Relation-like set

[:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] is Relation-like set

F is set

the carrier of (C1) is set

the carrier of (C1) \/ the carrier' of (C1) is set

S1 is set

S2 is Relation-like Function-like set

[S1,S2] is V21() set

{S1,S2} is non empty set

{S1} is non empty set

{{S1,S2},{S1}} is non empty set

proj2 S2 is set

2 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{0},(2 -tuples_on C1):] is Relation-like set

F is set

<*F,F*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*F,F*>] is V21() set

{0,<*F,F*>} is functional non empty set

{{0,<*F,F*>},{0}} is non empty set

proj2 <*F,F*> is non empty set

{F,F} is non empty set

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

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

C1 is set

(C1) is strict feasible () (C1)

A1 is set

F is set

S1 is set

S2 is set

F is set

F is Relation-like Function-like set

proj1 F is set

proj2 F is set

S1 is Relation-like NAT -defined NAT -valued Function-like non empty total V36( NAT , NAT ) Element of bool [:NAT,NAT:]

the carrier of (C1) is set

((C1)) is set

the carrier' of (C1) is set

2 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{0},(2 -tuples_on C1):] is Relation-like set

S2 is set

A1 is set

A2 is set

[A1,A2] is V21() set

{A1,A2} is non empty set

{A1} is non empty set

{{A1,A2},{A1}} is non empty set

f is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

G is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty V24() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V78() Element of NAT

S1 . G is V6() V7() V8() V12() Element of NAT

B1 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[G,B1] is V21() set

{G,B1} is functional non empty set

{G} is functional non empty set

{{G,B1},{G}} is non empty set

len B1 is V6() V7() V8() V12() Element of NAT

(S1 . G) -tuples_on ((C1)) is functional FinSequence-membered FinSequenceSet of ((C1))

[:{G},((S1 . G) -tuples_on ((C1))):] is Relation-like set

S2 is set

1 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{1},(1 -tuples_on C1):] is Relation-like set

3 -tuples_on C1 is functional FinSequence-membered FinSequenceSet of C1

[:{2},(3 -tuples_on C1):] is Relation-like set

[:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] is Relation-like set

A1 is set

A2 is set

[A1,A2] is V21() set

{A1,A2} is non empty set

{A1} is non empty set

{{A1,A2},{A1}} is non empty set

G is V6() V7() V8() V12() non empty Element of NAT

S1 . G is V6() V7() V8() V12() Element of NAT

{G} is non empty set

(S1 . G) -tuples_on ((C1)) is functional FinSequence-membered FinSequenceSet of ((C1))

[:{G},((S1 . G) -tuples_on ((C1))):] is Relation-like set

f is Relation-like NAT -defined C1 -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of C1

[G,f] is V21() set

{G,f} is non empty set

{{G,f},{G}} is non empty set

len f is V6() V7() V8() V12() Element of NAT

A1 is set

A2 is set

[A1,A2] is V21() set

{A1,A2} is non empty set

{A1} is non empty set

{{A1,A2},{A1}} is non empty set

G is V6() V7() V8() V12() non empty Element of NAT

S1 . G is V6() V7() V8() V12() Element of NAT

{G} is non empty set

(S1 . G) -tuples_on ((C1)) is functional FinSequence-membered FinSequenceSet of ((C1))

[:{G},((S1 . G) -tuples_on ((C1))):] is Relation-like set

f is Relation-like NAT -defined C1 -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of C1

[G,f] is V21() set

{G,f} is non empty set

{{G,f},{G}} is non empty set

len f is V6() V7() V8() V12() Element of NAT

({{}}) is non empty non void feasible strict feasible () () ({{}})

C1 is set

(C1) is strict feasible () () (C1)

C1 is () ManySortedSign

the carrier of C1 is set

the carrier' of C1 is set

(C1) is set

C2 is set

the carrier of C1 \/ the carrier' of C1 is set

F is Relation-like NAT -defined NAT -valued Function-like non empty total V36( NAT , NAT ) Element of bool [:NAT,NAT:]

S1 is V6() V7() V8() V12() Element of NAT

S2 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[S1,S2] is V21() set

{S1,S2} is non empty set

{S1} is non empty set

{{S1,S2},{S1}} is non empty set

len S2 is V6() V7() V8() V12() Element of NAT

F . S1 is V6() V7() V8() V12() Element of NAT

(F . S1) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)

[:{S1},((F . S1) -tuples_on (C1)):] is Relation-like set

proj2 S2 is set

A1 is set

S1 is V6() V7() V8() V12() Element of NAT

S2 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[S1,S2] is V21() set

{S1,S2} is non empty set

{S1} is non empty set

{{S1,S2},{S1}} is non empty set

len S2 is V6() V7() V8() V12() Element of NAT

F . S1 is V6() V7() V8() V12() Element of NAT

(F . S1) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)

[:{S1},((F . S1) -tuples_on (C1)):] is Relation-like set

proj2 S2 is set

A1 is set

C1 is () ManySortedSign

the carrier of C1 is set

the carrier' of C1 is set

C2 is set

F is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[C2,F] is V21() set

{C2,F} is non empty set

{C2} is non empty set

{{C2,F},{C2}} is non empty set

S1 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[C2,S1] is V21() set

{C2,S1} is non empty set

{{C2,S1},{C2}} is non empty set

len F is V6() V7() V8() V12() Element of NAT

len S1 is V6() V7() V8() V12() Element of NAT

(C1) is set

S2 is Relation-like NAT -defined NAT -valued Function-like non empty total V36( NAT , NAT ) Element of bool [:NAT,NAT:]

A1 is V6() V7() V8() V12() Element of NAT

A2 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[A1,A2] is V21() set

{A1,A2} is non empty set

{A1} is non empty set

{{A1,A2},{A1}} is non empty set

len A2 is V6() V7() V8() V12() Element of NAT

S2 . A1 is V6() V7() V8() V12() Element of NAT

(S2 . A1) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)

[:{A1},((S2 . A1) -tuples_on (C1)):] is Relation-like set

f is V6() V7() V8() V12() Element of NAT

G is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[f,G] is V21() set

{f,G} is non empty set

{f} is non empty set

{{f,G},{f}} is non empty set

len G is V6() V7() V8() V12() Element of NAT

S2 . f is V6() V7() V8() V12() Element of NAT

(S2 . f) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)

[:{f},((S2 . f) -tuples_on (C1)):] is Relation-like set

A1 is V6() V7() V8() V12() Element of NAT

A2 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[A1,A2] is V21() set

{A1,A2} is non empty set

{A1} is non empty set

{{A1,A2},{A1}} is non empty set

len A2 is V6() V7() V8() V12() Element of NAT

S2 . A1 is V6() V7() V8() V12() Element of NAT

(S2 . A1) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)

[:{A1},((S2 . A1) -tuples_on (C1)):] is Relation-like set

f is V6() V7() V8() V12() Element of NAT

G is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[f,G] is V21() set

{f,G} is non empty set

{f} is non empty set

{{f,G},{f}} is non empty set

len G is V6() V7() V8() V12() Element of NAT

S2 . f is V6() V7() V8() V12() Element of NAT

(S2 . f) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)

[:{f},((S2 . f) -tuples_on (C1)):] is Relation-like set

C1 is () ManySortedSign

(C1) is set

the carrier of C1 is set

the carrier' of C1 is set

C2 is set

S1 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

len S1 is V6() V7() V8() V12() Element of NAT

F is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

len F is V6() V7() V8() V12() Element of NAT

proj2 S1 is set

[C2,F] is V21() set

{C2,F} is non empty set

{C2} is non empty set

{{C2,F},{C2}} is non empty set

[C2,S1] is V21() set

{C2,S1} is non empty set

{{C2,S1},{C2}} is non empty set

S2 is Relation-like NAT -defined NAT -valued Function-like non empty total V36( NAT , NAT ) Element of bool [:NAT,NAT:]

A1 is V6() V7() V8() V12() Element of NAT

A2 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[A1,A2] is V21() set

{A1,A2} is non empty set

{A1} is non empty set

{{A1,A2},{A1}} is non empty set

len A2 is V6() V7() V8() V12() Element of NAT

S2 . A1 is V6() V7() V8() V12() Element of NAT

(S2 . A1) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)

[:{A1},((S2 . A1) -tuples_on (C1)):] is Relation-like set

A1 is V6() V7() V8() V12() Element of NAT

A2 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[A1,A2] is V21() set

{A1,A2} is non empty set

{A1} is non empty set

{{A1,A2},{A1}} is non empty set

len A2 is V6() V7() V8() V12() Element of NAT

S2 . A1 is V6() V7() V8() V12() Element of NAT

(S2 . A1) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)

[:{A1},((S2 . A1) -tuples_on (C1)):] is Relation-like set

C1 is non empty non void feasible feasible () () ManySortedSign

(C1) is set

the carrier of C1 is non empty set

the Element of the carrier of C1 is Element of the carrier of C1

F is set

(F) is strict feasible () () (F)

2 -tuples_on F is functional FinSequence-membered FinSequenceSet of F

[:{0},(2 -tuples_on F):] is Relation-like set

the carrier' of C1 is non empty set

S1 is Relation-like NAT -defined NAT -valued Function-like non empty total V36( NAT , NAT ) Element of bool [:NAT,NAT:]

S2 is V6() V7() V8() V12() Element of NAT

A1 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[S2,A1] is V21() set

{S2,A1} is non empty set

{S2} is non empty set

{{S2,A1},{S2}} is non empty set

len A1 is V6() V7() V8() V12() Element of NAT

S1 . S2 is V6() V7() V8() V12() Element of NAT

(S1 . S2) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)

[:{S2},((S1 . S2) -tuples_on (C1)):] is Relation-like set

A2 is set

<*A2,A2*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*A2,A2*>] is V21() set

{0,<*A2,A2*>} is functional non empty set

{{0,<*A2,A2*>},{0}} is non empty set

the carrier of C1 \/ the carrier' of C1 is non empty set

proj2 <*A2,A2*> is non empty set

{A2,A2} is non empty set

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

A2 is set

<*A2,A2*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

C1 is non empty non void feasible feasible () ManySortedSign

the carrier of C1 is non empty set

C2 is Element of the carrier of C1

C2 `2 is set

F is set

(F) is strict feasible () () (F)

2 -tuples_on F is functional FinSequence-membered FinSequenceSet of F

[:{0},(2 -tuples_on F):] is Relation-like set

C1 is non empty feasible feasible () ManySortedSign

the carrier of C1 is non empty set

C2 is Element of the carrier of C1

C2 `2 is set

(C1) is set

F is V6() V7() V8() V12() Element of NAT

S1 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[F,S1] is V21() set

{F,S1} is non empty set

{F} is non empty set

{{F,S1},{F}} is non empty set

proj2 S1 is set

C1 is non void () ManySortedSign

the carrier' of C1 is non empty set

C2 is Element of the carrier' of C1

C2 `2 is set

(C1) is set

F is V6() V7() V8() V12() Element of NAT

S1 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[F,S1] is V21() set

{F,S1} is non empty set

{F} is non empty set

{{F,S1},{F}} is non empty set

proj2 S1 is set

C1 is non empty non void feasible feasible () ManySortedSign

the carrier of C1 is non empty set

C2 is Element of the carrier of C1

C2 `2 is Relation-like Function-like set

F is set

(F) is strict feasible () () (F)

2 -tuples_on F is functional FinSequence-membered FinSequenceSet of F

[:{0},(2 -tuples_on F):] is Relation-like set

S1 is set

S2 is set

<*S1,S2*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

C1 is non empty feasible feasible () ManySortedSign

the carrier of C1 is non empty set

C2 is Element of the carrier of C1

C2 `2 is Relation-like Function-like set

(C1) is set

F is V6() V7() V8() V12() Element of NAT

S1 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[F,S1] is V21() set

{F,S1} is non empty set

{F} is non empty set

{{F,S1},{F}} is non empty set

proj2 S1 is set

C1 is non void () ManySortedSign

the carrier' of C1 is non empty set

C2 is Element of the carrier' of C1

C2 `2 is Relation-like Function-like set

(C1) is set

F is V6() V7() V8() V12() Element of NAT

S1 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set

[F,S1] is V21() set

{F,S1} is non empty set

{F} is non empty set

{{F,S1},{F}} is non empty set

proj2 S1 is set

C1 is set

<*C1*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[1,<*C1*>] is V21() set

{1,<*C1*>} is non empty set

{{1,<*C1*>},{1}} is non empty set

C2 is set

<*C1,C2*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*C1,C2*>] is V21() set

{0,<*C1,C2*>} is functional non empty set

{{0,<*C1,C2*>},{0}} is non empty set

F is set

<*C1,C2,F*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set

[2,<*C1,C2,F*>] is V21() set

{2,<*C1,C2,F*>} is non empty set

{{2,<*C1,C2,F*>},{2}} is non empty set

C1 is non empty set

C2 is non empty non void feasible feasible () (C1)

the carrier' of C2 is non empty set

the carrier of C2 is non empty set

F is Element of C1

(F) is set

<*F*> is Relation-like NAT -defined Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set

[1,<*F*>] is V21() set

{1,<*F*>} is non empty set

{{1,<*F*>},{1}} is non empty set

(C1) is non empty non void feasible strict feasible () () (C1)

the carrier' of (C1) is non empty set

1 -tuples_on C1 is functional non empty FinSequence-membered FinSequenceSet of C1

[:{1},(1 -tuples_on C1):] is Relation-like non empty set

3 -tuples_on C1 is functional non empty FinSequence-membered FinSequenceSet of C1

[:{2},(3 -tuples_on C1):] is Relation-like non empty set

[:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] is Relation-like non empty set

the carrier of (C1) is non empty set

<*F*> is Relation-like NAT -defined C1 -valued Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like FinSequence of C1

[1,<*F*>] is V21() set

{1,<*F*>} is non empty set

{{1,<*F*>},{1}} is non empty set

S1 is Element of C1

(F,S1) is set

<*F,S1*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

[0,<*F,S1*>] is V21() set

{0,<*F,S1*>} is functional non empty set

{{0,<*F,S1*>},{0}} is non empty set

2 -tuples_on C1 is functional non empty FinSequence-membered FinSequenceSet of C1

[:{0},(2 -tuples_on C1):] is Relation-like non empty set

<*F,S1*> is Relation-like NAT -defined C1 -valued Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like FinSequence of C1

[0,<*F,S1*>] is V21() set

{0,<*F,S1*>} is functional non empty set

{{0,<*F,S1*>},{0}} is non empty