:: IDEA_1 semantic presentation

REAL is set
NAT is non empty V4() V5() V6() V45() V66() V67() Element of K6(REAL)
K6(REAL) is set
COMPLEX is set
RAT is set
INT is set
K7(NAT,REAL) is Relation-like set
K6(K7(NAT,REAL)) is set
K7(COMPLEX,COMPLEX) is Relation-like set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is Relation-like set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is Relation-like set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is Relation-like set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is Relation-like set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is Relation-like set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is Relation-like set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is Relation-like set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is Relation-like V45() set
K7(K7(NAT,NAT),NAT) is Relation-like V45() set
K6(K7(K7(NAT,NAT),NAT)) is V45() set
NAT is non empty V4() V5() V6() V45() V66() V67() set
K6(NAT) is V45() set
K6(NAT) is V45() set
BOOLEAN is non empty set
1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative V45() V66() Element of NAT
{} is empty V4() V5() V6() V8() V9() V10() V11() V12() integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V35() V36() V37() V38() V45() Function-yielding V66() V68( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V74() FuncSeq-like set
2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative V45() V66() Element of NAT
3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative V45() V66() Element of NAT
0 is empty V4() V5() V6() V8() V9() V10() V11() V12() integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V35() V36() V37() V38() V45() Function-yielding V66() V68( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V74() FuncSeq-like Element of NAT
Seg 1 is non empty V2() V45() V68(1) Element of K6(NAT)
FALSE is boolean Element of BOOLEAN
TRUE is boolean Element of BOOLEAN
K326() is set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n gcd lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
lk * Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk * 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key2 is V11() V12() integer ext-real set
Key2 * lk is V11() V12() integer ext-real set
r is V11() V12() integer ext-real set
r * n is V11() V12() integer ext-real set
(Key2 * lk) + (r * n) is V11() V12() integer ext-real set
ks1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ke1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ke1 * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks2 * n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ke1 * lk) + (ks2 * n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
((ke1 * lk) + (ks2 * n)) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ks2 * n) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ke1 * lk) + ((ks2 * n) mod n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
((ke1 * lk) + ((ks2 * n) mod n)) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ke1 * lk) + 0 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
((ke1 * lk) + 0) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ke1 * lk) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
0 - r is V11() V12() integer ext-real set
ks2 is V11() V12() integer ext-real set
ks1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ke1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ke1 * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ke1 * lk) + (r * n) is V11() V12() integer ext-real set
ke2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ke2 * n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
((ke1 * lk) + (r * n)) + (ke2 * n) is V11() V12() integer ext-real set
(ke1 * lk) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks2 * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ks2 * lk) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
0 - Key2 is V11() V12() integer ext-real set
ks1 is V11() V12() integer ext-real set
ks2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks2 div n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ks2 div n) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative V45() V66() Element of NAT
ke1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ke1 * n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key2 + (ke1 * n) is V11() V12() integer ext-real set
ke2 is V11() V12() integer ext-real set
- ks2 is V11() V12() integer ext-real non positive set
(ks2 div n) * n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(- ks2) + ((ks2 div n) * n) is V11() V12() integer ext-real set
((- ks2) + ((ks2 div n) * n)) + n is V11() V12() integer ext-real set
n * (ks2 div n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
(n * (ks2 div n)) + m is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
- m is V11() V12() integer ext-real non positive set
(- m) + n is V11() V12() integer ext-real set
(- m) + m is V11() V12() integer ext-real set
m1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ke1 * n) * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 + ((ke1 * n) * lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1 + ((ke1 * n) * lk)) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ke1 * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ke1 * lk) * n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 + ((ke1 * lk) * n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1 + ((ke1 * lk) * n)) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
PF is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
PF * n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key2 * lk) + (PF * n) is V11() V12() integer ext-real set
((Key2 * lk) + (PF * n)) + ((ke1 * n) * lk) is V11() V12() integer ext-real set
m2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
m2 * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(m2 * lk) + (PF * n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(m2 * lk) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
m1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
0 - r is V11() V12() integer ext-real set
m2 is V11() V12() integer ext-real set
(ke1 * n) * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 + ((ke1 * n) * lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
QF is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
QF * n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1 + ((ke1 * n) * lk)) + (QF * n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ke1 * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ke1 * lk) + QF is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
((ke1 * lk) + QF) * n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 + (((ke1 * lk) + QF) * n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
PF is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
PF * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(PF * lk) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
PF is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
PF * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(PF * lk) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks1 * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ks1 * lk) mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key2 * n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key2 * n) mod lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key2 mod lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
r * n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(r * n) mod lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 mod n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 - lk is V11() V12() integer ext-real set
Key1 div n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk div n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1 div n) - (lk div n) is V11() V12() integer ext-real set
Key2 is V11() V12() integer ext-real set
(lk div n) - (lk div n) is V11() V12() integer ext-real set
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n * r is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n * (lk div n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n * (lk div n)) + (lk mod n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n * (Key1 div n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n * (Key1 div n)) + (Key1 mod n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n - lk is V11() V12() integer ext-real set
n - 0 is V11() V12() integer ext-real non negative set
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk - n is V11() V12() integer ext-real set
Key1 - n is V11() V12() integer ext-real set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n * lk) mod Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n * lk) div Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 * ((n * lk) div Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1 * ((n * lk) div Key1)) + 0 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n |-> FALSE is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like V45() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
Seg n is V45() V68(n) Element of K6(NAT)
(Seg n) --> FALSE is Relation-like Seg n -defined {FALSE} -valued Function-like total quasi_total V45() FinSequence-like FinSubsequence-like Element of K6(K7((Seg n),{FALSE}))
{FALSE} is non empty V2() V68(1) set
K7((Seg n),{FALSE}) is Relation-like set
K6(K7((Seg n),{FALSE})) is set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Seg n is V45() V68(n) Element of K6(NAT)
lk is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Key1 is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Key2 is Relation-like NAT -defined BOOLEAN -valued Function-like V45() FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
dom Key2 is Element of K6(NAT)
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like V45() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
r is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
ks1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
r /. ks1 is boolean Element of BOOLEAN
lk /. ks1 is boolean Element of BOOLEAN
Key1 /. ks1 is boolean Element of BOOLEAN
(lk /. ks1) 'xor' (Key1 /. ks1) is boolean Element of BOOLEAN
K332((lk /. ks1),(Key1 /. ks1)) is set
K331((lk /. ks1),(Key1 /. ks1)) is set
'not' (lk /. ks1) is boolean set
1 - (lk /. ks1) is set
K330(('not' (lk /. ks1)),(Key1 /. ks1)) is set
'not' ('not' (lk /. ks1)) is boolean set
1 - ('not' (lk /. ks1)) is set
'not' (Key1 /. ks1) is boolean set
1 - (Key1 /. ks1) is set
('not' ('not' (lk /. ks1))) '&' ('not' (Key1 /. ks1)) is set
('not' ('not' (lk /. ks1))) * ('not' (Key1 /. ks1)) is set
'not' (('not' ('not' (lk /. ks1))) '&' ('not' (Key1 /. ks1))) is boolean set
K331((Key1 /. ks1),(lk /. ks1)) is set
K330(('not' (Key1 /. ks1)),(lk /. ks1)) is set
'not' ('not' (Key1 /. ks1)) is boolean set
1 - ('not' (Key1 /. ks1)) is set
('not' ('not' (Key1 /. ks1))) '&' ('not' (lk /. ks1)) is set
('not' ('not' (Key1 /. ks1))) * ('not' (lk /. ks1)) is set
'not' (('not' ('not' (Key1 /. ks1))) '&' ('not' (lk /. ks1))) is boolean set
K331((lk /. ks1),(Key1 /. ks1)) '&' K331((Key1 /. ks1),(lk /. ks1)) is set
'not' K332((lk /. ks1),(Key1 /. ks1)) is boolean set
dom r is V68(n) Element of K6(NAT)
r . ks1 is set
Key2 is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
r is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
dom Key2 is V68(n) Element of K6(NAT)
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
dom r is V68(n) Element of K6(NAT)
Key2 . ks1 is set
Key2 /. ks1 is boolean Element of BOOLEAN
lk /. ks1 is boolean Element of BOOLEAN
Key1 /. ks1 is boolean Element of BOOLEAN
(lk /. ks1) 'xor' (Key1 /. ks1) is boolean Element of BOOLEAN
K332((lk /. ks1),(Key1 /. ks1)) is set
K331((lk /. ks1),(Key1 /. ks1)) is set
'not' (lk /. ks1) is boolean set
1 - (lk /. ks1) is set
K330(('not' (lk /. ks1)),(Key1 /. ks1)) is set
'not' ('not' (lk /. ks1)) is boolean set
1 - ('not' (lk /. ks1)) is set
'not' (Key1 /. ks1) is boolean set
1 - (Key1 /. ks1) is set
('not' ('not' (lk /. ks1))) '&' ('not' (Key1 /. ks1)) is set
('not' ('not' (lk /. ks1))) * ('not' (Key1 /. ks1)) is set
'not' (('not' ('not' (lk /. ks1))) '&' ('not' (Key1 /. ks1))) is boolean set
K331((Key1 /. ks1),(lk /. ks1)) is set
K330(('not' (Key1 /. ks1)),(lk /. ks1)) is set
'not' ('not' (Key1 /. ks1)) is boolean set
1 - ('not' (Key1 /. ks1)) is set
('not' ('not' (Key1 /. ks1))) '&' ('not' (lk /. ks1)) is set
('not' ('not' (Key1 /. ks1))) * ('not' (lk /. ks1)) is set
'not' (('not' ('not' (Key1 /. ks1))) '&' ('not' (lk /. ks1))) is boolean set
K331((lk /. ks1),(Key1 /. ks1)) '&' K331((Key1 /. ks1),(lk /. ks1)) is set
'not' K332((lk /. ks1),(Key1 /. ks1)) is boolean set
r /. ks1 is boolean Element of BOOLEAN
r . ks1 is set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n |-> FALSE is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like V45() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
Seg n is V45() V68(n) Element of K6(NAT)
(Seg n) --> FALSE is Relation-like Seg n -defined {FALSE} -valued Function-like total quasi_total V45() FinSequence-like FinSubsequence-like Element of K6(K7((Seg n),{FALSE}))
K7((Seg n),{FALSE}) is Relation-like set
K6(K7((Seg n),{FALSE})) is set
lk is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,lk,lk) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (n,lk,lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
dom (n,lk,lk) is V68(n) Element of K6(NAT)
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
(n) . Key1 is set
(n,lk,lk) . Key1 is set
(n,lk,lk) /. Key1 is boolean Element of BOOLEAN
lk /. Key1 is boolean Element of BOOLEAN
(lk /. Key1) 'xor' (lk /. Key1) is boolean Element of BOOLEAN
K332((lk /. Key1),(lk /. Key1)) is set
K331((lk /. Key1),(lk /. Key1)) is set
'not' (lk /. Key1) is boolean set
1 - (lk /. Key1) is set
K330(('not' (lk /. Key1)),(lk /. Key1)) is set
'not' ('not' (lk /. Key1)) is boolean set
1 - ('not' (lk /. Key1)) is set
('not' ('not' (lk /. Key1))) '&' ('not' (lk /. Key1)) is set
('not' ('not' (lk /. Key1))) * ('not' (lk /. Key1)) is set
'not' (('not' ('not' (lk /. Key1))) '&' ('not' (lk /. Key1))) is boolean set
K331((lk /. Key1),(lk /. Key1)) '&' K331((lk /. Key1),(lk /. Key1)) is set
'not' K332((lk /. Key1),(lk /. Key1)) is boolean set
len (n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Key1 is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,lk,Key1) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,Key1,lk) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (n,lk,Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
dom (n,lk,Key1) is V68(n) Element of K6(NAT)
Seg n is V45() V68(n) Element of K6(NAT)
len (n,Key1,lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
dom (n,Key1,lk) is V68(n) Element of K6(NAT)
(n,lk,Key1) . Key2 is set
(n,lk,Key1) /. Key2 is boolean Element of BOOLEAN
Key1 /. Key2 is boolean Element of BOOLEAN
lk /. Key2 is boolean Element of BOOLEAN
(Key1 /. Key2) 'xor' (lk /. Key2) is boolean Element of BOOLEAN
K332((Key1 /. Key2),(lk /. Key2)) is set
K331((Key1 /. Key2),(lk /. Key2)) is set
'not' (Key1 /. Key2) is boolean set
1 - (Key1 /. Key2) is set
K330(('not' (Key1 /. Key2)),(lk /. Key2)) is set
'not' ('not' (Key1 /. Key2)) is boolean set
1 - ('not' (Key1 /. Key2)) is set
'not' (lk /. Key2) is boolean set
1 - (lk /. Key2) is set
('not' ('not' (Key1 /. Key2))) '&' ('not' (lk /. Key2)) is set
('not' ('not' (Key1 /. Key2))) * ('not' (lk /. Key2)) is set
'not' (('not' ('not' (Key1 /. Key2))) '&' ('not' (lk /. Key2))) is boolean set
K331((lk /. Key2),(Key1 /. Key2)) is set
K330(('not' (lk /. Key2)),(Key1 /. Key2)) is set
'not' ('not' (lk /. Key2)) is boolean set
1 - ('not' (lk /. Key2)) is set
('not' ('not' (lk /. Key2))) '&' ('not' (Key1 /. Key2)) is set
('not' ('not' (lk /. Key2))) * ('not' (Key1 /. Key2)) is set
'not' (('not' ('not' (lk /. Key2))) '&' ('not' (Key1 /. Key2))) is boolean set
K331((Key1 /. Key2),(lk /. Key2)) '&' K331((lk /. Key2),(Key1 /. Key2)) is set
'not' K332((Key1 /. Key2),(lk /. Key2)) is boolean set
(n,Key1,lk) /. Key2 is boolean Element of BOOLEAN
(n,Key1,lk) . Key2 is set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key2 is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
r is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,Key2,r) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,r,Key2) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n |-> FALSE is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like V45() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
Seg n is V45() V68(n) Element of K6(NAT)
(Seg n) --> FALSE is Relation-like Seg n -defined {FALSE} -valued Function-like total quasi_total V45() FinSequence-like FinSubsequence-like Element of K6(K7((Seg n),{FALSE}))
K7((Seg n),{FALSE}) is Relation-like set
K6(K7((Seg n),{FALSE})) is set
lk is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,(n),lk) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (n,(n),lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
dom (n,(n),lk) is V68(n) Element of K6(NAT)
len lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
dom lk is V68(n) Element of K6(NAT)
dom (n) is V68(n) Element of K6(NAT)
(n) /. Key1 is boolean Element of BOOLEAN
(n |-> FALSE) . Key1 is set
(n,(n),lk) . Key1 is set
(n,(n),lk) /. Key1 is boolean Element of BOOLEAN
lk /. Key1 is boolean Element of BOOLEAN
FALSE 'xor' (lk /. Key1) is boolean Element of BOOLEAN
K332(FALSE,(lk /. Key1)) is set
K331(FALSE,(lk /. Key1)) is set
'not' FALSE is boolean set
1 - FALSE is set
K330(('not' FALSE),(lk /. Key1)) is set
'not' ('not' FALSE) is boolean set
1 - ('not' FALSE) is set
'not' (lk /. Key1) is boolean set
1 - (lk /. Key1) is set
('not' ('not' FALSE)) '&' ('not' (lk /. Key1)) is set
('not' ('not' FALSE)) * ('not' (lk /. Key1)) is set
'not' (('not' ('not' FALSE)) '&' ('not' (lk /. Key1))) is boolean set
K331((lk /. Key1),FALSE) is set
K330(('not' (lk /. Key1)),FALSE) is set
'not' ('not' (lk /. Key1)) is boolean set
1 - ('not' (lk /. Key1)) is set
('not' ('not' (lk /. Key1))) '&' ('not' FALSE) is set
('not' ('not' (lk /. Key1))) * ('not' FALSE) is set
'not' (('not' ('not' (lk /. Key1))) '&' ('not' FALSE)) is boolean set
K331(FALSE,(lk /. Key1)) '&' K331((lk /. Key1),FALSE) is set
'not' K332(FALSE,(lk /. Key1)) is boolean set
lk . Key1 is set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Key1 is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,lk,Key1) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Key2 is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,(n,lk,Key1),Key2) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,Key1,Key2) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,lk,(n,Key1,Key2)) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (n,(n,lk,Key1),Key2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
dom (n,(n,lk,Key1),Key2) is V68(n) Element of K6(NAT)
Seg n is V45() V68(n) Element of K6(NAT)
len (n,lk,(n,Key1,Key2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
dom (n,lk,(n,Key1,Key2)) is V68(n) Element of K6(NAT)
(n,(n,lk,Key1),Key2) . r is set
(n,(n,lk,Key1),Key2) /. r is boolean Element of BOOLEAN
(n,lk,Key1) /. r is boolean Element of BOOLEAN
Key2 /. r is boolean Element of BOOLEAN
((n,lk,Key1) /. r) 'xor' (Key2 /. r) is boolean Element of BOOLEAN
K332(((n,lk,Key1) /. r),(Key2 /. r)) is set
K331(((n,lk,Key1) /. r),(Key2 /. r)) is set
'not' ((n,lk,Key1) /. r) is boolean set
1 - ((n,lk,Key1) /. r) is set
K330(('not' ((n,lk,Key1) /. r)),(Key2 /. r)) is set
'not' ('not' ((n,lk,Key1) /. r)) is boolean set
1 - ('not' ((n,lk,Key1) /. r)) is set
'not' (Key2 /. r) is boolean set
1 - (Key2 /. r) is set
('not' ('not' ((n,lk,Key1) /. r))) '&' ('not' (Key2 /. r)) is set
('not' ('not' ((n,lk,Key1) /. r))) * ('not' (Key2 /. r)) is set
'not' (('not' ('not' ((n,lk,Key1) /. r))) '&' ('not' (Key2 /. r))) is boolean set
K331((Key2 /. r),((n,lk,Key1) /. r)) is set
K330(('not' (Key2 /. r)),((n,lk,Key1) /. r)) is set
'not' ('not' (Key2 /. r)) is boolean set
1 - ('not' (Key2 /. r)) is set
('not' ('not' (Key2 /. r))) '&' ('not' ((n,lk,Key1) /. r)) is set
('not' ('not' (Key2 /. r))) * ('not' ((n,lk,Key1) /. r)) is set
'not' (('not' ('not' (Key2 /. r))) '&' ('not' ((n,lk,Key1) /. r))) is boolean set
K331(((n,lk,Key1) /. r),(Key2 /. r)) '&' K331((Key2 /. r),((n,lk,Key1) /. r)) is set
'not' K332(((n,lk,Key1) /. r),(Key2 /. r)) is boolean set
lk /. r is boolean Element of BOOLEAN
Key1 /. r is boolean Element of BOOLEAN
(lk /. r) 'xor' (Key1 /. r) is boolean Element of BOOLEAN
K332((lk /. r),(Key1 /. r)) is set
K331((lk /. r),(Key1 /. r)) is set
'not' (lk /. r) is boolean set
1 - (lk /. r) is set
K330(('not' (lk /. r)),(Key1 /. r)) is set
'not' ('not' (lk /. r)) is boolean set
1 - ('not' (lk /. r)) is set
'not' (Key1 /. r) is boolean set
1 - (Key1 /. r) is set
('not' ('not' (lk /. r))) '&' ('not' (Key1 /. r)) is set
('not' ('not' (lk /. r))) * ('not' (Key1 /. r)) is set
'not' (('not' ('not' (lk /. r))) '&' ('not' (Key1 /. r))) is boolean set
K331((Key1 /. r),(lk /. r)) is set
K330(('not' (Key1 /. r)),(lk /. r)) is set
'not' ('not' (Key1 /. r)) is boolean set
1 - ('not' (Key1 /. r)) is set
('not' ('not' (Key1 /. r))) '&' ('not' (lk /. r)) is set
('not' ('not' (Key1 /. r))) * ('not' (lk /. r)) is set
'not' (('not' ('not' (Key1 /. r))) '&' ('not' (lk /. r))) is boolean set
K331((lk /. r),(Key1 /. r)) '&' K331((Key1 /. r),(lk /. r)) is set
'not' K332((lk /. r),(Key1 /. r)) is boolean set
((lk /. r) 'xor' (Key1 /. r)) 'xor' (Key2 /. r) is boolean Element of BOOLEAN
K332(((lk /. r) 'xor' (Key1 /. r)),(Key2 /. r)) is set
K331(((lk /. r) 'xor' (Key1 /. r)),(Key2 /. r)) is set
'not' ((lk /. r) 'xor' (Key1 /. r)) is boolean set
1 - ((lk /. r) 'xor' (Key1 /. r)) is set
K330(('not' ((lk /. r) 'xor' (Key1 /. r))),(Key2 /. r)) is set
'not' ('not' ((lk /. r) 'xor' (Key1 /. r))) is boolean set
1 - ('not' ((lk /. r) 'xor' (Key1 /. r))) is set
('not' ('not' ((lk /. r) 'xor' (Key1 /. r)))) '&' ('not' (Key2 /. r)) is set
('not' ('not' ((lk /. r) 'xor' (Key1 /. r)))) * ('not' (Key2 /. r)) is set
'not' (('not' ('not' ((lk /. r) 'xor' (Key1 /. r)))) '&' ('not' (Key2 /. r))) is boolean set
K331((Key2 /. r),((lk /. r) 'xor' (Key1 /. r))) is set
K330(('not' (Key2 /. r)),((lk /. r) 'xor' (Key1 /. r))) is set
('not' ('not' (Key2 /. r))) '&' ('not' ((lk /. r) 'xor' (Key1 /. r))) is set
('not' ('not' (Key2 /. r))) * ('not' ((lk /. r) 'xor' (Key1 /. r))) is set
'not' (('not' ('not' (Key2 /. r))) '&' ('not' ((lk /. r) 'xor' (Key1 /. r)))) is boolean set
K331(((lk /. r) 'xor' (Key1 /. r)),(Key2 /. r)) '&' K331((Key2 /. r),((lk /. r) 'xor' (Key1 /. r))) is set
'not' K332(((lk /. r) 'xor' (Key1 /. r)),(Key2 /. r)) is boolean set
(Key1 /. r) 'xor' (Key2 /. r) is boolean Element of BOOLEAN
K332((Key1 /. r),(Key2 /. r)) is set
K331((Key1 /. r),(Key2 /. r)) is set
K330(('not' (Key1 /. r)),(Key2 /. r)) is set
('not' ('not' (Key1 /. r))) '&' ('not' (Key2 /. r)) is set
('not' ('not' (Key1 /. r))) * ('not' (Key2 /. r)) is set
'not' (('not' ('not' (Key1 /. r))) '&' ('not' (Key2 /. r))) is boolean set
K331((Key2 /. r),(Key1 /. r)) is set
K330(('not' (Key2 /. r)),(Key1 /. r)) is set
('not' ('not' (Key2 /. r))) '&' ('not' (Key1 /. r)) is set
('not' ('not' (Key2 /. r))) * ('not' (Key1 /. r)) is set
'not' (('not' ('not' (Key2 /. r))) '&' ('not' (Key1 /. r))) is boolean set
K331((Key1 /. r),(Key2 /. r)) '&' K331((Key2 /. r),(Key1 /. r)) is set
'not' K332((Key1 /. r),(Key2 /. r)) is boolean set
(lk /. r) 'xor' ((Key1 /. r) 'xor' (Key2 /. r)) is boolean Element of BOOLEAN
K332((lk /. r),((Key1 /. r) 'xor' (Key2 /. r))) is set
K331((lk /. r),((Key1 /. r) 'xor' (Key2 /. r))) is set
K330(('not' (lk /. r)),((Key1 /. r) 'xor' (Key2 /. r))) is set
'not' ((Key1 /. r) 'xor' (Key2 /. r)) is boolean set
1 - ((Key1 /. r) 'xor' (Key2 /. r)) is set
('not' ('not' (lk /. r))) '&' ('not' ((Key1 /. r) 'xor' (Key2 /. r))) is set
('not' ('not' (lk /. r))) * ('not' ((Key1 /. r) 'xor' (Key2 /. r))) is set
'not' (('not' ('not' (lk /. r))) '&' ('not' ((Key1 /. r) 'xor' (Key2 /. r)))) is boolean set
K331(((Key1 /. r) 'xor' (Key2 /. r)),(lk /. r)) is set
K330(('not' ((Key1 /. r) 'xor' (Key2 /. r))),(lk /. r)) is set
'not' ('not' ((Key1 /. r) 'xor' (Key2 /. r))) is boolean set
1 - ('not' ((Key1 /. r) 'xor' (Key2 /. r))) is set
('not' ('not' ((Key1 /. r) 'xor' (Key2 /. r)))) '&' ('not' (lk /. r)) is set
('not' ('not' ((Key1 /. r) 'xor' (Key2 /. r)))) * ('not' (lk /. r)) is set
'not' (('not' ('not' ((Key1 /. r) 'xor' (Key2 /. r)))) '&' ('not' (lk /. r))) is boolean set
K331((lk /. r),((Key1 /. r) 'xor' (Key2 /. r))) '&' K331(((Key1 /. r) 'xor' (Key2 /. r)),(lk /. r)) is set
'not' K332((lk /. r),((Key1 /. r) 'xor' (Key2 /. r))) is boolean set
(n,Key1,Key2) /. r is boolean Element of BOOLEAN
(lk /. r) 'xor' ((n,Key1,Key2) /. r) is boolean Element of BOOLEAN
K332((lk /. r),((n,Key1,Key2) /. r)) is set
K331((lk /. r),((n,Key1,Key2) /. r)) is set
K330(('not' (lk /. r)),((n,Key1,Key2) /. r)) is set
'not' ((n,Key1,Key2) /. r) is boolean set
1 - ((n,Key1,Key2) /. r) is set
('not' ('not' (lk /. r))) '&' ('not' ((n,Key1,Key2) /. r)) is set
('not' ('not' (lk /. r))) * ('not' ((n,Key1,Key2) /. r)) is set
'not' (('not' ('not' (lk /. r))) '&' ('not' ((n,Key1,Key2) /. r))) is boolean set
K331(((n,Key1,Key2) /. r),(lk /. r)) is set
K330(('not' ((n,Key1,Key2) /. r)),(lk /. r)) is set
'not' ('not' ((n,Key1,Key2) /. r)) is boolean set
1 - ('not' ((n,Key1,Key2) /. r)) is set
('not' ('not' ((n,Key1,Key2) /. r))) '&' ('not' (lk /. r)) is set
('not' ('not' ((n,Key1,Key2) /. r))) * ('not' (lk /. r)) is set
'not' (('not' ('not' ((n,Key1,Key2) /. r))) '&' ('not' (lk /. r))) is boolean set
K331((lk /. r),((n,Key1,Key2) /. r)) '&' K331(((n,Key1,Key2) /. r),(lk /. r)) is set
'not' K332((lk /. r),((n,Key1,Key2) /. r)) is boolean set
(n,lk,(n,Key1,Key2)) /. r is boolean Element of BOOLEAN
(n,lk,(n,Key1,Key2)) . r is set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n -BinarySequence 0 is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n) is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n |-> FALSE is Relation-like NAT -defined BOOLEAN -valued Function-like V45() V68(n) FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like V45() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
Seg n is V45() V68(n) Element of K6(NAT)
(Seg n) --> FALSE is Relation-like Seg n -defined {FALSE} -valued Function-like total quasi_total V45() FinSequence-like FinSubsequence-like Element of K6(K7((Seg n),{FALSE}))
K7((Seg n),{FALSE}) is Relation-like set
K6(K7((Seg n),{FALSE})) is set
len (n -BinarySequence 0) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
dom (n -BinarySequence 0) is V68(n) Element of K6(NAT)
len (n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
dom (n) is V68(n) Element of K6(NAT)
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
lk -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power (lk -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
0 div (2 to_power (lk -' 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(0 div (2 to_power (lk -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
0 mod 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n) /. lk is boolean Element of BOOLEAN
(n |-> FALSE) . lk is set
(n -BinarySequence 0) . lk is set
(n -BinarySequence 0) /. lk is boolean Element of BOOLEAN
IFEQ (((0 div (2 to_power (lk -' 1))) mod 2),0,FALSE,TRUE) is boolean Element of BOOLEAN
(n) . lk is set
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
lk + Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk + Key1) mod (2 to_power n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(2 to_power n) - lk is V11() V12() integer ext-real set
lk - lk is V11() V12() integer ext-real set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk) mod (2 to_power n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk,n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk,n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk,n) mod (2 to_power lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk,n,(lk,n)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n + (lk,n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
(n + (lk,n)) mod (2 to_power lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n + (lk,n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(2 to_power lk) - n is V11() V12() integer ext-real set
n + ((2 to_power lk) - n) is V11() V12() integer ext-real set
0 + (2 to_power lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(2 to_power lk) mod (2 to_power lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1,n,lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n + lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
2 to_power Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n + lk) mod (2 to_power Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1,lk,n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk + n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
(lk + n) mod (2 to_power Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk,0,n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
0 + n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
2 to_power lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(0 + n) mod (2 to_power lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1,n,lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n + lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
2 to_power Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n + lk) mod (2 to_power Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1,(Key1,n,lk),Key2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1,n,lk) + Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
((Key1,n,lk) + Key2) mod (2 to_power Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1,lk,Key2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk + Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
(lk + Key2) mod (2 to_power Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1,n,(Key1,lk,Key2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n + (Key1,lk,Key2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
(n + (Key1,lk,Key2)) mod (2 to_power Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n + lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n + lk) + Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
((n + lk) + Key2) mod (2 to_power Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk + Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n + (lk + Key2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n + (lk + Key2)) mod (2 to_power Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key1,n,lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n + lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
2 to_power Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n + lk) mod (2 to_power Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk,n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk,n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk,n) mod (2 to_power lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
2 to_power n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk,n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk,n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
(n,lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() set
(n,Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk) * (n,Key1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(2 to_power n) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative V45() V66() Element of NAT
((n,lk) * (n,Key1)) mod ((2 to_power n) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,(((n,lk) * (n,Key1)) mod ((2 to_power n) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
n is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative V45() V66() Element of NAT
lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(2 to_power n) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative V45() V66() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative V45() V66() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative V45() V66() Element of NAT
(1 + 1) - 1 is V11() V12() integer ext-real set
((2 to_power n) + 1) - 1 is V11() V12() integer ext-real set
((1 + 1) - 1) - 1 is V11() V12() integer ext-real set
(((2 to_power n) + 1) - 1) - 1 is V11() V12() integer ext-real set
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
r * r is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
Key2 * Key1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(Key2 * Key1) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative V45() V66() Element of NAT
(r * r) mod Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
1 mod Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk,ks2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,ks2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk) * (n,ks2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
((n,lk) * (n,ks2)) mod ((2 to_power n) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,(((n,lk) * (n,ks2)) mod ((2 to_power n) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,0) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(2 to_power n) * (n,0) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
((2 to_power n) * (n,0)) mod Key2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,(((2 to_power n) * (n,0)) mod Key2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,((r * r) mod Key2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks1 * lk is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(ks1 * lk) mod ((2 to_power n) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,ks1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk,ks2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,ks2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk) * (n,ks2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
((n,lk) * (n,ks2)) mod ((2 to_power n) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,(((n,lk) * (n,ks2)) mod ((2 to_power n) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk * (n,ks2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk * (n,ks2)) mod ((2 to_power n) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,((lk * (n,ks2)) mod ((2 to_power n) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk * ks1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk * ks1) mod ((2 to_power n) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,((lk * ks1) mod ((2 to_power n) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
ks2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk,ks2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,ks2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,lk) * (n,ks2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
((n,lk) * (n,ks2)) mod ((2 to_power n) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,(((n,lk) * (n,ks2)) mod ((2 to_power n) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk * (n,ks2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk * (n,ks2)) mod ((2 to_power n) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,((lk * (n,ks2)) mod ((2 to_power n) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
lk * ks1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(lk * ks1) mod ((2 to_power n) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative V45() V66() Element of NAT
(n,((lk * ks1) mod ((2