REAL is set
NAT is V1() V4() V5() V6() Element of bool REAL
bool REAL is V1() set
COMPLEX is set
NAT is V1() V4() V5() V6() set
bool NAT is V1() set
bool NAT is V1() set
1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
2 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
3 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
0 is V1() V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative functional V32() FinSequence-membered Element of NAT
0 is V1() V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative functional V32() FinSequence-membered set
Y is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
Y + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
Y is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
n is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
n + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
n is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
n -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
n - 1 is V11() ext-real V32() set
m - 1 is V11() ext-real V32() set
n + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
m + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(n - 1) + 1 is V11() ext-real V32() set
(m - 1) + 1 is V11() ext-real V32() set
n is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
n + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
Y is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
n is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
n -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
n is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Seg n is V35() V42(n) Element of bool NAT
m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
n |-> m is Relation-like NAT -defined NAT -valued Function-like V35() V42(n) FinSequence-like FinSubsequence-like Element of n -tuples_on NAT
n -tuples_on NAT is V1() functional FinSequence-membered FinSequenceSet of NAT
NAT * is V1() functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = n } is set
K230((Seg n),m) is Relation-like Seg n -defined {m} -valued Function-like V29( Seg n,{m}) V35() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{m}:]
{m} is V1() set
[:(Seg n),{m}:] is set
bool [:(Seg n),{m}:] is V1() set
(n |-> m) . S is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m -' S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S -' m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(m -' S) + (S -' m) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((m -' S) + (S -' m)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
S - S is V11() ext-real V32() set
m - S is V11() ext-real V32() set
S - m is V11() ext-real V32() set
(S - m) + 1 is V11() ext-real V32() set
0 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
S + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(S + 1) - m is V11() ext-real V32() set
(S + 1) -' m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m + ((S + 1) -' m) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(m + ((S + 1) -' m)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(m + ((S + 1) -' m)) - 1 is V11() ext-real V32() set
Y is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
len Y is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
dom Y is Element of bool NAT
Y is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
len Y is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
dom Y is Element of bool NAT
m - m is V11() ext-real V32() set
Y . 1 is set
m + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(m + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
rng Y is set
F is set
i1 is set
Y . i1 is set
Seg (len Y) is V35() V42( len Y) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT : ( 1 <= b1 & b1 <= len Y ) } is set
j1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y . j1 is set
m + j1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(m + j1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
len F is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i1 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
F . (i1 + 1) is set
F /. i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(F /. i1) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
F . i1 is set
F /. (i1 + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(F /. (i1 + 1)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
1 + i1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
m + (i1 + 1) is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(m + (i1 + 1)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m + i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
1 + (m + i1) is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
1 - 1 is V11() ext-real V32() set
(1 + (m + i1)) - 1 is V11() ext-real V32() set
(1 + (m + i1)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
1 + 0 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(m + i1) - 1 is V11() ext-real V32() set
(m + i1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
1 + ((m + i1) -' 1) is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
1 + ((m + i1) - 1) is V11() ext-real V32() set
dom F is Element of bool NAT
i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y . i1 is set
j1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i1 + m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(i1 + m) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(i1 + m) - 1 is V11() ext-real V32() set
m - 1 is V11() ext-real V32() set
i1 + (m - 1) is V11() ext-real V32() set
1 + (m - 1) is V11() ext-real V32() set
((S + 1) -' m) + m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((S + 1) - m) + m is V11() ext-real V32() set
(S + 1) - 1 is V11() ext-real V32() set
Y . (len Y) is set
m - S is V11() ext-real V32() set
Seg 1 is V1() V35() V42(1) Element of bool NAT
{m} is V1() set
Y is Relation-like Function-like set
dom Y is set
rng Y is set
F is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
len F is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i1 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
F . (i1 + 1) is set
F /. i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(F /. i1) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
F . i1 is set
F /. (i1 + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(F /. (i1 + 1)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
F . 1 is set
i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
j1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F . i1 is set
S - S is V11() ext-real V32() set
m - S is V11() ext-real V32() set
- (m - S) is V11() ext-real V32() set
- (- (m - S)) is V11() ext-real V32() set
S - m is V11() ext-real V32() set
m - m is V11() ext-real V32() set
S - m is V11() ext-real V32() set
(m - S) + 1 is V11() ext-real V32() set
((m - S) + 1) + (S -' m) is V11() ext-real V32() set
m + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(m + 1) - S is V11() ext-real V32() set
(m + 1) - 1 is V11() ext-real V32() set
0 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(m + 1) -' S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(m + 1) - ((m + 1) -' S) is V11() ext-real V32() set
(m + 1) - ((m + 1) - S) is V11() ext-real V32() set
Y is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
len Y is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
dom Y is Element of bool NAT
Y is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
len Y is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
dom Y is Element of bool NAT
Y . 1 is set
(m + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
rng Y is set
F is set
i1 is set
Y . i1 is set
Seg (len Y) is V35() V42( len Y) Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT : ( 1 <= b1 & b1 <= len Y ) } is set
j1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y . j1 is set
(m + 1) -' j1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
len F is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i1 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
F . (i1 + 1) is set
F /. i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(F /. i1) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
F . i1 is set
F /. (i1 + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(F /. (i1 + 1)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
i1 + S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m - i1 is V11() ext-real V32() set
(m + 1) -' (i1 + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
1 + ((m + 1) -' (i1 + 1)) is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(m + 1) - (i1 + 1) is V11() ext-real V32() set
1 + ((m + 1) - (i1 + 1)) is V11() ext-real V32() set
(m + 1) - i1 is V11() ext-real V32() set
dom F is Element of bool NAT
(m + 1) -' i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y . i1 is set
j1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i1 + S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((m + 1) - S) + S is V11() ext-real V32() set
(i1 + S) - i1 is V11() ext-real V32() set
(m + 1) - i1 is V11() ext-real V32() set
- i1 is V11() ext-real non positive V32() set
- 1 is V11() ext-real non positive V32() set
(- i1) + (m + 1) is V11() ext-real V32() set
(- 1) + (m + 1) is V11() ext-real V32() set
(m + 1) -' i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y . (len Y) is set
(m + 1) -' ((m + 1) -' S) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
Y . 1 is set
len Y is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y . (len Y) is set
F is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
F . 1 is set
len F is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F . (len F) is set
i1 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
i1 . 1 is set
len i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i1 . (len i1) is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m -' S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S -' m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(m -' S) + (S -' m) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((m -' S) + (S -' m)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
Y is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
Y . 1 is set
len Y is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y . (len Y) is set
F is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y /. F is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
Y /. (F + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y . F is set
Y . (F + 1) is set
(Y /. F) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(Y /. (F + 1)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
n is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
S -' F is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F -' S is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(S -' F) + (F -' S) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Y -' i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((S -' F) + (F -' S)) + (Y -' i1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i1 -' Y is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(((S -' F) + (F -' S)) + (Y -' i1)) + (i1 -' Y) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((((S -' F) + (F -' S)) + (Y -' i1)) + (i1 -' Y)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
((S -' F) + (F -' S)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
j1 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
j1 . 1 is set
len j1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
j1 . (len j1) is set
(Y -' i1) + (i1 -' Y) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((Y -' i1) + (i1 -' Y)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
i2 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
i2 . 1 is set
len i2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i2 . (len i2) is set
1 - 1 is V11() ext-real V32() set
(len i2) - 1 is V11() ext-real V32() set
(len i2) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((len i2) -' 1) |-> F is Relation-like NAT -defined NAT -valued Function-like V35() V42((len i2) -' 1) FinSequence-like FinSubsequence-like Element of ((len i2) -' 1) -tuples_on NAT
((len i2) -' 1) -tuples_on NAT is V1() functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = (len i2) -' 1 } is set
Seg ((len i2) -' 1) is V35() V42((len i2) -' 1) Element of bool NAT
K230((Seg ((len i2) -' 1)),F) is Relation-like Seg ((len i2) -' 1) -defined {F} -valued Function-like V29( Seg ((len i2) -' 1),{F}) V35() FinSequence-like FinSubsequence-like Element of bool [:(Seg ((len i2) -' 1)),{F}:]
{F} is V1() set
[:(Seg ((len i2) -' 1)),{F}:] is set
bool [:(Seg ((len i2) -' 1)),{F}:] is V1() set
j1 ^ (((len i2) -' 1) |-> F) is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
(len j1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((len j1) -' 1) |-> Y is Relation-like NAT -defined NAT -valued Function-like V35() V42((len j1) -' 1) FinSequence-like FinSubsequence-like Element of ((len j1) -' 1) -tuples_on NAT
((len j1) -' 1) -tuples_on NAT is V1() functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = (len j1) -' 1 } is set
Seg ((len j1) -' 1) is V35() V42((len j1) -' 1) Element of bool NAT
K230((Seg ((len j1) -' 1)),Y) is Relation-like Seg ((len j1) -' 1) -defined {Y} -valued Function-like V29( Seg ((len j1) -' 1),{Y}) V35() FinSequence-like FinSubsequence-like Element of bool [:(Seg ((len j1) -' 1)),{Y}:]
{Y} is V1() set
[:(Seg ((len j1) -' 1)),{Y}:] is set
bool [:(Seg ((len j1) -' 1)),{Y}:] is V1() set
(((len j1) -' 1) |-> Y) ^ i2 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
len (j1 ^ (((len i2) -' 1) |-> F)) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
len (((len i2) -' 1) |-> F) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(len j1) + (len (((len i2) -' 1) |-> F)) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(len j1) + ((len i2) -' 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(len j1) + ((len i2) - 1) is V11() ext-real V32() set
(len j1) - 1 is V11() ext-real V32() set
((len j1) - 1) + (len i2) is V11() ext-real V32() set
((len j1) -' 1) + (len i2) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
len (((len j1) -' 1) |-> Y) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(len (((len j1) -' 1) |-> Y)) + (len i2) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
len ((((len j1) -' 1) |-> Y) ^ i2) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
dom (j1 ^ (((len i2) -' 1) |-> F)) is Element of bool NAT
dom ((((len j1) -' 1) |-> Y) ^ i2) is Element of bool NAT
Seg ((len (((len j1) -' 1) |-> Y)) + (len i2)) is V35() V42((len (((len j1) -' 1) |-> Y)) + (len i2)) Element of bool NAT
fs2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(j1 ^ (((len i2) -' 1) |-> F)) . fs2 is set
((((len j1) -' 1) |-> Y) ^ i2) . fs2 is set
p1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
p2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Seg (len (j1 ^ (((len i2) -' 1) |-> F))) is V35() V42( len (j1 ^ (((len i2) -' 1) |-> F))) Element of bool NAT
((len j1) -' 1) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
((len j1) - 1) + 1 is V11() ext-real V32() set
(len j1) - ((len j1) - 1) is V11() ext-real V32() set
fs2 - ((len j1) - 1) is V11() ext-real V32() set
(len ((((len j1) -' 1) |-> Y) ^ i2)) - ((len j1) - 1) is V11() ext-real V32() set
fs2 - (len j1) is V11() ext-real V32() set
(fs2 - (len j1)) + 1 is V11() ext-real V32() set
(len ((((len j1) -' 1) |-> Y) ^ i2)) - (len j1) is V11() ext-real V32() set
((len ((((len j1) -' 1) |-> Y) ^ i2)) - (len j1)) + 1 is V11() ext-real V32() set
fs2 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(fs2 + 1) - (len j1) is V11() ext-real V32() set
(len ((((len j1) -' 1) |-> Y) ^ i2)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
((len ((((len j1) -' 1) |-> Y) ^ i2)) + 1) - (len j1) is V11() ext-real V32() set
(((len j1) - 1) + (len i2)) + 1 is V11() ext-real V32() set
((((len j1) - 1) + (len i2)) + 1) - (len j1) is V11() ext-real V32() set
(fs2 + 1) -' (len j1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Seg (len i2) is V35() V42( len i2) Element of bool NAT
dom i2 is Element of bool NAT
((len j1) - 1) + ((fs2 + 1) - (len j1)) is V11() ext-real V32() set
(len (((len j1) -' 1) |-> Y)) + ((fs2 + 1) -' (len j1)) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i2 . ((fs2 + 1) -' (len j1)) is set
Seg (len (((len j1) -' 1) |-> Y)) is V35() V42( len (((len j1) -' 1) |-> Y)) Element of bool NAT
dom (((len j1) -' 1) |-> Y) is Element of bool NAT
(((len j1) -' 1) |-> Y) . fs2 is set
Seg ((len j1) + (len (((len i2) -' 1) |-> F))) is V35() V42((len j1) + (len (((len i2) -' 1) |-> F))) Element of bool NAT
(len (j1 ^ (((len i2) -' 1) |-> F))) -' (len j1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(len (j1 ^ (((len i2) -' 1) |-> F))) - (len j1) is V11() ext-real V32() set
(len j1) - (len j1) is V11() ext-real V32() set
dom j1 is Element of bool NAT
j1 . fs2 is set
fs2 -' (len j1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
0 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
Seg ((len (j1 ^ (((len i2) -' 1) |-> F))) -' (len j1)) is V35() V42((len (j1 ^ (((len i2) -' 1) |-> F))) -' (len j1)) Element of bool NAT
(len j1) + (fs2 - (len j1)) is V11() ext-real V32() set
Seg (len (((len i2) -' 1) |-> F)) is V35() V42( len (((len i2) -' 1) |-> F)) Element of bool NAT
dom (((len i2) -' 1) |-> F) is Element of bool NAT
(((len i2) -' 1) |-> F) . (fs2 -' (len j1)) is set
fs2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(j1 ^ (((len i2) -' 1) |-> F)) /. fs2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((((len j1) -' 1) |-> Y) ^ i2) /. fs2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
fs2 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(j1 ^ (((len i2) -' 1) |-> F)) /. (fs2 + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((((len j1) -' 1) |-> Y) ^ i2) /. (fs2 + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(fs2 + 1) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
((len j1) - 1) + 1 is V11() ext-real V32() set
dom j1 is Element of bool NAT
(j1 ^ (((len i2) -' 1) |-> F)) . (fs2 + 1) is set
j1 . (fs2 + 1) is set
j1 /. (fs2 + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(j1 ^ (((len i2) -' 1) |-> F)) . fs2 is set
j1 . fs2 is set
j1 /. fs2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
0 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
dom j1 is Element of bool NAT
(j1 ^ (((len i2) -' 1) |-> F)) . (fs2 + 1) is set
j1 . (fs2 + 1) is set
j1 /. (fs2 + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(j1 ^ (((len i2) -' 1) |-> F)) . fs2 is set
j1 . fs2 is set
j1 /. fs2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
dom (((len j1) -' 1) |-> Y) is Element of bool NAT
dom ((((len j1) -' 1) |-> Y) ^ i2) is Element of bool NAT
((((len j1) -' 1) |-> Y) ^ i2) . (fs2 + 1) is set
(((len j1) -' 1) |-> Y) . (fs2 + 1) is set
((len j1) -' 1) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
((len j1) - 1) + 1 is V11() ext-real V32() set
dom ((((len j1) -' 1) |-> Y) ^ i2) is Element of bool NAT
Seg ((len (((len j1) -' 1) |-> Y)) + (len i2)) is V35() V42((len (((len j1) -' 1) |-> Y)) + (len i2)) Element of bool NAT
Seg (len ((((len j1) -' 1) |-> Y) ^ i2)) is V35() V42( len ((((len j1) -' 1) |-> Y) ^ i2)) Element of bool NAT
Seg (len i2) is V35() V42( len i2) Element of bool NAT
dom i2 is Element of bool NAT
(len (((len j1) -' 1) |-> Y)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
((((len j1) -' 1) |-> Y) ^ i2) . (fs2 + 1) is set
dom (((len j1) -' 1) |-> Y) is Element of bool NAT
dom ((((len j1) -' 1) |-> Y) ^ i2) is Element of bool NAT
(fs2 + 1) - 1 is V11() ext-real V32() set
((((len j1) -' 1) |-> Y) ^ i2) . fs2 is set
(((len j1) -' 1) |-> Y) . fs2 is set
(fs2 + 1) - (len j1) is V11() ext-real V32() set
(fs2 + 1) -' (len j1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((fs2 + 1) -' (len j1)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(len (((len j1) -' 1) |-> Y)) + (((fs2 + 1) -' (len j1)) + 1) is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
((len j1) -' 1) + (((fs2 + 1) -' (len j1)) + 1) is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
((len j1) - 1) + (((fs2 + 1) -' (len j1)) + 1) is V11() ext-real V32() set
((fs2 + 1) - (len j1)) + 1 is V11() ext-real V32() set
((len j1) - 1) + (((fs2 + 1) - (len j1)) + 1) is V11() ext-real V32() set
(len j1) + ((fs2 + 1) - (len j1)) is V11() ext-real V32() set
(len j1) + ((fs2 + 1) -' (len j1)) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
fs2 - (len j1) is V11() ext-real V32() set
0 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(fs2 - (len j1)) + 1 is V11() ext-real V32() set
fs2 -' (len j1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Seg (len j1) is V35() V42( len j1) Element of bool NAT
dom j1 is Element of bool NAT
(j1 ^ (((len i2) -' 1) |-> F)) . fs2 is set
((fs2 + 1) - (len j1)) + (len j1) is V11() ext-real V32() set
((len i2) - 1) + (len j1) is V11() ext-real V32() set
Seg (len (((len i2) -' 1) |-> F)) is V35() V42( len (((len i2) -' 1) |-> F)) Element of bool NAT
dom (((len i2) -' 1) |-> F) is Element of bool NAT
(j1 ^ (((len i2) -' 1) |-> F)) . (fs2 + 1) is set
(((len i2) -' 1) |-> F) . ((fs2 + 1) -' (len j1)) is set
(len (((len j1) -' 1) |-> Y)) + ((fs2 + 1) -' (len j1)) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((len j1) -' 1) + ((fs2 + 1) -' (len j1)) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((len j1) - 1) + ((fs2 + 1) -' (len j1)) is V11() ext-real V32() set
((len j1) - 1) + ((fs2 - (len j1)) + 1) is V11() ext-real V32() set
((len j1) + ((len i2) -' 1)) - (len j1) is V11() ext-real V32() set
(((len j1) - 1) + (len i2)) - ((len j1) - 1) is V11() ext-real V32() set
fs2 - ((len j1) - 1) is V11() ext-real V32() set
Seg (len i2) is V35() V42( len i2) Element of bool NAT
dom i2 is Element of bool NAT
((len i2) -' 1) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
((len i2) - 1) + 1 is V11() ext-real V32() set
(len j1) + (fs2 - (len j1)) is V11() ext-real V32() set
(len j1) + (fs2 -' (len j1)) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(((len i2) -' 1) |-> F) . (fs2 -' (len j1)) is set
dom ((((len j1) -' 1) |-> Y) ^ i2) is Element of bool NAT
((((len j1) -' 1) |-> Y) ^ i2) . ((len (((len j1) -' 1) |-> Y)) + ((fs2 + 1) -' (len j1))) is set
i2 . ((fs2 + 1) -' (len j1)) is set
i2 /. ((fs2 + 1) -' (len j1)) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Seg (len (j1 ^ (((len i2) -' 1) |-> F))) is V35() V42( len (j1 ^ (((len i2) -' 1) |-> F))) Element of bool NAT
((((len j1) -' 1) |-> Y) ^ i2) . ((len (((len j1) -' 1) |-> Y)) + (((fs2 + 1) -' (len j1)) + 1)) is set
i2 . (((fs2 + 1) -' (len j1)) + 1) is set
i2 /. (((fs2 + 1) -' (len j1)) + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
<*> NAT is V1() proper V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like NAT -defined NAT -valued Function-like functional V32() V35() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of NAT
[:NAT,NAT:] is V1() set
(<*> NAT) ^ i2 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
((((len j1) -' 1) |-> Y) ^ i2) . 1 is set
((((len j1) -' 1) |-> Y) ^ i2) . (len ((((len j1) -' 1) |-> Y) ^ i2)) is set
0 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
dom (((len j1) -' 1) |-> Y) is Element of bool NAT
((((len j1) -' 1) |-> Y) ^ i2) . 1 is set
(((len j1) -' 1) |-> Y) . 1 is set
dom i2 is Element of bool NAT
((((len j1) -' 1) |-> Y) ^ i2) . (len ((((len j1) -' 1) |-> Y) ^ i2)) is set
((((len j1) -' 1) |-> Y) ^ i2) . 1 is set
((((len j1) -' 1) |-> Y) ^ i2) . (len ((((len j1) -' 1) |-> Y) ^ i2)) is set
((((len j1) -' 1) |-> Y) ^ i2) . 1 is set
((((len j1) -' 1) |-> Y) ^ i2) . (len ((((len j1) -' 1) |-> Y) ^ i2)) is set
dom j1 is Element of bool NAT
<*> NAT is V1() proper V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like NAT -defined NAT -valued Function-like functional V32() V35() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of NAT
[:NAT,NAT:] is V1() set
j1 ^ (<*> NAT) is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
(j1 ^ (((len i2) -' 1) |-> F)) . 1 is set
(j1 ^ (((len i2) -' 1) |-> F)) . (len (j1 ^ (((len i2) -' 1) |-> F))) is set
0 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
dom (((len i2) -' 1) |-> F) is Element of bool NAT
(((len i2) -' 1) |-> F) . (len (((len i2) -' 1) |-> F)) is set
(j1 ^ (((len i2) -' 1) |-> F)) . 1 is set
(j1 ^ (((len i2) -' 1) |-> F)) . (len (j1 ^ (((len i2) -' 1) |-> F))) is set
(j1 ^ (((len i2) -' 1) |-> F)) . 1 is set
(j1 ^ (((len i2) -' 1) |-> F)) . (len (j1 ^ (((len i2) -' 1) |-> F))) is set
(j1 ^ (((len i2) -' 1) |-> F)) . 1 is set
(j1 ^ (((len i2) -' 1) |-> F)) . (len (j1 ^ (((len i2) -' 1) |-> F))) is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Seg n is V35() V42(n) Element of bool NAT
m is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Seg m is V35() V42(m) Element of bool NAT
S is set
bool S is V1() set
(bool S) * is V1() functional FinSequence-membered FinSequenceSet of bool S
Y is Element of bool S
F is Relation-like NAT -defined (bool S) * -valued Function-like V35() FinSequence-like FinSubsequence-like tabular Matrix of n,m, bool S
i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
j1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F * (i1,j1) is Element of bool S
i1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
j1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F * (i1,j1) is Element of bool S
1 - 1 is V11() ext-real V32() set
i1 - 1 is V11() ext-real V32() set
i1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
j1 - 1 is V11() ext-real V32() set
j1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
i2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
j2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F * (i2,j2) is Element of bool S
i2 - 1 is V11() ext-real V32() set
i2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
j2 - 1 is V11() ext-real V32() set
j2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
0 + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
m - 1 is V11() ext-real V32() set
m -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
n - 1 is V11() ext-real V32() set
n -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(i1 -' 1) -' (i2 -' 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(i2 -' 1) -' (i1 -' 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((i1 -' 1) -' (i2 -' 1)) + ((i2 -' 1) -' (i1 -' 1)) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(j1 -' 1) -' (j2 -' 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(((i1 -' 1) -' (i2 -' 1)) + ((i2 -' 1) -' (i1 -' 1))) + ((j1 -' 1) -' (j2 -' 1)) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(j2 -' 1) -' (j1 -' 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((((i1 -' 1) -' (i2 -' 1)) + ((i2 -' 1) -' (i1 -' 1))) + ((j1 -' 1) -' (j2 -' 1))) + ((j2 -' 1) -' (j1 -' 1)) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(((((i1 -' 1) -' (i2 -' 1)) + ((i2 -' 1) -' (i1 -' 1))) + ((j1 -' 1) -' (j2 -' 1))) + ((j2 -' 1) -' (j1 -' 1))) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
fs1 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
dom fs1 is Element of bool NAT
fs2 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
fs1 . 1 is set
len fs1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
fs1 . (len fs1) is set
fs2 . 1 is set
len fs2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
fs2 . (len fs2) is set
p1 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
len p1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
dom p1 is Element of bool NAT
p1 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
len p1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
dom p1 is Element of bool NAT
p2 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
len p2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
dom p2 is Element of bool NAT
p2 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of NAT
len p2 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
dom p2 is Element of bool NAT
Seg (len fs2) is V35() V42( len fs2) Element of bool NAT
Seg (len fs1) is V35() V42( len fs1) Element of bool NAT
k is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
k + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
p1 /. (k + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
p2 /. (k + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F * ((p1 /. (k + 1)),(p2 /. (k + 1))) is Element of bool S
(k + 1) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
p1 /. ((k + 1) + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
p2 /. ((k + 1) + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F * ((p1 /. ((k + 1) + 1)),(p2 /. ((k + 1) + 1))) is Element of bool S
fs1 /. ((k + 1) + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
fs2 /. ((k + 1) + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
Seg (len p1) is V35() V42( len p1) Element of bool NAT
dom fs2 is Element of bool NAT
fs2 . ((k + 1) + 1) is set
fs1 . ((k + 1) + 1) is set
(fs1 /. ((k + 1) + 1)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(n - 1) + 1 is V11() ext-real V32() set
p2 . ((k + 1) + 1) is set
(fs2 /. ((k + 1) + 1)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
(m - 1) + 1 is V11() ext-real V32() set
1 + (fs2 /. ((k + 1) + 1)) is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
p1 . ((k + 1) + 1) is set
fs1 /. (k + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
fs2 /. (k + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
fs2 . (k + 1) is set
p1 . (k + 1) is set
(fs1 /. (k + 1)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
fs1 . (k + 1) is set
1 + (fs1 /. (k + 1)) is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
p2 . (k + 1) is set
(fs2 /. (k + 1)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
1 + (fs2 /. (k + 1)) is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
1 + (fs1 /. ((k + 1) + 1)) is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
dom fs2 is Element of bool NAT
fs2 /. 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
p2 /. 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
p2 . 1 is set
(j1 -' 1) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
fs1 /. 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
p1 /. 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
p1 . 1 is set
(i1 -' 1) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
p1 /. (0 + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
p2 /. (0 + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
F * ((p1 /. (0 + 1)),(p2 /. (0 + 1))) is Element of bool S
(len fs1) - 1 is V11() ext-real V32() set
(len fs1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
((len fs1) -' 1) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
fs2 /. (len fs1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
p1 /. (len fs1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
p1 . (len fs1) is set
fs1 /. (len fs1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
(fs1 /. (len fs1)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
p2 /. (len fs1) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
p2 . (len fs1) is set
(fs2 /. (len fs1)) + 1 is V1() V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT