:: BINARI_3 semantic presentation

REAL is set
NAT is non empty V4() V5() V6() Element of bool REAL

NAT is non empty V4() V5() V6() set

RAT is set
INT 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 () 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

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

Absval x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT

{ 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 V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element 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
() + (IFEQ (z,FALSE,0,(2 to_power n))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
() + 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
() + (2 to_power 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 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

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

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

Absval x 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

{ 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 V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element 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

y is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element 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
() + (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
() + (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

Absval n 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
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN

z 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 set

{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set

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

{ 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

{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set

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

{ 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

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 () is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
x . k is set
() . k is set
() /. 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

{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set

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)

{ 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

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 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 () 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
() + (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

{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 1 } is set

(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

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

{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set

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

Absval () 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
- () is V11() V12() V13() ext-real non positive set
(- ()) + (2 to_power n) is V11() V12() V13() ext-real set
((- ()) + (2 to_power n)) - 1 is V11() V12() V13() ext-real set
- 0 is V11() V12() V13() ext-real non positive set
() + (2 to_power n) is V11() V12() V13() ext-real set
(() + (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

{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set

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 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

{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set

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
dom () is Element of bool NAT
len () is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len ()) is V34() V41( len ()) Element of bool NAT
n - k is V11() V12() V13() ext-real set
(n - k) + 1 is V11() V12() V13() ext-real set
(len ()) - k is V11() V12() V13() ext-real set
((len ()) - k) + 1 is V11() V12() V13() ext-real set
(Rev ()) . k is set
() . (((len ()) - k) + 1) is set

{ 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 ()) - k) + 1) is set
(n |-> 1) . k is set
() . k is set
dom (Rev ()) is Element of bool NAT
len (Rev ()) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Seg (len (Rev ())) is V34() V41( len (Rev ())) Element of bool NAT

(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 V4() V5() V6() V10() V11() V12() V13() ext-real non negative set

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

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) ^ 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) ^ ) 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
() '&' () is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
() * () is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (() '&' ()) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (() '&' ()) 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

x is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN

add_ovfl (<*n*>,<*x*>) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
/. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
() '&' () is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
() * () 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*>)) /. 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

() /. 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
() '&' (() /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
() * (() /. 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(() '&' ()) 'or' (() '&' (() /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' (() '&' ()) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (() '&' ()) is V11() V12() V13() ext-real set
'not' (() '&' (() /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (() '&' (() /. 1)) is V11() V12() V13() ext-real set
('not' (() '&' ())) '&' ('not' (() '&' (() /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' (() '&' ())) * ('not' (() '&' (() /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' (() '&' ())) '&' ('not' (() '&' (() /. 1)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' (() '&' ())) '&' ('not' (() '&' (() /. 1)))) is V11() V12() V13() ext-real set
((() '&' ()) 'or' (() '&' (() /. 1))) 'or' (() '&' (() /. 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' ((() '&' ()) 'or' (() '&' (() /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - ((() '&' ()) 'or' (() '&' (() /. 1))) is V11() V12() V13() ext-real set
('not' ((() '&' ()) 'or' (() '&' (() /. 1)))) '&' ('not' (() '&' (() /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
('not' ((() '&' ()) 'or' (() '&' (() /. 1)))) * ('not' (() '&' (() /. 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
'not' (('not' ((() '&' ()) 'or' (() '&' (() /. 1)))) '&' ('not' (() '&' (() /. 1)))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean set
1 - (('not' ((() '&' ()) 'or' (() '&' (() /. 1)))) '&' ('not' (() '&' (() /. 1)))) is V11() V12() V13() ext-real set

n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
len 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
. 1 is set
len is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
. n is set
/. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' () is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
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
. n is set

n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
len 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
. 1 is set
len is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
. n is set
/. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
'not' () is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
1 - () 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

add_ovfl (,) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
Absval is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Absval is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
+ is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
+ 0 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set

add_ovfl (,) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
Absval is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Absval is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Absval is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
+ is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
+ 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 (,) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
Absval is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
+ is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
+ 0 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set

add_ovfl (,) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN
Absval is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
() + 2 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(() + 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
() + (2 to_power 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(() + (2 to_power 1)) - 2 is V11() V12() V13() ext-real set
IFEQ ((),FALSE,0,(2 to_power 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
() + (IFEQ ((),FALSE,0,(2 to_power 1))) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(() + (IFEQ ((),FALSE,0,(2 to_power 1)))) - 2 is V11() V12() V13() ext-real set
Absval is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
+ is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
() - 2 is V11() V12() V13() ext-real set
+ 1 is non empty V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
( + 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 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

x /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element 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

x /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element 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

{ b1 where b1 is V15() V18( NAT ) V19( REAL ) Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set

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

x /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of BOOLEAN

(carry (x,(Bin1 n))) /. n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative boolean Element of