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() 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
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 . e 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
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
(m,k,f) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
Sum (m,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 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
(Radix k) |^ m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
f mod ((Radix k) |^ m) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
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
(f mod ((Radix k) |^ m)) div ((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
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 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
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(k) 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,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 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) |^ e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
f mod ((Radix m) |^ e) 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
(f mod ((Radix m) |^ e)) div ((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
ie is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
e is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(k) 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 V4() V5() V6() V10() V11() V12() integer ext-real non negative set
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,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 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) |^ e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
f mod ((Radix m) |^ e) 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
(f mod ((Radix m) |^ e)) div ((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
e . e is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of 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
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
k -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
f is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(m,k,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(k -SD ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of k -SD
DigitSD ie is V15() V18( NAT ) V19( INT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
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
len (m,k,f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom (m,k,f) is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
Seg m is V28() V35(m) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
e 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
DigA (ie,e) is V11() V12() integer ext-real set
DigB (ie,e) is V11() V12() integer V43() ext-real Element of INT
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
dom (DigitSD ie) is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
(m,k,f) . e 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) /. 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
DigB (ie,e) is V11() V12() integer V43() ext-real Element of INT
((Radix k) |^ (e -' 1)) * (DigB (ie,e)) is V11() V12() integer ext-real Element of REAL
SubDigit (ie,e,k) is V11() V12() integer V43() ext-real Element of INT
(DigitSD ie) /. e is V11() V12() integer V43() ext-real Element of INT
(DigitSD ie) . e 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
k -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
f is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(m,k,f) 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) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
Sum (m,k,f) 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(k -SD ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of k -SD
SDDec ie is V11() V12() integer ext-real set
DigitSD ie is V15() V18( NAT ) V19( INT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
Sum (DigitSD ie) is V11() V12() integer V43() ext-real Element of INT
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
(f,k,m) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
DecSD (m,k,f) is V15() V18( NAT ) V19(f -SD ) Function-like V28() V35(k) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of f -SD
f -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
len (f,k,m) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom (f,k,m) is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
Seg k is V28() V35(k) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
ie is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(f,k,m) . ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(ie,f,m) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
Radix f is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) |^ ie is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m mod ((Radix f) |^ ie) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) |^ (ie -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m mod ((Radix f) |^ ie)) div ((Radix f) |^ (ie -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
DigitDC (m,ie,f) is V11() V12() integer V43() ext-real Element of f -SD
DigA ((DecSD (m,k,f)),ie) is V11() V12() integer ext-real set
(DecSD (m,k,f)) . ie is V11() V12() ext-real Element of REAL
len (DecSD (m,k,f)) 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
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(f,m,k) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(m,f,(f,m,k)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m,f,(f,m,k)) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
Sum (m,f,(f,m,k)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
DecSD (k,m,f) is V15() V18( NAT ) V19(f -SD ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of f -SD
f -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
SDDec (DecSD (k,m,f)) is V11() V12() integer ext-real set
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
ie is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
ie -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
m is V11() V12() integer ext-real set
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e is V15() V18( NAT ) V19(ie -SD ) Function-like V28() V35(e) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of ie -SD
DigA (e,f) is V11() V12() integer ext-real set
m * (DigA (e,f)) is V11() V12() integer ext-real set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(m * (DigA (e,f))) mod k is V11() V12() integer ext-real set
ie 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
k -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
m is V11() V12() integer ext-real set
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e is V15() V18( NAT ) V19(k -SD ) Function-like V28() V35(ie) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of k -SD
(m,f,ie,k,ie,e) is V11() V12() integer ext-real set
DigA (e,ie) is V11() V12() integer ext-real set
m * (DigA (e,ie)) is V11() V12() integer ext-real set
(m * (DigA (e,ie))) mod f is V11() V12() integer ext-real set
ie - 1 is V11() V12() integer ext-real Element of REAL
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 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie -' en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m,f,(ie -' en),k,ie,e) is V11() V12() integer ext-real set
DigA (e,(ie -' en)) is V11() V12() integer ext-real set
m * (DigA (e,(ie -' en))) is V11() V12() integer ext-real set
(m * (DigA (e,(ie -' en)))) mod f is V11() V12() integer ext-real set
en is V11() V12() integer V43() ext-real Element of INT
ien is V11() V12() integer ext-real set
(Radix k) * ien is V11() V12() integer ext-real set
((Radix k) * ien) + (m,f,(ie -' en),k,ie,e) is V11() V12() integer ext-real set
(((Radix k) * ien) + (m,f,(ie -' en),k,ie,e)) mod f is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
nn is V11() V12() integer V43() ext-real Element of INT
n is V11() V12() integer V43() ext-real Element of INT
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
en . 1 is V11() V12() integer ext-real Element of REAL
en is V15() V18( NAT ) V19( INT ) Function-like V28() V35(ie) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
en . 1 is V11() V12() integer ext-real Element of REAL
ien is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
en . ien is V11() V12() integer ext-real Element of REAL
ien + 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
en . (ien + 1) is V11() V12() integer ext-real Element of REAL
ie -' ien is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m,f,(ie -' ien),k,ie,e) is V11() V12() integer ext-real set
DigA (e,(ie -' ien)) is V11() V12() integer ext-real set
m * (DigA (e,(ie -' ien))) is V11() V12() integer ext-real set
(m * (DigA (e,(ie -' ien)))) mod f is V11() V12() integer ext-real set
e is V15() V18( NAT ) V19( INT ) Function-like V28() V35(ie) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
e . 1 is V11() V12() integer ext-real Element of REAL
n is V15() V18( NAT ) V19( INT ) Function-like V28() V35(ie) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
n . 1 is V11() V12() integer ext-real Element of REAL
en is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e . en is V11() V12() integer ext-real Element of REAL
n . en is V11() V12() integer ext-real Element of REAL
en + 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
e . (en + 1) is V11() V12() integer ext-real Element of REAL
n . (en + 1) is V11() V12() integer ext-real Element of REAL
0 + 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
ie -' en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m,f,(ie -' en),k,ie,e) is V11() V12() integer ext-real set
DigA (e,(ie -' en)) is V11() V12() integer ext-real set
m * (DigA (e,(ie -' en))) is V11() V12() integer ext-real set
(m * (DigA (e,(ie -' en)))) mod f is V11() V12() integer ext-real set
en is V11() V12() integer ext-real set
ien is V11() V12() integer ext-real set
(Radix k) * en is V11() V12() integer ext-real set
((Radix k) * en) + (m,f,(ie -' en),k,ie,e) is V11() V12() integer ext-real set
(((Radix k) * en) + (m,f,(ie -' en),k,ie,e)) mod f is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
nn is V11() V12() integer ext-real set
(Radix k) * i is V11() V12() integer ext-real set
((Radix k) * i) + (m,f,(ie -' en),k,ie,e) is V11() V12() integer ext-real set
(((Radix k) * i) + (m,f,(ie -' en),k,ie,e)) mod f is V11() V12() integer ext-real set
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 . 0 is V11() V12() integer ext-real Element of REAL
n . 0 is V11() V12() integer ext-real Element of REAL
e . ie is V11() V12() integer ext-real Element of REAL
n . ie is V11() V12() integer ext-real Element of REAL
1 - 1 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
en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e . en is V11() V12() integer ext-real Element of REAL
en + 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
e . (en + 1) is V11() V12() integer ext-real Element of REAL
ie -' en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m,f,(ie -' en),k,ie,e) is V11() V12() integer ext-real set
DigA (e,(ie -' en)) is V11() V12() integer ext-real set
m * (DigA (e,(ie -' en))) is V11() V12() integer ext-real set
(m * (DigA (e,(ie -' en)))) mod f is V11() V12() integer ext-real set
n . en is V11() V12() integer ext-real Element of REAL
n . (en + 1) is V11() V12() integer ext-real Element of REAL
en is V11() V12() integer ext-real set
ien is V11() V12() integer ext-real set
(Radix k) * en is V11() V12() integer ext-real set
((Radix k) * en) + (m,f,(ie -' en),k,ie,e) is V11() V12() integer ext-real set
(((Radix k) * en) + (m,f,(ie -' en),k,ie,e)) mod f is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
nn is V11() V12() integer ext-real set
(Radix k) * i is V11() V12() integer ext-real set
((Radix k) * i) + (m,f,(ie -' en),k,ie,e) is V11() V12() integer ext-real set
(((Radix k) * i) + (m,f,(ie -' en),k,ie,e)) mod f is V11() V12() integer ext-real set
en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e . en is V11() V12() integer ext-real Element of REAL
n . en is V11() V12() integer ext-real Element of REAL
1 - 1 is V11() V12() integer ext-real Element of REAL
(len e) - 1 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
en + 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
len n 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 V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
k is V11() V12() integer ext-real set
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
ie is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
DecSD (f,(m + 1),e) is V15() V18( NAT ) V19(e -SD ) Function-like V28() V35(m + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of e -SD
k * f is V11() V12() integer ext-real set
(k * f) mod ie is V11() V12() integer ext-real set
e is V15() V18( NAT ) V19(e -SD ) Function-like V28() V35(m + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of e -SD
(k,e,ie,(m + 1),e) is V15() V18( NAT ) V19( INT ) Function-like V28() V35(m + 1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
(k,e,ie,(m + 1),e) . (m + 1) is V11() V12() integer ext-real Element of REAL
n is V15() V18( NAT ) V19( INT ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
len n is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom n is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
Seg m is V28() V35(m) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
rng n is V82() V83() V84() V85() V86() Element of K6(REAL)
en is set
en is set
n . en is V11() V12() integer ext-real Element of REAL
ien is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ien + 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 (m + 1) is V1() V28() V35(m + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
DigA (e,(ien + 1)) is V11() V12() integer ext-real set
DigB (e,(ien + 1)) is V11() V12() integer V43() ext-real Element of INT
en is V15() V18( NAT ) V19(e -SD ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of e -SD
(e,(m + 1),f) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m + 1) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
Radix e is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i is V15() V18( NAT ) V19( NAT ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
len i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom i is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
nn is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(m,e,nn) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m,e,nn) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
Sum (m,e,nn) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) |^ (m + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V15() V18( NAT ) V19(e -SD ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of e -SD
SDDec en is V11() V12() integer ext-real set
len en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
en . i is V11() V12() ext-real Element of REAL
nn . i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i + 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 (m + 1) is V1() V28() V35(m + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
DigB (e,(i + 1)) is V11() V12() integer V43() ext-real Element of INT
DigA (e,(i + 1)) is V11() V12() integer ext-real set
e . (i + 1) is V11() V12() ext-real Element of REAL
(e,(m + 1),f) . (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 + m 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 + m) is V1() V28() V35(1 + m) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
(Radix e) * (m,e,nn) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(e,(m + 1),f) . 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix e) * (m,e,nn)) + ((e,(m + 1),f) . 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(1,e,(m + 1),(e,(m + 1),f)) 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
(Radix e) |^ (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 e) |^ (1 -' 1)) * ((e,(m + 1),f) . 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
<*(1,e,(m + 1),(e,(m + 1),f))*> is V1() V15() V18( NAT ) V19( NAT ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
len <*(1,e,(m + 1),(e,(m + 1),f))*> 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 V11() V12() integer ext-real Element of REAL
rs2 is V15() V18( NAT ) V19( REAL ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of REAL
len rs2 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom rs2 is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
dom (m,e,nn) is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
len (m,e,nn) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
Seg (len (m,e,nn)) is V28() V35( len (m,e,nn)) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
m -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
rs is V15() V18( NAT ) V19( REAL ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of REAL
dom rs is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
(Radix e) * (m,e,nn) is V15() V18( NAT ) V19( REAL ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of REAL
len ((Radix e) * (m,e,nn)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i1 is V35(m) FinSequence-like Element of m -tuples_on REAL
i is V11() V12() ext-real Element of REAL
i * i1 is V15() V18( NAT ) V19( REAL ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() Element of m -tuples_on REAL
len (i * i1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
<*(1,e,(m + 1),(e,(m + 1),f))*> ^ ((Radix e) * (m,e,nn)) is V1() V15() V18( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set
len (<*(1,e,(m + 1),(e,(m + 1),f))*> ^ ((Radix e) * (m,e,nn))) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(len <*(1,e,(m + 1),(e,(m + 1),f))*>) + (len ((Radix e) * (m,e,nn))) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((m + 1),e,(e,(m + 1),f)) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m + 1) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
len ((m + 1),e,(e,(m + 1),f)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
((m + 1),e,(e,(m + 1),f)) . i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(<*(1,e,(m + 1),(e,(m + 1),f))*> ^ ((Radix e) * (m,e,nn))) . i is set
Seg (m + 1) is V1() V28() V35(m + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
dom ((m + 1),e,(e,(m + 1),f)) is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
((m + 1),e,(e,(m + 1),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 + 1),e,(e,(m + 1),f)) . 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i - 1 is V11() V12() integer ext-real Element of REAL
(m,e,nn) . (i - 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
rs . (i - 1) is V11() V12() ext-real Element of REAL
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
(1 + 1) - 1 is V11() V12() integer ext-real Element of REAL
(m + 1) - 1 is V11() V12() integer ext-real Element of REAL
i1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix e) * (m,e,nn)) . (i - 1) is V11() V12() ext-real Element of REAL
i * rs is V15() V18( NAT ) V19( REAL ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of REAL
(i * rs) . (i - 1) is V11() V12() ext-real Element of REAL
rs is V11() V12() ext-real Element of REAL
i * rs is V11() V12() ext-real Element of REAL
rs2 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) * rs2 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m,e,nn) /. i1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) * ((m,e,nn) /. i1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(i1,e,m,nn) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i1 -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) |^ (i1 -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
nn . i1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix e) |^ (i1 -' 1)) * (nn . i1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) * (i1,e,m,nn) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) * ((Radix e) |^ (i1 -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix e) * ((Radix e) |^ (i1 -' 1))) * (nn . i1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(i1 -' 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
(Radix e) |^ ((i1 -' 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 e) |^ ((i1 -' 1) + 1)) * (nn . i1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) |^ i1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix e) |^ i1) * (nn . i1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i1 + 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
(e,(m + 1),f) . (i1 + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix e) |^ i1) * ((e,(m + 1),f) . (i1 + 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(i,e,(m + 1),(e,(m + 1),f)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) |^ (i -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(e,(m + 1),f) . i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix e) |^ (i -' 1)) * ((e,(m + 1),f) . i) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((m + 1),e,(e,(m + 1),f)) /. i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((m + 1),e,(e,(m + 1),f)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
Sum ((m + 1),e,(e,(m + 1),f)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
Sum ((Radix e) * (m,e,nn)) is V11() V12() ext-real Element of REAL
(1,e,(m + 1),(e,(m + 1),f)) + (Sum ((Radix e) * (m,e,nn))) is V11() V12() ext-real Element of REAL
i * rs is V15() V18( NAT ) V19( REAL ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of REAL
Sum (i * rs) is V11() V12() ext-real Element of REAL
(1,e,(m + 1),(e,(m + 1),f)) + (Sum (i * rs)) is V11() V12() ext-real Element of REAL
Sum rs is V11() V12() ext-real Element of REAL
i * (Sum rs) is V11() V12() ext-real Element of REAL
(1,e,(m + 1),(e,(m + 1),f)) + (i * (Sum rs)) is V11() V12() ext-real Element of REAL
(1,e,(m + 1),(e,(m + 1),f)) + ((Radix e) * (m,e,nn)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) |^ 0 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix e) |^ 0) * ((e,(m + 1),f) . 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((Radix e) |^ 0) * ((e,(m + 1),f) . 1)) + ((Radix e) * (m,e,nn)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
1 * ((e,(m + 1),f) . 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(1 * ((e,(m + 1),f) . 1)) + ((Radix e) * (m,e,nn)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k * (Radix e) is V11() V12() integer ext-real set
(k * (Radix e)) * (m,e,nn) is V11() V12() integer ext-real Element of REAL
k * ((e,(m + 1),f) . 1) is V11() V12() integer ext-real Element of REAL
((k * (Radix e)) * (m,e,nn)) + (k * ((e,(m + 1),f) . 1)) is V11() V12() integer ext-real Element of REAL
(((k * (Radix e)) * (m,e,nn)) + (k * ((e,(m + 1),f) . 1))) mod ie is V11() V12() integer ext-real set
k * (m,e,nn) is V11() V12() integer ext-real Element of REAL
(Radix e) * (k * (m,e,nn)) is V11() V12() integer ext-real Element of REAL
((Radix e) * (k * (m,e,nn))) mod ie is V11() V12() integer ext-real set
(k * ((e,(m + 1),f) . 1)) mod ie is V11() V12() integer ext-real set
(((Radix e) * (k * (m,e,nn))) mod ie) + ((k * ((e,(m + 1),f) . 1)) mod ie) is V11() V12() integer ext-real set
((((Radix e) * (k * (m,e,nn))) mod ie) + ((k * ((e,(m + 1),f) . 1)) mod ie)) mod ie is V11() V12() integer ext-real set
(k * (m,e,nn)) mod ie is V11() V12() integer ext-real set
(Radix e) * ((k * (m,e,nn)) mod ie) is V11() V12() integer ext-real set
((Radix e) * ((k * (m,e,nn)) mod ie)) mod ie is V11() V12() integer ext-real set
(((Radix e) * ((k * (m,e,nn)) mod ie)) mod ie) + ((k * ((e,(m + 1),f) . 1)) mod ie) is V11() V12() integer ext-real set
((((Radix e) * ((k * (m,e,nn)) mod ie)) mod ie) + ((k * ((e,(m + 1),f) . 1)) mod ie)) mod ie is V11() V12() integer ext-real set
((Radix e) * ((k * (m,e,nn)) mod ie)) + ((k * ((e,(m + 1),f) . 1)) mod ie) is V11() V12() integer ext-real set
(((Radix e) * ((k * (m,e,nn)) mod ie)) + ((k * ((e,(m + 1),f) . 1)) mod ie)) mod ie is V11() V12() integer ext-real set
(e,m,(m,e,nn)) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(1,e,f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) |^ 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
f mod ((Radix e) |^ 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
(Radix e) |^ (1 -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f mod ((Radix e) |^ 1)) div ((Radix e) |^ (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 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 mod ((Radix 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 e) |^ 0 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f mod ((Radix e) |^ 1)) div ((Radix e) |^ 0) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f mod ((Radix e) |^ 1)) div 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
f mod (Radix e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m,e,nn) * (Radix e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((e,(m + 1),f) . 1) + ((m,e,nn) * (Radix e)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((e,(m + 1),f) . 1) + ((m,e,nn) * (Radix e))) div (Radix e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((e,(m + 1),f) . 1) + ((m,e,nn) * (Radix e))) / (Radix e) is V11() V12() ext-real non negative Element of REAL
[\((((e,(m + 1),f) . 1) + ((m,e,nn) * (Radix e))) / (Radix e))/] is V11() V12() integer ext-real set
((e,(m + 1),f) . 1) / (Radix e) is V11() V12() ext-real non negative Element of REAL
(((e,(m + 1),f) . 1) / (Radix e)) + (m,e,nn) is V11() V12() ext-real non negative Element of REAL
[\((((e,(m + 1),f) . 1) / (Radix e)) + (m,e,nn))/] is V11() V12() integer ext-real set
[\(((e,(m + 1),f) . 1) / (Radix e))/] is V11() V12() integer ext-real set
[\(((e,(m + 1),f) . 1) / (Radix e))/] + (m,e,nn) is V11() V12() integer ext-real Element of REAL
((e,(m + 1),f) . 1) div (Radix e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((e,(m + 1),f) . 1) div (Radix e)) + (m,e,nn) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
0 + (m,e,nn) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
en . i is V11() V12() ext-real Element of REAL
(e,m,(m,e,nn)) . i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
rs2 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
rs2 + 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 (m + 1) is V1() V28() V35(m + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
en . rs2 is V11() V12() ext-real Element of REAL
(e,(m + 1),f) . (rs2 + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((rs2 + 1),e,f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) |^ (rs2 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
f mod ((Radix e) |^ (rs2 + 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(rs2 + 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 e) |^ ((rs2 + 1) -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f mod ((Radix e) |^ (rs2 + 1))) div ((Radix e) |^ ((rs2 + 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,e,nn) * (Radix e)) + ((e,(m + 1),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,e,nn) * (Radix e)) + ((e,(m + 1),f) . 1)) div ((Radix e) |^ ((rs2 + 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,e,nn) * (Radix e)) + ((e,(m + 1),f) . 1)) div ((Radix e) |^ ((rs2 + 1) -' 1))) mod (Radix e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) |^ rs2 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((m,e,nn) * (Radix e)) + ((e,(m + 1),f) . 1)) div ((Radix e) |^ rs2) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((m,e,nn) * (Radix e)) + ((e,(m + 1),f) . 1)) div ((Radix e) |^ rs2)) mod (Radix e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
rs2 -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) |^ (rs2 -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) * ((Radix e) |^ (rs2 -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((m,e,nn) * (Radix e)) + ((e,(m + 1),f) . 1)) div ((Radix e) * ((Radix e) |^ (rs2 -' 1))) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((m,e,nn) * (Radix e)) + ((e,(m + 1),f) . 1)) div ((Radix e) * ((Radix e) |^ (rs2 -' 1)))) mod (Radix e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(m,e,nn) div ((Radix e) |^ (rs2 -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((m,e,nn) div ((Radix e) |^ (rs2 -' 1))) mod (Radix e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(rs2,e,(m,e,nn)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) |^ rs2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(m,e,nn) mod ((Radix e) |^ rs2) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((m,e,nn) mod ((Radix e) |^ rs2)) div ((Radix e) |^ (rs2 -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
len (e,m,(m,e,nn)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
DecSD (i,m,e) is V15() V18( NAT ) V19(e -SD ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of e -SD
(m,e,nn) * (Radix e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix e) |^ m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
((Radix e) |^ m) * (Radix e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
rs2 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
DigA (en,rs2) is V11() V12() integer ext-real set
rs2 + 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
DigA (e,(rs2 + 1)) is V11() V12() integer ext-real set
DigB (e,(rs2 + 1)) is V11() V12() integer V43() ext-real Element of INT
en . rs2 is V11() V12() ext-real Element of REAL
(k,e,ie,m,en) is V15() V18( NAT ) V19( INT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
rs2 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(k,e,ie,m,en) . rs2 is V11() V12() integer ext-real Element of REAL
(k,e,ie,(m + 1),e) . rs2 is V11() V12() integer ext-real Element of REAL
rs2 + 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,e,ie,m,en) . (rs2 + 1) is V11() V12() integer ext-real Element of REAL
(k,e,ie,(m + 1),e) . (rs2 + 1) is V11() V12() integer ext-real Element of REAL
1 + 0 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
(rs2 + 1) - 1 is V11() V12() integer ext-real Element of REAL
m - 1 is V11() V12() integer ext-real Element of REAL
(k,ie,m,e,m,en) is V11() V12() integer ext-real set
DigA (en,m) is V11() V12() integer ext-real set
k * (DigA (en,m)) is V11() V12() integer ext-real set
(k * (DigA (en,m))) mod ie is V11() V12() integer ext-real set
(k,ie,(m + 1),e,(m + 1),e) is V11() V12() integer ext-real set
DigA (e,(m + 1)) is V11() V12() integer ext-real set
k * (DigA (e,(m + 1))) is V11() V12() integer ext-real set
(k * (DigA (e,(m + 1)))) mod ie is V11() V12() integer ext-real set
(k,e,ie,(m + 1),e) . 1 is V11() V12() integer ext-real Element of REAL
rs is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
rs + 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 + 1) - 1 is V11() V12() integer ext-real Element of REAL
(m + 1) -' rs2 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(k,ie,((m + 1) -' rs2),e,(m + 1),e) is V11() V12() integer ext-real set
DigA (e,((m + 1) -' rs2)) is V11() V12() integer ext-real set
k * (DigA (e,((m + 1) -' rs2))) is V11() V12() integer ext-real set
(k * (DigA (e,((m + 1) -' rs2)))) mod ie is V11() V12() integer ext-real set
m -' rs2 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
1 + rs2 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
(1 + rs2) - rs2 is V11() V12() integer ext-real Element of REAL
m - rs2 is V11() V12() integer ext-real Element of REAL
(k,ie,(m -' rs2),e,m,en) is V11() V12() integer ext-real set
DigA (en,(m -' rs2)) is V11() V12() integer ext-real set
k * (DigA (en,(m -' rs2))) is V11() V12() integer ext-real set
(k * (DigA (en,(m -' rs2)))) mod ie is V11() V12() integer ext-real set
(Radix e) * ((k,e,ie,(m + 1),e) . rs2) is V11() V12() integer ext-real Element of REAL
(m -' rs2) + 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
DigA (e,((m -' rs2) + 1)) is V11() V12() integer ext-real set
k * (DigA (e,((m -' rs2) + 1))) is V11() V12() integer ext-real set
(k * (DigA (e,((m -' rs2) + 1)))) mod ie is V11() V12() integer ext-real set
((Radix e) * ((k,e,ie,(m + 1),e) . rs2)) + ((k * (DigA (e,((m -' rs2) + 1)))) mod ie) is V11() V12() integer ext-real Element of REAL
(((Radix e) * ((k,e,ie,(m + 1),e) . rs2)) + ((k * (DigA (e,((m -' rs2) + 1)))) mod ie)) mod ie is V11() V12() integer ext-real set
i1 is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
(Radix e) * i1 is V11() V12() integer ext-real set
((Radix e) * i1) + (k,ie,(m -' rs2),e,m,en) is V11() V12() integer ext-real set
(((Radix e) * i1) + (k,ie,(m -' rs2),e,m,en)) mod ie is V11() V12() integer ext-real set
i1 is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
(Radix e) * i1 is V11() V12() integer ext-real set
((Radix e) * i1) + (k,ie,((m + 1) -' rs2),e,(m + 1),e) is V11() V12() integer ext-real set
(((Radix e) * i1) + (k,ie,((m + 1) -' rs2),e,(m + 1),e)) mod ie is V11() V12() integer ext-real set
(k,e,ie,m,en) . 0 is V11() V12() integer ext-real Element of REAL
(k,e,ie,(m + 1),e) . 0 is V11() V12() integer ext-real Element of REAL
rs2 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(k,e,ie,m,en) . rs2 is V11() V12() integer ext-real Element of REAL
(k,e,ie,(m + 1),e) . rs2 is V11() V12() integer ext-real Element of REAL
(m + 1) - 1 is V11() V12() integer ext-real Element of REAL
(k,e,ie,(m + 1),e) . m is V11() V12() integer ext-real Element of REAL
(m + 1) -' m is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(k,ie,((m + 1) -' m),e,(m + 1),e) is V11() V12() integer ext-real set
DigA (e,((m + 1) -' m)) is V11() V12() integer ext-real set
k * (DigA (e,((m + 1) -' m))) is V11() V12() integer ext-real set
(k * (DigA (e,((m + 1) -' m)))) mod ie is V11() V12() integer ext-real set
(k,e,ie,m,en) . m is V11() V12() integer ext-real Element of REAL
(Radix e) * ((k,e,ie,m,en) . m) is V11() V12() integer ext-real Element of REAL
((Radix e) * ((k,e,ie,m,en) . m)) + (k,ie,((m + 1) -' m),e,(m + 1),e) is V11() V12() integer ext-real Element of REAL
(((Radix e) * ((k,e,ie,m,en) . m)) + (k,ie,((m + 1) -' m),e,(m + 1),e)) mod ie is V11() V12() integer ext-real set
k * i is V11() V12() integer ext-real Element of REAL
(k * i) mod ie is V11() V12() integer ext-real set
(Radix e) * ((k * i) mod ie) is V11() V12() integer ext-real set
((Radix e) * ((k * i) mod ie)) + (k,ie,((m + 1) -' m),e,(m + 1),e) is V11() V12() integer ext-real set
(((Radix e) * ((k * i) mod ie)) + (k,ie,((m + 1) -' m),e,(m + 1),e)) mod ie is V11() V12() integer ext-real set
((Radix e) * ((k * (m,e,nn)) mod ie)) + (k,ie,((m + 1) -' m),e,(m + 1),e) is V11() V12() integer ext-real set
(((Radix e) * ((k * (m,e,nn)) mod ie)) + (k,ie,((m + 1) -' m),e,(m + 1),e)) mod ie is V11() V12() integer ext-real set
DigA (e,1) is V11() V12() integer ext-real set
k * (DigA (e,1)) is V11() V12() integer ext-real set
(k * (DigA (e,1))) mod ie is V11() V12() integer ext-real set
((Radix e) * ((k * (m,e,nn)) mod ie)) + ((k * (DigA (e,1))) mod ie) is V11() V12() integer ext-real set
(((Radix e) * ((k * (m,e,nn)) mod ie)) + ((k * (DigA (e,1))) mod ie)) mod ie is V11() V12() integer ext-real set
rs2 is V11() V12() integer ext-real set
rs is V11() V12() integer ext-real set
(Radix e) * rs2 is V11() V12() integer ext-real set
((Radix e) * rs2) + (k,ie,((m + 1) -' m),e,(m + 1),e) is V11() V12() integer ext-real set
(((Radix e) * rs2) + (k,ie,((m + 1) -' m),e,(m + 1),e)) mod ie is V11() V12() integer ext-real set
m is V11() V12() integer ext-real set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
ie is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
ie -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
DecSD (k,1,ie) is V15() V18( NAT ) V19(ie -SD ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of ie -SD
m * k is V11() V12() integer ext-real set
(m * k) mod f is V11() V12() integer ext-real set
e is V15() V18( NAT ) V19(ie -SD ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of ie -SD
(m,ie,f,1,e) is V15() V18( NAT ) V19( INT ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
(m,ie,f,1,e) . 1 is V11() V12() integer ext-real Element of REAL
(m,f,1,ie,1,e) is V11() V12() integer ext-real set
DigA (e,1) is V11() V12() integer ext-real set
m * (DigA (e,1)) is V11() V12() integer ext-real set
(m * (DigA (e,1))) mod f is V11() V12() integer ext-real set
SDDec (DecSD (k,1,ie)) is V11() V12() integer ext-real set
m * (SDDec (DecSD (k,1,ie))) is V11() V12() integer ext-real set
(m * (SDDec (DecSD (k,1,ie)))) mod f is V11() V12() integer ext-real set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e -SD is V1() V82() V83() V84() V85() V86() Element of K6(INT)
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
ie is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e is V15() V18( NAT ) V19(e -SD ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of e -SD
DecSD (f,m,e) is V15() V18( NAT ) V19(e -SD ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of e -SD
k is V11() V12() integer ext-real set
(k,e,ie,m,e) is V15() V18( NAT ) V19( INT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of INT
(k,e,ie,m,e) . m is V11() V12() integer ext-real Element of REAL
k * f is V11() V12() integer ext-real set
(k * f) mod ie is V11() V12() integer ext-real set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
ie is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e /. f is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie |^ (e /. 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
(ie |^ (e /. f)) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie 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
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(ie) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(ie,k,ie,f,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e /. ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
f |^ (e /. ie) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(f |^ (e /. ie)) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie - 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
e is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e -' en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(ie,k,(e -' en),f,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e /. (e -' en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
f |^ (e /. (e -' en)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(f |^ (e /. (e -' en))) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ien is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ien |^ (Radix m) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(ien |^ (Radix m)) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie -' en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(ie,k,(ie -' en),f,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e /. (ie -' en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
f |^ (e /. (ie -' en)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(f |^ (e /. (ie -' en))) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((ien |^ (Radix m)) mod k) * (ie,k,(ie -' en),f,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((ien |^ (Radix m)) mod k) * (ie,k,(ie -' en),f,e)) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
nn is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V15() V18( NAT ) V19( NAT ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
len en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en . 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(ie) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
en . 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ien is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
en . ien is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ien + 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
en . (ien + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie -' ien is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(ie,k,(ie -' ien),f,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e /. (ie -' ien) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
f |^ (e /. (ie -' ien)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(f |^ (e /. (ie -' ien))) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(ie) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence 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
n is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(ie) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
n . 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e . en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
n . en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en + 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
e . (en + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
n . (en + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
0 + 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
ie -' en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(ie,k,(ie -' en),f,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e /. (ie -' en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
f |^ (e /. (ie -' en)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(f |^ (e /. (ie -' en))) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
ien is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
en |^ (Radix m) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(en |^ (Radix m)) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((en |^ (Radix m)) mod k) * (ie,k,(ie -' en),f,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((en |^ (Radix m)) mod k) * (ie,k,(ie -' en),f,e)) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
nn is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
i |^ (Radix m) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(i |^ (Radix m)) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((i |^ (Radix m)) mod k) * (ie,k,(ie -' en),f,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((i |^ (Radix m)) mod k) * (ie,k,(ie -' en),f,e)) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of 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 . 0 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
n . 0 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e . ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
n . ie 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 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
en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e . en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en + 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
e . (en + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie -' en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(ie,k,(ie -' en),f,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e /. (ie -' en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
f |^ (e /. (ie -' en)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(f |^ (e /. (ie -' en))) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
n . en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
n . (en + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
ien is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
en |^ (Radix m) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(en |^ (Radix m)) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((en |^ (Radix m)) mod k) * (ie,k,(ie -' en),f,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((en |^ (Radix m)) mod k) * (ie,k,(ie -' en),f,e)) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
nn is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
i |^ (Radix m) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(i |^ (Radix m)) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((i |^ (Radix m)) mod k) * (ie,k,(ie -' en),f,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((i |^ (Radix m)) mod k) * (ie,k,(ie -' en),f,e)) mod k is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e . en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
n . en 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 V11() V12() integer ext-real Element of REAL
(len e) - 1 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
en + 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
len n 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 V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive 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
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
ie is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(f,(m + 1),e) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m + 1) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k |^ e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ e) mod 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 V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m + 1) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(f,ie,k,(m + 1),e) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m + 1) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(f,ie,k,(m + 1),e) . (m + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V15() V18( NAT ) V19( NAT ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
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)
Seg n is V28() V35(n) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
Radix f is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
n + 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 f) |^ (n + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(n) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(n,f,en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(n,f,en) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(n) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
Sum (n,f,en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
1 + n 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 + n) is V1() V28() V35(1 + n) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
(n,f,en) * (Radix f) 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
((n,f,en) * (Radix f)) + (e /. 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(1,f,(m + 1),e) 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
(Radix 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
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 f) |^ (1 -' 1)) * (e . 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
<*(1,f,(m + 1),e)*> is V1() V15() V18( NAT ) V19( NAT ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
len <*(1,f,(m + 1),e)*> is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
nn is V15() V18( NAT ) V19( REAL ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of REAL
len nn is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom nn is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
rD is V15() V18( NAT ) V19( REAL ) Function-like V28() V35(n) FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of REAL
dom rD is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
n -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
dom (n,f,en) is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
len (n,f,en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
Seg (len (n,f,en)) is V28() V35( len (n,f,en)) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
(Radix f) * (n,f,en) is V15() V18( NAT ) V19( REAL ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of REAL
len ((Radix f) * (n,f,en)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
rD1 is V35(n) FinSequence-like Element of n -tuples_on REAL
i is V11() V12() ext-real Element of REAL
i * rD1 is V15() V18( NAT ) V19( REAL ) Function-like V28() V35(n) FinSequence-like FinSubsequence-like V72() V73() V74() Element of n -tuples_on REAL
len (i * rD1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
<*(1,f,(m + 1),e)*> ^ ((Radix f) * (n,f,en)) is V1() V15() V18( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set
len (<*(1,f,(m + 1),e)*> ^ ((Radix f) * (n,f,en))) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(len <*(1,f,(m + 1),e)*>) + (len ((Radix f) * (n,f,en))) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((m + 1),f,e) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m + 1) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
len ((m + 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
i is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
((m + 1),f,e) . i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(<*(1,f,(m + 1),e)*> ^ ((Radix f) * (n,f,en))) . i is set
Seg (n + 1) is V1() V28() V35(n + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
dom ((m + 1),f,e) is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
((m + 1),f,e) /. 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((m + 1),f,e) . 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i - 1 is V11() V12() integer ext-real Element of REAL
(n,f,en) . (i - 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
rD . (i - 1) is V11() V12() ext-real Element of REAL
1 - 1 is V11() V12() integer ext-real Element of REAL
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
(1 + 1) - 1 is V11() V12() integer ext-real Element of REAL
(n + 1) - 1 is V11() V12() integer ext-real Element of REAL
i1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix f) * (n,f,en)) . (i - 1) is V11() V12() ext-real Element of REAL
i * rD is V15() V18( NAT ) V19( REAL ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of REAL
(i * rD) . (i - 1) is V11() V12() ext-real Element of REAL
rs is V11() V12() ext-real Element of REAL
i * rs is V11() V12() ext-real Element of REAL
rs2 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) * rs2 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(n,f,en) /. i1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) * ((n,f,en) /. i1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(i1,f,n,en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i1 -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) |^ (i1 -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en . i1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix f) |^ (i1 -' 1)) * (en . i1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) * (i1,f,n,en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) * ((Radix f) |^ (i1 -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix f) * ((Radix f) |^ (i1 -' 1))) * (en . i1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(i1 -' 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
(Radix f) |^ ((i1 -' 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 f) |^ ((i1 -' 1) + 1)) * (en . i1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) |^ i1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix f) |^ i1) * (en . i1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i1 + 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
e . (i1 + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix f) |^ i1) * (e . (i1 + 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(i,f,(m + 1),e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) |^ (i -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e . i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix f) |^ (i -' 1)) * (e . i) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((m + 1),f,e) /. i 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)
len e is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
Seg (len e) is V28() V35( len e) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
1 - 1 is V11() V12() integer ext-real Element of REAL
((m + 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
Sum ((m + 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
Sum ((Radix f) * (n,f,en)) is V11() V12() ext-real Element of REAL
(1,f,(m + 1),e) + (Sum ((Radix f) * (n,f,en))) is V11() V12() ext-real Element of REAL
i * rD is V15() V18( NAT ) V19( REAL ) Function-like V28() FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of REAL
Sum (i * rD) is V11() V12() ext-real Element of REAL
(1,f,(m + 1),e) + (Sum (i * rD)) is V11() V12() ext-real Element of REAL
Sum rD is V11() V12() ext-real Element of REAL
i * (Sum rD) is V11() V12() ext-real Element of REAL
(1,f,(m + 1),e) + (i * (Sum rD)) is V11() V12() ext-real Element of REAL
(Radix f) * (n,f,en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(1,f,(m + 1),e) + ((Radix f) * (n,f,en)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) |^ 0 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix f) |^ 0) * (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 f) |^ 0) * (e . 1)) + ((Radix f) * (n,f,en)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
1 * (e . 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(1 * (e . 1)) + ((Radix f) * (n,f,en)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) |^ n is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((Radix f) |^ n) * (Radix f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
Seg (n + 1) is V1() V28() V35(n + 1) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
(f,ie,k,n,en) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(n) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f,ie,k,n,en) . i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f,ie,k,(m + 1),e) . i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i + 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
(f,ie,k,n,en) . (i + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f,ie,k,(m + 1),e) . (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 + 0 is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom en is V82() V83() V84() V85() V86() V87() Element of K6(NAT)
(i + 1) - 1 is V11() V12() integer ext-real Element of REAL
n - 1 is V11() V12() integer ext-real Element of REAL
dom e 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
Seg (len e) is V28() V35( len e) V82() V83() V84() V85() V86() V87() Element of K6(NAT)
(n,ie,n,k,en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en /. n is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (en /. n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (en /. n)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en . n is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (en . n) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (en . n)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e . (n + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (e . (n + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (e . (n + 1))) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((m + 1),ie,(n + 1),k,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e /. (n + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (e /. (n + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (e /. (n + 1))) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f,ie,k,(m + 1),e) . 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
nn is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
nn + 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
(n + 1) - 1 is V11() V12() integer ext-real Element of REAL
(n + 1) -' i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((m + 1),ie,((n + 1) -' i),k,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e /. ((n + 1) -' i) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (e /. ((n + 1) -' i)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (e /. ((n + 1) -' i))) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
n -' i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(n,ie,(n -' i),k,en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en /. (n -' i) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (en /. (n -' i)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (en /. (n -' i))) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(n + 1) -' nn is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(n + 1) - (n - 1) is V11() V12() integer ext-real Element of REAL
1 + i is V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() Element of NAT
(1 + i) - i is V11() V12() integer ext-real Element of REAL
n - i is V11() V12() integer ext-real Element of REAL
((f,ie,k,(m + 1),e) . i) |^ (Radix f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((f,ie,k,(m + 1),e) . i) |^ (Radix f)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
en . (n -' i) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (en . (n -' i)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (en . (n -' i))) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((f,ie,k,(m + 1),e) . i) |^ (Radix f)) mod ie) * ((k |^ (en . (n -' i))) mod ie) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((((f,ie,k,(m + 1),e) . i) |^ (Radix f)) mod ie) * ((k |^ (en . (n -' i))) mod ie)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(n -' i) + 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
e . ((n -' i) + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (e . ((n -' i) + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (e . ((n -' i) + 1))) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((f,ie,k,(m + 1),e) . i) |^ (Radix f)) mod ie) * ((k |^ (e . ((n -' i) + 1))) mod ie) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((((f,ie,k,(m + 1),e) . i) |^ (Radix f)) mod ie) * ((k |^ (e . ((n -' i) + 1))) mod ie)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e . ((n + 1) -' i) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (e . ((n + 1) -' i)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (e . ((n + 1) -' i))) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((f,ie,k,(m + 1),e) . i) |^ (Radix f)) mod ie) * ((k |^ (e . ((n + 1) -' i))) mod ie) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((((f,ie,k,(m + 1),e) . i) |^ (Radix f)) mod ie) * ((k |^ (e . ((n + 1) -' i))) mod ie)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((f,ie,k,(m + 1),e) . i) |^ (Radix f)) mod ie) * ((m + 1),ie,((n + 1) -' i),k,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((((f,ie,k,(m + 1),e) . i) |^ (Radix f)) mod ie) * ((m + 1),ie,((n + 1) -' i),k,e)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
rD is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
rD1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
rD |^ (Radix f) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(rD |^ (Radix f)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((rD |^ (Radix f)) mod ie) * (n,ie,(n -' i),k,en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((rD |^ (Radix f)) mod ie) * (n,ie,(n -' i),k,en)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
rD is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
rD1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
rD |^ (Radix f) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(rD |^ (Radix f)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((rD |^ (Radix f)) mod ie) * ((m + 1),ie,((n + 1) -' i),k,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((rD |^ (Radix f)) mod ie) * ((m + 1),ie,((n + 1) -' i),k,e)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f,ie,k,n,en) . 0 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f,ie,k,(m + 1),e) . 0 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f,ie,k,n,en) . i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f,ie,k,(m + 1),e) . i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
len en is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f,n,(n,f,en)) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(n) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
dom e 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
Seg (len e) is V28() V35( len e) V82() V83() V84() V85() V86() V87() Element of K6(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
(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
(Radix f) |^ 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e mod ((Radix f) |^ 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
(Radix 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
(e mod ((Radix f) |^ 1)) div ((Radix 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
(Radix f) |^ 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e mod ((Radix f) |^ 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) |^ 0 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(e mod ((Radix f) |^ 1)) div ((Radix f) |^ 0) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(e mod ((Radix f) |^ 1)) div 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e mod (Radix f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(e . 1) + ((n,f,en) * (Radix f)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((e . 1) + ((n,f,en) * (Radix f))) div (Radix f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((e . 1) + ((n,f,en) * (Radix f))) / (Radix f) is V11() V12() ext-real non negative Element of REAL
[\(((e . 1) + ((n,f,en) * (Radix f))) / (Radix f))/] is V11() V12() integer ext-real set
(e . 1) / (Radix f) is V11() V12() ext-real non negative Element of REAL
((e . 1) / (Radix f)) + (n,f,en) is V11() V12() ext-real non negative Element of REAL
[\(((e . 1) / (Radix f)) + (n,f,en))/] is V11() V12() integer ext-real set
[\((e . 1) / (Radix f))/] is V11() V12() integer ext-real set
[\((e . 1) / (Radix f))/] + (n,f,en) is V11() V12() integer ext-real Element of REAL
(e . 1) div (Radix f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((e . 1) div (Radix f)) + (n,f,en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
0 + (n,f,en) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
en . i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f,n,(n,f,en)) . i is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i + 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
e . (i + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((i + 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
(Radix f) |^ (i + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e mod ((Radix f) |^ (i + 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(i + 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 f) |^ ((i + 1) -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(e mod ((Radix f) |^ (i + 1))) div ((Radix f) |^ ((i + 1) -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((n,f,en) * (Radix f)) + (e /. 1)) div ((Radix f) |^ ((i + 1) -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((n,f,en) * (Radix f)) + (e /. 1)) div ((Radix f) |^ ((i + 1) -' 1))) mod (Radix f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((n,f,en) * (Radix f)) + (e . 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((n,f,en) * (Radix f)) + (e . 1)) div ((Radix f) |^ ((i + 1) -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((n,f,en) * (Radix f)) + (e . 1)) div ((Radix f) |^ ((i + 1) -' 1))) mod (Radix f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) |^ i is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(((n,f,en) * (Radix f)) + (e . 1)) div ((Radix f) |^ i) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((n,f,en) * (Radix f)) + (e . 1)) div ((Radix f) |^ i)) mod (Radix f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i -' 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) |^ (i -' 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix f) * ((Radix f) |^ (i -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((n,f,en) * (Radix f)) + (e . 1)) div ((Radix f) * ((Radix f) |^ (i -' 1))) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((n,f,en) * (Radix f)) + (e . 1)) div ((Radix f) * ((Radix f) |^ (i -' 1)))) mod (Radix f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((e . 1) + ((n,f,en) * (Radix f))) div (Radix f)) div ((Radix f) |^ (i -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((e . 1) + ((n,f,en) * (Radix f))) div (Radix f)) div ((Radix f) |^ (i -' 1))) mod (Radix f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(i,f,(n,f,en)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(n,f,en) mod ((Radix f) |^ i) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((n,f,en) mod ((Radix f) |^ i)) div ((Radix f) |^ (i -' 1)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
len (f,n,(n,f,en)) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(n + 1) - 1 is V11() V12() integer ext-real Element of REAL
(f,ie,k,(m + 1),e) . n is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f,ie,k,(m + 1),e) . (n + 1) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(n + 1) -' n is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((m + 1),ie,((n + 1) -' n),k,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e /. ((n + 1) -' n) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (e /. ((n + 1) -' n)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (e /. ((n + 1) -' n))) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(f,ie,k,n,en) . n is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((f,ie,k,n,en) . n) |^ (Radix f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((f,ie,k,n,en) . n) |^ (Radix f)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((f,ie,k,n,en) . n) |^ (Radix f)) mod ie) * ((m + 1),ie,((n + 1) -' n),k,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((((f,ie,k,n,en) . n) |^ (Radix f)) mod ie) * ((m + 1),ie,((n + 1) -' n),k,e)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (n,f,en) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (n,f,en)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((k |^ (n,f,en)) mod ie) |^ (Radix f) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((k |^ (n,f,en)) mod ie) |^ (Radix f)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((k |^ (n,f,en)) mod ie) |^ (Radix f)) mod ie) * ((m + 1),ie,((n + 1) -' n),k,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((((k |^ (n,f,en)) mod ie) |^ (Radix f)) mod ie) * ((m + 1),ie,((n + 1) -' n),k,e)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(k |^ (n,f,en)) |^ (Radix f) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
((k |^ (n,f,en)) |^ (Radix f)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((k |^ (n,f,en)) |^ (Radix f)) mod ie) * ((m + 1),ie,((n + 1) -' n),k,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((((k |^ (n,f,en)) |^ (Radix f)) mod ie) * ((m + 1),ie,((n + 1) -' n),k,e)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((k |^ (n,f,en)) |^ (Radix f)) * ((m + 1),ie,((n + 1) -' n),k,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((k |^ (n,f,en)) |^ (Radix f)) * ((m + 1),ie,((n + 1) -' n),k,e)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ ((n,f,en) * (Radix f)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ ((n,f,en) * (Radix f))) * ((m + 1),ie,((n + 1) -' n),k,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((k |^ ((n,f,en) * (Radix f))) * ((m + 1),ie,((n + 1) -' n),k,e)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (e /. 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (e /. 1)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(k |^ ((n,f,en) * (Radix f))) * ((k |^ (e /. 1)) mod ie) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((k |^ ((n,f,en) * (Radix f))) * ((k |^ (e /. 1)) mod ie)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(k |^ ((n,f,en) * (Radix f))) * (k |^ (e /. 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
((k |^ ((n,f,en) * (Radix f))) * (k |^ (e /. 1))) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ (((n,f,en) * (Radix f)) + (e /. 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ (((n,f,en) * (Radix f)) + (e /. 1))) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
i is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
nn is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
i |^ (Radix f) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(i |^ (Radix f)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
((i |^ (Radix f)) mod ie) * ((m + 1),ie,((n + 1) -' n),k,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(((i |^ (Radix f)) mod ie) * ((m + 1),ie,((n + 1) -' n),k,e)) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie 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
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k,1,ie) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m |^ ie is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(m |^ ie) mod 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
(Radix k) |^ 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
e is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(k,f,m,1,e) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(1) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(k,f,m,1,e) . 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 V11() V12() integer ext-real Element of REAL
len (k,1,ie) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
dom (k,1,ie) is V82() V83() V84() V85() V86() V87() Element of K6(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
(k,1,ie) . 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(1,k,ie) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(Radix k) |^ 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
ie mod ((Radix k) |^ 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
(Radix 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
(ie mod ((Radix k) |^ 1)) div ((Radix 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
ie mod ((Radix k) |^ 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) |^ 0 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(ie mod ((Radix k) |^ 1)) div ((Radix k) |^ 0) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(ie mod ((Radix k) |^ 1)) div 1 is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
ie mod (Radix k) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
(1,f,1,m,e) is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
m |^ (e /. 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(m |^ (e /. 1)) mod f 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
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
ie is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(f,m,e) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(f,ie,k,m,e) is V15() V18( NAT ) V19( NAT ) Function-like V28() V35(m) FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
(f,ie,k,m,e) . m is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT
k |^ e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(k |^ e) mod ie is V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() Element of NAT