:: BINARI_2 semantic presentation

REAL is set
NAT is non empty V32() V33() V34() V42() V47() V48() Element of K19(REAL)
K19(REAL) is set
{} is functional empty V29() V31() V32() V33() V34() V36() V37() V38() V39() V40() integer V42() V47() V49( {} ) FinSequence-membered V81() set
NAT is non empty V32() V33() V34() V42() V47() V48() set
K19(NAT) is V42() set
K19(NAT) is V42() set
K101(NAT) is V27() set
COMPLEX is set
RAT is set
INT is set
K20(NAT,REAL) is set
K19(K20(NAT,REAL)) is set
K20(COMPLEX,COMPLEX) is set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(REAL,REAL) is set
K19(K20(REAL,REAL)) is set
K20(K20(REAL,REAL),REAL) is set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is V42() set
K20(K20(NAT,NAT),NAT) is V42() set
K19(K20(K20(NAT,NAT),NAT)) is V42() set
BOOLEAN is non empty set
1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
0 is functional empty V29() V31() V32() V33() V34() V36() V37() V38() V39() V40() integer V42() V47() V49( {} ) FinSequence-membered V81() Element of NAT
2 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
3 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
FALSE is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
addnat is V1() V4(K20(NAT,NAT)) V5( NAT ) Function-like V18(K20(NAT,NAT), NAT ) V21( NAT ) V22( NAT ) V28( NAT ) Element of K19(K20(K20(NAT,NAT),NAT))
<*FALSE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
TRUE is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
<*TRUE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
FALSE is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
TRUE is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
Seg m is V42() V49(m) Element of K19(NAT)
z1 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
z2 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len z2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
dom z1 is V49(m) Element of K19(NAT)
d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
z1 . d1 is set
z2 . d1 is set
dom z2 is V49(m) Element of K19(NAT)
z1 /. d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
z2 /. d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
Seg m is V42() V49(m) Element of K19(NAT)
z1 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
dom z1 is Element of K19(NAT)
m -tuples_on BOOLEAN is functional non empty FinSequence-membered FinSequenceSet of BOOLEAN
z2 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
z2 /. d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
IFEQ (d1,1,TRUE,FALSE) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
dom z2 is V49(m) Element of K19(NAT)
z2 . d1 is set
z1 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z2 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
len z2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
dom z1 is V49(m) Element of K19(NAT)
d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
dom z2 is V49(m) Element of K19(NAT)
z1 . d1 is set
z1 /. d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
IFEQ (d1,1,TRUE,FALSE) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
z2 /. d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
z2 . d1 is set
m is non empty V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
z1 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' z1 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(m) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
('not' z1) + (m) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
z1 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z1 /. m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
Absval z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval z1) - (2 to_power m) is V29() V39() V40() integer Element of INT
m is non empty V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
z1 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z1 /. m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
'not' (z1 /. m) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
1 - (z1 /. m) is V29() V39() V40() integer set
z2 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z2 /. m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
'not' (z2 /. m) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
1 - (z2 /. m) is V29() V39() V40() integer set
('not' (z1 /. m)) '&' ('not' (z2 /. m)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
('not' (z1 /. m)) * ('not' (z2 /. m)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
carry (z1,z2) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (z1,z2)) /. m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(('not' (z1 /. m)) '&' ('not' (z2 /. m))) '&' ((carry (z1,z2)) /. m) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(('not' (z1 /. m)) '&' ('not' (z2 /. m))) * ((carry (z1,z2)) /. m) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
m is non empty V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
z1 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z1 /. m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
z2 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z2 /. m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(z1 /. m) '&' (z2 /. m) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(z1 /. m) * (z2 /. m) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
carry (z1,z2) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry (z1,z2)) /. m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
'not' ((carry (z1,z2)) /. m) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
1 - ((carry (z1,z2)) /. m) is V29() V39() V40() integer set
((z1 /. m) '&' (z2 /. m)) '&' ('not' ((carry (z1,z2)) /. m)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
((z1 /. m) '&' (z2 /. m)) * ('not' ((carry (z1,z2)) /. m)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
<*FALSE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*FALSE*> ^ <*FALSE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(1 + 1) V49(1 + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
1 + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
1 + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
m is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(2,m) is V29() V39() V40() integer set
Binary m is V1() V4( NAT ) V5( NAT ) Function-like V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of NAT
z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
z2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*z1,z2*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of NAT
<*FALSE,FALSE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
m /. 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
m /. 2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
Seg 1 is non empty V12() V42() V49(1) Element of K19(NAT)
Seg 2 is non empty V42() V49(2) Element of K19(NAT)
(Binary m) /. 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
1 -' 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (1 -' 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
IFEQ ((m /. 1),FALSE,0,(2 to_power (1 -' 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Binary m) /. 2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 -' 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (2 -' 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
IFEQ ((m /. 2),FALSE,0,(2 to_power (2 -' 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
Absval m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*0,0*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of NAT
addnat $$ <*0,0*> is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*0*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ <*0*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V42() V49(1 + 1) V49(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
addnat $$ (<*0*> ^ <*0*>) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat $$ <*0*> is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat . ((addnat $$ <*0*>),(addnat $$ <*0*>)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat . (0,(addnat $$ <*0*>)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat . (0,0) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
0 + 0 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*TRUE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*TRUE*> ^ <*FALSE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(1 + 1) V49(1 + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
m is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(2,m) is V29() V39() V40() integer set
Binary m is V1() V4( NAT ) V5( NAT ) Function-like V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of NAT
z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
z2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*z1,z2*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of NAT
<*TRUE,FALSE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
m /. 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
m /. 2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
Seg 1 is non empty V12() V42() V49(1) Element of K19(NAT)
Seg 2 is non empty V42() V49(2) Element of K19(NAT)
(Binary m) /. 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
1 -' 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (1 -' 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
IFEQ ((m /. 1),FALSE,0,(2 to_power (1 -' 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
1 - 1 is V29() V39() V40() integer Element of INT
(Binary m) /. 2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 -' 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (2 -' 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
IFEQ ((m /. 2),FALSE,0,(2 to_power (2 -' 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
Absval m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*1,0*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of NAT
addnat $$ <*1,0*> is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*1*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ <*0*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V42() V49(1 + 1) V49(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
addnat $$ (<*1*> ^ <*0*>) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat $$ <*1*> is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat $$ <*0*> is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat . ((addnat $$ <*1*>),(addnat $$ <*0*>)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat . (1,(addnat $$ <*0*>)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat . (1,0) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
1 + 0 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*FALSE*> ^ <*TRUE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(1 + 1) V49(1 + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
- 2 is V29() V30() V39() V40() integer Element of INT
m is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(2,m) is V29() V39() V40() integer set
Binary m is V1() V4( NAT ) V5( NAT ) Function-like V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of NAT
z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
z2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*z1,z2*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of NAT
<*FALSE,TRUE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
m /. 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
m /. 2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
Absval m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (1 + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval m) - (2 to_power (1 + 1)) is V29() V39() V40() integer Element of INT
2 to_power 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(2 to_power 1) * (2 to_power 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval m) - ((2 to_power 1) * (2 to_power 1)) is V29() V39() V40() integer Element of INT
2 * (2 to_power 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval m) - (2 * (2 to_power 1)) is V29() V39() V40() integer Element of INT
2 * 2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval m) - (2 * 2) is V29() V39() V40() integer Element of INT
4 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval m) - 4 is V29() V39() V40() integer Element of INT
Seg 1 is non empty V12() V42() V49(1) Element of K19(NAT)
Seg 2 is non empty V42() V49(2) Element of K19(NAT)
(Binary m) /. 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
1 -' 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (1 -' 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
IFEQ ((m /. 1),FALSE,0,(2 to_power (1 -' 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Binary m) /. 2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 -' 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (2 -' 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
IFEQ ((m /. 2),FALSE,0,(2 to_power (2 -' 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 - 1 is V29() V39() V40() integer Element of INT
<*0,2*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of NAT
addnat $$ <*0,2*> is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*0*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ <*2*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V42() V49(1 + 1) V49(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
addnat $$ (<*0*> ^ <*2*>) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat $$ <*0*> is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat $$ <*2*> is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat . ((addnat $$ <*0*>),(addnat $$ <*2*>)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat . (0,(addnat $$ <*2*>)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat . (0,2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
0 + 2 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*TRUE*> ^ <*TRUE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(1 + 1) V49(1 + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
- 1 is V29() V30() V39() V40() integer Element of INT
m is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(2,m) is V29() V39() V40() integer set
Binary m is V1() V4( NAT ) V5( NAT ) Function-like V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of NAT
z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
z2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*z1,z2*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of NAT
<*TRUE,TRUE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
m /. 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
m /. 2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
Absval m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (1 + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval m) - (2 to_power (1 + 1)) is V29() V39() V40() integer Element of INT
2 to_power 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(2 to_power 1) * (2 to_power 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval m) - ((2 to_power 1) * (2 to_power 1)) is V29() V39() V40() integer Element of INT
2 * (2 to_power 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval m) - (2 * (2 to_power 1)) is V29() V39() V40() integer Element of INT
2 * 2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval m) - (2 * 2) is V29() V39() V40() integer Element of INT
4 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval m) - 4 is V29() V39() V40() integer Element of INT
Seg 1 is non empty V12() V42() V49(1) Element of K19(NAT)
Seg 2 is non empty V42() V49(2) Element of K19(NAT)
(Binary m) /. 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
1 -' 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (1 -' 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
IFEQ ((m /. 1),FALSE,0,(2 to_power (1 -' 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
1 - 1 is V29() V39() V40() integer Element of INT
(Binary m) /. 2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 -' 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (2 -' 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
IFEQ ((m /. 2),FALSE,0,(2 to_power (2 -' 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 - 1 is V29() V39() V40() integer Element of INT
<*1,2*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V42() V49(2) FinSequence-like FinSubsequence-like FinSequence of NAT
addnat $$ <*1,2*> is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
<*1*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ <*2*> is V1() V4( NAT ) V5( NAT ) Function-like non empty V42() V49(1 + 1) V49(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
addnat $$ (<*1*> ^ <*2*>) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat $$ <*1*> is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat $$ <*2*> is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat . ((addnat $$ <*1*>),(addnat $$ <*2*>)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat . (1,(addnat $$ <*2*>)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
addnat . (1,2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
1 + 2 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
Seg m is V42() V49(m) Element of K19(NAT)
(m) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
(m) /. z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
IFEQ (z1,1,TRUE,FALSE) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
Seg m is V42() V49(m) Element of K19(NAT)
(m) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
(m) /. z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
IFEQ (z1,1,TRUE,FALSE) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
m is non empty V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
m + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
((m + 1)) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(m) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(m) ^ <*FALSE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(m + 1) V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
m + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
len ((m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
len ((m) ^ <*FALSE*>) is non empty V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
Seg (m + 1) is non empty V42() V49(m + 1) Element of K19(NAT)
z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
((m + 1)) /. z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
((m) ^ <*FALSE*>) /. z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
Seg m is non empty V42() V49(m) Element of K19(NAT)
(m) /. z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(m) /. z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
Seg m is non empty V42() V49(m) Element of K19(NAT)
(1) is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(1) ^ <*FALSE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(1 + 1) V49(1 + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((1 + 1),((1) ^ <*FALSE*>)) is V29() V39() V40() integer set
m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
<*m*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(1) /. 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
Seg 1 is non empty V12() V42() V49(1) Element of K19(NAT)
m is non empty V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
m + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(m) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(m) ^ <*FALSE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(m + 1) V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
m + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
((m + 1),((m) ^ <*FALSE*>)) is V29() V39() V40() integer set
((m) ^ <*FALSE*>) /. (m + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
Absval ((m) ^ <*FALSE*>) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
((m + 1)) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((m + 1)) ^ <*FALSE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49((m + 1) + 1) V49((m + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(m + 1) + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(m + 1) + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(((m + 1)) ^ <*FALSE*>) /. ((m + 1) + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(((m + 1) + 1),(((m + 1)) ^ <*FALSE*>)) is V29() V39() V40() integer set
Absval (((m + 1)) ^ <*FALSE*>) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(m + 1) + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
((m) ^ <*FALSE*>) ^ <*FALSE*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49((m + 1) + 1) V49((m + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(m + 1) + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
Absval (((m) ^ <*FALSE*>) ^ <*FALSE*>) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (m + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
IFEQ (FALSE,FALSE,0,(2 to_power (m + 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval ((m) ^ <*FALSE*>)) + (IFEQ (FALSE,FALSE,0,(2 to_power (m + 1)))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
1 + 0 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
m is non empty V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
m + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
z1 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' z1 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
<*z2*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z1 ^ <*z2*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(m + 1) V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
m + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
'not' (z1 ^ <*z2*>) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' z2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
1 - z2 is V29() V39() V40() integer set
<*('not' z2)*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
('not' z1) ^ <*('not' z2)*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(m + 1) V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len ('not' (z1 ^ <*z2*>)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
len (('not' z1) ^ <*('not' z2)*>) is non empty V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
Seg (m + 1) is non empty V42() V49(m + 1) Element of K19(NAT)
d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
('not' (z1 ^ <*z2*>)) /. d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(('not' z1) ^ <*('not' z2)*>) /. d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
Seg m is non empty V42() V49(m) Element of K19(NAT)
(z1 ^ <*z2*>) /. d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
'not' ((z1 ^ <*z2*>) /. d1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
1 - ((z1 ^ <*z2*>) /. d1) is V29() V39() V40() integer set
z1 /. d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
'not' (z1 /. d1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
1 - (z1 /. d1) is V29() V39() V40() integer set
('not' z1) /. d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(z1 ^ <*z2*>) /. d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
'not' ((z1 ^ <*z2*>) /. d1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
1 - ((z1 ^ <*z2*>) /. d1) is V29() V39() V40() integer set
Seg m is non empty V42() V49(m) Element of K19(NAT)
m is non empty V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
m + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
z1 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
z2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
<*z2*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z1 ^ <*z2*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(m + 1) V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
m + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
((m + 1),(z1 ^ <*z2*>)) is V29() V39() V40() integer set
IFEQ (z2,FALSE,0,(2 to_power m)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval z1) - (IFEQ (z2,FALSE,0,(2 to_power m))) is V29() V39() V40() integer Element of INT
(z1 ^ <*z2*>) /. (m + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
Absval (z1 ^ <*z2*>) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval z1) + (IFEQ (z2,FALSE,0,(2 to_power m))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval z1) + 0 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval z1) - 0 is V29() V39() V40() integer Element of INT
(z1 ^ <*z2*>) /. (m + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
Absval (z1 ^ <*z2*>) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (m + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval (z1 ^ <*z2*>)) - (2 to_power (m + 1)) is V29() V39() V40() integer Element of INT
(Absval z1) + (IFEQ (z2,FALSE,0,(2 to_power m))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
((Absval z1) + (IFEQ (z2,FALSE,0,(2 to_power m)))) - (2 to_power (m + 1)) is V29() V39() V40() integer Element of INT
(Absval z1) + (2 to_power m) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
((Absval z1) + (2 to_power m)) - (2 to_power (m + 1)) is V29() V39() V40() integer Element of INT
2 to_power 1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(2 to_power m) * (2 to_power 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
((Absval z1) + (2 to_power m)) - ((2 to_power m) * (2 to_power 1)) is V29() V39() V40() integer Element of INT
2 * (2 to_power m) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
((Absval z1) + (2 to_power m)) - (2 * (2 to_power m)) is V29() V39() V40() integer Element of INT
(Absval z1) - (2 to_power m) is V29() V39() V40() integer Element of INT
m is non empty V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
m + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
m + 1 is non empty V29() V30() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
2 to_power (m + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
z1 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z2 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
<*d1*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z1 ^ <*d1*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(m + 1) V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
d2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
<*d2*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
z2 ^ <*d2*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(m + 1) V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(z1 ^ <*d1*>) + (z2 ^ <*d2*>) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((m + 1),((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) is V29() V39() V40() integer set
((m + 1),(z1 ^ <*d1*>),(z2 ^ <*d2*>)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(z1 ^ <*d1*>) /. (m + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
'not' ((z1 ^ <*d1*>) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
1 - ((z1 ^ <*d1*>) /. (m + 1)) is V29() V39() V40() integer set
(z2 ^ <*d2*>) /. (m + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
'not' ((z2 ^ <*d2*>) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
1 - ((z2 ^ <*d2*>) /. (m + 1)) is V29() V39() V40() integer set
('not' ((z1 ^ <*d1*>) /. (m + 1))) '&' ('not' ((z2 ^ <*d2*>) /. (m + 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
('not' ((z1 ^ <*d1*>) /. (m + 1))) * ('not' ((z2 ^ <*d2*>) /. (m + 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>)) is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(('not' ((z1 ^ <*d1*>) /. (m + 1))) '&' ('not' ((z2 ^ <*d2*>) /. (m + 1)))) '&' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(('not' ((z1 ^ <*d1*>) /. (m + 1))) '&' ('not' ((z2 ^ <*d2*>) /. (m + 1)))) * ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
IFEQ (((m + 1),(z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE,0,(2 to_power (m + 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
((m + 1),((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (((m + 1),(z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE,0,(2 to_power (m + 1)))) is V29() V39() V40() integer Element of INT
((m + 1),(z1 ^ <*d1*>),(z2 ^ <*d2*>)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
((z1 ^ <*d1*>) /. (m + 1)) '&' ((z2 ^ <*d2*>) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
((z1 ^ <*d1*>) /. (m + 1)) * ((z2 ^ <*d2*>) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
'not' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
1 - ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)) is V29() V39() V40() integer set
(((z1 ^ <*d1*>) /. (m + 1)) '&' ((z2 ^ <*d2*>) /. (m + 1))) '&' ('not' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(((z1 ^ <*d1*>) /. (m + 1)) '&' ((z2 ^ <*d2*>) /. (m + 1))) * ('not' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
IFEQ (((m + 1),(z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE,0,(2 to_power (m + 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(((m + 1),((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (((m + 1),(z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE,0,(2 to_power (m + 1))))) - (IFEQ (((m + 1),(z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE,0,(2 to_power (m + 1)))) is V29() V39() V40() integer Element of INT
((m + 1),(z1 ^ <*d1*>)) is V29() V39() V40() integer set
((m + 1),(z2 ^ <*d2*>)) is V29() V39() V40() integer set
((m + 1),(z1 ^ <*d1*>)) + ((m + 1),(z2 ^ <*d2*>)) is V29() V39() V40() integer Element of INT
z1 + z2 is V1() V4( NAT ) V5( BOOLEAN ) Function-like V42() V49(m) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval (z1 + z2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
Absval z1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
Absval z2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(Absval z1) + (Absval z2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
add_ovfl (z1,z2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
2 to_power m is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power m)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
((Absval z1) + (Absval z2)) - (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power m))) is V29() V39() V40() integer Element of INT
(Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power m))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
((Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power m)))) - (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power m))) is V29() V39() V40() integer Element of INT
d1 'xor' d2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
d1 <=> d2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
d1 => d2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
'not' d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - d1 is V29() V39() V40() integer set
('not' d1) 'or' d2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
'not' ('not' d1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - ('not' d1) is V29() V39() V40() integer set
'not' d2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - d2 is V29() V39() V40() integer set
('not' ('not' d1)) '&' ('not' d2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
('not' ('not' d1)) * ('not' d2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
'not' (('not' ('not' d1)) '&' ('not' d2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - (('not' ('not' d1)) '&' ('not' d2)) is V29() V39() V40() integer set
d2 => d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
('not' d2) 'or' d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
'not' ('not' d2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - ('not' d2) is V29() V39() V40() integer set
('not' ('not' d2)) '&' ('not' d1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
('not' ('not' d2)) * ('not' d1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
'not' (('not' ('not' d2)) '&' ('not' d1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - (('not' ('not' d2)) '&' ('not' d1)) is V29() V39() V40() integer set
(d1 => d2) '&' (d2 => d1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
(d1 => d2) * (d2 => d1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
'not' (d1 <=> d2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - (d1 <=> d2) is V29() V39() V40() integer set
(d1 'xor' d2) 'xor' (add_ovfl (z1,z2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(d1 'xor' d2) <=> (add_ovfl (z1,z2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
(d1 'xor' d2) => (add_ovfl (z1,z2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
'not' (d1 'xor' d2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - (d1 'xor' d2) is V29() V39() V40() integer set
('not' (d1 'xor' d2)) 'or' (add_ovfl (z1,z2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
'not' ('not' (d1 'xor' d2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - ('not' (d1 'xor' d2)) is V29() V39() V40() integer set
'not' (add_ovfl (z1,z2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - (add_ovfl (z1,z2)) is V29() V39() V40() integer set
('not' ('not' (d1 'xor' d2))) '&' ('not' (add_ovfl (z1,z2))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
('not' ('not' (d1 'xor' d2))) * ('not' (add_ovfl (z1,z2))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
'not' (('not' ('not' (d1 'xor' d2))) '&' ('not' (add_ovfl (z1,z2)))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - (('not' ('not' (d1 'xor' d2))) '&' ('not' (add_ovfl (z1,z2)))) is V29() V39() V40() integer set
(add_ovfl (z1,z2)) => (d1 'xor' d2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
('not' (add_ovfl (z1,z2))) 'or' (d1 'xor' d2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
'not' ('not' (add_ovfl (z1,z2))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - ('not' (add_ovfl (z1,z2))) is V29() V39() V40() integer set
('not' ('not' (add_ovfl (z1,z2)))) '&' ('not' (d1 'xor' d2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
('not' ('not' (add_ovfl (z1,z2)))) * ('not' (d1 'xor' d2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
'not' (('not' ('not' (add_ovfl (z1,z2)))) '&' ('not' (d1 'xor' d2))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - (('not' ('not' (add_ovfl (z1,z2)))) '&' ('not' (d1 'xor' d2))) is V29() V39() V40() integer set
((d1 'xor' d2) => (add_ovfl (z1,z2))) '&' ((add_ovfl (z1,z2)) => (d1 'xor' d2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
((d1 'xor' d2) => (add_ovfl (z1,z2))) * ((add_ovfl (z1,z2)) => (d1 'xor' d2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
'not' ((d1 'xor' d2) <=> (add_ovfl (z1,z2))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean set
1 - ((d1 'xor' d2) <=> (add_ovfl (z1,z2))) is V29() V39() V40() integer set
<*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V12() V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*> is V1() V4( NAT ) V5( BOOLEAN ) Function-like non empty V42() V49(m + 1) V49(m + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
((m + 1),((z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>)) is V29() V39() V40() integer set
IFEQ (((d1 'xor' d2) 'xor' (add_ovfl (z1,z2))),FALSE,0,(2 to_power m)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() Element of NAT
(((Absval z1) + (Absval z2)) - (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power m)))) - (IFEQ (((d1 'xor' d2) 'xor' (add_ovfl (z1,z2))),FALSE,0,(2 to_power m))) is V29() V39() V40() integer Element of INT
'not' d1 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(z2 ^ <*d2*>) /. (m + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
'not' ((z2 ^ <*d2*>) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
1 - ((z2 ^ <*d2*>) /. (m + 1)) is V29() V39() V40() integer set
('not' d1) '&' ('not' ((z2 ^ <*d2*>) /. (m + 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
('not' d1) * ('not' ((z2 ^ <*d2*>) /. (m + 1))) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(('not' d1) '&' ('not' ((z2 ^ <*d2*>) /. (m + 1)))) '&' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(('not' d1) '&' ('not' ((z2 ^ <*d2*>) /. (m + 1)))) * ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
'not' d2 is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
('not' d1) '&' ('not' d2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
('not' d1) * ('not' d2) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
(('not' d1) '&' ('not' d2)) '&' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(('not' d1) '&' ('not' d2)) * ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
(('not' d1) '&' ('not' d2)) '&' (add_ovfl (z1,z2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
(('not' d1) '&' ('not' d2)) * (add_ovfl (z1,z2)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
d1 '&' ((z2 ^ <*d2*>) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
d1 * ((z2 ^ <*d2*>) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() set
'not' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)) is V29() V31() V32() V33() V34() V38() V39() V40() integer V42() V47() boolean Element of BOOLEAN
1 - ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)) is V29() V39() V40() integer set
(d1 '&' ((z2 ^