REAL is V1() V28() V82() V83() V84() V88() set
NAT is V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V1() V28() V82() V88() set
NAT is V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() set
K6(NAT) is set
K6(NAT) is set
RAT is V1() V28() V82() V83() V84() V85() V88() set
INT is V1() V28() V82() V83() V84() V85() V86() V88() set
K7(COMPLEX,COMPLEX) is V72() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V72() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is V72() V73() V74() set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is V72() V73() V74() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V19( RAT ) V72() V73() V74() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V19( RAT ) V72() V73() V74() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V19( RAT ) V19( INT ) V72() V73() V74() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V19( RAT ) V19( INT ) V72() V73() V74() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V19( RAT ) V19( INT ) V72() V73() V74() V75() set
K7(K7(NAT,NAT),NAT) is V19( RAT ) V19( INT ) V72() V73() V74() V75() set
K6(K7(K7(NAT,NAT),NAT)) is set
K297() is set
1 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() integer functional FinSequence-membered ext-real non positive non negative V82() V83() V84() V85() V86() V87() V88() set
{0,1} is V1() V82() V83() V84() V85() V86() V87() set
K492() is set
K6(K492()) is set
K493() is Element of K6(K492())
K549() is V105() V133() L8()
the U1 of K549() is set
K6(INT) is set
0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() integer functional FinSequence-membered V43() ext-real non positive non negative V82() V83() V84() V85() V86() V87() V88() Element of NAT
2 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
3 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
Seg 1 is V1() V28() V35(1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
{1} is V1() V82() V83() V84() V85() V86() V87() set
Seg 2 is V1() V28() V35(2) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
{1,2} is V1() V82() V83() V84() V85() V86() V87() set
SD_Add_Carry 0 is V11() V12() integer ext-real set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m mod 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
1 * m is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(1 * m) + 0 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
m is V11() V12() integer ext-real set
k is V11() V12() integer ext-real set
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m mod f is V11() V12() integer ext-real set
k mod f is V11() V12() integer ext-real set
(m mod f) + (k mod f) is V11() V12() integer ext-real set
((m mod f) + (k mod f)) mod f is V11() V12() integer ext-real set
m + (k mod f) is V11() V12() integer ext-real set
(m + (k mod f)) mod f is V11() V12() integer ext-real set
m div f is V11() V12() integer ext-real set
(m div f) * f is V11() V12() integer ext-real set
(m mod f) + ((m div f) * f) is V11() V12() integer ext-real set
m - ((m div f) * f) is V11() V12() integer ext-real set
(m - ((m div f) * f)) + ((m div f) * f) is V11() V12() integer ext-real set
m + 0 is V11() V12() integer ext-real Element of REAL
(m + (k mod f)) - ((m mod f) + (k mod f)) is V11() V12() integer ext-real set
m is V11() V12() integer ext-real set
k is V11() V12() integer ext-real set
m * k is V11() V12() integer ext-real set
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(m * k) mod f is V11() V12() integer ext-real set
k mod f is V11() V12() integer ext-real set
m * (k mod f) is V11() V12() integer ext-real set
(m * (k mod f)) mod f is V11() V12() integer ext-real set
k div f is V11() V12() integer ext-real set
(k div f) * f is V11() V12() integer ext-real set
(k mod f) + ((k div f) * f) is V11() V12() integer ext-real set
k - ((k div f) * f) is V11() V12() integer ext-real set
(k - ((k div f) * f)) + ((k div f) * f) is V11() V12() integer ext-real set
k + 0 is V11() V12() integer ext-real Element of REAL
(m * k) - (m * (k mod f)) is V11() V12() integer ext-real set
m * (k div f) is V11() V12() integer ext-real set
(m * (k div f)) * f is V11() V12() integer ext-real set
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k |^ f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m mod (k |^ f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
f -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (f -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(m mod (k |^ f)) div (k |^ (f -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
m div (k |^ (f -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m div (k |^ (f -' 1))) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f -' 1) + 1 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ ((f -' 1) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m mod (k |^ ((f -' 1) + 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
m div (k |^ ((f -' 1) + 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(k |^ ((f -' 1) + 1)) * (m div (k |^ ((f -' 1) + 1))) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
m - ((k |^ ((f -' 1) + 1)) * (m div (k |^ ((f -' 1) + 1)))) is V11() V12() integer ext-real Element of REAL
- (m div (k |^ ((f -' 1) + 1))) is V11() V12() integer ext-real non positive set
k * (- (m div (k |^ ((f -' 1) + 1)))) is V11() V12() integer ext-real non positive set
f - 1 is V11() V12() integer ext-real Element of REAL
(f - 1) + 1 is V11() V12() integer ext-real Element of REAL
(k |^ ((f -' 1) + 1)) * (- (m div (k |^ ((f -' 1) + 1)))) is V11() V12() integer ext-real non positive set
m + ((k |^ ((f -' 1) + 1)) * (- (m div (k |^ ((f -' 1) + 1))))) is V11() V12() integer ext-real set
(m + ((k |^ ((f -' 1) + 1)) * (- (m div (k |^ ((f -' 1) + 1)))))) div (k |^ (f -' 1)) is V11() V12() integer ext-real set
(k |^ (f -' 1)) * k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
((k |^ (f -' 1)) * k) * (- (m div (k |^ ((f -' 1) + 1)))) is V11() V12() integer ext-real non positive set
m + (((k |^ (f -' 1)) * k) * (- (m div (k |^ ((f -' 1) + 1))))) is V11() V12() integer ext-real set
(m + (((k |^ (f -' 1)) * k) * (- (m div (k |^ ((f -' 1) + 1)))))) div (k |^ (f -' 1)) is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
(k |^ (f -' 1)) * n is V11() V12() integer ext-real set
m + ((k |^ (f -' 1)) * n) is V11() V12() integer ext-real set
(m + ((k |^ (f -' 1)) * n)) / (k |^ (f -' 1)) is V11() V12() ext-real set
[\((m + ((k |^ (f -' 1)) * n)) / (k |^ (f -' 1)))/] is V11() V12() integer ext-real set
m / (k |^ (f -' 1)) is V11() V12() ext-real non negative set
(m / (k |^ (f -' 1))) + n is V11() V12() ext-real set
[\((m / (k |^ (f -' 1))) + n)/] is V11() V12() integer ext-real set
[\(m / (k |^ (f -' 1)))/] is V11() V12() integer ext-real set
[\(m / (k |^ (f -' 1)))/] + n is V11() V12() integer ext-real set
k * (m div (k |^ ((f -' 1) + 1))) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
- (k * (m div (k |^ ((f -' 1) + 1)))) is V11() V12() integer ext-real non positive Element of REAL
(m div (k |^ (f -' 1))) + (- (k * (m div (k |^ ((f -' 1) + 1))))) is V11() V12() integer ext-real Element of REAL
(m div (k |^ (f -' 1))) - (k * (m div (k |^ ((f -' 1) + 1)))) is V11() V12() integer ext-real Element of REAL
m div ((k |^ (f -' 1)) * k) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k * (m div ((k |^ (f -' 1)) * k)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m div (k |^ (f -' 1))) - (k * (m div ((k |^ (f -' 1)) * k))) is V11() V12() integer ext-real Element of REAL
(m div (k |^ (f -' 1))) div k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k * ((m div (k |^ (f -' 1))) div k) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m div (k |^ (f -' 1))) - (k * ((m div (k |^ (f -' 1))) div k)) is V11() V12() integer ext-real Element of REAL
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Seg k is V28() V35(k) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
m + 1 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
k + 1 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
Seg (k + 1) is V1() V28() V35(k + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
1 + 1 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Radix m is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
2 to_power m is V11() V12() ext-real set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
1 - 1 is V11() V12() integer ext-real Element of REAL
1 -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
SDDec k is V11() V12() integer ext-real set
DigA (k,1) is V11() V12() integer ext-real set
DigitSD k is V15() V18( NAT ) V19( INT ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
(DigitSD k) /. 1 is V11() V12() integer V43() ext-real Element of INT
SubDigit (k,1,m) is V11() V12() integer V43() ext-real Element of INT
len (DigitSD k) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom (DigitSD k) is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
(DigitSD k) . 1 is V11() V12() integer ext-real Element of REAL
Sum (DigitSD k) is V11() V12() integer V43() ext-real Element of INT
<*(SubDigit (k,1,m))*> is V1() V15() V18( NAT ) V19( INT ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
Sum <*(SubDigit (k,1,m))*> is V11() V12() integer V43() ext-real Element of INT
Radix m is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix m) |^ 0 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
DigB (k,1) is V11() V12() integer V43() ext-real Element of INT
((Radix m) |^ 0) * (DigB (k,1)) is V11() V12() integer ext-real Element of REAL
1 * (DigB (k,1)) is V11() V12() integer ext-real Element of REAL
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Radix m is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k is V11() V12() integer ext-real set
SD_Add_Data (k,m) is V11() V12() integer ext-real set
SD_Add_Carry k is V11() V12() integer ext-real set
(SD_Add_Carry k) * (Radix m) is V11() V12() integer ext-real set
(SD_Add_Data (k,m)) + ((SD_Add_Carry k) * (Radix m)) is V11() V12() integer ext-real set
k - ((SD_Add_Carry k) * (Radix m)) is V11() V12() integer ext-real set
(k - ((SD_Add_Carry k) * (Radix m))) + ((SD_Add_Carry k) * (Radix m)) is V11() V12() integer ext-real set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k + 1 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
Seg k is V28() V35(k) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
f is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
DigitSD f is V15() V18( NAT ) V19( INT ) Function-like V28() V35(k + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
Sum (DigitSD f) is V11() V12() integer V43() ext-real Element of INT
SubDigit (f,(k + 1),m) is V11() V12() integer V43() ext-real Element of INT
<*(SubDigit (f,(k + 1),m))*> is V1() V15() V18( NAT ) V19( INT ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
ie is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
DigitSD ie is V15() V18( NAT ) V19( INT ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
(DigitSD ie) ^ <*(SubDigit (f,(k + 1),m))*> is V1() V15() V18( NAT ) V19( INT ) Function-like V28() V35(k + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
Sum ((DigitSD ie) ^ <*(SubDigit (f,(k + 1),m))*>) is V11() V12() integer V43() ext-real Element of INT
len (DigitSD f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
DigA (f,e) is V11() V12() integer ext-real set
DigA (ie,e) is V11() V12() integer ext-real set
Seg (k + 1) is V1() V28() V35(k + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
f . e is V11() V12() ext-real Element of REAL
ie . e is V11() V12() ext-real Element of REAL
len (DigitSD ie) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(DigitSD f) . e is V11() V12() integer ext-real Element of REAL
((DigitSD ie) ^ <*(SubDigit (f,(k + 1),m))*>) . e is V11() V12() integer ext-real Element of REAL
Seg (k + 1) is V1() V28() V35(k + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
dom (DigitSD f) is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
dom (DigitSD ie) is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
(DigitSD ie) . e is V11() V12() integer ext-real Element of REAL
(DigitSD ie) /. e is V11() V12() integer V43() ext-real Element of INT
SubDigit (ie,e,m) is V11() V12() integer V43() ext-real Element of INT
Radix m is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix m) |^ (e -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
DigB (ie,e) is V11() V12() integer V43() ext-real Element of INT
((Radix m) |^ (e -' 1)) * (DigB (ie,e)) is V11() V12() integer ext-real Element of REAL
DigA (ie,e) is V11() V12() integer ext-real set
((Radix m) |^ (e -' 1)) * (DigA (ie,e)) is V11() V12() integer ext-real Element of REAL
DigA (f,e) is V11() V12() integer ext-real set
((Radix m) |^ (e -' 1)) * (DigA (f,e)) is V11() V12() integer ext-real Element of REAL
DigB (f,e) is V11() V12() integer V43() ext-real Element of INT
((Radix m) |^ (e -' 1)) * (DigB (f,e)) is V11() V12() integer ext-real Element of REAL
SubDigit (f,e,m) is V11() V12() integer V43() ext-real Element of INT
(DigitSD f) /. e is V11() V12() integer V43() ext-real Element of INT
dom (DigitSD f) is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
(len (DigitSD ie)) + 1 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
((DigitSD ie) ^ <*(SubDigit (f,(k + 1),m))*>) . ((len (DigitSD ie)) + 1) is V11() V12() integer ext-real Element of REAL
(DigitSD f) /. (k + 1) is V11() V12() integer V43() ext-real Element of INT
(DigitSD f) . (k + 1) is V11() V12() integer ext-real Element of REAL
len <*(SubDigit (f,(k + 1),m))*> is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
len ((DigitSD ie) ^ <*(SubDigit (f,(k + 1),m))*>) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(len (DigitSD ie)) + (len <*(SubDigit (f,(k + 1),m))*>) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
Radix m is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k + 1 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
Seg k is V28() V35(k) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
(Radix m) |^ k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
f is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
DigA (f,(k + 1)) is V11() V12() integer ext-real set
((Radix m) |^ k) * (DigA (f,(k + 1))) is V11() V12() integer ext-real set
SDDec f is V11() V12() integer ext-real set
ie is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
SDDec ie is V11() V12() integer ext-real set
(SDDec ie) + (((Radix m) |^ k) * (DigA (f,(k + 1)))) is V11() V12() integer ext-real set
DigitSD f is V15() V18( NAT ) V19( INT ) Function-like V28() V35(k + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
Sum (DigitSD f) is V11() V12() integer V43() ext-real Element of INT
DigitSD ie is V15() V18( NAT ) V19( INT ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
SubDigit (f,(k + 1),m) is V11() V12() integer V43() ext-real Element of INT
<*(SubDigit (f,(k + 1),m))*> is V1() V15() V18( NAT ) V19( INT ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
(DigitSD ie) ^ <*(SubDigit (f,(k + 1),m))*> is V1() V15() V18( NAT ) V19( INT ) Function-like V28() V35(k + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
Sum ((DigitSD ie) ^ <*(SubDigit (f,(k + 1),m))*>) is V11() V12() integer V43() ext-real Element of INT
Sum (DigitSD ie) is V11() V12() integer V43() ext-real Element of INT
(Sum (DigitSD ie)) + (SubDigit (f,(k + 1),m)) is V11() V12() integer ext-real set
(k + 1) -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix m) |^ ((k + 1) -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
DigB (f,(k + 1)) is V11() V12() integer V43() ext-real Element of INT
((Radix m) |^ ((k + 1) -' 1)) * (DigB (f,(k + 1))) is V11() V12() integer ext-real Element of REAL
(Sum (DigitSD ie)) + (((Radix m) |^ ((k + 1) -' 1)) * (DigB (f,(k + 1)))) is V11() V12() integer ext-real Element of REAL
((Radix m) |^ k) * (DigB (f,(k + 1))) is V11() V12() integer ext-real set
(Sum (DigitSD ie)) + (((Radix m) |^ k) * (DigB (f,(k + 1)))) is V11() V12() integer ext-real set
(Sum (DigitSD ie)) + (((Radix m) |^ k) * (DigA (f,(k + 1)))) is V11() V12() integer ext-real set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
Radix m is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(Radix m) |^ k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k + 1 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix m) |^ (k + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Seg k is V28() V35(k) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
f is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
ie is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
f '+' ie is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
SDDec (f '+' ie) is V11() V12() integer ext-real set
DigA (f,(k + 1)) is V11() V12() integer ext-real set
DigA (ie,(k + 1)) is V11() V12() integer ext-real set
(DigA (f,(k + 1))) + (DigA (ie,(k + 1))) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))) is V11() V12() integer ext-real set
(SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * ((Radix m) |^ (k + 1)) is V11() V12() integer ext-real set
(SDDec (f '+' ie)) + ((SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * ((Radix m) |^ (k + 1))) is V11() V12() integer ext-real set
SDDec f is V11() V12() integer ext-real set
SDDec ie is V11() V12() integer ext-real set
(SDDec f) + (SDDec ie) is V11() V12() integer ext-real set
e is V15() V18( NAT ) V19( INT ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
len e is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom e is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
rng e is V82() V83() V84() V85() V86() Element of K6(REAL)
e is set
n is set
e . n is V11() V12() integer ext-real Element of REAL
en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
Seg (k + 1) is V1() V28() V35(k + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
DigA (f,en) is V11() V12() integer ext-real set
DigB (f,en) is V11() V12() integer V43() ext-real Element of INT
e is V15() V18( NAT ) V19(m -SD ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e . n is V11() V12() ext-real Element of REAL
f . n is V11() V12() ext-real Element of REAL
Seg (k + 1) is V1() V28() V35(k + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
DigB (f,n) is V11() V12() integer V43() ext-real Element of INT
DigA (f,n) is V11() V12() integer ext-real set
en is V15() V18( NAT ) V19( INT ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
len en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom en is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
rng en is V82() V83() V84() V85() V86() Element of K6(REAL)
en is set
ien is set
en . ien is V11() V12() integer ext-real Element of REAL
i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
Seg (k + 1) is V1() V28() V35(k + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
DigA (ie,i) is V11() V12() integer ext-real set
DigB (ie,i) is V11() V12() integer V43() ext-real Element of INT
en is V15() V18( NAT ) V19(m -SD ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
ien is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
en . ien is V11() V12() ext-real Element of REAL
ie . ien is V11() V12() ext-real Element of REAL
Seg (k + 1) is V1() V28() V35(k + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
DigB (ie,ien) is V11() V12() integer V43() ext-real Element of INT
DigA (ie,ien) is V11() V12() integer ext-real set
ien is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
i is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA (ie,i) is V11() V12() integer ext-real set
DigA (ien,i) is V11() V12() integer ext-real set
Seg (k + 1) is V1() V28() V35(k + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
ie . i is V11() V12() ext-real Element of REAL
ien . i is V11() V12() ext-real Element of REAL
Seg (k + 1) is V1() V28() V35(k + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
n is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
DigA (f,i) is V11() V12() integer ext-real set
DigA (n,i) is V11() V12() integer ext-real set
f . i is V11() V12() ext-real Element of REAL
n . i is V11() V12() ext-real Element of REAL
n '+' ien is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
i is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(f '+' ie) . i is V11() V12() ext-real Element of REAL
(n '+' ien) . i is V11() V12() ext-real Element of REAL
i - 1 is V11() V12() integer ext-real Element of REAL
1 - 1 is V11() V12() integer ext-real Element of REAL
i -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(k + 1) - 1 is V11() V12() integer ext-real Element of REAL
DigA ((f '+' ie),i) is V11() V12() integer ext-real set
Add (f,ie,i,m) is V11() V12() integer V43() ext-real Element of m -SD
DigA (f,i) is V11() V12() integer ext-real set
DigA (ie,i) is V11() V12() integer ext-real set
(DigA (f,i)) + (DigA (ie,i)) is V11() V12() integer ext-real set
SD_Add_Data (((DigA (f,i)) + (DigA (ie,i))),m) is V11() V12() integer ext-real set
DigA (f,(i -' 1)) is V11() V12() integer ext-real set
DigA (ie,(i -' 1)) is V11() V12() integer ext-real set
(DigA (f,(i -' 1))) + (DigA (ie,(i -' 1))) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (f,(i -' 1))) + (DigA (ie,(i -' 1)))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (f,i)) + (DigA (ie,i))),m)) + (SD_Add_Carry ((DigA (f,(i -' 1))) + (DigA (ie,(i -' 1))))) is V11() V12() integer ext-real set
DigA (n,i) is V11() V12() integer ext-real set
(DigA (n,i)) + (DigA (ie,i)) is V11() V12() integer ext-real set
SD_Add_Data (((DigA (n,i)) + (DigA (ie,i))),m) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (n,i)) + (DigA (ie,i))),m)) + (SD_Add_Carry ((DigA (f,(i -' 1))) + (DigA (ie,(i -' 1))))) is V11() V12() integer ext-real set
DigA (n,(i -' 1)) is V11() V12() integer ext-real set
(DigA (n,(i -' 1))) + (DigA (ie,(i -' 1))) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (n,(i -' 1))) + (DigA (ie,(i -' 1)))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (n,i)) + (DigA (ie,i))),m)) + (SD_Add_Carry ((DigA (n,(i -' 1))) + (DigA (ie,(i -' 1))))) is V11() V12() integer ext-real set
DigA (ien,i) is V11() V12() integer ext-real set
(DigA (n,i)) + (DigA (ien,i)) is V11() V12() integer ext-real set
SD_Add_Data (((DigA (n,i)) + (DigA (ien,i))),m) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (n,i)) + (DigA (ien,i))),m)) + (SD_Add_Carry ((DigA (n,(i -' 1))) + (DigA (ie,(i -' 1))))) is V11() V12() integer ext-real set
DigA (ien,(i -' 1)) is V11() V12() integer ext-real set
(DigA (n,(i -' 1))) + (DigA (ien,(i -' 1))) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (n,(i -' 1))) + (DigA (ien,(i -' 1)))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (n,i)) + (DigA (ien,i))),m)) + (SD_Add_Carry ((DigA (n,(i -' 1))) + (DigA (ien,(i -' 1))))) is V11() V12() integer ext-real set
Add (n,ien,i,m) is V11() V12() integer V43() ext-real Element of m -SD
DigA ((n '+' ien),i) is V11() V12() integer ext-real set
DigA ((f '+' ie),i) is V11() V12() integer ext-real set
Add (f,ie,i,m) is V11() V12() integer V43() ext-real Element of m -SD
DigA (f,i) is V11() V12() integer ext-real set
DigA (ie,i) is V11() V12() integer ext-real set
(DigA (f,i)) + (DigA (ie,i)) is V11() V12() integer ext-real set
SD_Add_Data (((DigA (f,i)) + (DigA (ie,i))),m) is V11() V12() integer ext-real set
1 -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
DigA (f,(1 -' 1)) is V11() V12() integer ext-real set
DigA (ie,(1 -' 1)) is V11() V12() integer ext-real set
(DigA (f,(1 -' 1))) + (DigA (ie,(1 -' 1))) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (f,(1 -' 1))) + (DigA (ie,(1 -' 1)))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (f,i)) + (DigA (ie,i))),m)) + (SD_Add_Carry ((DigA (f,(1 -' 1))) + (DigA (ie,(1 -' 1))))) is V11() V12() integer ext-real set
DigA (f,0) is V11() V12() integer ext-real set
(DigA (f,0)) + (DigA (ie,(1 -' 1))) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (f,0)) + (DigA (ie,(1 -' 1)))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (f,i)) + (DigA (ie,i))),m)) + (SD_Add_Carry ((DigA (f,0)) + (DigA (ie,(1 -' 1))))) is V11() V12() integer ext-real set
DigA (ie,0) is V11() V12() integer ext-real set
(DigA (f,0)) + (DigA (ie,0)) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (f,0)) + (DigA (ie,0))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (f,i)) + (DigA (ie,i))),m)) + (SD_Add_Carry ((DigA (f,0)) + (DigA (ie,0)))) is V11() V12() integer ext-real set
0 + (DigA (ie,0)) is V11() V12() integer ext-real Element of REAL
SD_Add_Carry (0 + (DigA (ie,0))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (f,i)) + (DigA (ie,i))),m)) + (SD_Add_Carry (0 + (DigA (ie,0)))) is V11() V12() integer ext-real set
0 + 0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() integer functional FinSequence-membered V43() ext-real non positive non negative V82() V83() V84() V85() V86() V87() V88() Element of NAT
SD_Add_Carry (0 + 0) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (f,i)) + (DigA (ie,i))),m)) + (SD_Add_Carry (0 + 0)) is V11() V12() integer ext-real set
DigA (n,0) is V11() V12() integer ext-real set
(DigA (n,0)) + 0 is V11() V12() integer ext-real Element of REAL
SD_Add_Carry ((DigA (n,0)) + 0) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (f,i)) + (DigA (ie,i))),m)) + (SD_Add_Carry ((DigA (n,0)) + 0)) is V11() V12() integer ext-real set
DigA (ien,0) is V11() V12() integer ext-real set
(DigA (n,0)) + (DigA (ien,0)) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (n,0)) + (DigA (ien,0))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (f,i)) + (DigA (ie,i))),m)) + (SD_Add_Carry ((DigA (n,0)) + (DigA (ien,0)))) is V11() V12() integer ext-real set
DigA (n,i) is V11() V12() integer ext-real set
(DigA (n,i)) + (DigA (ie,i)) is V11() V12() integer ext-real set
SD_Add_Data (((DigA (n,i)) + (DigA (ie,i))),m) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (n,i)) + (DigA (ie,i))),m)) + (SD_Add_Carry ((DigA (n,0)) + (DigA (ien,0)))) is V11() V12() integer ext-real set
DigA (ien,i) is V11() V12() integer ext-real set
(DigA (n,i)) + (DigA (ien,i)) is V11() V12() integer ext-real set
SD_Add_Data (((DigA (n,i)) + (DigA (ien,i))),m) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (n,i)) + (DigA (ien,i))),m)) + (SD_Add_Carry ((DigA (n,0)) + (DigA (ien,0)))) is V11() V12() integer ext-real set
DigA (n,(1 -' 1)) is V11() V12() integer ext-real set
(DigA (n,(1 -' 1))) + (DigA (ien,0)) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (n,(1 -' 1))) + (DigA (ien,0))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (n,i)) + (DigA (ien,i))),m)) + (SD_Add_Carry ((DigA (n,(1 -' 1))) + (DigA (ien,0)))) is V11() V12() integer ext-real set
i -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
DigA (n,(i -' 1)) is V11() V12() integer ext-real set
DigA (ien,(i -' 1)) is V11() V12() integer ext-real set
(DigA (n,(i -' 1))) + (DigA (ien,(i -' 1))) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (n,(i -' 1))) + (DigA (ien,(i -' 1)))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (n,i)) + (DigA (ien,i))),m)) + (SD_Add_Carry ((DigA (n,(i -' 1))) + (DigA (ien,(i -' 1))))) is V11() V12() integer ext-real set
Add (n,ien,i,m) is V11() V12() integer V43() ext-real Element of m -SD
DigA ((n '+' ien),i) is V11() V12() integer ext-real set
DigitSD (f '+' ie) is V15() V18( NAT ) V19( INT ) Function-like V28() V35(k + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
Sum (DigitSD (f '+' ie)) is V11() V12() integer V43() ext-real Element of INT
DigitSD (n '+' ien) is V15() V18( NAT ) V19( INT ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
SubDigit ((f '+' ie),(k + 1),m) is V11() V12() integer V43() ext-real Element of INT
<*(SubDigit ((f '+' ie),(k + 1),m))*> is V1() V15() V18( NAT ) V19( INT ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
(DigitSD (n '+' ien)) ^ <*(SubDigit ((f '+' ie),(k + 1),m))*> is V1() V15() V18( NAT ) V19( INT ) Function-like V28() V35(k + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
Sum ((DigitSD (n '+' ien)) ^ <*(SubDigit ((f '+' ie),(k + 1),m))*>) is V11() V12() integer V43() ext-real Element of INT
Sum (DigitSD (n '+' ien)) is V11() V12() integer V43() ext-real Element of INT
(Sum (DigitSD (n '+' ien))) + (SubDigit ((f '+' ie),(k + 1),m)) is V11() V12() integer ext-real set
(k + 1) -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix m) |^ ((k + 1) -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
DigB ((f '+' ie),(k + 1)) is V11() V12() integer V43() ext-real Element of INT
((Radix m) |^ ((k + 1) -' 1)) * (DigB ((f '+' ie),(k + 1))) is V11() V12() integer ext-real Element of REAL
(Sum (DigitSD (n '+' ien))) + (((Radix m) |^ ((k + 1) -' 1)) * (DigB ((f '+' ie),(k + 1)))) is V11() V12() integer ext-real Element of REAL
((Radix m) |^ k) * (DigB ((f '+' ie),(k + 1))) is V11() V12() integer ext-real set
(Sum (DigitSD (n '+' ien))) + (((Radix m) |^ k) * (DigB ((f '+' ie),(k + 1)))) is V11() V12() integer ext-real set
DigA ((f '+' ie),(k + 1)) is V11() V12() integer ext-real set
((Radix m) |^ k) * (DigA ((f '+' ie),(k + 1))) is V11() V12() integer ext-real set
(Sum (DigitSD (n '+' ien))) + (((Radix m) |^ k) * (DigA ((f '+' ie),(k + 1)))) is V11() V12() integer ext-real set
Add (f,ie,(k + 1),m) is V11() V12() integer V43() ext-real Element of m -SD
((Radix m) |^ k) * (Add (f,ie,(k + 1),m)) is V11() V12() integer ext-real set
(Sum (DigitSD (n '+' ien))) + (((Radix m) |^ k) * (Add (f,ie,(k + 1),m))) is V11() V12() integer ext-real set
SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m) is V11() V12() integer ext-real set
DigA (f,((k + 1) -' 1)) is V11() V12() integer ext-real set
DigA (ie,((k + 1) -' 1)) is V11() V12() integer ext-real set
(DigA (f,((k + 1) -' 1))) + (DigA (ie,((k + 1) -' 1))) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (f,((k + 1) -' 1))) + (DigA (ie,((k + 1) -' 1)))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) + (SD_Add_Carry ((DigA (f,((k + 1) -' 1))) + (DigA (ie,((k + 1) -' 1))))) is V11() V12() integer ext-real set
((Radix m) |^ k) * ((SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) + (SD_Add_Carry ((DigA (f,((k + 1) -' 1))) + (DigA (ie,((k + 1) -' 1)))))) is V11() V12() integer ext-real set
(Sum (DigitSD (n '+' ien))) + (((Radix m) |^ k) * ((SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) + (SD_Add_Carry ((DigA (f,((k + 1) -' 1))) + (DigA (ie,((k + 1) -' 1))))))) is V11() V12() integer ext-real set
DigA (f,k) is V11() V12() integer ext-real set
(DigA (f,k)) + (DigA (ie,((k + 1) -' 1))) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (f,k)) + (DigA (ie,((k + 1) -' 1)))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) + (SD_Add_Carry ((DigA (f,k)) + (DigA (ie,((k + 1) -' 1))))) is V11() V12() integer ext-real set
((Radix m) |^ k) * ((SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) + (SD_Add_Carry ((DigA (f,k)) + (DigA (ie,((k + 1) -' 1)))))) is V11() V12() integer ext-real set
(Sum (DigitSD (n '+' ien))) + (((Radix m) |^ k) * ((SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) + (SD_Add_Carry ((DigA (f,k)) + (DigA (ie,((k + 1) -' 1))))))) is V11() V12() integer ext-real set
DigA (ie,k) is V11() V12() integer ext-real set
(DigA (f,k)) + (DigA (ie,k)) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (f,k)) + (DigA (ie,k))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) + (SD_Add_Carry ((DigA (f,k)) + (DigA (ie,k)))) is V11() V12() integer ext-real set
((Radix m) |^ k) * ((SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) + (SD_Add_Carry ((DigA (f,k)) + (DigA (ie,k))))) is V11() V12() integer ext-real set
(Sum (DigitSD (n '+' ien))) + (((Radix m) |^ k) * ((SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) + (SD_Add_Carry ((DigA (f,k)) + (DigA (ie,k)))))) is V11() V12() integer ext-real set
((Radix m) |^ k) * (SD_Add_Carry ((DigA (f,k)) + (DigA (ie,k)))) is V11() V12() integer ext-real set
(Sum (DigitSD (n '+' ien))) + (((Radix m) |^ k) * (SD_Add_Carry ((DigA (f,k)) + (DigA (ie,k))))) is V11() V12() integer ext-real set
((Radix m) |^ k) * (SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) is V11() V12() integer ext-real set
((Sum (DigitSD (n '+' ien))) + (((Radix m) |^ k) * (SD_Add_Carry ((DigA (f,k)) + (DigA (ie,k)))))) + (((Radix m) |^ k) * (SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m))) is V11() V12() integer ext-real set
SDDec (n '+' ien) is V11() V12() integer ext-real set
(SDDec (n '+' ien)) + (((Radix m) |^ k) * (SD_Add_Carry ((DigA (f,k)) + (DigA (ie,k))))) is V11() V12() integer ext-real set
((SDDec (n '+' ien)) + (((Radix m) |^ k) * (SD_Add_Carry ((DigA (f,k)) + (DigA (ie,k)))))) + (((Radix m) |^ k) * (SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m))) is V11() V12() integer ext-real set
DigA (n,k) is V11() V12() integer ext-real set
(DigA (n,k)) + (DigA (ie,k)) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (n,k)) + (DigA (ie,k))) is V11() V12() integer ext-real set
((Radix m) |^ k) * (SD_Add_Carry ((DigA (n,k)) + (DigA (ie,k)))) is V11() V12() integer ext-real set
(SDDec (n '+' ien)) + (((Radix m) |^ k) * (SD_Add_Carry ((DigA (n,k)) + (DigA (ie,k))))) is V11() V12() integer ext-real set
((SDDec (n '+' ien)) + (((Radix m) |^ k) * (SD_Add_Carry ((DigA (n,k)) + (DigA (ie,k)))))) + (((Radix m) |^ k) * (SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m))) is V11() V12() integer ext-real set
DigA (ien,k) is V11() V12() integer ext-real set
(DigA (n,k)) + (DigA (ien,k)) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (n,k)) + (DigA (ien,k))) is V11() V12() integer ext-real set
((Radix m) |^ k) * (SD_Add_Carry ((DigA (n,k)) + (DigA (ien,k)))) is V11() V12() integer ext-real set
(SDDec (n '+' ien)) + (((Radix m) |^ k) * (SD_Add_Carry ((DigA (n,k)) + (DigA (ien,k))))) is V11() V12() integer ext-real set
((SDDec (n '+' ien)) + (((Radix m) |^ k) * (SD_Add_Carry ((DigA (n,k)) + (DigA (ien,k)))))) + (((Radix m) |^ k) * (SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m))) is V11() V12() integer ext-real set
SDDec n is V11() V12() integer ext-real set
SDDec ien is V11() V12() integer ext-real set
(SDDec n) + (SDDec ien) is V11() V12() integer ext-real set
((SDDec n) + (SDDec ien)) + (((Radix m) |^ k) * (SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m))) is V11() V12() integer ext-real set
(Radix m) |^ (k + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * ((Radix m) |^ (k + 1)) is V11() V12() integer ext-real Element of REAL
(SDDec (f '+' ie)) + ((SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * ((Radix m) |^ (k + 1))) is V11() V12() integer ext-real Element of REAL
(((Radix m) |^ k) * (SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m))) + ((SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * ((Radix m) |^ (k + 1))) is V11() V12() integer ext-real Element of REAL
((SDDec n) + (SDDec ien)) + ((((Radix m) |^ k) * (SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m))) + ((SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * ((Radix m) |^ (k + 1)))) is V11() V12() integer ext-real Element of REAL
((Radix m) |^ k) * (Radix m) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * (((Radix m) |^ k) * (Radix m)) is V11() V12() integer ext-real Element of REAL
(((Radix m) |^ k) * (SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m))) + ((SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * (((Radix m) |^ k) * (Radix m))) is V11() V12() integer ext-real Element of REAL
((SDDec n) + (SDDec ien)) + ((((Radix m) |^ k) * (SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m))) + ((SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * (((Radix m) |^ k) * (Radix m)))) is V11() V12() integer ext-real Element of REAL
(SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * (Radix m) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) + ((SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * (Radix m)) is V11() V12() integer ext-real set
((Radix m) |^ k) * ((SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) + ((SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * (Radix m))) is V11() V12() integer ext-real set
((SDDec n) + (SDDec ien)) + (((Radix m) |^ k) * ((SD_Add_Data (((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))),m)) + ((SD_Add_Carry ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) * (Radix m)))) is V11() V12() integer ext-real set
((Radix m) |^ k) * ((DigA (f,(k + 1))) + (DigA (ie,(k + 1)))) is V11() V12() integer ext-real set
((SDDec n) + (SDDec ien)) + (((Radix m) |^ k) * ((DigA (f,(k + 1))) + (DigA (ie,(k + 1))))) is V11() V12() integer ext-real set
((Radix m) |^ k) * (DigA (f,(k + 1))) is V11() V12() integer ext-real set
(SDDec n) + (((Radix m) |^ k) * (DigA (f,(k + 1)))) is V11() V12() integer ext-real set
((Radix m) |^ k) * (DigA (ie,(k + 1))) is V11() V12() integer ext-real set
(SDDec ien) + (((Radix m) |^ k) * (DigA (ie,(k + 1)))) is V11() V12() integer ext-real set
((SDDec n) + (((Radix m) |^ k) * (DigA (f,(k + 1))))) + ((SDDec ien) + (((Radix m) |^ k) * (DigA (ie,(k + 1))))) is V11() V12() integer ext-real set
(SDDec f) + ((SDDec ien) + (((Radix m) |^ k) * (DigA (ie,(k + 1))))) is V11() V12() integer ext-real set
(Radix m) |^ 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
1 - 1 is V11() V12() integer ext-real Element of REAL
1 -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
f is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
k '+' f is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
SDDec (k '+' f) is V11() V12() integer ext-real set
DigA (k,1) is V11() V12() integer ext-real set
DigA (f,1) is V11() V12() integer ext-real set
(DigA (k,1)) + (DigA (f,1)) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (k,1)) + (DigA (f,1))) is V11() V12() integer ext-real set
(SD_Add_Carry ((DigA (k,1)) + (DigA (f,1)))) * ((Radix m) |^ 1) is V11() V12() integer ext-real set
(SDDec (k '+' f)) + ((SD_Add_Carry ((DigA (k,1)) + (DigA (f,1)))) * ((Radix m) |^ 1)) is V11() V12() integer ext-real set
SDDec k is V11() V12() integer ext-real set
SDDec f is V11() V12() integer ext-real set
(SDDec k) + (SDDec f) is V11() V12() integer ext-real set
SD_Add_Data (((DigA (k,1)) + (DigA (f,1))),m) is V11() V12() integer ext-real set
(SD_Add_Carry ((DigA (k,1)) + (DigA (f,1)))) * (Radix m) is V11() V12() integer ext-real set
((DigA (k,1)) + (DigA (f,1))) - ((SD_Add_Carry ((DigA (k,1)) + (DigA (f,1)))) * (Radix m)) is V11() V12() integer ext-real set
DigA ((k '+' f),1) is V11() V12() integer ext-real set
Add (k,f,1,m) is V11() V12() integer V43() ext-real Element of m -SD
DigA (k,0) is V11() V12() integer ext-real set
DigA (f,0) is V11() V12() integer ext-real set
(DigA (k,0)) + (DigA (f,0)) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (k,0)) + (DigA (f,0))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (k,1)) + (DigA (f,1))),m)) + (SD_Add_Carry ((DigA (k,0)) + (DigA (f,0)))) is V11() V12() integer ext-real set
0 + (DigA (f,0)) is V11() V12() integer ext-real Element of REAL
SD_Add_Carry (0 + (DigA (f,0))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (k,1)) + (DigA (f,1))),m)) + (SD_Add_Carry (0 + (DigA (f,0)))) is V11() V12() integer ext-real set
(SD_Add_Data (((DigA (k,1)) + (DigA (f,1))),m)) + 0 is V11() V12() integer ext-real Element of REAL
(Radix m) |^ 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(SD_Add_Carry ((DigA (k,1)) + (DigA (f,1)))) * ((Radix m) |^ 1) is V11() V12() integer ext-real Element of REAL
(SDDec (k '+' f)) + ((SD_Add_Carry ((DigA (k,1)) + (DigA (f,1)))) * ((Radix m) |^ 1)) is V11() V12() integer ext-real Element of REAL
(SD_Add_Data (((DigA (k,1)) + (DigA (f,1))),m)) + ((SD_Add_Carry ((DigA (k,1)) + (DigA (f,1)))) * (Radix m)) is V11() V12() integer ext-real set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
f is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
ie is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
f '+' ie is V15() V18( NAT ) V19(m -SD ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of m -SD
SDDec (f '+' ie) is V11() V12() integer ext-real set
DigA (f,k) is V11() V12() integer ext-real set
DigA (ie,k) is V11() V12() integer ext-real set
(DigA (f,k)) + (DigA (ie,k)) is V11() V12() integer ext-real set
SD_Add_Carry ((DigA (f,k)) + (DigA (ie,k))) is V11() V12() integer ext-real set
(Radix m) |^ k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(SD_Add_Carry ((DigA (f,k)) + (DigA (ie,k)))) * ((Radix m) |^ k) is V11() V12() integer ext-real set
(SDDec (f '+' ie)) + ((SD_Add_Carry ((DigA (f,k)) + (DigA (ie,k)))) * ((Radix m) |^ k)) is V11() V12() integer ext-real set
SDDec f is V11() V12() integer ext-real set
SDDec ie is V11() V12() integer ext-real set
(SDDec f) + (SDDec ie) is V11() V12() integer ext-real set
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Radix k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix k) |^ (m -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(f) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
ie . m is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix k) |^ (m -' 1)) * (ie . m) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Seg m is V28() V35(m) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
f is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
ie is V15() V18( NAT ) V19( NAT ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
len ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom ie is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
e is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e /. e is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(e,k,m,f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
Radix k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix k) |^ (e -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
f . e is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix k) |^ (e -' 1)) * (f . e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom e is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
e . e is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
e is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
len ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom ie is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
len e is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
dom e is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
ie . e is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie /. e is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(e,k,m,f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
Radix k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix k) |^ (e -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
f . e is V4()