REAL is V1() V28() set
NAT is V1() V4() V5() V6() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V1() V28() set
NAT is V1() V4() V5() V6() set
K6(NAT) is set
K6(NAT) is set
RAT is V1() V28() set
INT is V1() V28() set
K7(REAL,REAL) is set
K6(K7(REAL,REAL)) is set
K335() is V69() V97() L8()
the U1 of K335() is set
K6(INT) is set
1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative Element of NAT
2 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
- 2 is V11() V12() V13() ext-real non positive set
- 1 is V11() V12() V13() ext-real non positive set
SD_Add_Carry 0 is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Radix n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix n) - 1 is V11() V12() V13() ext-real set
n -SD is V1() Element of K6(INT)
(Radix n) + (Radix n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
1 + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
0 + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(0 + 1) - (Radix n) is V11() V12() V13() ext-real set
- (Radix n) is V11() V12() V13() ext-real non positive set
(- (Radix n)) + 1 is V11() V12() V13() ext-real set
{ b1 where b1 is V11() V12() V13() ext-real Element of INT : ( b1 <= (Radix n) - 1 & (- (Radix n)) + 1 <= b1 ) } is set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg m is Element of K6(NAT)
n -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n - 1 is V11() V12() V13() ext-real set
1 - 1 is V11() V12() V13() ext-real set
0 + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
4 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative Element of NAT
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Radix n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
Radix (n + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
2 to_power (n + 1) is V11() V12() ext-real set
2 to_power 1 is V11() V12() ext-real Element of REAL
2 to_power n is V11() V12() ext-real set
(2 to_power 1) * (2 to_power n) is V11() V12() ext-real set
2 * (2 to_power n) is V11() V12() ext-real set
2 * (Radix n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Radix 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
1 + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 to_power (1 + 1) is V11() V12() ext-real set
2 to_power 1 is V11() V12() ext-real Element of REAL
(2 to_power 1) * (2 to_power 1) is V11() V12() ext-real set
2 * (2 to_power 1) is V11() V12() ext-real set
2 * 2 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Radix n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n -SD is V1() Element of K6(INT)
m is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like FinSequence of n -SD
SDDec m is V11() V12() V13() ext-real set
DigA (m,1) is V11() V12() V13() ext-real set
Seg 1 is Element of K6(NAT)
DigitSD m is V15() V18( NAT ) V19( INT ) Function-like V35(1) FinSequence-like FinSequence of INT
(DigitSD m) /. 1 is V11() V12() V13() ext-real Element of INT
SubDigit (m,1,n) is V11() V12() V13() ext-real Element of INT
Radix n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix n) |^ (1 -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigB (m,1) is V11() V12() V13() ext-real Element of INT
((Radix n) |^ (1 -' 1)) * (DigB (m,1)) is V11() V12() V13() ext-real set
((Radix n) |^ (1 -' 1)) * (DigA (m,1)) is V11() V12() V13() ext-real set
(Radix n) |^ 0 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((Radix n) |^ 0) * (DigA (m,1)) is V11() V12() V13() ext-real set
1 * (DigA (m,1)) is V11() V12() V13() ext-real set
len (DigitSD m) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom (DigitSD m) is Element of K6(NAT)
(DigitSD m) . 1 is set
Sum (DigitSD m) is V11() V12() V13() ext-real Element of INT
k is V11() V12() V13() ext-real Element of INT
<*k*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like FinSequence of INT
Sum <*k*> is V11() V12() V13() ext-real Element of INT
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg k is Element of K6(NAT)
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DecSD (0,k,m) is V15() V18( NAT ) V19(m -SD ) Function-like V35(k) FinSequence-like FinSequence of m -SD
m -SD is V1() Element of K6(INT)
DigA ((DecSD (0,k,m)),n) is V11() V12() V13() ext-real set
DigitDC (0,n,m) is Element of m -SD
Radix m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix m) |^ n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
0 mod ((Radix m) |^ n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix m) |^ (n -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(0 mod ((Radix m) |^ n)) div ((Radix m) |^ (n -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0 div ((Radix m) |^ (n -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(0 div ((Radix m) |^ (n -' 1))) mod (Radix m) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0 mod (Radix m) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DecSD (0,n,m) is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
m -SD is V1() Element of K6(INT)
SDDec (DecSD (0,n,m)) is V11() V12() V13() ext-real set
0 + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
Radix m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix m) |^ n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg m is Element of K6(NAT)
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DecSD (1,m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m) FinSequence-like FinSequence of n -SD
n -SD is V1() Element of K6(INT)
DigA ((DecSD (1,m,n)),1) is V11() V12() V13() ext-real set
Radix n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigitDC (1,1,n) is Element of n -SD
(Radix n) |^ 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
1 mod ((Radix n) |^ 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix n) |^ (1 -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(1 mod ((Radix n) |^ 1)) div ((Radix n) |^ (1 -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
1 div ((Radix n) |^ (1 -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(1 div ((Radix n) |^ (1 -' 1))) mod (Radix n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix n) |^ 0 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
1 div ((Radix n) |^ 0) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(1 div ((Radix n) |^ 0)) mod (Radix n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
1 div 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(1 div 1) mod (Radix n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
1 mod (Radix n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg k is Element of K6(NAT)
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DecSD (1,k,m) is V15() V18( NAT ) V19(m -SD ) Function-like V35(k) FinSequence-like FinSequence of m -SD
m -SD is V1() Element of K6(INT)
DigA ((DecSD (1,k,m)),n) is V11() V12() V13() ext-real set
n - 1 is V11() V12() V13() ext-real set
1 - 1 is V11() V12() V13() ext-real set
n -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
Radix m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix m) |^ (n -' 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
1 div ((Radix m) |^ (n -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigitDC (1,n,m) is Element of m -SD
(Radix m) |^ n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
1 mod ((Radix m) |^ n) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(1 mod ((Radix m) |^ n)) div ((Radix m) |^ (n -' 1)) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(1 div ((Radix m) |^ (n -' 1))) mod (Radix m) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DecSD (1,n,m) is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
m -SD is V1() Element of K6(INT)
SDDec (DecSD (1,n,m)) is V11() V12() V13() ext-real set
Radix m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
0 + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(Radix m) |^ n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Radix n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
SD_Add_Carry (Radix n) is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Radix n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
SD_Add_Data ((Radix n),n) is V11() V12() V13() ext-real set
SD_Add_Carry (Radix n) is V11() V12() V13() ext-real set
(SD_Add_Carry (Radix n)) * (Radix n) is V11() V12() V13() ext-real set
(Radix n) - ((SD_Add_Carry (Radix n)) * (Radix n)) is V11() V12() V13() ext-real set
(Radix n) - (Radix n) is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Radix n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix n) - 1 is V11() V12() V13() ext-real set
SD_Add_Carry ((Radix n) - 1) is V11() V12() V13() ext-real set
4 - 1 is V11() V12() V13() ext-real set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg n is Element of K6(NAT)
DecSD (1,n,m) is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
m -SD is V1() Element of K6(INT)
DigA ((DecSD (1,n,m)),k) is V11() V12() V13() ext-real set
SD_Add_Carry (DigA ((DecSD (1,n,m)),k)) is V11() V12() V13() ext-real set
SD_Add_Carry 1 is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg n is Element of K6(NAT)
n + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
Seg (n + 1) is Element of K6(NAT)
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m -SD is V1() Element of K6(INT)
k is V15() V18( NAT ) V19(m -SD ) Function-like V35(n + 1) FinSequence-like FinSequence of m -SD
i is V15() V18( NAT ) V19(m -SD ) Function-like V35(n + 1) FinSequence-like FinSequence of m -SD
SDDec k is V11() V12() V13() ext-real set
SDDec i is V11() V12() V13() ext-real set
a is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like FinSequence of INT
len a is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom a is Element of K6(NAT)
rng a is set
b is set
txn is set
a . txn is set
txn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigA (k,txn) is V11() V12() V13() ext-real set
DigB (k,txn) is V11() V12() V13() ext-real Element of INT
b is V15() V18( NAT ) V19(m -SD ) Function-like FinSequence-like FinSequence of m -SD
txn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
b . txn is set
k . txn is set
DigB (k,txn) is V11() V12() V13() ext-real Element of INT
DigA (k,txn) is V11() V12() V13() ext-real set
txn is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like FinSequence of INT
len txn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom txn is Element of K6(NAT)
rng txn is set
txn is set
tyn is set
txn . tyn is set
tyn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigA (i,tyn) is V11() V12() V13() ext-real set
DigB (i,tyn) is V11() V12() V13() ext-real Element of INT
txn is V15() V18( NAT ) V19(m -SD ) Function-like FinSequence-like FinSequence of m -SD
tyn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
txn . tyn is set
i . tyn is set
DigB (i,tyn) is V11() V12() V13() ext-real Element of INT
DigA (i,tyn) is V11() V12() V13() ext-real set
tyn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
tyn -tuples_on (m -SD) is V1() functional FinSequence-membered FinSequenceSet of m -SD
tyn is V15() V18( NAT ) V19(m -SD ) Function-like V35(tyn) FinSequence-like FinSequence of m -SD
SDDec tyn is V11() V12() V13() ext-real set
Radix m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix m) |^ tyn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
tyn + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
DigA (i,(tyn + 1)) is V11() V12() V13() ext-real set
((Radix m) |^ tyn) * (DigA (i,(tyn + 1))) is V11() V12() V13() ext-real set
(SDDec tyn) + (((Radix m) |^ tyn) * (DigA (i,(tyn + 1)))) is V11() V12() V13() ext-real set
Seg tyn is Element of K6(NAT)
tzn is V15() V18( NAT ) V19(m -SD ) Function-like V35(tyn) FinSequence-like FinSequence of m -SD
tzn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DigA (tzn,tzn) is V11() V12() V13() ext-real set
DigA (tyn,tzn) is V11() V12() V13() ext-real set
tyn . tzn is set
DigB (i,tzn) is V11() V12() V13() ext-real Element of INT
DigA (i,tzn) is V11() V12() V13() ext-real set
tzn . tzn is set
DigB (k,tzn) is V11() V12() V13() ext-real Element of INT
DigA (k,tzn) is V11() V12() V13() ext-real set
SDDec tzn is V11() V12() V13() ext-real set
DigA (k,(tyn + 1)) is V11() V12() V13() ext-real set
((Radix m) |^ tyn) * (DigA (k,(tyn + 1))) is V11() V12() V13() ext-real set
(SDDec tzn) + (((Radix m) |^ tyn) * (DigA (k,(tyn + 1)))) is V11() V12() V13() ext-real set
Seg 1 is Element of K6(NAT)
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n -SD is V1() Element of K6(INT)
m is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like FinSequence of n -SD
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like FinSequence of n -SD
SDDec m is V11() V12() V13() ext-real set
SDDec k is V11() V12() V13() ext-real set
DigA (k,1) is V11() V12() V13() ext-real set
DigA (m,1) is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m -SD is V1() Element of K6(INT)
Seg n is Element of K6(NAT)
k is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
i is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
SDDec k is V11() V12() V13() ext-real set
SDDec i is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg n is Element of K6(NAT)
n + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
Seg (n + 1) is Element of K6(NAT)
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m -SD is V1() Element of K6(INT)
i is V15() V18( NAT ) V19(m -SD ) Function-like V35(n + 1) FinSequence-like FinSequence of m -SD
k is V15() V18( NAT ) V19(m -SD ) Function-like V35(n + 1) FinSequence-like FinSequence of m -SD
SDDec i is V11() V12() V13() ext-real set
SDDec k is V11() V12() V13() ext-real set
a is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
b is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like FinSequence of INT
len b is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom b is Element of K6(NAT)
txn is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like FinSequence of INT
len txn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom txn is Element of K6(NAT)
Seg a is Element of K6(NAT)
rng txn is set
txn is set
tyn is set
txn . tyn is set
tyn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
a + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
Seg (a + 1) is Element of K6(NAT)
DigA (i,tyn) is V11() V12() V13() ext-real set
DigB (i,tyn) is V11() V12() V13() ext-real Element of INT
txn is V15() V18( NAT ) V19(m -SD ) Function-like FinSequence-like FinSequence of m -SD
tyn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
txn . tyn is set
i . tyn is set
a + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
Seg (a + 1) is Element of K6(NAT)
DigB (i,tyn) is V11() V12() V13() ext-real Element of INT
DigA (i,tyn) is V11() V12() V13() ext-real set
a -tuples_on (m -SD) is V1() functional FinSequence-membered FinSequenceSet of m -SD
rng b is set
tyn is set
tzn is set
b . tzn is set
tzn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
a + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
Seg (a + 1) is Element of K6(NAT)
DigA (k,tzn) is V11() V12() V13() ext-real set
DigB (k,tzn) is V11() V12() V13() ext-real Element of INT
tyn is V15() V18( NAT ) V19(m -SD ) Function-like FinSequence-like FinSequence of m -SD
tzn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
tyn . tzn is set
k . tzn is set
a + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
Seg (a + 1) is Element of K6(NAT)
DigB (k,tzn) is V11() V12() V13() ext-real Element of INT
DigA (k,tzn) is V11() V12() V13() ext-real set
tyn is V15() V18( NAT ) V19(m -SD ) Function-like V35(a) FinSequence-like FinSequence of m -SD
tzn is V15() V18( NAT ) V19(m -SD ) Function-like V35(a) FinSequence-like FinSequence of m -SD
tzn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DigA (tyn,tzn) is V11() V12() V13() ext-real set
DigA (tzn,tzn) is V11() V12() V13() ext-real set
tyn . tzn is set
DigB (i,tzn) is V11() V12() V13() ext-real Element of INT
DigA (i,tzn) is V11() V12() V13() ext-real set
tzn . tzn is set
DigB (k,tzn) is V11() V12() V13() ext-real Element of INT
DigA (k,tzn) is V11() V12() V13() ext-real set
SDDec tyn is V11() V12() V13() ext-real set
SDDec tzn is V11() V12() V13() ext-real set
a + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
Seg (a + 1) is Element of K6(NAT)
Radix m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix m) |^ a is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigA (i,(a + 1)) is V11() V12() V13() ext-real set
((Radix m) |^ a) * (DigA (i,(a + 1))) is V11() V12() V13() ext-real set
DigA (k,(a + 1)) is V11() V12() V13() ext-real set
((Radix m) |^ a) * (DigA (k,(a + 1))) is V11() V12() V13() ext-real set
(SDDec tyn) + (((Radix m) |^ a) * (DigA (i,(a + 1)))) is V11() V12() V13() ext-real set
(SDDec tzn) + (((Radix m) |^ a) * (DigA (k,(a + 1)))) is V11() V12() V13() ext-real set
Seg 1 is Element of K6(NAT)
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n -SD is V1() Element of K6(INT)
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like FinSequence of n -SD
m is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like FinSequence of n -SD
SDDec k is V11() V12() V13() ext-real set
SDDec m is V11() V12() V13() ext-real set
DigA (k,1) is V11() V12() V13() ext-real set
DigA (m,1) is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m -SD is V1() Element of K6(INT)
Seg n is Element of K6(NAT)
i is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
k is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
SDDec i is V11() V12() V13() ext-real set
SDDec k is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg n is Element of K6(NAT)
n + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
Seg (n + 1) is Element of K6(NAT)
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m -SD is V1() Element of K6(INT)
k is V15() V18( NAT ) V19(m -SD ) Function-like V35(n + 1) FinSequence-like FinSequence of m -SD
a is V15() V18( NAT ) V19(m -SD ) Function-like V35(n + 1) FinSequence-like FinSequence of m -SD
i is V15() V18( NAT ) V19(m -SD ) Function-like V35(n + 1) FinSequence-like FinSequence of m -SD
b is V15() V18( NAT ) V19(m -SD ) Function-like V35(n + 1) FinSequence-like FinSequence of m -SD
SDDec a is V11() V12() V13() ext-real set
SDDec b is V11() V12() V13() ext-real set
(SDDec a) + (SDDec b) is V11() V12() V13() ext-real set
SDDec k is V11() V12() V13() ext-real set
SDDec i is V11() V12() V13() ext-real set
(SDDec k) + (SDDec i) is V11() V12() V13() ext-real set
txn is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like FinSequence of INT
len txn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom txn is Element of K6(NAT)
rng txn is set
txn is set
tyn is set
txn . tyn is set
tyn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigA (k,tyn) is V11() V12() V13() ext-real set
DigB (k,tyn) is V11() V12() V13() ext-real Element of INT
txn is V15() V18( NAT ) V19(m -SD ) Function-like FinSequence-like FinSequence of m -SD
tyn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
txn . tyn is set
k . tyn is set
DigB (k,tyn) is V11() V12() V13() ext-real Element of INT
DigA (k,tyn) is V11() V12() V13() ext-real set
tyn is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like FinSequence of INT
len tyn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom tyn is Element of K6(NAT)
rng tyn is set
tyn is set
tzn is set
tyn . tzn is set
tzn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigA (i,tzn) is V11() V12() V13() ext-real set
DigB (i,tzn) is V11() V12() V13() ext-real Element of INT
tyn is V15() V18( NAT ) V19(m -SD ) Function-like FinSequence-like FinSequence of m -SD
tzn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
tyn . tzn is set
i . tzn is set
DigB (i,tzn) is V11() V12() V13() ext-real Element of INT
DigA (i,tzn) is V11() V12() V13() ext-real set
tzn is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like FinSequence of INT
len tzn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom tzn is Element of K6(NAT)
rng tzn is set
tzn is set
twn is set
tzn . twn is set
twn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigA (a,twn) is V11() V12() V13() ext-real set
DigB (a,twn) is V11() V12() V13() ext-real Element of INT
tzn is V15() V18( NAT ) V19(m -SD ) Function-like FinSequence-like FinSequence of m -SD
twn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
tzn . twn is set
a . twn is set
DigB (a,twn) is V11() V12() V13() ext-real Element of INT
DigA (a,twn) is V11() V12() V13() ext-real set
twn is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like FinSequence of INT
len twn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom twn is Element of K6(NAT)
rng twn is set
twn is set
n is set
twn . n is set
twn is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigA (b,twn) is V11() V12() V13() ext-real set
DigB (b,twn) is V11() V12() V13() ext-real Element of INT
twn is V15() V18( NAT ) V19(m -SD ) Function-like FinSequence-like FinSequence of m -SD
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
twn . n is set
b . n is set
DigB (b,n) is V11() V12() V13() ext-real Element of INT
DigA (b,n) is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n -tuples_on (m -SD) is V1() functional FinSequence-membered FinSequenceSet of m -SD
tyn is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
SDDec tyn is V11() V12() V13() ext-real set
Radix m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix m) |^ n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
n + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
DigA (i,(n + 1)) is V11() V12() V13() ext-real set
((Radix m) |^ n) * (DigA (i,(n + 1))) is V11() V12() V13() ext-real set
(SDDec tyn) + (((Radix m) |^ n) * (DigA (i,(n + 1)))) is V11() V12() V13() ext-real set
Seg (n + 1) is Element of K6(NAT)
DigA (k,(n + 1)) is V11() V12() V13() ext-real set
DigA (a,(n + 1)) is V11() V12() V13() ext-real set
DigA (b,(n + 1)) is V11() V12() V13() ext-real set
twn is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
SDDec twn is V11() V12() V13() ext-real set
((Radix m) |^ n) * (DigA (b,(n + 1))) is V11() V12() V13() ext-real set
(SDDec twn) + (((Radix m) |^ n) * (DigA (b,(n + 1)))) is V11() V12() V13() ext-real set
tzn is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
SDDec tzn is V11() V12() V13() ext-real set
((Radix m) |^ n) * (DigA (a,(n + 1))) is V11() V12() V13() ext-real set
(SDDec tzn) + (((Radix m) |^ n) * (DigA (a,(n + 1)))) is V11() V12() V13() ext-real set
Seg n is Element of K6(NAT)
txn is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DigA (txn,i) is V11() V12() V13() ext-real set
DigA (tzn,i) is V11() V12() V13() ext-real set
DigA (tyn,i) is V11() V12() V13() ext-real set
DigA (twn,i) is V11() V12() V13() ext-real set
DigA (i,i) is V11() V12() V13() ext-real set
i . i is set
tyn . i is set
DigA (b,i) is V11() V12() V13() ext-real set
b . i is set
twn . i is set
DigA (a,i) is V11() V12() V13() ext-real set
a . i is set
tzn . i is set
DigA (k,i) is V11() V12() V13() ext-real set
k . i is set
txn . i is set
(SDDec tzn) + (SDDec twn) is V11() V12() V13() ext-real set
SDDec txn is V11() V12() V13() ext-real set
(SDDec txn) + (SDDec tyn) is V11() V12() V13() ext-real set
((Radix m) |^ n) * (DigA (k,(n + 1))) is V11() V12() V13() ext-real set
(SDDec txn) + (((Radix m) |^ n) * (DigA (k,(n + 1)))) is V11() V12() V13() ext-real set
Seg 1 is Element of K6(NAT)
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n -SD is V1() Element of K6(INT)
m is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like FinSequence of n -SD
i is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like FinSequence of n -SD
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like FinSequence of n -SD
a is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like FinSequence of n -SD
SDDec i is V11() V12() V13() ext-real set
SDDec a is V11() V12() V13() ext-real set
(SDDec i) + (SDDec a) is V11() V12() V13() ext-real set
SDDec m is V11() V12() V13() ext-real set
SDDec k is V11() V12() V13() ext-real set
(SDDec m) + (SDDec k) is V11() V12() V13() ext-real set
m '+' k is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like FinSequence of n -SD
SDDec (m '+' k) is V11() V12() V13() ext-real set
DigA ((m '+' k),1) is V11() V12() V13() ext-real set
Add (m,k,1,n) is Element of n -SD
DigA (m,1) is V11() V12() V13() ext-real set
DigA (k,1) is V11() V12() V13() ext-real set
(DigA (m,1)) + (DigA (k,1)) is V11() V12() V13() ext-real set
SD_Add_Data (((DigA (m,1)) + (DigA (k,1))),n) is V11() V12() V13() ext-real set
1 -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigA (m,(1 -' 1)) is V11() V12() V13() ext-real set
DigA (k,(1 -' 1)) is V11() V12() V13() ext-real set
(DigA (m,(1 -' 1))) + (DigA (k,(1 -' 1))) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA (m,(1 -' 1))) + (DigA (k,(1 -' 1)))) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (m,1)) + (DigA (k,1))),n)) + (SD_Add_Carry ((DigA (m,(1 -' 1))) + (DigA (k,(1 -' 1))))) is V11() V12() V13() ext-real set
DigA (m,0) is V11() V12() V13() ext-real set
(DigA (m,0)) + (DigA (k,(1 -' 1))) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA (m,0)) + (DigA (k,(1 -' 1)))) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (m,1)) + (DigA (k,1))),n)) + (SD_Add_Carry ((DigA (m,0)) + (DigA (k,(1 -' 1))))) is V11() V12() V13() ext-real set
DigA (k,0) is V11() V12() V13() ext-real set
(DigA (m,0)) + (DigA (k,0)) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA (m,0)) + (DigA (k,0))) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (m,1)) + (DigA (k,1))),n)) + (SD_Add_Carry ((DigA (m,0)) + (DigA (k,0)))) is V11() V12() V13() ext-real set
(DigA (m,0)) + 0 is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA (m,0)) + 0) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (m,1)) + (DigA (k,1))),n)) + (SD_Add_Carry ((DigA (m,0)) + 0)) is V11() V12() V13() ext-real set
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
SD_Add_Carry (0 + 0) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (m,1)) + (DigA (k,1))),n)) + (SD_Add_Carry (0 + 0)) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (m,1)) + (DigA (k,1))),n)) + 0 is V11() V12() V13() ext-real set
i '+' a is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like FinSequence of n -SD
SDDec (i '+' a) is V11() V12() V13() ext-real set
DigA ((i '+' a),1) is V11() V12() V13() ext-real set
Add (i,a,1,n) is Element of n -SD
DigA (i,1) is V11() V12() V13() ext-real set
DigA (a,1) is V11() V12() V13() ext-real set
(DigA (i,1)) + (DigA (a,1)) is V11() V12() V13() ext-real set
SD_Add_Data (((DigA (i,1)) + (DigA (a,1))),n) is V11() V12() V13() ext-real set
DigA (i,(1 -' 1)) is V11() V12() V13() ext-real set
DigA (a,(1 -' 1)) is V11() V12() V13() ext-real set
(DigA (i,(1 -' 1))) + (DigA (a,(1 -' 1))) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA (i,(1 -' 1))) + (DigA (a,(1 -' 1)))) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (i,1)) + (DigA (a,1))),n)) + (SD_Add_Carry ((DigA (i,(1 -' 1))) + (DigA (a,(1 -' 1))))) is V11() V12() V13() ext-real set
DigA (i,0) is V11() V12() V13() ext-real set
(DigA (i,0)) + (DigA (a,(1 -' 1))) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA (i,0)) + (DigA (a,(1 -' 1)))) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (i,1)) + (DigA (a,1))),n)) + (SD_Add_Carry ((DigA (i,0)) + (DigA (a,(1 -' 1))))) is V11() V12() V13() ext-real set
DigA (a,0) is V11() V12() V13() ext-real set
(DigA (i,0)) + (DigA (a,0)) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA (i,0)) + (DigA (a,0))) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (i,1)) + (DigA (a,1))),n)) + (SD_Add_Carry ((DigA (i,0)) + (DigA (a,0)))) is V11() V12() V13() ext-real set
(DigA (i,0)) + 0 is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA (i,0)) + 0) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (i,1)) + (DigA (a,1))),n)) + (SD_Add_Carry ((DigA (i,0)) + 0)) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (i,1)) + (DigA (a,1))),n)) + (SD_Add_Carry (0 + 0)) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (i,1)) + (DigA (a,1))),n)) + 0 is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA (m,1)) + (DigA (k,1))) is V11() V12() V13() ext-real set
Radix n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix n) |^ 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(SD_Add_Carry ((DigA (m,1)) + (DigA (k,1)))) * ((Radix n) |^ 1) is V11() V12() V13() ext-real set
(SDDec (m '+' k)) + ((SD_Add_Carry ((DigA (m,1)) + (DigA (k,1)))) * ((Radix n) |^ 1)) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA (m,1)) + (DigA (k,1))) is V11() V12() V13() ext-real set
Radix n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix n) |^ 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(SD_Add_Carry ((DigA (m,1)) + (DigA (k,1)))) * ((Radix n) |^ 1) is V11() V12() V13() ext-real set
(SDDec (m '+' k)) + ((SD_Add_Carry ((DigA (m,1)) + (DigA (k,1)))) * ((Radix n) |^ 1)) is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m -SD is V1() Element of K6(INT)
Seg n is Element of K6(NAT)
k is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
a is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
i is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
b is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
SDDec a is V11() V12() V13() ext-real set
SDDec b is V11() V12() V13() ext-real set
(SDDec a) + (SDDec b) is V11() V12() V13() ext-real set
SDDec k is V11() V12() V13() ext-real set
SDDec i is V11() V12() V13() ext-real set
(SDDec k) + (SDDec i) is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m -SD is V1() Element of K6(INT)
Seg n is Element of K6(NAT)
DecSD (0,n,m) is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
SDDec (DecSD (0,n,m)) is V11() V12() V13() ext-real set
k is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
a is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
i is V15() V18( NAT ) V19(m -SD ) Function-like V35(n) FinSequence-like FinSequence of m -SD
SDDec a is V11() V12() V13() ext-real set
(SDDec a) + (SDDec (DecSD (0,n,m))) is V11() V12() V13() ext-real set
SDDec k is V11() V12() V13() ext-real set
SDDec i is V11() V12() V13() ext-real set
(SDDec k) + (SDDec i) is V11() V12() V13() ext-real set
b is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DigA (k,b) is V11() V12() V13() ext-real set
DigA (a,b) is V11() V12() V13() ext-real set
DigA (i,b) is V11() V12() V13() ext-real set
DigA ((DecSD (0,n,m)),b) is V11() V12() V13() ext-real set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
- (Radix k) is V11() V12() V13() ext-real non positive set
(- (Radix k)) + 1 is V11() V12() V13() ext-real set
k -SD is V1() Element of K6(INT)
(Radix k) + (Radix k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
1 + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
(Radix k) - 1 is V11() V12() V13() ext-real set
1 - (Radix k) is V11() V12() V13() ext-real set
{ b1 where b1 is V11() V12() V13() ext-real Element of INT : ( b1 <= (Radix k) - 1 & (- (Radix k)) + 1 <= b1 ) } is set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k -SD is V1() Element of K6(INT)
Seg n is Element of K6(NAT)
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
i is V15() V18( NAT ) V19(k -SD ) Function-like FinSequence-like FinSequence of k -SD
len i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom i is Element of K6(NAT)
n -tuples_on (k -SD) is V1() functional FinSequence-membered FinSequenceSet of k -SD
a is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
b is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DigA (a,b) is V11() V12() V13() ext-real set
(b,m,k) is Element of k -SD
a . b is set
i is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
a is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
len i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom i is Element of K6(NAT)
b is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
i . b is set
DigA (i,b) is V11() V12() V13() ext-real set
(b,m,k) is Element of k -SD
DigA (a,b) is V11() V12() V13() ext-real set
a . b is set
len a is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix k) - 1 is V11() V12() V13() ext-real set
k -SD is V1() Element of K6(INT)
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k -SD is V1() Element of K6(INT)
Seg n is Element of K6(NAT)
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
i is V15() V18( NAT ) V19(k -SD ) Function-like FinSequence-like FinSequence of k -SD
len i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom i is Element of K6(NAT)
n -tuples_on (k -SD) is V1() functional FinSequence-membered FinSequenceSet of k -SD
a is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
b is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DigA (a,b) is V11() V12() V13() ext-real set
(b,m,k) is Element of k -SD
a . b is set
i is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
a is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
len i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom i is Element of K6(NAT)
b is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
i . b is set
DigA (i,b) is V11() V12() V13() ext-real set
(b,m,k) is Element of k -SD
DigA (a,b) is V11() V12() V13() ext-real set
a . b is set
len a is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k -SD is V1() Element of K6(INT)
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
- (Radix k) is V11() V12() V13() ext-real non positive set
(- 2) + 1 is V11() V12() V13() ext-real set
(- (Radix k)) + 1 is V11() V12() V13() ext-real set
(Radix k) - 1 is V11() V12() V13() ext-real set
{ b1 where b1 is V11() V12() V13() ext-real Element of INT : ( b1 <= (Radix k) - 1 & (- (Radix k)) + 1 <= b1 ) } is set
(Radix k) + (- 1) is V11() V12() V13() ext-real set
2 + (- 1) is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k -SD is V1() Element of K6(INT)
Seg n is Element of K6(NAT)
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
i is V15() V18( NAT ) V19(k -SD ) Function-like FinSequence-like FinSequence of k -SD
len i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom i is Element of K6(NAT)
n -tuples_on (k -SD) is V1() functional FinSequence-membered FinSequenceSet of k -SD
a is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
b is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DigA (a,b) is V11() V12() V13() ext-real set
(b,m,k) is Element of k -SD
a . b is set
i is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
a is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
len i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom i is Element of K6(NAT)
b is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
i . b is set
DigA (i,b) is V11() V12() V13() ext-real set
(b,m,k) is Element of k -SD
DigA (a,b) is V11() V12() V13() ext-real set
a . b is set
len a is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix k) - 1 is V11() V12() V13() ext-real set
k -SD is V1() Element of K6(INT)
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k -SD is V1() Element of K6(INT)
Seg n is Element of K6(NAT)
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
i is V15() V18( NAT ) V19(k -SD ) Function-like FinSequence-like FinSequence of k -SD
len i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom i is Element of K6(NAT)
n -tuples_on (k -SD) is V1() functional FinSequence-membered FinSequenceSet of k -SD
a is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
b is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DigA (a,b) is V11() V12() V13() ext-real set
(b,m,k) is Element of k -SD
a . b is set
i is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
a is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
len i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
dom i is Element of K6(NAT)
b is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
i . b is set
DigA (i,b) is V11() V12() V13() ext-real set
(b,m,k) is Element of k -SD
DigA (a,b) is V11() V12() V13() ext-real set
a . b is set
len a is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg n is Element of K6(NAT)
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(n,m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
k -SD is V1() Element of K6(INT)
(n,m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DigA ((n,m,k),i) is V11() V12() V13() ext-real set
DigA ((n,m,k),i) is V11() V12() V13() ext-real set
(DigA ((n,m,k),i)) + (DigA ((n,m,k),i)) is V11() V12() V13() ext-real set
(i,m,k) is Element of k -SD
(i,m,k) is Element of k -SD
a is V11() V12() V13() ext-real Element of INT
b is V11() V12() V13() ext-real Element of INT
a + b is V11() V12() V13() ext-real set
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
- (Radix k) is V11() V12() V13() ext-real non positive set
(- (Radix k)) + 1 is V11() V12() V13() ext-real set
((- (Radix k)) + 1) + b is V11() V12() V13() ext-real set
(Radix k) - 1 is V11() V12() V13() ext-real set
((- (Radix k)) + 1) + ((Radix k) - 1) is V11() V12() V13() ext-real set
a is V11() V12() V13() ext-real Element of INT
b is V11() V12() V13() ext-real Element of INT
a + b is V11() V12() V13() ext-real set
0 + b is V11() V12() V13() ext-real set
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg n is Element of K6(NAT)
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(n,m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
k -SD is V1() Element of K6(INT)
SDDec (n,m,k) is V11() V12() V13() ext-real set
(n,m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
SDDec (n,m,k) is V11() V12() V13() ext-real set
(SDDec (n,m,k)) + (SDDec (n,m,k)) is V11() V12() V13() ext-real set
DecSD (0,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
SDDec (DecSD (0,n,k)) is V11() V12() V13() ext-real set
(n,m,k) '+' (n,m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DigA ((DecSD (0,n,k)),i) is V11() V12() V13() ext-real set
DigA (((n,m,k) '+' (n,m,k)),i) is V11() V12() V13() ext-real set
Add ((n,m,k),(n,m,k),i,k) is Element of k -SD
DigA ((n,m,k),i) is V11() V12() V13() ext-real set
DigA ((n,m,k),i) is V11() V12() V13() ext-real set
(DigA ((n,m,k),i)) + (DigA ((n,m,k),i)) is V11() V12() V13() ext-real set
SD_Add_Data (((DigA ((n,m,k),i)) + (DigA ((n,m,k),i))),k) is V11() V12() V13() ext-real set
i -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigA ((n,m,k),(i -' 1)) is V11() V12() V13() ext-real set
DigA ((n,m,k),(i -' 1)) is V11() V12() V13() ext-real set
(DigA ((n,m,k),(i -' 1))) + (DigA ((n,m,k),(i -' 1))) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA ((n,m,k),(i -' 1))) + (DigA ((n,m,k),(i -' 1)))) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA ((n,m,k),i)) + (DigA ((n,m,k),i))),k)) + (SD_Add_Carry ((DigA ((n,m,k),(i -' 1))) + (DigA ((n,m,k),(i -' 1))))) is V11() V12() V13() ext-real set
SD_Add_Data (0,k) is V11() V12() V13() ext-real set
(SD_Add_Data (0,k)) + (SD_Add_Carry ((DigA ((n,m,k),(i -' 1))) + (DigA ((n,m,k),(i -' 1))))) is V11() V12() V13() ext-real set
0 + (SD_Add_Carry ((DigA ((n,m,k),(i -' 1))) + (DigA ((n,m,k),(i -' 1))))) is V11() V12() V13() ext-real set
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
SD_Add_Carry (0 + 0) is V11() V12() V13() ext-real set
SDDec ((n,m,k) '+' (n,m,k)) is V11() V12() V13() ext-real set
DigA ((n,m,k),n) is V11() V12() V13() ext-real set
DigA ((n,m,k),n) is V11() V12() V13() ext-real set
(DigA ((n,m,k),n)) + (DigA ((n,m,k),n)) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA ((n,m,k),n)) + (DigA ((n,m,k),n))) is V11() V12() V13() ext-real set
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix k) |^ n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(SD_Add_Carry ((DigA ((n,m,k),n)) + (DigA ((n,m,k),n)))) * ((Radix k) |^ n) is V11() V12() V13() ext-real set
(SDDec ((n,m,k) '+' (n,m,k))) + ((SD_Add_Carry ((DigA ((n,m,k),n)) + (DigA ((n,m,k),n)))) * ((Radix k) |^ n)) is V11() V12() V13() ext-real set
(SD_Add_Carry 0) * ((Radix k) |^ n) is V11() V12() V13() ext-real set
(SDDec ((n,m,k) '+' (n,m,k))) + ((SD_Add_Carry 0) * ((Radix k) |^ n)) is V11() V12() V13() ext-real set
0 * ((Radix k) |^ n) is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
(SDDec ((n,m,k) '+' (n,m,k))) + (0 * ((Radix k) |^ n)) is V11() V12() V13() ext-real set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg n is Element of K6(NAT)
Seg 1 is Element of K6(NAT)
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(n,m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
k -SD is V1() Element of K6(INT)
SDDec (n,m,k) is V11() V12() V13() ext-real set
(n,m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
SDDec (n,m,k) is V11() V12() V13() ext-real set
DecSD (1,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
SDDec (DecSD (1,n,k)) is V11() V12() V13() ext-real set
(SDDec (n,m,k)) + (SDDec (DecSD (1,n,k))) is V11() V12() V13() ext-real set
(1,m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(1) FinSequence-like FinSequence of k -SD
SDDec (1,m,k) is V11() V12() V13() ext-real set
DigA ((1,m,k),1) is V11() V12() V13() ext-real set
(1,m,k) is Element of k -SD
(1,m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(1) FinSequence-like FinSequence of k -SD
DigA ((1,m,k),1) is V11() V12() V13() ext-real set
(1,m,k) is Element of k -SD
DecSD (1,1,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(1) FinSequence-like FinSequence of k -SD
(1,m,k) '+' (DecSD (1,1,k)) is V15() V18( NAT ) V19(k -SD ) Function-like V35(1) FinSequence-like FinSequence of k -SD
SDDec ((1,m,k) '+' (DecSD (1,1,k))) is V11() V12() V13() ext-real set
DigA (((1,m,k) '+' (DecSD (1,1,k))),1) is V11() V12() V13() ext-real set
Add ((1,m,k),(DecSD (1,1,k)),1,k) is Element of k -SD
DigA ((DecSD (1,1,k)),1) is V11() V12() V13() ext-real set
(DigA ((1,m,k),1)) + (DigA ((DecSD (1,1,k)),1)) is V11() V12() V13() ext-real set
SD_Add_Data (((DigA ((1,m,k),1)) + (DigA ((DecSD (1,1,k)),1))),k) is V11() V12() V13() ext-real set
1 -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigA ((1,m,k),(1 -' 1)) is V11() V12() V13() ext-real set
DigA ((DecSD (1,1,k)),(1 -' 1)) is V11() V12() V13() ext-real set
(DigA ((1,m,k),(1 -' 1))) + (DigA ((DecSD (1,1,k)),(1 -' 1))) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA ((1,m,k),(1 -' 1))) + (DigA ((DecSD (1,1,k)),(1 -' 1)))) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA ((1,m,k),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((1,m,k),(1 -' 1))) + (DigA ((DecSD (1,1,k)),(1 -' 1))))) is V11() V12() V13() ext-real set
DigA ((1,m,k),0) is V11() V12() V13() ext-real set
(DigA ((1,m,k),0)) + (DigA ((DecSD (1,1,k)),(1 -' 1))) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA ((1,m,k),0)) + (DigA ((DecSD (1,1,k)),(1 -' 1)))) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA ((1,m,k),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((1,m,k),0)) + (DigA ((DecSD (1,1,k)),(1 -' 1))))) is V11() V12() V13() ext-real set
DigA ((DecSD (1,1,k)),0) is V11() V12() V13() ext-real set
(DigA ((1,m,k),0)) + (DigA ((DecSD (1,1,k)),0)) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA ((1,m,k),0)) + (DigA ((DecSD (1,1,k)),0))) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA ((1,m,k),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((1,m,k),0)) + (DigA ((DecSD (1,1,k)),0)))) is V11() V12() V13() ext-real set
(DigA ((1,m,k),0)) + 0 is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA ((1,m,k),0)) + 0) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA ((1,m,k),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((1,m,k),0)) + 0)) is V11() V12() V13() ext-real set
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
SD_Add_Carry (0 + 0) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA ((1,m,k),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry (0 + 0)) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA ((1,m,k),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + 0 is V11() V12() V13() ext-real set
(DigA ((1,m,k),1)) + 1 is V11() V12() V13() ext-real set
SD_Add_Data (((DigA ((1,m,k),1)) + 1),k) is V11() V12() V13() ext-real set
SD_Add_Carry 1 is V11() V12() V13() ext-real set
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(SD_Add_Carry 1) * (Radix k) is V11() V12() V13() ext-real set
1 - ((SD_Add_Carry 1) * (Radix k)) is V11() V12() V13() ext-real set
0 * (Radix k) is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
1 - (0 * (Radix k)) is V1() V11() V12() V13() ext-real positive non negative set
SDDec (1,m,k) is V11() V12() V13() ext-real set
SDDec (DecSD (1,1,k)) is V11() V12() V13() ext-real set
(SDDec (1,m,k)) + (SDDec (DecSD (1,1,k))) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA ((1,m,k),1)) + (DigA ((DecSD (1,1,k)),1))) is V11() V12() V13() ext-real set
(Radix k) |^ 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(SD_Add_Carry ((DigA ((1,m,k),1)) + (DigA ((DecSD (1,1,k)),1)))) * ((Radix k) |^ 1) is V11() V12() V13() ext-real set
(SDDec ((1,m,k) '+' (DecSD (1,1,k)))) + ((SD_Add_Carry ((DigA ((1,m,k),1)) + (DigA ((DecSD (1,1,k)),1)))) * ((Radix k) |^ 1)) is V11() V12() V13() ext-real set
0 + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
SD_Add_Carry (0 + 1) is V11() V12() V13() ext-real set
(SD_Add_Carry (0 + 1)) * ((Radix k) |^ 1) is V11() V12() V13() ext-real set
1 + ((SD_Add_Carry (0 + 1)) * ((Radix k) |^ 1)) is V11() V12() V13() ext-real set
0 * ((Radix k) |^ 1) is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
1 + (0 * ((Radix k) |^ 1)) is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
DigA ((n,m,k),n) is V11() V12() V13() ext-real set
(n,m,k) is Element of k -SD
(n,m,k) '+' (DecSD (1,n,k)) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DigA ((n,m,k),i) is V11() V12() V13() ext-real set
DigA (((n,m,k) '+' (DecSD (1,n,k))),i) is V11() V12() V13() ext-real set
Add ((n,m,k),(DecSD (1,n,k)),i,k) is Element of k -SD
DigA ((n,m,k),i) is V11() V12() V13() ext-real set
DigA ((DecSD (1,n,k)),i) is V11() V12() V13() ext-real set
(DigA ((n,m,k),i)) + (DigA ((DecSD (1,n,k)),i)) is V11() V12() V13() ext-real set
SD_Add_Data (((DigA ((n,m,k),i)) + (DigA ((DecSD (1,n,k)),i))),k) is V11() V12() V13() ext-real set
i -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigA ((n,m,k),(i -' 1)) is V11() V12() V13() ext-real set
DigA ((DecSD (1,n,k)),(i -' 1)) is V11() V12() V13() ext-real set
(DigA ((n,m,k),(i -' 1))) + (DigA ((DecSD (1,n,k)),(i -' 1))) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA ((n,m,k),(i -' 1))) + (DigA ((DecSD (1,n,k)),(i -' 1)))) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA ((n,m,k),i)) + (DigA ((DecSD (1,n,k)),i))),k)) + (SD_Add_Carry ((DigA ((n,m,k),(i -' 1))) + (DigA ((DecSD (1,n,k)),(i -' 1))))) is V11() V12() V13() ext-real set
(i,m,k) is Element of k -SD
(i,m,k) is Element of k -SD
m + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
DigA ((n,m,k),m) is V11() V12() V13() ext-real set
(m,m,k) is Element of k -SD
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
SD_Add_Data ((0 + 0),k) is V11() V12() V13() ext-real set
(SD_Add_Data ((0 + 0),k)) + 0 is V11() V12() V13() ext-real set
i - 1 is V11() V12() V13() ext-real set
(m + 1) - 1 is V11() V12() V13() ext-real set
((i -' 1),m,k) is Element of k -SD
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
SD_Add_Data ((0 + 0),k) is V11() V12() V13() ext-real set
(SD_Add_Data ((0 + 0),k)) + 0 is V11() V12() V13() ext-real set
m + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
m -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(m,m,k) is Element of k -SD
((m -' 1),m,k) is Element of k -SD
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix k) - 1 is V11() V12() V13() ext-real set
1 + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 - 1 is V11() V12() V13() ext-real set
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
SD_Add_Data ((0 + 0),k) is V11() V12() V13() ext-real set
((Radix k) - 1) + 1 is V11() V12() V13() ext-real set
SD_Add_Carry (((Radix k) - 1) + 1) is V11() V12() V13() ext-real set
(SD_Add_Data ((0 + 0),k)) + (SD_Add_Carry (((Radix k) - 1) + 1)) is V11() V12() V13() ext-real set
0 + (SD_Add_Carry (((Radix k) - 1) + 1)) is V11() V12() V13() ext-real set
i - 1 is V11() V12() V13() ext-real set
2 - 1 is V11() V12() V13() ext-real set
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
SD_Add_Data ((0 + 0),k) is V11() V12() V13() ext-real set
((Radix k) - 1) + 0 is V11() V12() V13() ext-real set
SD_Add_Carry (((Radix k) - 1) + 0) is V11() V12() V13() ext-real set
(SD_Add_Data ((0 + 0),k)) + (SD_Add_Carry (((Radix k) - 1) + 0)) is V11() V12() V13() ext-real set
SD_Add_Carry ((Radix k) - 1) is V11() V12() V13() ext-real set
0 + (SD_Add_Carry ((Radix k) - 1)) is V11() V12() V13() ext-real set
1 + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
2 - 1 is V11() V12() V13() ext-real set
((i -' 1),m,k) is Element of k -SD
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix k) - 1 is V11() V12() V13() ext-real set
SD_Add_Data (((Radix k) - 1),k) is V11() V12() V13() ext-real set
(Radix k) + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
((Radix k) + 1) - 1 is V11() V12() V13() ext-real set
SD_Add_Carry (((Radix k) + 1) - 1) is V11() V12() V13() ext-real set
(SD_Add_Data (((Radix k) - 1),k)) + (SD_Add_Carry (((Radix k) + 1) - 1)) is V11() V12() V13() ext-real set
(SD_Add_Data (((Radix k) - 1),k)) + 1 is V11() V12() V13() ext-real set
SD_Add_Carry ((Radix k) - 1) is V11() V12() V13() ext-real set
(SD_Add_Carry ((Radix k) - 1)) * (Radix k) is V11() V12() V13() ext-real set
((Radix k) - 1) - ((SD_Add_Carry ((Radix k) - 1)) * (Radix k)) is V11() V12() V13() ext-real set
(((Radix k) - 1) - ((SD_Add_Carry ((Radix k) - 1)) * (Radix k))) + 1 is V11() V12() V13() ext-real set
1 * (Radix k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((Radix k) - 1) - (1 * (Radix k)) is V11() V12() V13() ext-real set
(((Radix k) - 1) - (1 * (Radix k))) + 1 is V11() V12() V13() ext-real set
i - 1 is V11() V12() V13() ext-real set
2 - 1 is V11() V12() V13() ext-real set
((i -' 1),m,k) is Element of k -SD
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix k) - 1 is V11() V12() V13() ext-real set
((Radix k) - 1) + 0 is V11() V12() V13() ext-real set
SD_Add_Data ((((Radix k) - 1) + 0),k) is V11() V12() V13() ext-real set
SD_Add_Carry (((Radix k) - 1) + 0) is V11() V12() V13() ext-real set
(SD_Add_Data ((((Radix k) - 1) + 0),k)) + (SD_Add_Carry (((Radix k) - 1) + 0)) is V11() V12() V13() ext-real set
SD_Add_Data (((Radix k) - 1),k) is V11() V12() V13() ext-real set
(SD_Add_Data (((Radix k) - 1),k)) + 1 is V11() V12() V13() ext-real set
SD_Add_Carry ((Radix k) - 1) is V11() V12() V13() ext-real set
(SD_Add_Carry ((Radix k) - 1)) * (Radix k) is V11() V12() V13() ext-real set
((Radix k) - 1) - ((SD_Add_Carry ((Radix k) - 1)) * (Radix k)) is V11() V12() V13() ext-real set
(((Radix k) - 1) - ((SD_Add_Carry ((Radix k) - 1)) * (Radix k))) + 1 is V11() V12() V13() ext-real set
1 * (Radix k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
((Radix k) - 1) - (1 * (Radix k)) is V11() V12() V13() ext-real set
(((Radix k) - 1) - (1 * (Radix k))) + 1 is V11() V12() V13() ext-real set
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix k) - 1 is V11() V12() V13() ext-real set
((Radix k) - 1) + 1 is V11() V12() V13() ext-real set
SD_Add_Data ((((Radix k) - 1) + 1),k) is V11() V12() V13() ext-real set
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
SD_Add_Carry (0 + 0) is V11() V12() V13() ext-real set
(SD_Add_Data ((((Radix k) - 1) + 1),k)) + (SD_Add_Carry (0 + 0)) is V11() V12() V13() ext-real set
SD_Add_Carry (Radix k) is V11() V12() V13() ext-real set
(SD_Add_Carry (Radix k)) * (Radix k) is V11() V12() V13() ext-real set
(Radix k) - ((SD_Add_Carry (Radix k)) * (Radix k)) is V11() V12() V13() ext-real set
1 * (Radix k) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(Radix k) - (1 * (Radix k)) is V11() V12() V13() ext-real set
1 + 0 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
SD_Add_Data ((1 + 0),k) is V11() V12() V13() ext-real set
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
SD_Add_Carry (0 + 0) is V11() V12() V13() ext-real set
(SD_Add_Data ((1 + 0),k)) + (SD_Add_Carry (0 + 0)) is V11() V12() V13() ext-real set
SD_Add_Carry 1 is V11() V12() V13() ext-real set
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(SD_Add_Carry 1) * (Radix k) is V11() V12() V13() ext-real set
1 - ((SD_Add_Carry 1) * (Radix k)) is V11() V12() V13() ext-real set
0 * (Radix k) is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
1 - (0 * (Radix k)) is V1() V11() V12() V13() ext-real positive non negative set
m + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
SDDec ((n,m,k) '+' (DecSD (1,n,k))) is V11() V12() V13() ext-real set
DigA ((DecSD (1,n,k)),n) is V11() V12() V13() ext-real set
(DigA ((n,m,k),n)) + (DigA ((DecSD (1,n,k)),n)) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA ((n,m,k),n)) + (DigA ((DecSD (1,n,k)),n))) is V11() V12() V13() ext-real set
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix k) |^ n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(SD_Add_Carry ((DigA ((n,m,k),n)) + (DigA ((DecSD (1,n,k)),n)))) * ((Radix k) |^ n) is V11() V12() V13() ext-real set
(SDDec ((n,m,k) '+' (DecSD (1,n,k)))) + ((SD_Add_Carry ((DigA ((n,m,k),n)) + (DigA ((DecSD (1,n,k)),n)))) * ((Radix k) |^ n)) is V11() V12() V13() ext-real set
0 * ((Radix k) |^ n) is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
(SDDec ((n,m,k) '+' (DecSD (1,n,k)))) + (0 * ((Radix k) |^ n)) is V11() V12() V13() ext-real set
m is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
Seg n is Element of K6(NAT)
k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
n + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
m + 1 is V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative set
((n + 1),(m + 1),k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + 1) FinSequence-like FinSequence of k -SD
k -SD is V1() Element of K6(INT)
SDDec ((n + 1),(m + 1),k) is V11() V12() V13() ext-real set
((n + 1),m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + 1) FinSequence-like FinSequence of k -SD
SDDec ((n + 1),m,k) is V11() V12() V13() ext-real set
((n + 1),m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + 1) FinSequence-like FinSequence of k -SD
SDDec ((n + 1),m,k) is V11() V12() V13() ext-real set
(SDDec ((n + 1),m,k)) + (SDDec ((n + 1),m,k)) is V11() V12() V13() ext-real set
Seg (n + 1) is Element of K6(NAT)
DigA (((n + 1),m,k),(n + 1)) is V11() V12() V13() ext-real set
((n + 1),m,k) is Element of k -SD
((n + 1),m,k) '+' ((n + 1),m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + 1) FinSequence-like FinSequence of k -SD
i is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
DigA (((n + 1),(m + 1),k),i) is V11() V12() V13() ext-real set
DigA ((((n + 1),m,k) '+' ((n + 1),m,k)),i) is V11() V12() V13() ext-real set
Add (((n + 1),m,k),((n + 1),m,k),i,k) is Element of k -SD
DigA (((n + 1),m,k),i) is V11() V12() V13() ext-real set
DigA (((n + 1),m,k),i) is V11() V12() V13() ext-real set
(DigA (((n + 1),m,k),i)) + (DigA (((n + 1),m,k),i)) is V11() V12() V13() ext-real set
SD_Add_Data (((DigA (((n + 1),m,k),i)) + (DigA (((n + 1),m,k),i))),k) is V11() V12() V13() ext-real set
i -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
DigA (((n + 1),m,k),(i -' 1)) is V11() V12() V13() ext-real set
DigA (((n + 1),m,k),(i -' 1)) is V11() V12() V13() ext-real set
(DigA (((n + 1),m,k),(i -' 1))) + (DigA (((n + 1),m,k),(i -' 1))) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA (((n + 1),m,k),(i -' 1))) + (DigA (((n + 1),m,k),(i -' 1)))) is V11() V12() V13() ext-real set
(SD_Add_Data (((DigA (((n + 1),m,k),i)) + (DigA (((n + 1),m,k),i))),k)) + (SD_Add_Carry ((DigA (((n + 1),m,k),(i -' 1))) + (DigA (((n + 1),m,k),(i -' 1))))) is V11() V12() V13() ext-real set
(i,(m + 1),k) is Element of k -SD
(i,m,k) is Element of k -SD
(i,m,k) is Element of k -SD
((m + 1),(m + 1),k) is Element of k -SD
DigA (((n + 1),m,k),m) is V11() V12() V13() ext-real set
(m,m,k) is Element of k -SD
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix k) - 1 is V11() V12() V13() ext-real set
((m + 1),m,k) is Element of k -SD
DigA (((n + 1),m,k),m) is V11() V12() V13() ext-real set
(m,m,k) is Element of k -SD
((m + 1),m,k) is Element of k -SD
1 + ((Radix k) - 1) is V11() V12() V13() ext-real set
SD_Add_Carry (1 + ((Radix k) - 1)) is V11() V12() V13() ext-real set
0 + (SD_Add_Carry (1 + ((Radix k) - 1))) is V11() V12() V13() ext-real set
i - 1 is V11() V12() V13() ext-real set
(m + 1) - 1 is V11() V12() V13() ext-real set
((i -' 1),m,k) is Element of k -SD
((i -' 1),m,k) is Element of k -SD
m -' 1 is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
((m -' 1),m,k) is Element of k -SD
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix k) - 1 is V11() V12() V13() ext-real set
(m,(m + 1),k) is Element of k -SD
((m -' 1),m,k) is Element of k -SD
1 + ((Radix k) - 1) is V11() V12() V13() ext-real set
SD_Add_Data ((1 + ((Radix k) - 1)),k) is V11() V12() V13() ext-real set
(SD_Add_Data ((1 + ((Radix k) - 1)),k)) + 0 is V11() V12() V13() ext-real set
((i -' 1),m,k) is Element of k -SD
((i -' 1),m,k) is Element of k -SD
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
SD_Add_Data ((0 + 0),k) is V11() V12() V13() ext-real set
SD_Add_Carry (0 + 0) is V11() V12() V13() ext-real set
(SD_Add_Data ((0 + 0),k)) + (SD_Add_Carry (0 + 0)) is V11() V12() V13() ext-real set
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
SD_Add_Data ((0 + 0),k) is V11() V12() V13() ext-real set
SD_Add_Carry (0 + 0) is V11() V12() V13() ext-real set
(SD_Add_Data ((0 + 0),k)) + (SD_Add_Carry (0 + 0)) is V11() V12() V13() ext-real set
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix k) - 1 is V11() V12() V13() ext-real set
1 + ((Radix k) - 1) is V11() V12() V13() ext-real set
SD_Add_Data ((1 + ((Radix k) - 1)),k) is V11() V12() V13() ext-real set
(SD_Add_Data ((1 + ((Radix k) - 1)),k)) + 0 is V11() V12() V13() ext-real set
DigA (((n + 1),m,k),(n + 1)) is V11() V12() V13() ext-real set
((n + 1),m,k) is Element of k -SD
SDDec (((n + 1),m,k) '+' ((n + 1),m,k)) is V11() V12() V13() ext-real set
(DigA (((n + 1),m,k),(n + 1))) + (DigA (((n + 1),m,k),(n + 1))) is V11() V12() V13() ext-real set
SD_Add_Carry ((DigA (((n + 1),m,k),(n + 1))) + (DigA (((n + 1),m,k),(n + 1)))) is V11() V12() V13() ext-real set
Radix k is V4() V5() V6() V10() V11() V12() V13() ext-real non negative Element of NAT
(Radix k) |^ (n + 1) is V4() V5() V6() V10() V11() V12() V13() ext-real non negative set
(SD_Add_Carry ((DigA (((n + 1),m,k),(n + 1))) + (DigA (((n + 1),m,k),(n + 1))))) * ((Radix k) |^ (n + 1)) is V11() V12() V13() ext-real set
(SDDec (((n + 1),m,k) '+' ((n + 1),m,k))) + ((SD_Add_Carry ((DigA (((n + 1),m,k),(n + 1))) + (DigA (((n + 1),m,k),(n + 1))))) * ((Radix k) |^ (n + 1))) is V11() V12() V13() ext-real set
0 * ((Radix k) |^ (n + 1)) is V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative set
(SDDec (((n + 1),m,k) '+' ((n + 1),m,k))) + (0 * ((Radix k) |^ (n + 1))) is V11() V12() V13() ext-real set