REAL is non empty V34() V60() V61() V62() V66() set
NAT is V6() V34() V39() V40() V60() V61() V62() V63() V64() V65() V66() Element of bool REAL
bool REAL is V34() set
COMPLEX is non empty V34() V60() V66() set
NAT is V6() V34() V39() V40() V60() V61() V62() V63() V64() V65() V66() set
bool NAT is V34() set
bool NAT is V34() set
RAT is non empty V34() V60() V61() V62() V63() V66() set
INT is non empty V34() V60() V61() V62() V63() V64() V66() set
[:NAT,REAL:] is Relation-like V34() V49() V50() V51() set
bool [:NAT,REAL:] is V34() set
[:COMPLEX,COMPLEX:] is Relation-like V34() V49() set
bool [:COMPLEX,COMPLEX:] is V34() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like V34() V49() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is V34() set
[:REAL,REAL:] is Relation-like V34() V49() V50() V51() set
bool [:REAL,REAL:] is V34() set
[:[:REAL,REAL:],REAL:] is Relation-like V34() V49() V50() V51() set
bool [:[:REAL,REAL:],REAL:] is V34() set
[:RAT,RAT:] is Relation-like RAT -valued V34() V49() V50() V51() set
bool [:RAT,RAT:] is V34() set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued V34() V49() V50() V51() set
bool [:[:RAT,RAT:],RAT:] is V34() set
[:INT,INT:] is Relation-like RAT -valued INT -valued V34() V49() V50() V51() set
bool [:INT,INT:] is V34() set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued V34() V49() V50() V51() set
bool [:[:INT,INT:],INT:] is V34() set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued V49() V50() V51() V52() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued V49() V50() V51() V52() set
bool [:[:NAT,NAT:],NAT:] is set
BOOLEAN is non empty set
1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
[:1,1:] is Relation-like RAT -valued INT -valued V49() V50() V51() V52() set
bool [:1,1:] is set
[:[:1,1:],1:] is Relation-like RAT -valued INT -valued V49() V50() V51() V52() set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is Relation-like V49() V50() V51() set
bool [:[:1,1:],REAL:] is set
2 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
[:2,2:] is Relation-like RAT -valued INT -valued V49() V50() V51() V52() set
[:[:2,2:],REAL:] is Relation-like V49() V50() V51() set
bool [:[:2,2:],REAL:] is set
TOP-REAL 2 is V175() L15()
the U1 of (TOP-REAL 2) is set
0 is empty V6() V10() V11() V12() integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() V39() V41( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V49() V50() V51() V52() V60() V61() V62() V63() V64() V65() V66() V75() set
3 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
0 is empty V6() V10() V11() V12() integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() V39() V41( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V49() V50() V51() V52() V59() V60() V61() V62() V63() V64() V65() V66() V75() Element of NAT
FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
<*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
<*TRUE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*FALSE*> + <*TRUE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*TRUE*> + <*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V34() V41(1) FinSequence-like FinSubsequence-like V49() V50() V51() V52() V53() V54() V55() V56() FinSequence of NAT
K43(1) is V11() V12() integer ext-real non positive Element of REAL
<*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*TRUE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
addreal is Relation-like Function-like V29([:REAL,REAL:], REAL ) V49() V50() V51() Element of bool [:[:REAL,REAL:],REAL:]
FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
h is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
h + 1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h * 2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
0 + 1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h + h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h + 1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power (h + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h * 2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
i * 2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power 0 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
0* h is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V49() V50() V51() Element of REAL h
REAL h is functional FinSequence-membered FinSequenceSet of REAL
h -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = h } is set
h |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like V49() V50() V51() Element of h -tuples_on REAL
Seg h is V34() V41(h) V60() V61() V62() V63() V64() V65() Element of bool NAT
(Seg h) --> 0 is Relation-like NAT -defined RAT -valued INT -valued Function-like V29( Seg h,{0}) V34() FinSequence-like FinSubsequence-like V49() V50() V51() V52() Element of bool [:(Seg h),{0}:]
{0} is non empty trivial functional V41(1) V60() V61() V62() V63() V64() V65() set
[:(Seg h),{0}:] is Relation-like RAT -valued INT -valued V49() V50() V51() V52() set
bool [:(Seg h),{0}:] is set
(0* h) + (0* h) is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V49() V50() V51() Element of REAL h
dom (0* h) is V60() V61() V62() V63() V64() V65() Element of bool NAT
dom addreal is set
rng (0* h) is V60() V61() V62() set
[:(rng (0* h)),(rng (0* h)):] is Relation-like V49() V50() V51() set
dom ((0* h) + (0* h)) is V60() V61() V62() V63() V64() V65() Element of bool NAT
addreal .: ((0* h),(0* h)) is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
dom (addreal .: ((0* h),(0* h))) is V60() V61() V62() V63() V64() V65() Element of bool NAT
(dom (0* h)) /\ (dom (0* h)) is V60() V61() V62() V63() V64() V65() set
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(0* h) . i is V11() V12() ext-real set
((0* h) + (0* h)) . i is V11() V12() ext-real set
0 + 0 is empty V6() V10() V11() V12() integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() V39() V41( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V49() V50() V51() V52() V59() V60() V61() V62() V63() V64() V65() V66() V75() Element of NAT
h is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
h + 1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h + 1) + 1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
n is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
0 + 1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
h is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
h is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
0* h is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V49() V50() V51() Element of REAL h
REAL h is functional FinSequence-membered FinSequenceSet of REAL
h -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = h } is set
h |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like V49() V50() V51() Element of h -tuples_on REAL
Seg h is non empty V34() V41(h) V60() V61() V62() V63() V64() V65() Element of bool NAT
(Seg h) --> 0 is Relation-like NAT -defined RAT -valued INT -valued Function-like V29( Seg h,{0}) V34() FinSequence-like FinSubsequence-like V49() V50() V51() V52() Element of bool [:(Seg h),{0}:]
{0} is non empty trivial functional V41(1) V60() V61() V62() V63() V64() V65() set
[:(Seg h),{0}:] is Relation-like RAT -valued INT -valued V49() V50() V51() V52() set
bool [:(Seg h),{0}:] is set
i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
carry (i,n) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
H is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(carry (i,n)) . H is set
H - 1 is V11() V12() integer ext-real V59() Element of INT
I is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
I + 1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
len (0* h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
i /. I is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(0* h) . I is V11() V12() ext-real set
len (carry (i,n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(carry (i,n)) /. H is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
FALSE '&' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(FALSE,FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(carry (i,n)) /. I is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
FALSE '&' ((carry (i,n)) /. I) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(FALSE,((carry (i,n)) /. I)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. I)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
'not' (FALSE '&' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(FALSE '&' FALSE)) is V11() V12() integer ext-real set
'not' (FALSE '&' ((carry (i,n)) /. I)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(FALSE '&' ((carry (i,n)) /. I))) is V11() V12() integer ext-real set
('not' (FALSE '&' FALSE)) '&' ('not' (FALSE '&' ((carry (i,n)) /. I))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' (FALSE '&' FALSE)),('not' (FALSE '&' ((carry (i,n)) /. I)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' (FALSE '&' FALSE)) '&' ('not' (FALSE '&' ((carry (i,n)) /. I)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' (FALSE '&' FALSE)) '&' ('not' (FALSE '&' ((carry (i,n)) /. I))))) is V11() V12() integer ext-real set
((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. I))) 'or' (FALSE '&' ((carry (i,n)) /. I)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
'not' ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. I))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. I)))) is V11() V12() integer ext-real set
('not' ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. I)))) '&' ('not' (FALSE '&' ((carry (i,n)) /. I))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. I)))),('not' (FALSE '&' ((carry (i,n)) /. I)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. I)))) '&' ('not' (FALSE '&' ((carry (i,n)) /. I)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. I)))) '&' ('not' (FALSE '&' ((carry (i,n)) /. I))))) is V11() V12() integer ext-real set
len (carry (i,n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(carry (i,n)) . 1 is set
(carry (i,n)) /. 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
H is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(carry (i,n)) . H is set
(0* h) . H is V11() V12() ext-real set
1 + 1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
1 + 1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
0* h is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V49() V50() V51() Element of REAL h
REAL h is functional FinSequence-membered FinSequenceSet of REAL
h -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = h } is set
h |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like V49() V50() V51() Element of h -tuples_on REAL
Seg h is non empty V34() V41(h) V60() V61() V62() V63() V64() V65() Element of bool NAT
(Seg h) --> 0 is Relation-like NAT -defined RAT -valued INT -valued Function-like V29( Seg h,{0}) V34() FinSequence-like FinSubsequence-like V49() V50() V51() V52() Element of bool [:(Seg h),{0}:]
{0} is non empty trivial functional V41(1) V60() V61() V62() V63() V64() V65() set
[:(Seg h),{0}:] is Relation-like RAT -valued INT -valued V49() V50() V51() V52() set
bool [:(Seg h),{0}:] is set
i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
i + n is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
H is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(i + n) . H is set
(0* h) . H is V11() V12() ext-real set
I is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(0* h) . I is V11() V12() ext-real set
len i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
n /. I is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
carry (i,n) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (carry (i,n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(carry (i,n)) /. I is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(carry (i,n)) . I is set
len (i + n) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(i + n) . I is set
(i + n) /. I is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
FALSE 'xor' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
FALSE <=> FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
FALSE => FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,FALSE) is V11() V12() integer ext-real set
('not' FALSE) 'or' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' ('not' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,('not' FALSE)) is V11() V12() integer ext-real set
('not' ('not' FALSE)) '&' ('not' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' ('not' FALSE)),('not' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' ('not' FALSE)) '&' ('not' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' ('not' FALSE)) '&' ('not' FALSE))) is V11() V12() integer ext-real set
(FALSE => FALSE) '&' (FALSE => FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37((FALSE => FALSE),(FALSE => FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (FALSE <=> FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(FALSE <=> FALSE)) is V11() V12() integer ext-real set
h is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
0* h is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V49() V50() V51() Element of REAL h
REAL h is functional FinSequence-membered FinSequenceSet of REAL
h -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = h } is set
h |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like V49() V50() V51() Element of h -tuples_on REAL
Seg h is non empty V34() V41(h) V60() V61() V62() V63() V64() V65() Element of bool NAT
(Seg h) --> 0 is Relation-like NAT -defined RAT -valued INT -valued Function-like V29( Seg h,{0}) V34() FinSequence-like FinSubsequence-like V49() V50() V51() V52() Element of bool [:(Seg h),{0}:]
{0} is non empty trivial functional V41(1) V60() V61() V62() V63() V64() V65() set
[:(Seg h),{0}:] is Relation-like RAT -valued INT -valued V49() V50() V51() V52() set
bool [:(Seg h),{0}:] is set
i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Intval i is V11() V12() integer ext-real set
len i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
i /. h is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
i . h is set
Absval i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
h + i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
n is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
n - 1 is V11() V12() integer ext-real V59() Element of INT
(h + i) - i is V11() V12() integer ext-real V59() Element of INT
(n - 1) - i is V11() V12() integer ext-real V59() Element of INT
n + i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
n - i is V11() V12() integer ext-real V59() Element of INT
(n + i) - i is V11() V12() integer ext-real V59() Element of INT
(n - i) - 1 is V11() V12() integer ext-real V59() Element of INT
n + h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
n - h is V11() V12() integer ext-real V59() Element of INT
(n + h) - h is V11() V12() integer ext-real V59() Element of INT
i + h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(i + h) - h is V11() V12() integer ext-real V59() Element of INT
(n - 1) - h is V11() V12() integer ext-real V59() Element of INT
(n - h) - 1 is V11() V12() integer ext-real V59() Element of INT
h is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
i + n is V11() V12() integer ext-real V59() Element of INT
h - n is V11() V12() integer ext-real V59() Element of INT
(i + n) - n is V11() V12() integer ext-real V59() Element of INT
0 + i is V11() V12() integer ext-real V59() Element of INT
- n is V11() V12() integer ext-real V59() Element of INT
h + (- n) is V11() V12() integer ext-real V59() Element of INT
n + (h + (- n)) is V11() V12() integer ext-real V59() Element of INT
h - i is V11() V12() integer ext-real V59() Element of INT
n + i is V11() V12() integer ext-real V59() Element of INT
(n + i) - i is V11() V12() integer ext-real V59() Element of INT
0 + n is V11() V12() integer ext-real V59() Element of INT
- i is V11() V12() integer ext-real V59() Element of INT
h + (- i) is V11() V12() integer ext-real V59() Element of INT
i + (h + (- i)) is V11() V12() integer ext-real V59() Element of INT
h is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
2 to_power h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(2 to_power h) - 1 is V11() V12() integer ext-real V59() Element of INT
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
h -BinarySequence i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
i + n is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h -BinarySequence n is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
add_ovfl ((h -BinarySequence i),(h -BinarySequence n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(h -BinarySequence i) + (h -BinarySequence n) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval ((h -BinarySequence i) + (h -BinarySequence n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(Absval ((h -BinarySequence i) + (h -BinarySequence n))) + (2 to_power h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
IFEQ ((add_ovfl ((h -BinarySequence i),(h -BinarySequence n))),FALSE,0,(2 to_power h)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(Absval ((h -BinarySequence i) + (h -BinarySequence n))) + (IFEQ ((add_ovfl ((h -BinarySequence i),(h -BinarySequence n))),FALSE,0,(2 to_power h))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
Absval (h -BinarySequence i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
Absval (h -BinarySequence n) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(Absval (h -BinarySequence i)) + (Absval (h -BinarySequence n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
i + (Absval (h -BinarySequence n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
2 to_power h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(2 to_power h) - 1 is V11() V12() integer ext-real V59() Element of INT
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
n is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
i + n is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h -BinarySequence i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
h -BinarySequence n is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h -BinarySequence i) + (h -BinarySequence n) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval ((h -BinarySequence i) + (h -BinarySequence n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
add_ovfl ((h -BinarySequence i),(h -BinarySequence n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
Absval (h -BinarySequence i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
Absval (h -BinarySequence n) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(Absval (h -BinarySequence i)) + (Absval (h -BinarySequence n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
i + (Absval (h -BinarySequence n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
h -' 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power (h -' 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h + 1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h + 1) -' 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power ((h + 1) -' 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
i /. (h + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
Absval i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h -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 Relation-like NAT -defined BOOLEAN -valued Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b1 = h } is set
n is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like Element of h -tuples_on BOOLEAN
H is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
<*H*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n ^ <*H*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(K215(h,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K215(h,1) is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
1 - 1 is V11() V12() integer ext-real V59() Element of INT
(h + 1) - 1 is V11() V12() integer ext-real V59() Element of INT
len i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n ^ <*H*>) . (h + 1) is set
Absval n is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
IFEQ (H,FALSE,0,(2 to_power h)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(Absval n) + (IFEQ (H,FALSE,0,(2 to_power h))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(Absval n) + (2 to_power h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
1 -' 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power (1 -' 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
h /. 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
Absval h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
len h is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h . 1 is set
1 - 1 is V11() V12() integer ext-real V59() Element of INT
2 to_power (1 - 1) is V11() V12() ext-real set
h is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
h -' 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power (h -' 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(2 to_power (h -' 1)) - 1 is V11() V12() integer ext-real V59() Element of INT
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
h -BinarySequence i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
i + n is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h -BinarySequence n is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
carry ((h -BinarySequence i),(h -BinarySequence n)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry ((h -BinarySequence i),(h -BinarySequence n))) /. h is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
1 - 1 is V11() V12() integer ext-real V59() Element of INT
h - 1 is V11() V12() integer ext-real V59() Element of INT
2 to_power h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(2 to_power h) - 1 is V11() V12() integer ext-real V59() Element of INT
Seg h is non empty V34() V41(h) V60() V61() V62() V63() V64() V65() Element of bool NAT
(h -BinarySequence n) /. h is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
n div (2 to_power (h -' 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n div (2 to_power (h -' 1))) mod 2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
IFEQ (((n div (2 to_power (h -' 1))) mod 2),0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
0 mod 2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
IFEQ ((0 mod 2),0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
IFEQ (0,0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(h -BinarySequence i) /. h is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
i div (2 to_power (h -' 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(i div (2 to_power (h -' 1))) mod 2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
IFEQ (((i div (2 to_power (h -' 1))) mod 2),0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(h -BinarySequence i) + (h -BinarySequence n) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((h -BinarySequence i) + (h -BinarySequence n)) /. h is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
FALSE 'xor' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
FALSE <=> FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
FALSE => FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,FALSE) is V11() V12() integer ext-real set
('not' FALSE) 'or' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' ('not' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,('not' FALSE)) is V11() V12() integer ext-real set
('not' ('not' FALSE)) '&' ('not' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' ('not' FALSE)),('not' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' ('not' FALSE)) '&' ('not' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' ('not' FALSE)) '&' ('not' FALSE))) is V11() V12() integer ext-real set
(FALSE => FALSE) '&' (FALSE => FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37((FALSE => FALSE),(FALSE => FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (FALSE <=> FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(FALSE <=> FALSE)) is V11() V12() integer ext-real set
(FALSE 'xor' FALSE) 'xor' TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(FALSE 'xor' FALSE) <=> TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
(FALSE 'xor' FALSE) => TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' (FALSE 'xor' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(FALSE 'xor' FALSE)) is V11() V12() integer ext-real set
('not' (FALSE 'xor' FALSE)) 'or' TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' ('not' (FALSE 'xor' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,('not' (FALSE 'xor' FALSE))) is V11() V12() integer ext-real set
'not' TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,TRUE) is V11() V12() integer ext-real set
('not' ('not' (FALSE 'xor' FALSE))) '&' ('not' TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' ('not' (FALSE 'xor' FALSE))),('not' TRUE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' ('not' (FALSE 'xor' FALSE))) '&' ('not' TRUE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' ('not' (FALSE 'xor' FALSE))) '&' ('not' TRUE))) is V11() V12() integer ext-real set
TRUE => (FALSE 'xor' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
('not' TRUE) 'or' (FALSE 'xor' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' ('not' TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,('not' TRUE)) is V11() V12() integer ext-real set
('not' ('not' TRUE)) '&' ('not' (FALSE 'xor' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' ('not' TRUE)),('not' (FALSE 'xor' FALSE))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' ('not' TRUE)) '&' ('not' (FALSE 'xor' FALSE))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' ('not' TRUE)) '&' ('not' (FALSE 'xor' FALSE)))) is V11() V12() integer ext-real set
((FALSE 'xor' FALSE) => TRUE) '&' (TRUE => (FALSE 'xor' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(((FALSE 'xor' FALSE) => TRUE),(TRUE => (FALSE 'xor' FALSE))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' ((FALSE 'xor' FALSE) <=> TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,((FALSE 'xor' FALSE) <=> TRUE)) is V11() V12() integer ext-real set
Absval ((h -BinarySequence i) + (h -BinarySequence n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
h + i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
n is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
n -' 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power (n -' 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(2 to_power (n -' 1)) - 1 is V11() V12() integer ext-real V59() Element of INT
n -BinarySequence h is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n -BinarySequence i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n -BinarySequence h) + (n -BinarySequence i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Intval ((n -BinarySequence h) + (n -BinarySequence i)) is V11() V12() integer ext-real set
1 - 1 is V11() V12() integer ext-real V59() Element of INT
n - 1 is V11() V12() integer ext-real V59() Element of INT
2 to_power n is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(2 to_power n) - 1 is V11() V12() integer ext-real V59() Element of INT
Seg n is non empty V34() V41(n) V60() V61() V62() V63() V64() V65() Element of bool NAT
(n -BinarySequence i) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
i div (2 to_power (n -' 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(i div (2 to_power (n -' 1))) mod 2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
IFEQ (((i div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
0 mod 2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
IFEQ ((0 mod 2),0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
IFEQ (0,0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(n -BinarySequence h) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
h div (2 to_power (n -' 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h div (2 to_power (n -' 1))) mod 2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
IFEQ (((h div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
((n -BinarySequence h) + (n -BinarySequence i)) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
FALSE 'xor' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
FALSE <=> FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
FALSE => FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,FALSE) is V11() V12() integer ext-real set
('not' FALSE) 'or' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' ('not' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,('not' FALSE)) is V11() V12() integer ext-real set
('not' ('not' FALSE)) '&' ('not' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' ('not' FALSE)),('not' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' ('not' FALSE)) '&' ('not' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' ('not' FALSE)) '&' ('not' FALSE))) is V11() V12() integer ext-real set
(FALSE => FALSE) '&' (FALSE => FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37((FALSE => FALSE),(FALSE => FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (FALSE <=> FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(FALSE <=> FALSE)) is V11() V12() integer ext-real set
carry ((n -BinarySequence h),(n -BinarySequence i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry ((n -BinarySequence h),(n -BinarySequence i))) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(FALSE 'xor' FALSE) 'xor' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(FALSE 'xor' FALSE) <=> ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
(FALSE 'xor' FALSE) => ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' (FALSE 'xor' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(FALSE 'xor' FALSE)) is V11() V12() integer ext-real set
('not' (FALSE 'xor' FALSE)) 'or' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' ('not' (FALSE 'xor' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,('not' (FALSE 'xor' FALSE))) is V11() V12() integer ext-real set
'not' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n)) is V11() V12() integer ext-real set
('not' ('not' (FALSE 'xor' FALSE))) '&' ('not' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' ('not' (FALSE 'xor' FALSE))),('not' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' ('not' (FALSE 'xor' FALSE))) '&' ('not' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' ('not' (FALSE 'xor' FALSE))) '&' ('not' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n)))) is V11() V12() integer ext-real set
((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n) => (FALSE 'xor' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
('not' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n)) 'or' (FALSE 'xor' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' ('not' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,('not' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n))) is V11() V12() integer ext-real set
('not' ('not' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n))) '&' ('not' (FALSE 'xor' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' ('not' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n))),('not' (FALSE 'xor' FALSE))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' ('not' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n))) '&' ('not' (FALSE 'xor' FALSE))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' ('not' ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n))) '&' ('not' (FALSE 'xor' FALSE)))) is V11() V12() integer ext-real set
((FALSE 'xor' FALSE) => ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n)) '&' (((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n) => (FALSE 'xor' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(((FALSE 'xor' FALSE) => ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n)),(((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n) => (FALSE 'xor' FALSE))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' ((FALSE 'xor' FALSE) <=> ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,((FALSE 'xor' FALSE) <=> ((carry ((n -BinarySequence h),(n -BinarySequence i))) /. n))) is V11() V12() integer ext-real set
Absval ((n -BinarySequence h) + (n -BinarySequence i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
- 1 is V11() V12() integer ext-real non positive V59() Element of INT
h is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Intval h is V11() V12() integer ext-real set
len h is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h /. 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
h . 1 is set
Absval h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(Absval h) - (2 to_power 1) is V11() V12() integer ext-real V59() Element of INT
1 - (2 to_power 1) is V11() V12() integer ext-real V59() Element of INT
1 + 1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
1 - (1 + 1) is V11() V12() integer ext-real V59() Element of INT
0 - 1 is non empty V11() V12() integer ext-real non positive negative V59() Element of INT
h is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Intval h is V11() V12() integer ext-real set
len h is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h /. 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
h . 1 is set
Absval h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
TRUE 'or' h is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
'not' TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,TRUE) is V11() V12() integer ext-real set
'not' h is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,h) is V11() V12() integer ext-real set
('not' TRUE) '&' ('not' h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' TRUE),('not' h)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' TRUE) '&' ('not' h)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' TRUE) '&' ('not' h))) is V11() V12() integer ext-real set
h is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
h -' 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power (h -' 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(2 to_power (h -' 1)) - 1 is V11() V12() integer ext-real V59() Element of INT
- (2 to_power (h -' 1)) is V11() V12() integer ext-real non positive V59() Element of INT
h + 1 is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h + 1) -' 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power ((h + 1) -' 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(2 to_power ((h + 1) -' 1)) - 1 is V11() V12() integer ext-real V59() Element of INT
- (2 to_power ((h + 1) -' 1)) is V11() V12() integer ext-real non positive V59() Element of INT
1 - 1 is V11() V12() integer ext-real V59() Element of INT
1 -' 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power (1 -' 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 to_power 0 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(2 to_power (1 -' 1)) - 1 is V11() V12() integer ext-real V59() Element of INT
- (2 to_power (1 -' 1)) is V11() V12() integer ext-real non positive V59() Element of INT
h is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
0* h is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V49() V50() V51() Element of REAL h
REAL h is functional FinSequence-membered FinSequenceSet of REAL
h -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = h } is set
h |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like V49() V50() V51() Element of h -tuples_on REAL
Seg h is non empty V34() V41(h) V60() V61() V62() V63() V64() V65() Element of bool NAT
(Seg h) --> 0 is Relation-like NAT -defined RAT -valued INT -valued Function-like V29( Seg h,{0}) V34() FinSequence-like FinSubsequence-like V49() V50() V51() V52() Element of bool [:(Seg h),{0}:]
{0} is non empty trivial functional V41(1) V60() V61() V62() V63() V64() V65() set
[:(Seg h),{0}:] is Relation-like RAT -valued INT -valued V49() V50() V51() V52() set
bool [:(Seg h),{0}:] is set
i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
i /. h is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(0* h) . h is V11() V12() ext-real set
add_ovfl (i,n) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
FALSE '&' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(FALSE,FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
carry (i,n) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (i,n)) /. h is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
FALSE '&' ((carry (i,n)) /. h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(FALSE,((carry (i,n)) /. h)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. h)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
'not' (FALSE '&' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(FALSE '&' FALSE)) is V11() V12() integer ext-real set
'not' (FALSE '&' ((carry (i,n)) /. h)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(FALSE '&' ((carry (i,n)) /. h))) is V11() V12() integer ext-real set
('not' (FALSE '&' FALSE)) '&' ('not' (FALSE '&' ((carry (i,n)) /. h))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' (FALSE '&' FALSE)),('not'