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
{ b1 where b1 is Relation-like NAT -defined C1 -valued Function-like V24() FinSequence-like FinSubsequence-like Element of C1 * : len b1 = 1 } is set
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
{ b1 where b1 is Relation-like NAT -defined C1 -valued Function-like V24() FinSequence-like FinSubsequence-like Element of C1 * : len b1 = 3 } is set
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
{ b1 where b1 is Relation-like NAT -defined C1 -valued Function-like V24() FinSequence-like FinSubsequence-like Element of C1 * : len b1 = 1 } is set
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
{ b1 where b1 is Relation-like NAT -defined C1 -valued Function-like V24() FinSequence-like FinSubsequence-like Element of C1 * : len b1 = 3 } is set
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
{ b1 where b1 is Relation-like NAT -defined C2 -valued Function-like V24() FinSequence-like FinSubsequence-like Element of C2 * : len b1 = 2 } is set
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