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' (FALSE '&' ((carry (i,n)) /. h)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' (FALSE '&' FALSE)) '&' ('not' (FALSE '&' ((carry (i,n)) /. h)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' (FALSE '&' FALSE)) '&' ('not' (FALSE '&' ((carry (i,n)) /. h))))) is V11() V12() integer ext-real set
((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. h))) '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) 'or' (FALSE '&' ((carry (i,n)) /. h))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. h)))) is V11() V12() integer ext-real set
('not' ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. h)))) '&' ('not' (FALSE '&' ((carry (i,n)) /. h))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. h)))),('not' (FALSE '&' ((carry (i,n)) /. h)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. h)))) '&' ('not' (FALSE '&' ((carry (i,n)) /. h)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (i,n)) /. h)))) '&' ('not' (FALSE '&' ((carry (i,n)) /. 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
i is V11() V12() integer ext-real set
i * h is V11() V12() integer ext-real V59() Element of INT
(i * h) mod h is V11() V12() integer ext-real set
i mod h is V11() V12() integer ext-real set
h mod h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(i mod h) * (h mod h) is V11() V12() integer ext-real V59() Element of INT
((i mod h) * (h mod h)) mod h is V11() V12() integer ext-real set
(i mod h) * 0 is V11() V12() integer ext-real V59() Element of INT
((i mod h) * 0) mod h is V11() V12() integer ext-real set
0 mod h 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
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
n is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
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 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 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
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 h 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
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
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 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
n is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(n,i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(n,h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power (n,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
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 set
(h,n) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power (h,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
(h,1) 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
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power 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
2 to_power 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 set
n is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
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
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
2 to_power 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 set
2 to_power (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 is V11() V12() integer ext-real set
h is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
abs i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h,(abs i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power (h,(abs i)) 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,(abs i))) + i is V11() V12() integer ext-real V59() Element of INT
abs ((2 to_power (h,(abs i))) + i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h -BinarySequence (abs ((2 to_power (h,(abs i))) + i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
h -BinarySequence (abs i) 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
(h,0) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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
abs 0 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h -BinarySequence (abs 0) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
h -BinarySequence 0 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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
i is V11() V12() integer ext-real set
(h,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Intval (h,i) is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h,n) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
abs 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 (abs n) 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
n + 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)) - 1) + 1 is V11() V12() integer ext-real V59() Element of INT
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
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
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
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) is V11() V12() integer ext-real non positive V59() Element of INT
(- (2 to_power h)) - i is V11() V12() integer ext-real V59() Element of INT
i - i is V11() V12() integer ext-real V59() Element of INT
(2 to_power h) + i is V11() V12() integer ext-real V59() Element of INT
- ((2 to_power h) + i) is V11() V12() integer ext-real V59() Element of INT
- 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 INT
abs i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
- i is V11() V12() integer ext-real V59() Element of INT
- (- (2 to_power (h -' 1))) is V11() V12() integer ext-real non negative V59() Element of INT
(h,(abs 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 V59() V60() V61() V62() V63() V64() V65() Element of NAT
abs 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 (abs n) 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
(2 to_power h) + 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 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) * (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 * (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)) + (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) + (- (2 to_power (h -' 1))) is V11() V12() integer ext-real V59() Element of INT
(2 to_power h) - (2 to_power (h -' 1)) is V11() V12() integer ext-real V59() Element of INT
((2 to_power 1) * (2 to_power (h -' 1))) - (2 to_power (h -' 1)) is V11() V12() integer ext-real V59() Element of INT
(2 * (2 to_power (h -' 1))) - (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
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 ((1 mod 2),0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
IFEQ (1,0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
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 n)) - (2 to_power h) is V11() V12() integer ext-real V59() Element of INT
n - (2 to_power h) is V11() V12() integer ext-real V59() Element of INT
0 + 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
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
i mod h 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 mod 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
n + H is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
H div h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(H div h) * h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() Element of INT
n + ((H div h) * h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() Element of INT
n div h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n div h) * h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((n div h) * h) + (n mod h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
i div h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(i div h) * h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((i div h) * h) + (n mod h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
H mod h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(i div h) - (n div h) is V11() V12() integer ext-real V59() Element of INT
((i div h) - (n div h)) * h is V11() V12() integer ext-real V59() Element of INT
(((i div h) - (n div h)) * h) mod h is V11() V12() integer ext-real set
(n + H) div h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n div h) + (H div h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((n div h) + (H div h)) * h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(((n div h) + (H div h)) * h) + (n mod h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(H div 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 div h) * h) + (((n div h) * h) + (n mod h)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((H div h) * h) + 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
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
i mod h 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 mod h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
0 * h 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
n + (0 * 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 V11() V12() integer ext-real set
H * h is V11() V12() integer ext-real V59() Element of INT
i + (H * h) is V11() V12() integer ext-real V59() Element of INT
- H is V11() V12() integer ext-real V59() Element of INT
(- H) * h is V11() V12() integer ext-real V59() Element of INT
n + ((- H) * h) is V11() V12() integer ext-real V59() Element of INT
H is V11() V12() integer ext-real set
H * h is V11() V12() integer ext-real V59() Element of INT
n + (H * h) is V11() V12() integer ext-real V59() Element of INT
H is V11() V12() integer ext-real set
H * h is V11() V12() integer ext-real V59() Element of INT
n + (H * h) 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
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
i mod (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
n is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
n mod (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 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) 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)) mod 2 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) 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)) mod 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
H + I is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 |^ h is V11() V12() ext-real Element of REAL
H1 is V11() V12() integer ext-real set
H1 * (2 to_power h) is V11() V12() integer ext-real V59() Element of INT
n + (H1 * (2 to_power h)) is V11() V12() integer ext-real V59() Element of INT
I1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power I1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
- H is V11() V12() integer ext-real non positive V59() Element of INT
h + (- H) is V11() V12() integer ext-real V59() Element of INT
H + (- H) is V11() V12() integer ext-real V59() Element of INT
I1 + 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
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
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 I1) mod 2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
H1 * (2 to_power I1) is V11() V12() integer ext-real V59() Element of INT
(H1 * (2 to_power I1)) mod 2 is V11() V12() integer ext-real set
H1 mod 2 is V11() V12() integer ext-real set
(H1 mod 2) * 0 is V11() V12() integer ext-real V59() Element of INT
((H1 mod 2) * 0) mod 2 is V11() V12() integer ext-real set
(2 to_power I1) * (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
H1 * ((2 to_power I1) * (2 to_power H)) is V11() V12() integer ext-real V59() Element of INT
n + (H1 * ((2 to_power I1) * (2 to_power H))) is V11() V12() integer ext-real V59() Element of INT
(n + (H1 * ((2 to_power I1) * (2 to_power H)))) div (2 to_power H) is V11() V12() integer ext-real set
(H1 * (2 to_power I1)) * (2 to_power H) is V11() V12() integer ext-real V59() Element of INT
n + ((H1 * (2 to_power I1)) * (2 to_power H)) is V11() V12() integer ext-real V59() Element of INT
(n + ((H1 * (2 to_power I1)) * (2 to_power H))) div (2 to_power H) is V11() V12() integer ext-real set
(n div (2 to_power H)) + (H1 * (2 to_power I1)) is V11() V12() integer ext-real V59() Element of INT
T is V11() V12() integer ext-real set
T div (2 to_power H) is V11() V12() integer ext-real set
(T div (2 to_power H)) mod 2 is V11() V12() integer ext-real set
((T div (2 to_power H)) mod 2) + 0 is V11() V12() integer ext-real V59() Element of INT
(((T div (2 to_power H)) mod 2) + 0) mod 2 is V11() V12() integer ext-real set
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
i is V11() V12() integer ext-real set
i mod (2 to_power h) is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
n mod (2 to_power h) is V11() V12() integer ext-real set
abs i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h,(abs i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power (h,(abs i)) 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,(abs i))) + i is V11() V12() integer ext-real V59() Element of INT
((2 to_power (h,(abs i))) + i) mod (2 to_power h) is V11() V12() integer ext-real set
abs n is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h,(abs n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power (h,(abs 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,(abs n))) + n is V11() V12() integer ext-real V59() Element of INT
((2 to_power (h,(abs n))) + n) mod (2 to_power h) is V11() V12() integer ext-real set
H is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
h + 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
I1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
h + I1 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
H1 is V11() V12() integer ext-real set
n2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power n2 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) * (2 to_power n2) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
H1 mod (2 to_power h) is V11() V12() integer ext-real set
(2 to_power h) mod (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) mod (2 to_power h)) * (2 to_power n2) 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) mod (2 to_power h)) * (2 to_power n2)) mod (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
0 * (2 to_power n2) 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
(0 * (2 to_power n2)) mod (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
I is V11() V12() integer ext-real set
F is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power F 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) * (2 to_power F) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
I mod (2 to_power h) is V11() V12() integer ext-real set
((2 to_power h) mod (2 to_power h)) * (2 to_power F) 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) mod (2 to_power h)) * (2 to_power F)) mod (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
0 * (2 to_power F) 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
(0 * (2 to_power F)) mod (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
I + n is V11() V12() integer ext-real V59() Element of INT
(I + n) mod (2 to_power h) is V11() V12() integer ext-real set
(I mod (2 to_power h)) + (n mod (2 to_power h)) is V11() V12() integer ext-real V59() Element of INT
((I mod (2 to_power h)) + (n mod (2 to_power h))) mod (2 to_power h) is V11() V12() integer ext-real set
(n mod (2 to_power h)) mod (2 to_power h) is V11() V12() integer ext-real set
H1 + i is V11() V12() integer ext-real V59() Element of INT
(H1 + i) mod (2 to_power h) is V11() V12() integer ext-real set
(H1 mod (2 to_power h)) + (i mod (2 to_power h)) is V11() V12() integer ext-real V59() Element of INT
((H1 mod (2 to_power h)) + (i mod (2 to_power h))) mod (2 to_power h) is V11() V12() integer ext-real set
(i mod (2 to_power h)) mod (2 to_power 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
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
i is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
i mod (2 to_power h) is V11() V12() integer ext-real set
n mod (2 to_power h) is V11() V12() integer ext-real set
(h,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h,n) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Seg h is non empty V34() V41(h) V60() V61() V62() V63() V64() V65() Element of bool NAT
abs i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h -BinarySequence (abs i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
abs 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 (abs 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
(h -BinarySequence (abs i)) . H is set
(h -BinarySequence (abs n)) . H is set
I is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
1 - 1 is V11() V12() integer ext-real V59() Element of INT
I - 1 is V11() V12() integer ext-real V59() Element of INT
I -' 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
len (h -BinarySequence (abs 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 (abs n)) . I is set
(h -BinarySequence (abs n)) /. I is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
2 to_power (I -' 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(abs n) div (2 to_power (I -' 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((abs n) div (2 to_power (I -' 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 ((((abs n) div (2 to_power (I -' 1))) mod 2),0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
len (h -BinarySequence (abs i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h -BinarySequence (abs i)) . I is set
(h -BinarySequence (abs i)) /. I is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(abs i) div (2 to_power (I -' 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((abs i) div (2 to_power (I -' 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 ((((abs i) div (2 to_power (I -' 1))) mod 2),0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
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
i is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
i mod (2 to_power h) is V11() V12() integer ext-real set
n mod (2 to_power h) is V11() V12() integer ext-real set
(h,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h,n) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
abs n is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
- n is V11() V12() integer ext-real V59() Element of INT
(h,(abs n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power (h,(abs n)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(- n) + n is V11() V12() integer ext-real V59() Element of INT
(2 to_power (h,(abs n))) + n is V11() V12() integer ext-real V59() Element of INT
abs i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
- i is V11() V12() integer ext-real V59() Element of INT
(h,(abs i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power (h,(abs i)) 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 V11() V12() integer ext-real V59() Element of INT
(2 to_power (h,(abs i))) + i 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 mod (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 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
H mod (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
Seg h is non empty V34() V41(h) V60() V61() V62() V63() V64() V65() Element of bool NAT
abs I is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h -BinarySequence (abs I) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
abs H is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h -BinarySequence (abs H) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
h -BinarySequence H is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (h -BinarySequence H) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
H1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(h -BinarySequence (abs I)) . H1 is set
(h -BinarySequence (abs H)) . H1 is set
1 - 1 is V11() V12() integer ext-real V59() Element of INT
I1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
I1 - 1 is V11() V12() integer ext-real V59() Element of INT
I1 -' 1 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
len (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
(h -BinarySequence (abs I)) . I1 is set
(h -BinarySequence I) /. I1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
2 to_power (I1 -' 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 (I1 -' 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 (I1 -' 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 (I1 -' 1))) mod 2),0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
H div (2 to_power (I1 -' 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 (I1 -' 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 (I1 -' 1))) mod 2),0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(h -BinarySequence H) /. I1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(h -BinarySequence H) . I1 is set
abs ((2 to_power (h,(abs i))) + i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h -BinarySequence (abs ((2 to_power (h,(abs i))) + i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
abs ((2 to_power (h,(abs n))) + 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 (abs ((2 to_power (h,(abs n))) + n)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
i is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
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
i mod (2 to_power h) is V11() V12() integer ext-real set
n mod (2 to_power h) is V11() V12() integer ext-real set
(h,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h,n) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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
i is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
(h,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h,n) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
i mod (2 to_power h) is V11() V12() integer ext-real set
n mod (2 to_power 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
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
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
i mod (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
n is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
n mod (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 -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
abs n is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h,n) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
abs i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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
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
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
i mod (2 to_power h) is V11() V12() integer ext-real set
n mod (2 to_power 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 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 V11() V12() integer ext-real set
((h + 1),i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h,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
((h + 1),i) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(h,i) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
Seg h is non empty V34() V41(h) V60() V61() V62() V63() V64() V65() Element of bool NAT
Seg (h + 1) is non empty V34() V41(h + 1) V60() V61() V62() V63() V64() V65() Element of bool NAT
abs i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h,(abs i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power (h,(abs i)) 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,(abs i))) + i is V11() V12() integer ext-real V59() Element of INT
abs ((2 to_power (h,(abs i))) + i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((h + 1),(abs i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power ((h + 1),(abs i)) 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),(abs i))) + i is V11() V12() integer ext-real V59() Element of INT
abs ((2 to_power ((h + 1),(abs i))) + i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
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
(abs ((2 to_power ((h + 1),(abs i))) + 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
((abs ((2 to_power ((h + 1),(abs i))) + 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
(abs ((2 to_power (h,(abs i))) + 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
((abs ((2 to_power (h,(abs i))) + 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
H1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(h,(abs i)) + H1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
I1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power I1 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,(abs i))) * (2 to_power I1) 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,(abs i))) * (2 to_power I1)) mod (2 to_power (h,(abs i))) is V11() V12() integer ext-real set
- i is V11() V12() integer ext-real V59() Element of INT
(- i) + i is V11() V12() integer ext-real V59() Element of INT
(h,(abs i)) + I1 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,(abs i)) + I1) 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,(abs i)) + I1)) + i is V11() V12() integer ext-real V59() Element of INT
((2 to_power (h,(abs i))) * (2 to_power I1)) + i is V11() V12() integer ext-real V59() Element of INT
(abs ((2 to_power ((h + 1),(abs i))) + i)) mod (2 to_power (h,(abs i))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
i mod (2 to_power (h,(abs i))) is V11() V12() integer ext-real set
(((2 to_power (h,(abs i))) * (2 to_power I1)) mod (2 to_power (h,(abs i)))) + (i mod (2 to_power (h,(abs i)))) is V11() V12() integer ext-real V59() Element of INT
((((2 to_power (h,(abs i))) * (2 to_power I1)) mod (2 to_power (h,(abs i)))) + (i mod (2 to_power (h,(abs i))))) mod (2 to_power (h,(abs i))) is V11() V12() integer ext-real set
(i mod (2 to_power (h,(abs i)))) mod (2 to_power (h,(abs i))) is V11() V12() integer ext-real set
(2 to_power (h,(abs i))) mod (2 to_power (h,(abs 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
n - 1 is V11() V12() integer ext-real V59() Element of INT
(abs ((2 to_power (h,(abs i))) + i)) mod (2 to_power (h,(abs i))) 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,(abs i))) mod (2 to_power (h,(abs i)))) + (i mod (2 to_power (h,(abs i)))) is V11() V12() integer ext-real V59() Element of INT
(((2 to_power (h,(abs i))) mod (2 to_power (h,(abs i)))) + (i mod (2 to_power (h,(abs i))))) mod (2 to_power (h,(abs i))) is V11() V12() integer ext-real set
H1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(h,H1) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h,H1) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
abs H1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h -BinarySequence (abs H1) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h -BinarySequence (abs H1)) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
h -BinarySequence H1 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h -BinarySequence H1) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
H1 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
(H1 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 (((H1 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
((h + 1),H1) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((h + 1),H1) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(h + 1) -BinarySequence (abs H1) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((h + 1) -BinarySequence (abs H1)) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(h + 1) -BinarySequence H1 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((h + 1) -BinarySequence H1) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
h -BinarySequence (abs ((2 to_power (h,(abs i))) + i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h -BinarySequence (abs ((2 to_power (h,(abs i))) + i))) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
IFEQ ((((abs ((2 to_power (h,(abs i))) + 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
(h + 1) -BinarySequence (abs ((2 to_power ((h + 1),(abs i))) + i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((h + 1) -BinarySequence (abs ((2 to_power ((h + 1),(abs i))) + i))) /. n is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
IFEQ ((((abs ((2 to_power ((h + 1),(abs i))) + 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
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
i is V11() V12() integer ext-real set
((h + 1),i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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
I is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
Seg I is non empty V34() V41(I) V60() V61() V62() V63() V64() V65() Element of bool NAT
(I,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(I) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (I,i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
H1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(I,i) . H1 is set
n . H1 is set
I1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
len n is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
dom n is V41(h) V60() V61() V62() V63() V64() V65() Element of bool 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
((I + 1),i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(I + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len ((I + 1),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),i) . I1 is set
((I + 1),i) /. I1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(I,i) /. I1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(I,i) . I1 is set
I is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
<*I*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
0 ^ <*I*> is non empty Relation-like NAT -defined Function-like V34() V41(K215(0,1)) FinSequence-like FinSubsequence-like set
K215(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 boolean Element of BOOLEAN
<*I*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h,i) ^ <*I*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(K215(h,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(h + 1) -BinarySequence i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
h -BinarySequence i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((h + 1),i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(h + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h,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 boolean Element of BOOLEAN
<*n*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(h,i) ^ <*n*> 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
abs i 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) ^ <*n*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(K215(h,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
h is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
h + i is V11() V12() integer ext-real V59() Element of INT
n is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
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) is V11() V12() integer ext-real non positive V59() Element of INT
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)) is V11() V12() integer ext-real non positive V59() Element of INT
n + 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 + 1),h) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1),i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
carry (((n + 1),h),((n + 1),i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (((n + 1),h),((n + 1),i))) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
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)) is V11() V12() integer ext-real non positive V59() Element of INT
(n + 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 ((n + 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 ((n + 1) -' 1)) is V11() V12() integer ext-real non positive V59() Element of INT
(n + 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 + 1) + 1),h) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41((n + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(((n + 1) + 1),i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41((n + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
carry ((((n + 1) + 1),h),(((n + 1) + 1),i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41((n + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. ((n + 1) + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(n + 1) - 1 is V11() V12() integer ext-real V59() Element of INT
(2 to_power ((n + 1) -' 1)) + (2 to_power ((n + 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 * (2 to_power ((n + 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 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) * (2 to_power ((n + 1) -' 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
0 + (n + 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 (0 + (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))) + (2 to_power (n + 1)) is V11() V12() integer ext-real V59() Element of INT
(2 to_power (n + 1)) + h is V11() V12() integer ext-real V59() Element of INT
(2 to_power (n + 1)) + i is V11() V12() integer ext-real V59() Element of INT
0 + (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
NH is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence NH is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len ((n + 1) -BinarySequence NH) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(((n + 1) + 1),h) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
((n + 1),h) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(((n + 1) + 1),i) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
((n + 1),i) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
abs i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
- i is V11() V12() integer ext-real V59() Element of INT
- (- (2 to_power ((n + 1) -' 1))) is V11() V12() integer ext-real non negative V59() Element of INT
((n + 1),(abs i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
abs NH is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence (abs NH) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1) -BinarySequence (abs NH)) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
((n + 1) -BinarySequence NH) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
((n + 1) -BinarySequence NH) . (n + 1) is set
T is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence T is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len ((n + 1) -BinarySequence T) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
abs 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 V11() V12() integer ext-real V59() Element of INT
((n + 1),(abs h)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
abs T is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence (abs T) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1) -BinarySequence (abs T)) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
((n + 1) -BinarySequence T) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
((n + 1) -BinarySequence T) . (n + 1) is set
TRUE '&' TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(TRUE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(TRUE,((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
'not' (TRUE '&' TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(TRUE '&' TRUE)) is V11() V12() integer ext-real set
'not' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1)))) is V11() V12() integer ext-real set
('not' (TRUE '&' TRUE)) '&' ('not' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' (TRUE '&' TRUE)),('not' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' (TRUE '&' TRUE)) '&' ('not' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' (TRUE '&' TRUE)) '&' ('not' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1)))))) is V11() V12() integer ext-real set
((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1)))) 'or' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
'not' ((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))))) is V11() V12() integer ext-real set
('not' ((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))))) '&' ('not' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' ((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))))),('not' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' ((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))))) '&' ('not' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' ((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))))) '&' ('not' (TRUE '&' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1)))))) is V11() V12() integer ext-real set
TRUE 'or' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
'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' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))) is V11() V12() integer ext-real set
('not' TRUE) '&' ('not' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' TRUE),('not' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' TRUE) '&' ('not' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' TRUE) '&' ('not' ((carry ((((n + 1) + 1),h),(((n + 1) + 1),i))) /. (n + 1))))) is V11() V12() integer ext-real set
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 1) is V11() V12() integer ext-real non positive 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 (1 -' 1)) is V11() V12() integer ext-real non positive 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),h) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1 + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((1 + 1),i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1 + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
carry (((1 + 1),h),((1 + 1),i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1 + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (((1 + 1),h),((1 + 1),i))) /. (1 + 1) 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
3 div (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
1 + 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
(1 + 2) div 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(3 div (2 to_power (1 -' 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
2 + 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 + 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
2 mod 2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(2 mod 2) + 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 mod 2) + 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
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
(0 + 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
- 2 is V11() V12() integer ext-real non positive V59() Element of INT
(- 2) + 1 is V11() V12() integer ext-real V59() Element of INT
(2,h) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(2,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Seg 2 is non empty V34() V41(2) V60() V61() V62() V63() V64() V65() Element of bool NAT
2 to_power 2 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
2 |^ (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 |^ 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(2 |^ 1) + (2 |^ 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) + (2 |^ 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) + (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 + (2 to_power 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 + 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 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
abs h 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 negative V59() Element of INT
(2,(abs h)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
2 to_power (2,(abs 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 (2,(abs h))) + h is V11() V12() integer ext-real V59() Element of INT
abs ((2 to_power (2,(abs h))) + h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
4 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
4 + (- 1) is V11() V12() integer ext-real V59() Element of INT
abs (4 + (- 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(2,h) /. 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
2 -BinarySequence 3 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(2 -BinarySequence 3) /. 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
IFEQ (1,0,FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
carry ((2,h),(2,i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry ((2,h),(2,i))) /. (1 + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
TRUE '&' TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(TRUE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(carry ((2,h),(2,i))) /. 1 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
TRUE '&' ((carry ((2,h),(2,i))) /. 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(TRUE,((carry ((2,h),(2,i))) /. 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((2,h),(2,i))) /. 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
'not' (TRUE '&' TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(TRUE '&' TRUE)) is V11() V12() integer ext-real set
'not' (TRUE '&' ((carry ((2,h),(2,i))) /. 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(TRUE '&' ((carry ((2,h),(2,i))) /. 1))) is V11() V12() integer ext-real set
('not' (TRUE '&' TRUE)) '&' ('not' (TRUE '&' ((carry ((2,h),(2,i))) /. 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' (TRUE '&' TRUE)),('not' (TRUE '&' ((carry ((2,h),(2,i))) /. 1)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' (TRUE '&' TRUE)) '&' ('not' (TRUE '&' ((carry ((2,h),(2,i))) /. 1)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' (TRUE '&' TRUE)) '&' ('not' (TRUE '&' ((carry ((2,h),(2,i))) /. 1))))) is V11() V12() integer ext-real set
((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((2,h),(2,i))) /. 1))) 'or' (TRUE '&' ((carry ((2,h),(2,i))) /. 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
'not' ((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((2,h),(2,i))) /. 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((2,h),(2,i))) /. 1)))) is V11() V12() integer ext-real set
('not' ((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((2,h),(2,i))) /. 1)))) '&' ('not' (TRUE '&' ((carry ((2,h),(2,i))) /. 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' ((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((2,h),(2,i))) /. 1)))),('not' (TRUE '&' ((carry ((2,h),(2,i))) /. 1)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' ((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((2,h),(2,i))) /. 1)))) '&' ('not' (TRUE '&' ((carry ((2,h),(2,i))) /. 1)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' ((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((2,h),(2,i))) /. 1)))) '&' ('not' (TRUE '&' ((carry ((2,h),(2,i))) /. 1))))) is V11() V12() integer ext-real set
TRUE 'or' ((carry ((2,h),(2,i))) /. 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
'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' ((carry ((2,h),(2,i))) /. 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,((carry ((2,h),(2,i))) /. 1)) is V11() V12() integer ext-real set
('not' TRUE) '&' ('not' ((carry ((2,h),(2,i))) /. 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K37(('not' TRUE),('not' ((carry ((2,h),(2,i))) /. 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' (('not' TRUE) '&' ('not' ((carry ((2,h),(2,i))) /. 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean set
K40(1,(('not' TRUE) '&' ('not' ((carry ((2,h),(2,i))) /. 1)))) is V11() V12() integer ext-real set
h is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
h + i is V11() V12() integer ext-real V59() Element of INT
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,h) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,h) + (n,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Intval ((n,h) + (n,i)) is V11() V12() integer ext-real set
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 Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
abs I is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
n -BinarySequence (abs I) 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
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 Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
abs H is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
n -BinarySequence (abs H) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n -BinarySequence H is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
h is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
h + i is V11() V12() integer ext-real V59() Element of INT
n is non empty V6() V10() V11() V12() integer V34() V39() ext-real positive non negative set
n + 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 + 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 ((n + 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 ((n + 1) -' 1)) is V11() V12() integer ext-real non positive V59() Element of INT
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)) is V11() V12() integer ext-real non positive V59() Element of INT
((n + 1),h) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1),i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1),h) + ((n + 1),i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Intval (((n + 1),h) + ((n + 1),i)) is V11() V12() integer ext-real set
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 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) is V11() V12() integer ext-real non positive V59() Element of INT
(2 to_power (n + 1)) + (- (2 to_power n)) is V11() V12() integer ext-real V59() Element of INT
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 1) * (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)) + ((2 to_power 1) * (2 to_power n)) is V11() V12() integer ext-real V59() Element of INT
2 * (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)) + (2 * (2 to_power n)) is V11() V12() integer ext-real V59() Element of INT
(n + 1) - 1 is V11() V12() integer ext-real V59() Element of INT
(2 to_power (n + 1)) + h is V11() V12() integer ext-real V59() Element of INT
(2 to_power (n + 1)) + i is V11() V12() integer ext-real V59() Element of INT
(n,h) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(2 to_power (n + 1)) + 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 n)) is V11() V12() integer ext-real non negative V59() Element of INT
- h is V11() V12() integer ext-real V59() Element of INT
abs h is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((n + 1),(abs h)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
abs ((2 to_power (n + 1)) + h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
H is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence H is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len ((n + 1),h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((n + 1),h) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
((n + 1),h) . (n + 1) is set
((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h))) . (n + 1) is set
((n + 1) -BinarySequence H) . (n + 1) is set
- i is V11() V12() integer ext-real V59() Element of INT
abs i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((n + 1),(abs i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
abs ((2 to_power (n + 1)) + i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
I is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence I is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len ((n + 1),i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((n + 1),i) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
((n + 1),i) . (n + 1) is set
((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i))) . (n + 1) is set
((n + 1) -BinarySequence I) . (n + 1) is set
Intval ((n + 1),i) is V11() V12() integer ext-real set
Absval ((n + 1),i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(Absval ((n + 1),i)) - (2 to_power (n + 1)) is V11() V12() integer ext-real V59() Element of INT
I - (2 to_power (n + 1)) is V11() V12() integer ext-real V59() Element of INT
carry (((n + 1),h),((n + 1),i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (((n + 1),h),((n + 1),i))) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
Int_add_ovfl (((n + 1),h),((n + 1),i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
'not' TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K40(1,TRUE) is V11() V12() integer ext-real set
FALSE '&' ('not' TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(FALSE,('not' TRUE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(FALSE '&' ('not' TRUE)) '&' TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37((FALSE '&' ('not' TRUE)),TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
Int_add_udfl (((n + 1),h),((n + 1),i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
TRUE '&' TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(TRUE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(TRUE '&' TRUE) '&' ('not' TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37((TRUE '&' TRUE),('not' TRUE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
Intval ((n + 1),h) is V11() V12() integer ext-real set
Absval ((n + 1),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 + 1),h)) - (2 to_power (n + 1)) is V11() V12() integer ext-real V59() Element of INT
H - (2 to_power (n + 1)) is V11() V12() integer ext-real V59() Element of INT
IFEQ (FALSE,FALSE,0,(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 + i) - (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1)))) is V11() V12() integer ext-real V59() Element of INT
((h + i) - (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1))))) + (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1)))) is V11() V12() integer ext-real V59() Element of INT
(h + i) - 0 is V11() V12() integer ext-real V59() Element of INT
((h + i) - 0) + 0 is V11() V12() integer ext-real V59() Element of INT
i is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
<*i*> 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) ^ <*i*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(K215(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K215(n,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
c13 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
<*c13*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,i) ^ <*c13*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(K215(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
h is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
h + i is V11() V12() integer ext-real V59() Element of INT
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)) is V11() V12() integer ext-real non positive V59() Element of INT
(2 to_power (n -' 1)) - 1 is V11() V12() integer ext-real V59() Element of INT
(n,h) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,h) + (n,i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Intval ((n,h) + (n,i)) is V11() V12() integer ext-real set
n + 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 + 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 ((n + 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 ((n + 1) -' 1)) is V11() V12() integer ext-real non positive V59() Element of INT
(2 to_power ((n + 1) -' 1)) - 1 is V11() V12() integer ext-real V59() Element of INT
((n + 1),h) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1),i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1),h) + ((n + 1),i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Intval (((n + 1),h) + ((n + 1),i)) is V11() V12() integer ext-real set
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
(n + 1) - 1 is V11() V12() integer ext-real V59() Element of INT
- (2 to_power n) is V11() V12() integer ext-real non positive V59() Element of INT
(2 to_power n) - 1 is V11() V12() integer ext-real V59() Element of INT
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)) + (- (2 to_power n)) is V11() V12() integer ext-real V59() Element of INT
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 1) * (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)) + ((2 to_power 1) * (2 to_power n)) is V11() V12() integer ext-real V59() Element of INT
2 * (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)) + (2 * (2 to_power n)) is V11() V12() integer ext-real V59() Element of INT
(2 to_power (n + 1)) + i is V11() V12() integer ext-real V59() Element of INT
abs i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
- i is V11() V12() integer ext-real V59() Element of INT
- (- (2 to_power n)) is V11() V12() integer ext-real non negative V59() Element of INT
((n + 1),(abs i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
abs ((2 to_power (n + 1)) + i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
NH is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence NH is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(2 to_power (n + 1)) + 0 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 V59() V60() V61() V62() V63() V64() V65() Element of NAT
abs i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence (abs i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n + 1) -BinarySequence i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1),h) . (n + 1) is set
n + 0 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 ((n + 1),i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((n + 1),i) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
((n + 1),i) . (n + 1) is set
((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i))) . (n + 1) is set
((n + 1) -BinarySequence NH) . (n + 1) is set
Intval ((n + 1),i) is V11() V12() integer ext-real set
Absval ((n + 1),i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(Absval ((n + 1),i)) - (2 to_power (n + 1)) is V11() V12() integer ext-real V59() Element of INT
NH - (2 to_power (n + 1)) is V11() V12() integer ext-real V59() Element of INT
len ((n + 1),h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((n + 1),h) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
Int_add_ovfl (((n + 1),h),((n + 1),i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
'not' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K40(1,FALSE) is V11() V12() integer ext-real set
'not' TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K40(1,TRUE) is V11() V12() integer ext-real set
('not' FALSE) '&' ('not' TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(('not' FALSE),('not' TRUE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
carry (((n + 1),h),((n + 1),i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (((n + 1),h),((n + 1),i))) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(('not' FALSE) '&' ('not' TRUE)) '&' ((carry (((n + 1),h),((n + 1),i))) /. (n + 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37((('not' FALSE) '&' ('not' TRUE)),((carry (((n + 1),h),((n + 1),i))) /. (n + 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
Int_add_udfl (((n + 1),h),((n + 1),i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
FALSE '&' TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(FALSE,TRUE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' ((carry (((n + 1),h),((n + 1),i))) /. (n + 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K40(1,((carry (((n + 1),h),((n + 1),i))) /. (n + 1))) is V11() V12() integer ext-real set
(FALSE '&' TRUE) '&' ('not' ((carry (((n + 1),h),((n + 1),i))) /. (n + 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37((FALSE '&' TRUE),('not' ((carry (((n + 1),h),((n + 1),i))) /. (n + 1)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
Intval ((n + 1),h) is V11() V12() integer ext-real set
Absval ((n + 1),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 V11() V12() integer ext-real V59() Element of INT
IFEQ (FALSE,FALSE,0,(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 + i) - (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1)))) is V11() V12() integer ext-real V59() Element of INT
((i + i) - (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1))))) + (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1)))) is V11() V12() integer ext-real V59() Element of INT
(i + i) - 0 is V11() V12() integer ext-real V59() Element of INT
((i + i) - 0) + 0 is V11() V12() integer ext-real V59() Element of INT
c13 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
<*c13*> 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) ^ <*c13*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(K215(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K215(n,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
c14 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
<*c14*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,i) ^ <*c14*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(K215(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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)) + (- (2 to_power n)) is V11() V12() integer ext-real V59() Element of INT
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 1) * (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)) + ((2 to_power 1) * (2 to_power n)) is V11() V12() integer ext-real V59() Element of INT
2 * (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)) + (2 * (2 to_power n)) is V11() V12() integer ext-real V59() Element of INT
(2 to_power (n + 1)) + h is V11() V12() integer ext-real V59() Element of INT
abs 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 V11() V12() integer ext-real V59() Element of INT
- (- (2 to_power n)) is V11() V12() integer ext-real non negative V59() Element of INT
((n + 1),(abs h)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
abs ((2 to_power (n + 1)) + h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
NH is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence NH is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(2 to_power (n + 1)) + 0 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 V59() V60() V61() V62() V63() V64() V65() Element of NAT
abs i is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
(n + 1) -BinarySequence (abs i) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n + 1) -BinarySequence i is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((n + 1),i) . (n + 1) is set
n + 0 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 ((n + 1),h) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((n + 1),h) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
((n + 1),h) . (n + 1) is set
((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h))) . (n + 1) is set
((n + 1) -BinarySequence NH) . (n + 1) is set
Intval ((n + 1),h) is V11() V12() integer ext-real set
Absval ((n + 1),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 + 1),h)) - (2 to_power (n + 1)) is V11() V12() integer ext-real V59() Element of INT
NH - (2 to_power (n + 1)) is V11() V12() integer ext-real V59() Element of INT
len ((n + 1),i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
((n + 1),i) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
Int_add_ovfl (((n + 1),h),((n + 1),i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
'not' TRUE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K40(1,TRUE) is V11() V12() integer ext-real set
'not' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K40(1,FALSE) is V11() V12() integer ext-real set
('not' TRUE) '&' ('not' FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(('not' TRUE),('not' FALSE)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
carry (((n + 1),h),((n + 1),i)) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(n + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (((n + 1),h),((n + 1),i))) /. (n + 1) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
(('not' TRUE) '&' ('not' FALSE)) '&' ((carry (((n + 1),h),((n + 1),i))) /. (n + 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37((('not' TRUE) '&' ('not' FALSE)),((carry (((n + 1),h),((n + 1),i))) /. (n + 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
Int_add_udfl (((n + 1),h),((n + 1),i)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
TRUE '&' FALSE is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37(TRUE,FALSE) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
'not' ((carry (((n + 1),h),((n + 1),i))) /. (n + 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K40(1,((carry (((n + 1),h),((n + 1),i))) /. (n + 1))) is V11() V12() integer ext-real set
(TRUE '&' FALSE) '&' ('not' ((carry (((n + 1),h),((n + 1),i))) /. (n + 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
K37((TRUE '&' FALSE),('not' ((carry (((n + 1),h),((n + 1),i))) /. (n + 1)))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
Intval ((n + 1),i) is V11() V12() integer ext-real set
Absval ((n + 1),i) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
h + i is V11() V12() integer ext-real V59() Element of INT
IFEQ (FALSE,FALSE,0,(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 + i) - (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1)))) is V11() V12() integer ext-real V59() Element of INT
((h + i) - (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1))))) + (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1)))) is V11() V12() integer ext-real V59() Element of INT
(h + i) - 0 is V11() V12() integer ext-real V59() Element of INT
((h + i) - 0) + 0 is V11() V12() integer ext-real V59() Element of INT
c13 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
<*c13*> 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) ^ <*c13*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(K215(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K215(n,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
c14 is V6() V10() V11() V12() integer V34() V39() ext-real non negative boolean Element of BOOLEAN
<*c14*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(n,i) ^ <*c14*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(K215(n,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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 (1 -' 1)) is V11() V12() integer ext-real non positive V59() Element of INT
(2 to_power (1 -' 1)) - 1 is V11() V12() integer ext-real V59() Element of INT
(1,h) is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(1,i) is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(1,h) + (1,i) is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Intval ((1,h) + (1,i)) is V11() V12() integer ext-real set
abs (- 1) 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 negative V59() Element of INT
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
n is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
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
(1,(abs (- 1))) is V6() V10() V11() V12() integer V34() V39() ext-real non negative set
(1,(- 1)) is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(2 to_power 1) + (- 1) is V11() V12() integer ext-real V59() Element of INT
abs ((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
1 -BinarySequence (abs ((2 to_power 1) + (- 1))) is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
2 + (- 1) is V11() V12() integer ext-real V59() Element of INT
abs (2 + (- 1)) is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
1 -BinarySequence (abs (2 + (- 1))) is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
1 -BinarySequence 1 is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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
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
(0 + 1) -BinarySequence (2 to_power 0) is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(0 + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
0* 0 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V49() V50() V51() Element of REAL 0
REAL 0 is functional FinSequence-membered FinSequenceSet of REAL
0 -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 = 0 } is set
0 |-> 0 is empty V6() V10() V11() V12() integer Relation-like non-empty empty-yielding NAT -defined REAL -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() Element of 0 -tuples_on REAL
Seg 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 ) 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() Element of bool NAT
(Seg 0) --> 0 is V8() Relation-like NAT -defined RAT -valued INT -valued Function-like V29( Seg 0,{0}) V34() FinSequence-like FinSubsequence-like V49() V50() V51() V52() Element of bool [:(Seg 0),{0}:]
{0} is non empty trivial functional V41(1) V60() V61() V62() V63() V64() V65() set
[:(Seg 0),{0}:] is Relation-like RAT -valued INT -valued V49() V50() V51() V52() set
bool [:(Seg 0),{0}:] is set
<*1*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant V34() V41(1) FinSequence-like FinSubsequence-like V49() V50() V51() V53() V54() V55() V56() FinSequence of REAL
(0* 0) ^ <*1*> is non empty Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
1 - 1 is V11() V12() integer ext-real V59() Element of INT
(1,0) is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
abs 0 is V6() V10() V11() V12() integer V34() V39() ext-real non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT
1 -BinarySequence (abs 0) is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
1 -BinarySequence 0 is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
0* 1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V49() V50() V51() Element of REAL 1
REAL 1 is functional FinSequence-membered FinSequenceSet of REAL
1 -tuples_on 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 = 1 } is set
1 |-> 0 is non empty trivial Relation-like empty-yielding NAT -defined REAL -valued Function-like one-to-one constant V34() V41(1) FinSequence-like FinSubsequence-like V49() V50() V51() V53() V54() V55() V56() Element of 1 -tuples_on REAL
Seg 1 is non empty trivial V34() V41(1) V60() V61() V62() V63() V64() V65() Element of bool NAT
(Seg 1) --> 0 is Relation-like NAT -defined RAT -valued INT -valued Function-like V29( Seg 1,{0}) V34() FinSequence-like FinSubsequence-like V49() V50() V51() V52() Element of bool [:(Seg 1),{0}:]
[:(Seg 1),{0}:] is Relation-like RAT -valued INT -valued V49() V50() V51() V52() set
bool [:(Seg 1),{0}:] is set