REAL is set
NAT is non empty V4() V5() V6() Element of bool REAL
bool REAL is set
COMPLEX is set
NAT is non empty V4() V5() V6() set
bool NAT is set
bool NAT is set
RAT is set
INT is set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is set
BOOLEAN is non empty set
1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
[:1,1:] is set
bool [:1,1:] is set
[:[:1,1:],1:] is set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is set
2 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
[:2,2:] is set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is set
TOP-REAL 2 is V187() L15()
the U1 of (TOP-REAL 2) is set
0 is empty trivial V4() V5() V6() V8() V9() V10() V11() V12() V13() functional FinSequence-membered ext-real non negative V75() Element of NAT
3 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
TRUE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
Seg 1 is non empty V34() V41(1) Element of bool NAT
K20(1) is non empty trivial set
Seg 2 is non empty V34() V41(2) Element of bool NAT
K21(1,2) is non empty set
{} is empty trivial V4() V5() V6() V8() V9() V10() V11() V12() V13() functional FinSequence-membered ext-real non negative V75() set
<*FALSE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*FALSE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K333() is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K334() is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power (n + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b1 where b1 is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b1 = n } is set
k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*z*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
k ^ <*z*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
Absval k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (z,FALSE,0,(2 to_power n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval k) + (IFEQ (z,FALSE,0,(2 to_power n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(Absval k) + 0 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(2 to_power n) + (2 to_power (n + 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(Absval x) + (2 to_power n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(Absval k) + (2 to_power n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(2 to_power n) + (2 to_power n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(2 to_power n) * 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power n) * (2 to_power 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*x*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b1 where b1 is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b1 = n } is set
z is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*z*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z ^ <*z*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
y is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*y*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
k ^ <*y*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (z,FALSE,0,(2 to_power n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval z) + (IFEQ (z,FALSE,0,(2 to_power n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Absval k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (y,FALSE,0,(2 to_power n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval k) + (IFEQ (y,FALSE,0,(2 to_power n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
IFEQ (z,FALSE,0,(2 to_power n)) is V11() V12() ext-real Element of REAL
IFEQ (y,FALSE,0,(2 to_power n)) is V11() V12() ext-real Element of REAL
IFEQ (y,FALSE,0,(2 to_power n)) is V11() V12() ext-real Element of REAL
IFEQ (z,FALSE,0,(2 to_power n)) is V11() V12() ext-real Element of REAL
n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*k*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*z*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is V15() V18( NAT ) Function-like V34() FinSequence-like FinSubsequence-like set
Rev n is V15() V18( NAT ) Function-like V34() FinSequence-like FinSubsequence-like set
x is V15() V18( NAT ) Function-like V34() FinSequence-like FinSubsequence-like set
Rev x is V15() V18( NAT ) Function-like V34() FinSequence-like FinSubsequence-like set
Rev (Rev n) is V15() V18( NAT ) Function-like V34() FinSequence-like FinSubsequence-like set
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
n |-> FALSE is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b1 where b1 is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b1 = n } is set
(Seg n) --> FALSE is V15() V18( Seg n) V19(K20(FALSE)) Function-like V29( Seg n,K20(FALSE)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(FALSE):]
K20(FALSE) is non empty trivial set
[:(Seg n),K20(FALSE):] is set
bool [:(Seg n),K20(FALSE):] is set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
n |-> 1 is V15() V18( NAT ) V19( NAT ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on NAT
n -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is V15() V18( NAT ) V19( NAT ) Function-like V34() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = n } is set
(Seg n) --> 1 is V15() V18( Seg n) V19(K20(1)) Function-like V29( Seg n,K20(1)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(1):]
[:(Seg n),K20(1):] is set
bool [:(Seg n),K20(1):] is set
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
len ('not' x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x . k is set
('not' x) . k is set
('not' x) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
x /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (x /. k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (x /. k) is V11() V12() V13() ext-real set
'not' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - FALSE is V11() V12() V13() ext-real set
(n |-> 1) . k is set
len (n |-> 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
0* (n + 1) is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL (n + 1)
REAL (n + 1) is functional FinSequence-membered FinSequenceSet of REAL
(n + 1) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n + 1 } is set
(n + 1) |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like Element of (n + 1) -tuples_on REAL
Seg (n + 1) is non empty V34() V41(n + 1) Element of bool NAT
(Seg (n + 1)) --> 0 is V15() V18( Seg (n + 1)) V19(K20(0)) Function-like V29( Seg (n + 1),K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg (n + 1)),K20(0):]
[:(Seg (n + 1)),K20(0):] is set
bool [:(Seg (n + 1)),K20(0):] is set
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
k ^ <*FALSE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
Absval (k ^ <*FALSE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Absval k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (FALSE,FALSE,0,(2 to_power n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval k) + (IFEQ (FALSE,FALSE,0,(2 to_power n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0 + (IFEQ (FALSE,FALSE,0,(2 to_power n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* 1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL 1
REAL 1 is functional FinSequence-membered FinSequenceSet of REAL
1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 1 } is set
1 |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on REAL
(Seg 1) --> 0 is V15() V18( Seg 1) V19(K20(0)) Function-like V29( Seg 1,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg 1),K20(0):]
K20(0) is non empty trivial set
[:(Seg 1),K20(0):] is set
bool [:(Seg 1),K20(0):] is set
n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power n) - 1 is V11() V12() V13() ext-real set
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval ('not' x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Absval x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
- (Absval x) is V11() V12() V13() ext-real non positive set
(- (Absval x)) + (2 to_power n) is V11() V12() V13() ext-real set
((- (Absval x)) + (2 to_power n)) - 1 is V11() V12() V13() ext-real set
- 0 is V11() V12() V13() ext-real non positive set
(- 0) + (2 to_power n) is V11() V12() V13() ext-real set
((- 0) + (2 to_power n)) - 1 is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
Rev (0* n) is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like FinSequence of REAL
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
dom (0* n) is Element of bool NAT
len (0* n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len (0* n)) is V34() V41( len (0* n)) Element of bool NAT
n - x is V11() V12() V13() ext-real set
(n - x) + 1 is V11() V12() V13() ext-real set
(len (0* n)) - x is V11() V12() V13() ext-real set
((len (0* n)) - x) + 1 is V11() V12() V13() ext-real set
(Rev (0* n)) . x is set
(0* n) . (((len (0* n)) - x) + 1) is set
(0* n) . x is set
dom (Rev (0* n)) is Element of bool NAT
len (Rev (0* n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len (Rev (0* n))) is V34() V41( len (Rev (0* n))) Element of bool NAT
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Rev ('not' x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
dom ('not' x) is Element of bool NAT
len ('not' x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len ('not' x)) is V34() V41( len ('not' x)) Element of bool NAT
n - k is V11() V12() V13() ext-real set
(n - k) + 1 is V11() V12() V13() ext-real set
(len ('not' x)) - k is V11() V12() V13() ext-real set
((len ('not' x)) - k) + 1 is V11() V12() V13() ext-real set
(Rev ('not' x)) . k is set
('not' x) . (((len ('not' x)) - k) + 1) is set
n |-> 1 is V15() V18( NAT ) V19( NAT ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on NAT
n -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is V15() V18( NAT ) V19( NAT ) Function-like V34() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = n } is set
(Seg n) --> 1 is V15() V18( Seg n) V19(K20(1)) Function-like V29( Seg n,K20(1)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(1):]
[:(Seg n),K20(1):] is set
bool [:(Seg n),K20(1):] is set
(n |-> 1) . (((len ('not' x)) - k) + 1) is set
(n |-> 1) . k is set
('not' x) . k is set
dom (Rev ('not' x)) is Element of bool NAT
len (Rev ('not' x)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len (Rev ('not' x))) is V34() V41( len (Rev ('not' x))) Element of bool NAT
Bin1 1 is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(Bin1 1) /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*n*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Bin1 n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval (Bin1 n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
Bin1 (n + 1) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval (Bin1 (n + 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
(Bin1 n) ^ <*FALSE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
Absval ((Bin1 n) ^ <*FALSE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (FALSE,FALSE,0,(2 to_power n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval (Bin1 n)) + (IFEQ (FALSE,FALSE,0,(2 to_power n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(Absval (Bin1 n)) + 0 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Absval (Bin1 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
n 'or' x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - n is V11() V12() V13() ext-real set
'not' x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - x is V11() V12() V13() ext-real set
('not' n) '&' ('not' x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' n) * ('not' x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' n) '&' ('not' x)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' n) '&' ('not' x)) is V11() V12() V13() ext-real set
'not' n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*n*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*x*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
add_ovfl (<*n*>,<*x*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*TRUE*> /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(<*TRUE*> /. 1) '&' (<*TRUE*> /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(<*TRUE*> /. 1) * (<*TRUE*> /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
<*n*> /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*x*> /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(<*n*> /. 1) '&' (<*x*> /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(<*n*> /. 1) * (<*x*> /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
carry (<*n*>,<*x*>) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (<*n*>,<*x*>)) /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(<*n*> /. 1) * ((carry (<*n*>,<*x*>)) /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((<*n*> /. 1) '&' (<*x*> /. 1)) 'or' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((<*n*> /. 1) '&' (<*x*> /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((<*n*> /. 1) '&' (<*x*> /. 1)) is V11() V12() V13() ext-real set
'not' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)) is V11() V12() V13() ext-real set
('not' ((<*n*> /. 1) '&' (<*x*> /. 1))) '&' ('not' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ((<*n*> /. 1) '&' (<*x*> /. 1))) * ('not' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ((<*n*> /. 1) '&' (<*x*> /. 1))) '&' ('not' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ((<*n*> /. 1) '&' (<*x*> /. 1))) '&' ('not' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)))) is V11() V12() V13() ext-real set
(<*x*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(<*x*> /. 1) * ((carry (<*n*>,<*x*>)) /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(((<*n*> /. 1) '&' (<*x*> /. 1)) 'or' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1))) 'or' ((<*x*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (((<*n*> /. 1) '&' (<*x*> /. 1)) 'or' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (((<*n*> /. 1) '&' (<*x*> /. 1)) 'or' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1))) is V11() V12() V13() ext-real set
'not' ((<*x*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((<*x*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)) is V11() V12() V13() ext-real set
('not' (((<*n*> /. 1) '&' (<*x*> /. 1)) 'or' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)))) '&' ('not' ((<*x*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' (((<*n*> /. 1) '&' (<*x*> /. 1)) 'or' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)))) * ('not' ((<*x*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' (((<*n*> /. 1) '&' (<*x*> /. 1)) 'or' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)))) '&' ('not' ((<*x*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' (((<*n*> /. 1) '&' (<*x*> /. 1)) 'or' ((<*n*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)))) '&' ('not' ((<*x*> /. 1) '&' ((carry (<*n*>,<*x*>)) /. 1)))) is V11() V12() V13() ext-real set
carry (<*TRUE*>,<*TRUE*>) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (<*TRUE*>,<*TRUE*>)) /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(<*TRUE*> /. 1) * ((carry (<*TRUE*>,<*TRUE*>)) /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1)) 'or' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1)) is V11() V12() V13() ext-real set
'not' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)) is V11() V12() V13() ext-real set
('not' ((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1))) '&' ('not' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1))) * ('not' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1))) '&' ('not' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1))) '&' ('not' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)))) is V11() V12() V13() ext-real set
(((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1)) 'or' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1))) 'or' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1)) 'or' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1)) 'or' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1))) is V11() V12() V13() ext-real set
('not' (((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1)) 'or' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)))) '&' ('not' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' (((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1)) 'or' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)))) * ('not' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' (((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1)) 'or' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)))) '&' ('not' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' (((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1)) 'or' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)))) '&' ('not' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)))) is V11() V12() V13() ext-real set
'not' <*FALSE*> is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
len <*FALSE*> is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
<*FALSE*> /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*FALSE*> . 1 is set
len ('not' <*FALSE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
('not' <*FALSE*>) . n is set
('not' <*FALSE*>) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (<*FALSE*> /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (<*FALSE*> /. n) is V11() V12() V13() ext-real set
'not' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - FALSE is V11() V12() V13() ext-real set
<*TRUE*> . n is set
'not' <*TRUE*> is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
len <*TRUE*> is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
<*TRUE*> /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*TRUE*> . 1 is set
len ('not' <*TRUE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
('not' <*TRUE*>) . n is set
('not' <*TRUE*>) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (<*TRUE*> /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (<*TRUE*> /. n) is V11() V12() V13() ext-real set
'not' TRUE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - TRUE is V11() V12() V13() ext-real set
<*FALSE*> . n is set
<*FALSE*> + <*FALSE*> is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
add_ovfl (<*FALSE*>,<*FALSE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
Absval (<*FALSE*> + <*FALSE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Absval <*FALSE*> is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval <*FALSE*>) + (Absval <*FALSE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(Absval <*FALSE*>) + 0 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
<*FALSE*> + <*TRUE*> is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*TRUE*> + <*FALSE*> is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
add_ovfl (<*FALSE*>,<*TRUE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
Absval (<*FALSE*> + <*TRUE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Absval <*FALSE*> is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Absval <*TRUE*> is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval <*FALSE*>) + (Absval <*TRUE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(Absval <*FALSE*>) + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
0 + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
add_ovfl (<*TRUE*>,<*FALSE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
Absval (<*TRUE*> + <*FALSE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval <*TRUE*>) + (Absval <*FALSE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(Absval <*TRUE*>) + 0 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
<*TRUE*> + <*TRUE*> is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
add_ovfl (<*TRUE*>,<*TRUE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
Absval (<*TRUE*> + <*TRUE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval (<*TRUE*> + <*TRUE*>)) + 2 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
((Absval (<*TRUE*> + <*TRUE*>)) + 2) - 2 is V11() V12() V13() ext-real set
2 to_power 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval (<*TRUE*> + <*TRUE*>)) + (2 to_power 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((Absval (<*TRUE*> + <*TRUE*>)) + (2 to_power 1)) - 2 is V11() V12() V13() ext-real set
IFEQ ((add_ovfl (<*TRUE*>,<*TRUE*>)),FALSE,0,(2 to_power 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval (<*TRUE*> + <*TRUE*>)) + (IFEQ ((add_ovfl (<*TRUE*>,<*TRUE*>)),FALSE,0,(2 to_power 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((Absval (<*TRUE*> + <*TRUE*>)) + (IFEQ ((add_ovfl (<*TRUE*>,<*TRUE*>)),FALSE,0,(2 to_power 1)))) - 2 is V11() V12() V13() ext-real set
Absval <*TRUE*> is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval <*TRUE*>) + (Absval <*TRUE*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((Absval <*TRUE*>) + (Absval <*TRUE*>)) - 2 is V11() V12() V13() ext-real set
(Absval <*TRUE*>) + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
((Absval <*TRUE*>) + 1) - 2 is V11() V12() V13() ext-real set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(1 + 1) - 2 is V11() V12() V13() ext-real set
Absval <*FALSE*> is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Bin1 n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
carry (x,(Bin1 n)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (x,(Bin1 n))) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
n -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (n -' 1) is V34() V41(n -' 1) Element of bool NAT
z is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
x /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(carry (x,(Bin1 n))) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
n -' z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n -' z) + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
z - 1 is V11() V12() V13() ext-real set
k is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n -' k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n -' k) + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
x /. ((n -' k) + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(carry (x,(Bin1 n))) /. ((n -' k) + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
k + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
n -' (k + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n -' (k + 1)) + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
x /. ((n -' (k + 1)) + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(carry (x,(Bin1 n))) /. ((n -' (k + 1)) + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
n - 1 is V11() V12() V13() ext-real set
(n - 1) - k is V11() V12() V13() ext-real set
n - k is V11() V12() V13() ext-real set
(n - k) - 1 is V11() V12() V13() ext-real set
Seg n is non empty V34() V41(n) Element of bool NAT
(Bin1 n) /. (n -' k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(carry (x,(Bin1 n))) /. (n -' k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
((Bin1 n) /. (n -' k)) '&' ((carry (x,(Bin1 n))) /. (n -' k)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
((Bin1 n) /. (n -' k)) * ((carry (x,(Bin1 n))) /. (n -' k)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
x /. (n -' k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x /. (n -' k)) '&' ((Bin1 n) /. (n -' k)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x /. (n -' k)) * ((Bin1 n) /. (n -' k)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(x /. (n -' k)) '&' ((carry (x,(Bin1 n))) /. (n -' k)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x /. (n -' k)) * ((carry (x,(Bin1 n))) /. (n -' k)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((x /. (n -' k)) '&' ((Bin1 n) /. (n -' k))) 'or' ((x /. (n -' k)) '&' ((carry (x,(Bin1 n))) /. (n -' k))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((x /. (n -' k)) '&' ((Bin1 n) /. (n -' k))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((x /. (n -' k)) '&' ((Bin1 n) /. (n -' k))) is V11() V12() V13() ext-real set
'not' ((x /. (n -' k)) '&' ((carry (x,(Bin1 n))) /. (n -' k))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((x /. (n -' k)) '&' ((carry (x,(Bin1 n))) /. (n -' k))) is V11() V12() V13() ext-real set
('not' ((x /. (n -' k)) '&' ((Bin1 n) /. (n -' k)))) '&' ('not' ((x /. (n -' k)) '&' ((carry (x,(Bin1 n))) /. (n -' k)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ((x /. (n -' k)) '&' ((Bin1 n) /. (n -' k)))) * ('not' ((x /. (n -' k)) '&' ((carry (x,(Bin1 n))) /. (n -' k)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ((x /. (n -' k)) '&' ((Bin1 n) /. (n -' k)))) '&' ('not' ((x /. (n -' k)) '&' ((carry (x,(Bin1 n))) /. (n -' k))))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ((x /. (n -' k)) '&' ((Bin1 n) /. (n -' k)))) '&' ('not' ((x /. (n -' k)) '&' ((carry (x,(Bin1 n))) /. (n -' k))))) is V11() V12() V13() ext-real set
n - z is V11() V12() V13() ext-real set
(n - z) + 1 is V11() V12() V13() ext-real set
n - (z - 1) is V11() V12() V13() ext-real set
n - 1 is V11() V12() V13() ext-real set
((n -' z) + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
n -' ((n -' z) + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n -' ((n -' z) + 1)) + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(n -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
x /. ((n -' 1) + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(carry (x,(Bin1 n))) /. ((n -' 1) + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Bin1 n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' (Bin1 n) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
carry (x,(Bin1 n)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (x,(Bin1 n))) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
len ('not' (Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
len (carry (x,(Bin1 n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg n is non empty V34() V41(n) Element of bool NAT
(carry (x,(Bin1 n))) . k is set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(carry (x,(Bin1 n))) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' TRUE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - TRUE is V11() V12() V13() ext-real set
(Bin1 n) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((Bin1 n) /. k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - ((Bin1 n) /. k) is V11() V12() V13() ext-real set
('not' (Bin1 n)) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
('not' (Bin1 n)) . k is set
(carry (x,(Bin1 n))) . k is set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(carry (x,(Bin1 n))) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - FALSE is V11() V12() V13() ext-real set
(Bin1 n) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((Bin1 n) /. k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - ((Bin1 n) /. k) is V11() V12() V13() ext-real set
('not' (Bin1 n)) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
('not' (Bin1 n)) . k is set
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
Bin1 n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
carry (x,(Bin1 n)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (x,(Bin1 n))) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
len ('not' k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
len k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
len (carry (x,(Bin1 n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k . z is set
x . z is set
('not' k) . z is set
'not' (Bin1 n) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len ('not' (Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(carry (x,(Bin1 n))) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(Bin1 n) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
((Bin1 n) /. z) '&' ((carry (x,(Bin1 n))) /. z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
((Bin1 n) /. z) * ((carry (x,(Bin1 n))) /. z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
z + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(carry (x,(Bin1 n))) . (z + 1) is set
('not' (Bin1 n)) . 2 is set
('not' (Bin1 n)) /. 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(Bin1 n) /. 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((Bin1 n) /. 2) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - ((Bin1 n) /. 2) is V11() V12() V13() ext-real set
'not' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - FALSE is V11() V12() V13() ext-real set
(carry (x,(Bin1 n))) /. (z + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
x /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x /. z) '&' ((Bin1 n) /. z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x /. z) * ((Bin1 n) /. z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(x /. z) '&' ((carry (x,(Bin1 n))) /. z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x /. z) * ((carry (x,(Bin1 n))) /. z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((x /. z) '&' ((Bin1 n) /. z)) 'or' ((x /. z) '&' ((carry (x,(Bin1 n))) /. z)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((x /. z) '&' ((Bin1 n) /. z)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((x /. z) '&' ((Bin1 n) /. z)) is V11() V12() V13() ext-real set
'not' ((x /. z) '&' ((carry (x,(Bin1 n))) /. z)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((x /. z) '&' ((carry (x,(Bin1 n))) /. z)) is V11() V12() V13() ext-real set
('not' ((x /. z) '&' ((Bin1 n) /. z))) '&' ('not' ((x /. z) '&' ((carry (x,(Bin1 n))) /. z))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ((x /. z) '&' ((Bin1 n) /. z))) * ('not' ((x /. z) '&' ((carry (x,(Bin1 n))) /. z))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ((x /. z) '&' ((Bin1 n) /. z))) '&' ('not' ((x /. z) '&' ((carry (x,(Bin1 n))) /. z)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ((x /. z) '&' ((Bin1 n) /. z))) '&' ('not' ((x /. z) '&' ((carry (x,(Bin1 n))) /. z)))) is V11() V12() V13() ext-real set
x . z is set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
x /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
k /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (k /. z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (k /. z) is V11() V12() V13() ext-real set
('not' k) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
('not' k) . z is set
x . z is set
('not' k) . z is set
x . z is set
('not' k) . z is set
x . z is set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
x /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - FALSE is V11() V12() V13() ext-real set
k /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (k /. z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (k /. z) is V11() V12() V13() ext-real set
('not' k) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
('not' k) . z is set
x . z is set
('not' k) . z is set
x . z is set
('not' k) . z is set
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
Bin1 n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' (Bin1 n) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
carry (('not' x),(Bin1 n)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x . n is set
('not' x) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
x /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (x /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (x /. n) is V11() V12() V13() ext-real set
'not' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - FALSE is V11() V12() V13() ext-real set
len ('not' (Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
len (carry (('not' x),(Bin1 n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(carry (('not' x),(Bin1 n))) . k is set
(carry (('not' x),(Bin1 n))) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' TRUE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - TRUE is V11() V12() V13() ext-real set
(Bin1 n) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((Bin1 n) /. k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - ((Bin1 n) /. k) is V11() V12() V13() ext-real set
('not' (Bin1 n)) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
('not' (Bin1 n)) . k is set
k is non empty non trivial V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(carry (('not' x),(Bin1 n))) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
k + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(carry (('not' x),(Bin1 n))) /. (k + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
x . k is set
('not' x) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
x /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (x /. k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (x /. k) is V11() V12() V13() ext-real set
(Bin1 n) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
((Bin1 n) /. k) '&' ((carry (('not' x),(Bin1 n))) /. k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
((Bin1 n) /. k) * ((carry (('not' x),(Bin1 n))) /. k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(('not' x) /. k) '&' ((Bin1 n) /. k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(('not' x) /. k) * ((Bin1 n) /. k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(('not' x) /. k) '&' ((carry (('not' x),(Bin1 n))) /. k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(('not' x) /. k) * ((carry (('not' x),(Bin1 n))) /. k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((('not' x) /. k) '&' ((Bin1 n) /. k)) 'or' ((('not' x) /. k) '&' ((carry (('not' x),(Bin1 n))) /. k)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((('not' x) /. k) '&' ((Bin1 n) /. k)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((('not' x) /. k) '&' ((Bin1 n) /. k)) is V11() V12() V13() ext-real set
'not' ((('not' x) /. k) '&' ((carry (('not' x),(Bin1 n))) /. k)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((('not' x) /. k) '&' ((carry (('not' x),(Bin1 n))) /. k)) is V11() V12() V13() ext-real set
('not' ((('not' x) /. k) '&' ((Bin1 n) /. k))) '&' ('not' ((('not' x) /. k) '&' ((carry (('not' x),(Bin1 n))) /. k))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ((('not' x) /. k) '&' ((Bin1 n) /. k))) * ('not' ((('not' x) /. k) '&' ((carry (('not' x),(Bin1 n))) /. k))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ((('not' x) /. k) '&' ((Bin1 n) /. k))) '&' ('not' ((('not' x) /. k) '&' ((carry (('not' x),(Bin1 n))) /. k)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ((('not' x) /. k) '&' ((Bin1 n) /. k))) '&' ('not' ((('not' x) /. k) '&' ((carry (('not' x),(Bin1 n))) /. k)))) is V11() V12() V13() ext-real set
(carry (('not' x),(Bin1 n))) /. 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
x . 1 is set
('not' x) /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
x /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (x /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (x /. 1) is V11() V12() V13() ext-real set
(Bin1 n) /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(('not' x) /. 1) '&' ((Bin1 n) /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(('not' x) /. 1) * ((Bin1 n) /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(carry (('not' x),(Bin1 n))) /. (1 + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(carry (('not' x),(Bin1 n))) /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(('not' x) /. 1) * ((carry (('not' x),(Bin1 n))) /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((('not' x) /. 1) '&' ((Bin1 n) /. 1)) 'or' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((('not' x) /. 1) '&' ((Bin1 n) /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((('not' x) /. 1) '&' ((Bin1 n) /. 1)) is V11() V12() V13() ext-real set
'not' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)) is V11() V12() V13() ext-real set
('not' ((('not' x) /. 1) '&' ((Bin1 n) /. 1))) '&' ('not' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ((('not' x) /. 1) '&' ((Bin1 n) /. 1))) * ('not' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ((('not' x) /. 1) '&' ((Bin1 n) /. 1))) '&' ('not' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ((('not' x) /. 1) '&' ((Bin1 n) /. 1))) '&' ('not' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)))) is V11() V12() V13() ext-real set
((Bin1 n) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
((Bin1 n) /. 1) * ((carry (('not' x),(Bin1 n))) /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(((('not' x) /. 1) '&' ((Bin1 n) /. 1)) 'or' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1))) 'or' (((Bin1 n) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (((('not' x) /. 1) '&' ((Bin1 n) /. 1)) 'or' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (((('not' x) /. 1) '&' ((Bin1 n) /. 1)) 'or' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1))) is V11() V12() V13() ext-real set
'not' (((Bin1 n) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (((Bin1 n) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)) is V11() V12() V13() ext-real set
('not' (((('not' x) /. 1) '&' ((Bin1 n) /. 1)) 'or' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)))) '&' ('not' (((Bin1 n) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' (((('not' x) /. 1) '&' ((Bin1 n) /. 1)) 'or' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)))) * ('not' (((Bin1 n) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' (((('not' x) /. 1) '&' ((Bin1 n) /. 1)) 'or' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)))) '&' ('not' (((Bin1 n) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' (((('not' x) /. 1) '&' ((Bin1 n) /. 1)) 'or' ((('not' x) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)))) '&' ('not' (((Bin1 n) /. 1) '&' ((carry (('not' x),(Bin1 n))) /. 1)))) is V11() V12() V13() ext-real set
(carry (('not' x),(Bin1 n))) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
Bin1 n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
add_ovfl (x,(Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(Bin1 n) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x /. n) '&' ((Bin1 n) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x /. n) * ((Bin1 n) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
carry (x,(Bin1 n)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (x,(Bin1 n))) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x /. n) '&' ((carry (x,(Bin1 n))) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x /. n) * ((carry (x,(Bin1 n))) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((x /. n) '&' ((Bin1 n) /. n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((x /. n) '&' ((Bin1 n) /. n)) is V11() V12() V13() ext-real set
'not' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)) is V11() V12() V13() ext-real set
('not' ((x /. n) '&' ((Bin1 n) /. n))) '&' ('not' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ((x /. n) '&' ((Bin1 n) /. n))) * ('not' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ((x /. n) '&' ((Bin1 n) /. n))) '&' ('not' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ((x /. n) '&' ((Bin1 n) /. n))) '&' ('not' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)))) is V11() V12() V13() ext-real set
((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
((Bin1 n) /. n) * ((carry (x,(Bin1 n))) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) 'or' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) is V11() V12() V13() ext-real set
'not' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)) is V11() V12() V13() ext-real set
('not' (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)))) '&' ('not' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)))) * ('not' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)))) '&' ('not' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)))) '&' ('not' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)))) is V11() V12() V13() ext-real set
len k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom k is Element of bool NAT
k /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
k . 1 is set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*z*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
x /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
k /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (k /. z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (k /. z) is V11() V12() V13() ext-real set
carry (x,(Bin1 n)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (x,(Bin1 n))) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (Bin1 n) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
('not' (Bin1 n)) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(Bin1 n) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((Bin1 n) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - ((Bin1 n) /. n) is V11() V12() V13() ext-real set
'not' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - FALSE is V11() V12() V13() ext-real set
len k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom k is Element of bool NAT
k /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
k . n is set
x /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (k /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (k /. n) is V11() V12() V13() ext-real set
(x /. n) '&' ((Bin1 n) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x /. n) * ((Bin1 n) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(x /. n) '&' ((carry (x,(Bin1 n))) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x /. n) * ((carry (x,(Bin1 n))) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((x /. n) '&' ((Bin1 n) /. n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((x /. n) '&' ((Bin1 n) /. n)) is V11() V12() V13() ext-real set
'not' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)) is V11() V12() V13() ext-real set
('not' ((x /. n) '&' ((Bin1 n) /. n))) '&' ('not' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ((x /. n) '&' ((Bin1 n) /. n))) * ('not' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ((x /. n) '&' ((Bin1 n) /. n))) '&' ('not' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ((x /. n) '&' ((Bin1 n) /. n))) '&' ('not' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)))) is V11() V12() V13() ext-real set
((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
((Bin1 n) /. n) * ((carry (x,(Bin1 n))) /. n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) 'or' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) is V11() V12() V13() ext-real set
'not' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)) is V11() V12() V13() ext-real set
('not' (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)))) '&' ('not' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)))) * ('not' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)))) '&' ('not' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)))) '&' ('not' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)))) is V11() V12() V13() ext-real set
len k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom k is Element of bool NAT
k /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
k . 1 is set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
<*z*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
('not' k) /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (k /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (k /. 1) is V11() V12() V13() ext-real set
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
Bin1 n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
('not' x) + (Bin1 n) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
add_ovfl (('not' x),(Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
Absval (('not' x) + (Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval (('not' x) + (Bin1 n))) + (2 to_power n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((Absval (('not' x) + (Bin1 n))) + (2 to_power n)) - (2 to_power n) is V11() V12() V13() ext-real set
IFEQ ((add_ovfl (('not' x),(Bin1 n))),FALSE,0,(2 to_power n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval (('not' x) + (Bin1 n))) + (IFEQ ((add_ovfl (('not' x),(Bin1 n))),FALSE,0,(2 to_power n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((Absval (('not' x) + (Bin1 n))) + (IFEQ ((add_ovfl (('not' x),(Bin1 n))),FALSE,0,(2 to_power n)))) - (2 to_power n) is V11() V12() V13() ext-real set
Absval ('not' x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Absval (Bin1 n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval ('not' x)) + (Absval (Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((Absval ('not' x)) + (Absval (Bin1 n))) - (2 to_power n) is V11() V12() V13() ext-real set
Absval x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
- (Absval x) is V11() V12() V13() ext-real non positive set
(- (Absval x)) + (2 to_power n) is V11() V12() V13() ext-real set
((- (Absval x)) + (2 to_power n)) - 1 is V11() V12() V13() ext-real set
(((- (Absval x)) + (2 to_power n)) - 1) + (Absval (Bin1 n)) is V11() V12() V13() ext-real set
((((- (Absval x)) + (2 to_power n)) - 1) + (Absval (Bin1 n))) - (2 to_power n) is V11() V12() V13() ext-real set
(((- (Absval x)) + (2 to_power n)) - 1) + 1 is V11() V12() V13() ext-real set
((((- (Absval x)) + (2 to_power n)) - 1) + 1) - (2 to_power n) is V11() V12() V13() ext-real set
- 0 is V11() V12() V13() ext-real non positive set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg n is V34() V41(n) Element of bool NAT
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
z is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom z is Element of bool NAT
Seg k is V34() V41(k) Element of bool NAT
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b1 where b1 is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b1 = n } is set
z is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
z /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
k -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power (k -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (((x div (2 to_power (k -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
dom z is Element of bool NAT
z . k is set
k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom k is Element of bool NAT
len z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
dom z is Element of bool NAT
k . z is set
k /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
z -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power (z -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x div (2 to_power (z -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div (2 to_power (z -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (((x div (2 to_power (z -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
z /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
z . z is set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(n,0) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
len (n,0) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom (n,0) is Element of bool NAT
(n,0) . k is set
(n,0) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
k -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power (k -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0 div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(0 div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (((0 div (2 to_power (k -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
0 mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ ((0 mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
IFEQ (0,0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x . k is set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
((n + 1),x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1),x) . (n + 1) is set
(n + 1) -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n + 1) - 1 is V11() V12() V13() ext-real set
2 to_power ((n + 1) -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x div (2 to_power ((n + 1) -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div (2 to_power ((n + 1) -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0 mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (n + 1) is non empty V34() V41(n + 1) Element of bool NAT
len ((n + 1),x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len ((n + 1),x)) is V34() V41( len ((n + 1),x)) Element of bool NAT
dom ((n + 1),x) is Element of bool NAT
((n + 1),x) /. (n + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
IFEQ (((x div (2 to_power ((n + 1) -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((n + 1),x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,x) ^ <*FALSE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg (n + 1) is non empty V34() V41(n + 1) Element of bool NAT
len ((n + 1),x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len ((n + 1),x)) is V34() V41( len ((n + 1),x)) Element of bool NAT
dom ((n + 1),x) is Element of bool NAT
Seg n is non empty V34() V41(n) Element of bool NAT
len (n,x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len (n,x)) is V34() V41( len (n,x)) Element of bool NAT
dom (n,x) is Element of bool NAT
((n + 1),x) . k is set
((n + 1),x) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
k -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power (k -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (((x div (2 to_power (k -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(n,x) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(n,x) . k is set
((n,x) ^ <*FALSE*>) . k is set
((n + 1),x) . k is set
((n,x) ^ <*FALSE*>) . k is set
Seg n is non empty V34() V41(n) Element of bool NAT
((n + 1),x) . k is set
((n,x) ^ <*FALSE*>) . k is set
((n + 1),x) . k is set
((n,x) ^ <*FALSE*>) . k is set
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((n + 1),(2 to_power n)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
(0* n) ^ <*TRUE*> is non empty V15() V18( NAT ) Function-like V34() FinSequence-like FinSubsequence-like set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg (n + 1) is non empty V34() V41(n + 1) Element of bool NAT
k - 1 is V11() V12() V13() ext-real set
(n + 1) - 1 is V11() V12() V13() ext-real set
k -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n - (k -' 1) is V11() V12() V13() ext-real set
(n - (k -' 1)) + (k -' 1) is V11() V12() V13() ext-real set
n -' (k -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n -' (k -' 1)) + (k -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power (n -' (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power (k -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power (n -' (k -' 1))) * (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len x) is V34() V41( len x) Element of bool NAT
dom x is Element of bool NAT
n - (k - 1) is V11() V12() V13() ext-real set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
z + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power z) * (2 to_power 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(2 to_power z) * 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(2 to_power n) div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((2 to_power n) div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power (n -' (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
len ((n + 1),(2 to_power n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len ((n + 1),(2 to_power n))) is V34() V41( len ((n + 1),(2 to_power n))) Element of bool NAT
dom ((n + 1),(2 to_power n)) is Element of bool NAT
((n + 1),(2 to_power n)) . k is set
((n + 1),(2 to_power n)) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
IFEQ ((((2 to_power n) div (2 to_power (k -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
x . k is set
x ^ <*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
(x ^ <*TRUE*>) . k is set
k -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n + 1) - 1 is V11() V12() V13() ext-real set
2 to_power (k -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power n) div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((2 to_power n) div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
1 mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
len ((n + 1),(2 to_power n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len ((n + 1),(2 to_power n))) is V34() V41( len ((n + 1),(2 to_power n))) Element of bool NAT
dom ((n + 1),(2 to_power n)) is Element of bool NAT
((n + 1),(2 to_power n)) . k is set
((n + 1),(2 to_power n)) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
IFEQ ((((2 to_power n) div (2 to_power (k -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x ^ <*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
(x ^ <*TRUE*>) . k is set
((n + 1),(2 to_power n)) . k is set
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x ^ <*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
(x ^ <*TRUE*>) . k is set
((n + 1),(2 to_power n)) . k is set
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x ^ <*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
(x ^ <*TRUE*>) . k is set
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power (n + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((n + 1),x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1),x) . (n + 1) is set
2 to_power 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power n) * (2 to_power 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 * (2 to_power n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(2 to_power n) + (2 to_power n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(n + 1) -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n + 1) - 1 is V11() V12() V13() ext-real set
2 to_power ((n + 1) -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x div (2 to_power ((n + 1) -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div (2 to_power ((n + 1) -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
1 mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (n + 1) is non empty V34() V41(n + 1) Element of bool NAT
len ((n + 1),x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len ((n + 1),x)) is V34() V41( len ((n + 1),x)) Element of bool NAT
dom ((n + 1),x) is Element of bool NAT
((n + 1),x) /. (n + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
IFEQ (((x div (2 to_power ((n + 1) -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power (n + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((n + 1),x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x -' (2 to_power n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n,(x -' (2 to_power n))) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,(x -' (2 to_power n))) ^ <*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg (n + 1) is non empty V34() V41(n + 1) Element of bool NAT
len ((n + 1),x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len ((n + 1),x)) is V34() V41( len ((n + 1),x)) Element of bool NAT
dom ((n + 1),x) is Element of bool NAT
Seg n is non empty V34() V41(n) Element of bool NAT
k -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power (k -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 * (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power (k -' 1)) * (2 to_power 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(k -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power ((k -' 1) + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k - 1 is V11() V12() V13() ext-real set
(k - 1) + 1 is V11() V12() V13() ext-real set
2 to_power ((k - 1) + 1) is V11() V12() ext-real set
2 to_power k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
z -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power (z -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 * (2 to_power (z -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
x div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x -' (2 to_power n)) div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((x -' (2 to_power n)) div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x -' (2 to_power n)) div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((x -' (2 to_power n)) div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x -' (2 to_power n)) div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((x -' (2 to_power n)) div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x -' (2 to_power n)) div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((x -' (2 to_power n)) div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
len (n,(x -' (2 to_power n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len (n,(x -' (2 to_power n)))) is V34() V41( len (n,(x -' (2 to_power n)))) Element of bool NAT
dom (n,(x -' (2 to_power n))) is Element of bool NAT
((n + 1),x) . k is set
((n + 1),x) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
IFEQ (((x div (2 to_power (k -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(n,(x -' (2 to_power n))) /. k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(n,(x -' (2 to_power n))) . k is set
((n,(x -' (2 to_power n))) ^ <*TRUE*>) . k is set
((n + 1),x) . k is set
((n,(x -' (2 to_power n))) ^ <*TRUE*>) . k is set
Seg n is non empty V34() V41(n) Element of bool NAT
((n + 1),x) . k is set
((n,(x -' (2 to_power n))) ^ <*TRUE*>) . k is set
((n + 1),x) . k is set
((n,(x -' (2 to_power n))) ^ <*TRUE*>) . k is set
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
(2 to_power n) - 1 is V11() V12() V13() ext-real set
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(n,x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0* z is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL z
REAL z is functional FinSequence-membered FinSequenceSet of REAL
z -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = z } is set
z |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(z) FinSequence-like FinSubsequence-like Element of z -tuples_on REAL
Seg z is non empty V34() V41(z) Element of bool NAT
(Seg z) --> 0 is V15() V18( Seg z) V19(K20(0)) Function-like V29( Seg z,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg z),K20(0):]
[:(Seg z),K20(0):] is set
bool [:(Seg z),K20(0):] is set
(2 to_power z) - 1 is V11() V12() V13() ext-real set
z + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power (z + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0* (z + 1) is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL (z + 1)
REAL (z + 1) is functional FinSequence-membered FinSequenceSet of REAL
(z + 1) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = z + 1 } is set
(z + 1) |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(z + 1) FinSequence-like FinSubsequence-like Element of (z + 1) -tuples_on REAL
Seg (z + 1) is non empty V34() V41(z + 1) Element of bool NAT
(Seg (z + 1)) --> 0 is V15() V18( Seg (z + 1)) V19(K20(0)) Function-like V29( Seg (z + 1),K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg (z + 1)),K20(0):]
[:(Seg (z + 1)),K20(0):] is set
bool [:(Seg (z + 1)),K20(0):] is set
(2 to_power (z + 1)) - 1 is V11() V12() V13() ext-real set
0 + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((z + 1),k) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(z + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
y is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(z + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' y is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(z + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
y . (z + 1) is set
z is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(z) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*0*> is non empty V15() V18( NAT ) V19( NAT ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of NAT
z ^ <*0*> is non empty V15() V18( NAT ) Function-like V34() V41(K192(z,1)) FinSequence-like FinSubsequence-like set
K192(z,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
len y is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
len ('not' y) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((z + 1),k) . (z + 1) is set
('not' y) /. (z + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
y /. (z + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (y /. (z + 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (y /. (z + 1)) is V11() V12() V13() ext-real set
'not' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - FALSE is V11() V12() V13() ext-real set
k -' (2 to_power z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(z,(k -' (2 to_power z))) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(z) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(z,(k -' (2 to_power z))) ^ <*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(z,1)) V41(K307(z,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(z,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
'not' z is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(z) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*('not' FALSE)*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
('not' z) ^ <*('not' FALSE)*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(z,1)) V41(K307(z,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
2 to_power 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power z) * (2 to_power 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 * (2 to_power z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(2 to_power z) + (2 to_power z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k - (2 to_power z) is V11() V12() V13() ext-real set
(2 to_power z) * 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((2 to_power z) * 2) - 1 is V11() V12() V13() ext-real set
((2 to_power z) * (2 to_power 1)) - 1 is V11() V12() V13() ext-real set
2 to_power 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0* 1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL 1
REAL 1 is functional FinSequence-membered FinSequenceSet of REAL
1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 1 } is set
1 |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on REAL
(Seg 1) --> 0 is V15() V18( Seg 1) V19(K20(0)) Function-like V29( Seg 1,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg 1),K20(0):]
[:(Seg 1),K20(0):] is set
bool [:(Seg 1),K20(0):] is set
(2 to_power 1) - 1 is V11() V12() V13() ext-real set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(1,z) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (1,z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
z is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' z is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*1*> is non empty V15() V18( NAT ) V19( NAT ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> . 1 is set
(1,z) /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power (1 -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
z div (2 to_power (1 -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(z div (2 to_power (1 -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (((z div (2 to_power (1 -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(1 + 1) - 1 is V11() V12() V13() ext-real set
len k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
z -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power (z -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
len ('not' k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n -' (z -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power (n -' (z -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(n + 1) - 1 is V11() V12() V13() ext-real set
z - 1 is V11() V12() V13() ext-real set
0 + (z -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n - (z -' 1) is V11() V12() V13() ext-real set
(2 to_power (n -' (z -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x div (2 to_power (z -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power n) -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((2 to_power n) -' 1) div (2 to_power (z -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power n) div (2 to_power (z -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((2 to_power n) div (2 to_power (z -' 1))) - 1 is V11() V12() V13() ext-real set
(2 to_power (n -' (z -' 1))) - 1 is V11() V12() V13() ext-real set
(2 to_power (n -' (z -' 1))) -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div (2 to_power (z -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k . z is set
len (n,x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len (n,x)) is V34() V41( len (n,x)) Element of bool NAT
dom (n,x) is Element of bool NAT
(n,x) . z is set
(n,x) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
IFEQ (((x div (2 to_power (z -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - FALSE is V11() V12() V13() ext-real set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (k /. z) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - (k /. z) is V11() V12() V13() ext-real set
('not' k) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
('not' k) . z is set
<*1*> is non empty V15() V18( NAT ) V19( NAT ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of NAT
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((n + 1),(2 to_power n)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
(0* n) ^ <*1*> is non empty V15() V18( NAT ) Function-like V34() FinSequence-like FinSubsequence-like set
k is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* k is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL k
REAL k is functional FinSequence-membered FinSequenceSet of REAL
k -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = k } is set
k |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(k) FinSequence-like FinSubsequence-like Element of k -tuples_on REAL
Seg k is non empty V34() V41(k) Element of bool NAT
(Seg k) --> 0 is V15() V18( Seg k) V19(K20(0)) Function-like V29( Seg k,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg k),K20(0):]
[:(Seg k),K20(0):] is set
bool [:(Seg k),K20(0):] is set
2 to_power k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power k) - 1 is V11() V12() V13() ext-real set
(k,1) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(k) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(k) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' z is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(k) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
k is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0* k is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL k
REAL k is functional FinSequence-membered FinSequenceSet of REAL
k -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = k } is set
k |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(k) FinSequence-like FinSubsequence-like Element of k -tuples_on REAL
Seg k is non empty V34() V41(k) Element of bool NAT
(Seg k) --> 0 is V15() V18( Seg k) V19(K20(0)) Function-like V29( Seg k,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg k),K20(0):]
[:(Seg k),K20(0):] is set
bool [:(Seg k),K20(0):] is set
(0* k) ^ <*1*> is non empty V15() V18( NAT ) Function-like V34() FinSequence-like FinSubsequence-like set
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power (n + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((n + 1),x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1),x) . (n + 1) is set
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power (n + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((n + 1),x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x -' (2 to_power n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n,(x -' (2 to_power n))) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,(x -' (2 to_power n))) ^ <*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
(n,x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(2 to_power n) - 1 is V11() V12() V13() ext-real set
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Bin1 n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
x + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(n,x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
add_ovfl ((n,x),(Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
(2 to_power n) - 1 is V11() V12() V13() ext-real set
k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Bin1 n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power (n + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Bin1 (n + 1) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
x + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
((n + 1),(x + 1)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1),x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1),x) + (Bin1 (n + 1)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
add_ovfl ((n,x),(Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(n,(x + 1)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,(x + 1)) ^ <*FALSE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
(n,x) + (Bin1 n) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
FALSE 'xor' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
K339(FALSE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K338(FALSE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - FALSE is V11() V12() V13() ext-real set
K337(('not' FALSE),FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' ('not' FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ('not' FALSE) is V11() V12() V13() ext-real set
('not' ('not' FALSE)) '&' ('not' FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ('not' FALSE)) * ('not' FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ('not' FALSE)) '&' ('not' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ('not' FALSE)) '&' ('not' FALSE)) is V11() V12() V13() ext-real set
K338(FALSE,FALSE) '&' K338(FALSE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K338(FALSE,FALSE) * K338(FALSE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' K339(FALSE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - K339(FALSE,FALSE) is V11() V12() V13() ext-real set
(FALSE 'xor' FALSE) 'xor' (add_ovfl ((n,x),(Bin1 n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
K339((FALSE 'xor' FALSE),(add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K338((FALSE 'xor' FALSE),(add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' (FALSE 'xor' FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (FALSE 'xor' FALSE) is V11() V12() V13() ext-real set
K337(('not' (FALSE 'xor' FALSE)),(add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' ('not' (FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ('not' (FALSE 'xor' FALSE)) is V11() V12() V13() ext-real set
'not' (add_ovfl ((n,x),(Bin1 n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (add_ovfl ((n,x),(Bin1 n))) is V11() V12() V13() ext-real set
('not' ('not' (FALSE 'xor' FALSE))) '&' ('not' (add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ('not' (FALSE 'xor' FALSE))) * ('not' (add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ('not' (FALSE 'xor' FALSE))) '&' ('not' (add_ovfl ((n,x),(Bin1 n))))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ('not' (FALSE 'xor' FALSE))) '&' ('not' (add_ovfl ((n,x),(Bin1 n))))) is V11() V12() V13() ext-real set
K338((add_ovfl ((n,x),(Bin1 n))),(FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K337(('not' (add_ovfl ((n,x),(Bin1 n)))),(FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' ('not' (add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ('not' (add_ovfl ((n,x),(Bin1 n)))) is V11() V12() V13() ext-real set
('not' ('not' (add_ovfl ((n,x),(Bin1 n))))) '&' ('not' (FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ('not' (add_ovfl ((n,x),(Bin1 n))))) * ('not' (FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ('not' (add_ovfl ((n,x),(Bin1 n))))) '&' ('not' (FALSE 'xor' FALSE))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ('not' (add_ovfl ((n,x),(Bin1 n))))) '&' ('not' (FALSE 'xor' FALSE))) is V11() V12() V13() ext-real set
K338((FALSE 'xor' FALSE),(add_ovfl ((n,x),(Bin1 n)))) '&' K338((add_ovfl ((n,x),(Bin1 n))),(FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K338((FALSE 'xor' FALSE),(add_ovfl ((n,x),(Bin1 n)))) * K338((add_ovfl ((n,x),(Bin1 n))),(FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' K339((FALSE 'xor' FALSE),(add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - K339((FALSE 'xor' FALSE),(add_ovfl ((n,x),(Bin1 n)))) is V11() V12() V13() ext-real set
<*((FALSE 'xor' FALSE) 'xor' (add_ovfl ((n,x),(Bin1 n))))*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n,x) + (Bin1 n)) ^ <*((FALSE 'xor' FALSE) 'xor' (add_ovfl ((n,x),(Bin1 n))))*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,x) ^ <*FALSE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(Bin1 n) ^ <*FALSE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n,x) ^ <*FALSE*>) + ((Bin1 n) ^ <*FALSE*>) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n,x) ^ <*FALSE*>) + (Bin1 (n + 1)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
2 to_power 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power n) * (2 to_power 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(2 to_power n) * 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(2 to_power n) + (2 to_power n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(x + 1) - (2 to_power n) is V11() V12() V13() ext-real set
x - (2 to_power n) is V11() V12() V13() ext-real set
(x - (2 to_power n)) + 1 is V11() V12() V13() ext-real set
x -' (2 to_power n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x -' (2 to_power n)) + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(n,(x -' (2 to_power n))) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x + 1) -' (2 to_power n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n,((x + 1) -' (2 to_power n))) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,((x + 1) -' (2 to_power n))) ^ <*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
(n,((x -' (2 to_power n)) + 1)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,((x -' (2 to_power n)) + 1)) ^ <*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,(x -' (2 to_power n))) + (Bin1 n) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
TRUE 'xor' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
K339(TRUE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K338(TRUE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' TRUE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - TRUE is V11() V12() V13() ext-real set
K337(('not' TRUE),FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' ('not' TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ('not' TRUE) is V11() V12() V13() ext-real set
'not' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - FALSE is V11() V12() V13() ext-real set
('not' ('not' TRUE)) '&' ('not' FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ('not' TRUE)) * ('not' FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ('not' TRUE)) '&' ('not' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ('not' TRUE)) '&' ('not' FALSE)) is V11() V12() V13() ext-real set
K338(FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K337(('not' FALSE),TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' ('not' FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ('not' FALSE) is V11() V12() V13() ext-real set
('not' ('not' FALSE)) '&' ('not' TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ('not' FALSE)) * ('not' TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ('not' FALSE)) '&' ('not' TRUE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ('not' FALSE)) '&' ('not' TRUE)) is V11() V12() V13() ext-real set
K338(TRUE,FALSE) '&' K338(FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K338(TRUE,FALSE) * K338(FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' K339(TRUE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - K339(TRUE,FALSE) is V11() V12() V13() ext-real set
(TRUE 'xor' FALSE) 'xor' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
K339((TRUE 'xor' FALSE),(add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K338((TRUE 'xor' FALSE),(add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' (TRUE 'xor' FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (TRUE 'xor' FALSE) is V11() V12() V13() ext-real set
K337(('not' (TRUE 'xor' FALSE)),(add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' ('not' (TRUE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ('not' (TRUE 'xor' FALSE)) is V11() V12() V13() ext-real set
'not' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))) is V11() V12() V13() ext-real set
('not' ('not' (TRUE 'xor' FALSE))) '&' ('not' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ('not' (TRUE 'xor' FALSE))) * ('not' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ('not' (TRUE 'xor' FALSE))) '&' ('not' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ('not' (TRUE 'xor' FALSE))) '&' ('not' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))))) is V11() V12() V13() ext-real set
K338((add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))),(TRUE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K337(('not' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)))),(TRUE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' ('not' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ('not' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)))) is V11() V12() V13() ext-real set
('not' ('not' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))))) '&' ('not' (TRUE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ('not' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))))) * ('not' (TRUE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ('not' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))))) '&' ('not' (TRUE 'xor' FALSE))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ('not' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))))) '&' ('not' (TRUE 'xor' FALSE))) is V11() V12() V13() ext-real set
K338((TRUE 'xor' FALSE),(add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)))) '&' K338((add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))),(TRUE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K338((TRUE 'xor' FALSE),(add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)))) * K338((add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))),(TRUE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' K339((TRUE 'xor' FALSE),(add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - K339((TRUE 'xor' FALSE),(add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n)))) is V11() V12() V13() ext-real set
<*((TRUE 'xor' FALSE) 'xor' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))))*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n,(x -' (2 to_power n))) + (Bin1 n)) ^ <*((TRUE 'xor' FALSE) 'xor' (add_ovfl ((n,(x -' (2 to_power n))),(Bin1 n))))*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,(x -' (2 to_power n))) ^ <*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(Bin1 n) ^ <*FALSE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n,(x -' (2 to_power n))) ^ <*TRUE*>) + ((Bin1 n) ^ <*FALSE*>) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n,(x -' (2 to_power n))) ^ <*TRUE*>) + (Bin1 (n + 1)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
(2 to_power n) - 1 is V11() V12() V13() ext-real set
(n,x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' k is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(0* n) ^ <*1*> is non empty V15() V18( NAT ) Function-like V34() FinSequence-like FinSubsequence-like set
('not' k) + (Bin1 n) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(('not' k) + (Bin1 n)) ^ <*TRUE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K307(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
K192(n,1) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
(n,x) + (Bin1 n) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
FALSE 'xor' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
K339(FALSE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K338(FALSE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' FALSE is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - FALSE is V11() V12() V13() ext-real set
K337(('not' FALSE),FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' ('not' FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ('not' FALSE) is V11() V12() V13() ext-real set
('not' ('not' FALSE)) '&' ('not' FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ('not' FALSE)) * ('not' FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ('not' FALSE)) '&' ('not' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ('not' FALSE)) '&' ('not' FALSE)) is V11() V12() V13() ext-real set
K338(FALSE,FALSE) '&' K338(FALSE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K338(FALSE,FALSE) * K338(FALSE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' K339(FALSE,FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - K339(FALSE,FALSE) is V11() V12() V13() ext-real set
add_ovfl ((n,x),(Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(FALSE 'xor' FALSE) 'xor' (add_ovfl ((n,x),(Bin1 n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
K339((FALSE 'xor' FALSE),(add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K338((FALSE 'xor' FALSE),(add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' (FALSE 'xor' FALSE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (FALSE 'xor' FALSE) is V11() V12() V13() ext-real set
K337(('not' (FALSE 'xor' FALSE)),(add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' ('not' (FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ('not' (FALSE 'xor' FALSE)) is V11() V12() V13() ext-real set
'not' (add_ovfl ((n,x),(Bin1 n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (add_ovfl ((n,x),(Bin1 n))) is V11() V12() V13() ext-real set
('not' ('not' (FALSE 'xor' FALSE))) '&' ('not' (add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ('not' (FALSE 'xor' FALSE))) * ('not' (add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ('not' (FALSE 'xor' FALSE))) '&' ('not' (add_ovfl ((n,x),(Bin1 n))))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ('not' (FALSE 'xor' FALSE))) '&' ('not' (add_ovfl ((n,x),(Bin1 n))))) is V11() V12() V13() ext-real set
K338((add_ovfl ((n,x),(Bin1 n))),(FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K337(('not' (add_ovfl ((n,x),(Bin1 n)))),(FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
'not' ('not' (add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ('not' (add_ovfl ((n,x),(Bin1 n)))) is V11() V12() V13() ext-real set
('not' ('not' (add_ovfl ((n,x),(Bin1 n))))) '&' ('not' (FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ('not' (add_ovfl ((n,x),(Bin1 n))))) * ('not' (FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ('not' (add_ovfl ((n,x),(Bin1 n))))) '&' ('not' (FALSE 'xor' FALSE))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ('not' (add_ovfl ((n,x),(Bin1 n))))) '&' ('not' (FALSE 'xor' FALSE))) is V11() V12() V13() ext-real set
K338((FALSE 'xor' FALSE),(add_ovfl ((n,x),(Bin1 n)))) '&' K338((add_ovfl ((n,x),(Bin1 n))),(FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
K338((FALSE 'xor' FALSE),(add_ovfl ((n,x),(Bin1 n)))) * K338((add_ovfl ((n,x),(Bin1 n))),(FALSE 'xor' FALSE)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' K339((FALSE 'xor' FALSE),(add_ovfl ((n,x),(Bin1 n)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - K339((FALSE 'xor' FALSE),(add_ovfl ((n,x),(Bin1 n)))) is V11() V12() V13() ext-real set
<*((FALSE 'xor' FALSE) 'xor' (add_ovfl ((n,x),(Bin1 n))))*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n,x) + (Bin1 n)) ^ <*((FALSE 'xor' FALSE) 'xor' (add_ovfl ((n,x),(Bin1 n))))*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,x) ^ <*FALSE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(Bin1 n) ^ <*FALSE*> is non empty V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) V41(K307(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n,x) ^ <*FALSE*>) + ((Bin1 n) ^ <*FALSE*>) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(K192(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n,x) ^ <*FALSE*>) + (Bin1 (n + 1)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
2 to_power 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0* 1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL 1
REAL 1 is functional FinSequence-membered FinSequenceSet of REAL
1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 1 } is set
1 |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on REAL
(Seg 1) --> 0 is V15() V18( Seg 1) V19(K20(0)) Function-like V29( Seg 1,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg 1),K20(0):]
K20(0) is non empty trivial set
[:(Seg 1),K20(0):] is set
bool [:(Seg 1),K20(0):] is set
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
x + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(1,(x + 1)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(1,x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(1,x) + (Bin1 1) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 - 1 is V11() V12() V13() ext-real set
(2 to_power 1) - 1 is V11() V12() V13() ext-real set
n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((n + 1),x) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
<*(x mod 2)*> is non empty V15() V18( NAT ) V19( NAT ) Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of NAT
x div 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n,(x div 2)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*(x mod 2)*> ^ (n,(x div 2)) is non empty V15() V18( NAT ) Function-like V34() FinSequence-like FinSubsequence-like set
len ((n + 1),x) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom ((n + 1),x) is Element of bool NAT
Seg (n + 1) is non empty V34() V41(n + 1) Element of bool NAT
len (<*(x mod 2)*> ^ (n,(x div 2))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
len (n,(x div 2)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
1 + (len (n,(x div 2))) is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
len <*(x mod 2)*> is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(k -' 1) -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((k -' 1) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power (((k -' 1) -' 1) + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power ((k -' 1) -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power ((k -' 1) -' 1)) * (2 to_power 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 * (2 to_power ((k -' 1) -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k - 1 is V11() V12() V13() ext-real set
1 - 1 is V11() V12() V13() ext-real set
0 + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power (k -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x div (2 to_power (k -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x div (2 to_power (((k -' 1) -' 1) + 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div 2) div (2 to_power ((k -' 1) -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg n is V34() V41(n) Element of bool NAT
((n + 1),x) . k is set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((n + 1),x) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(x div (2 to_power (k -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (((x div (2 to_power (k -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(n,(x div 2)) /. (k -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(n,(x div 2)) . (k -' 1) is set
(n,(x div 2)) . (k - 1) is set
(<*(x mod 2)*> ^ (n,(x div 2))) . k is set
IFEQ ((x mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
IFEQ ((x mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
IFEQ ((x mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
IFEQ ((x mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
2 to_power 0 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((n + 1),x) . k is set
z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((n + 1),x) /. z is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power (1 -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x div (2 to_power (1 -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div (2 to_power (1 -' 1))) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (((x div (2 to_power (1 -' 1))) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
x div 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(x div 1) mod 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
IFEQ (((x div 1) mod 2),0,FALSE,TRUE) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(<*(x mod 2)*> ^ (n,(x div 2))) . k is set
((n + 1),x) . k is set
(<*(x mod 2)*> ^ (n,(x div 2))) . k is set
((n + 1),x) . k is set
(<*(x mod 2)*> ^ (n,(x div 2))) . k is set
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(n,k) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval (n,k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k + 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(n,(k + 1)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval (n,(k + 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(2 to_power n) - 1 is V11() V12() V13() ext-real set
(k + 1) - 1 is V11() V12() V13() ext-real set
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Bin1 n is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
add_ovfl ((n,k),(Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
(n,k) + (Bin1 n) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval ((n,k) + (Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Absval (Bin1 n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Absval (n,k)) + (Absval (Bin1 n)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(n,0) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval (n,0) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0* n is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
n |-> 0 is V15() empty-yielding V18( NAT ) V19( REAL ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty V34() V41(n) Element of bool NAT
(Seg n) --> 0 is V15() V18( Seg n) V19(K20(0)) Function-like V29( Seg n,K20(0)) V34() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),K20(0):]
K20(0) is non empty trivial set
[:(Seg n),K20(0):] is set
bool [:(Seg n),K20(0):] is set
n is non empty V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
x is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(n,(Absval x)) is V15() V18( NAT ) V19( BOOLEAN ) Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
2 to_power n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Absval (n,(Absval x)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT