REAL is V1() V28() V70() V71() V72() V76() set
NAT is V70() V71() V72() V73() V74() V75() V76() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V1() V28() V70() V76() set
NAT is V70() V71() V72() V73() V74() V75() V76() set
K6(NAT) is set
K6(NAT) is set
RAT is V1() V28() V70() V71() V72() V73() V76() set
INT is V1() V28() V70() V71() V72() V73() V74() V76() set
K7(COMPLEX,COMPLEX) is V60() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V60() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is V60() V61() V62() set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is V60() V61() V62() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V19( RAT ) V60() V61() V62() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V19( RAT ) V60() V61() V62() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V19( RAT ) V19( INT ) V60() V61() V62() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V19( RAT ) V19( INT ) V60() V61() V62() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V19( RAT ) V19( INT ) V60() V61() V62() V63() set
K7(K7(NAT,NAT),NAT) is V19( RAT ) V19( INT ) V60() V61() V62() V63() set
K6(K7(K7(NAT,NAT),NAT)) is set
K297() is set
1 is V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
K454() is V82() V110() L8()
the U1 of K454() is set
K6(INT) is set
0 is V1() V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() V76() Element of NAT
2 is V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
- 1 is V11() V12() integer ext-real non positive set
n is V6() V10() V11() V12() integer ext-real non negative set
Radix n is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
k is V6() V10() V11() V12() integer ext-real non negative set
Radix k is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
k + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
Radix (k + 1) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k + 1) is V11() V12() ext-real set
2 to_power 1 is V11() V12() ext-real Element of REAL
(2 to_power 1) * (2 to_power k) is V11() V12() ext-real set
2 * (Radix k) is V6() V10() V11() V12() integer ext-real non negative set
Radix 2 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power 2 is V11() V12() ext-real set
1 + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
2 to_power (1 + 1) is V11() V12() ext-real set
2 to_power 1 is V11() V12() ext-real Element of REAL
(2 to_power 1) * (2 to_power 1) is V11() V12() ext-real set
2 * (2 to_power 1) is V11() V12() ext-real set
2 * 2 is V6() V10() V11() V12() integer ext-real non negative set
4 is V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
n is V6() V10() V11() V12() integer ext-real non negative set
n -SD_Sub_S is V1() V70() V71() V72() V73() V74() Element of K6(INT)
n -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
k is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (n -' 1)) <= b1 & b1 <= (Radix (n -' 1)) - 1 ) } is set
x is V11() V12() integer V43() ext-real Element of INT
n is V6() V10() V11() V12() integer ext-real non negative set
Seg n is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
n + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
k is V6() V10() V11() V12() integer ext-real non negative set
x is V6() V10() V11() V12() integer ext-real non negative set
DecSD (k,(n + 1),x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD
x -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
Radix x is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power x is V11() V12() ext-real set
(Radix x) - 1 is V11() V12() integer ext-real set
- (Radix x) is V11() V12() integer ext-real non positive set
(- (Radix x)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix x) - 1 & (- (Radix x)) + 1 <= b1 ) } is set
DecSD (k,n,x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of x -SD
y is V6() V10() V11() V12() integer ext-real non negative set
DigA ((DecSD (k,(n + 1),x)),y) is V11() V12() integer ext-real set
DigA ((DecSD (k,n,x)),y) is V11() V12() integer ext-real set
Seg (n + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
DigitDC (k,y,x) is V11() V12() integer V43() ext-real Element of x -SD
(Radix x) |^ y is V6() V10() V11() V12() integer ext-real non negative set
k mod ((Radix x) |^ y) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
y -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix x) |^ (y -' 1) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(k mod ((Radix x) |^ y)) div ((Radix x) |^ (y -' 1)) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
x is V6() V10() V11() V12() integer ext-real non negative set
n is V6() V10() V11() V12() integer ext-real non negative set
k is V6() V10() V11() V12() integer ext-real non negative set
Radix n is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
(Radix n) |^ x is V6() V10() V11() V12() integer ext-real non negative set
k mod ((Radix n) |^ x) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DecSD ((k mod ((Radix n) |^ x)),x,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(x) FinSequence-like V60() V61() V62() FinSequence of n -SD
n -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
(Radix n) - 1 is V11() V12() integer ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix n) - 1 & (- (Radix n)) + 1 <= b1 ) } is set
DigA ((DecSD ((k mod ((Radix n) |^ x)),x,n)),x) is V11() V12() integer ext-real set
DecSD (k,x,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(x) FinSequence-like V60() V61() V62() FinSequence of n -SD
DigA ((DecSD (k,x,n)),x) is V11() V12() integer ext-real set
Seg x is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
DigitDC ((k mod ((Radix n) |^ x)),x,n) is V11() V12() integer V43() ext-real Element of n -SD
(k mod ((Radix n) |^ x)) mod ((Radix n) |^ x) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
x -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix n) |^ (x -' 1) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
((k mod ((Radix n) |^ x)) mod ((Radix n) |^ x)) div ((Radix n) |^ (x -' 1)) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigitDC (k,x,n) is V11() V12() integer V43() ext-real Element of n -SD
(k mod ((Radix n) |^ x)) div ((Radix n) |^ (x -' 1)) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
3 is V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
n is V11() V12() integer ext-real set
k is V11() V12() integer ext-real set
x is V6() V10() V11() V12() integer ext-real non negative set
SDSub_Add_Carry (n,x) is V11() V12() integer ext-real set
SDSub_Add_Carry (k,x) is V11() V12() integer ext-real set
(SDSub_Add_Carry (n,x)) + (SDSub_Add_Carry (k,x)) is V11() V12() integer ext-real set
SDSub_Add_Carry (((SDSub_Add_Carry (n,x)) + (SDSub_Add_Carry (k,x))),x) is V11() V12() integer ext-real set
(- 1) + (- 1) is V11() V12() integer ext-real non positive set
3 - 1 is V11() V12() integer ext-real set
x - 1 is V11() V12() integer ext-real set
x -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (x -' 1) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (x -' 1) is V11() V12() ext-real set
1 + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
- (Radix (x -' 1)) is V11() V12() integer ext-real non positive set
- 2 is V11() V12() integer ext-real non positive set
n is V6() V10() V11() V12() integer ext-real non negative set
k is V6() V10() V11() V12() integer ext-real non negative set
x is V6() V10() V11() V12() integer ext-real non negative set
x + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
DecSD (k,x,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(x) FinSequence-like V60() V61() V62() FinSequence of n -SD
n -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
Radix n is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
(Radix n) - 1 is V11() V12() integer ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix n) - 1 & (- (Radix n)) + 1 <= b1 ) } is set
SD2SDSub (DecSD (k,x,n)) is V15() V18( NAT ) V19(n -SD_Sub ) Function-like V35(x + 1) FinSequence-like V60() V61() V62() FinSequence of n -SD_Sub
n -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
DigA_SDSub ((SD2SDSub (DecSD (k,x,n))),(x + 1)) is V11() V12() integer ext-real set
DigA ((DecSD (k,x,n)),x) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (k,x,n)),x)),n) is V11() V12() integer ext-real set
0 + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
Seg (x + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
SD2SDSubDigitS ((DecSD (k,x,n)),(x + 1),n) is V11() V12() integer V43() ext-real Element of n -SD_Sub
SD2SDSubDigit ((DecSD (k,x,n)),(x + 1),n) is V11() V12() integer ext-real set
(x + 1) -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigA ((DecSD (k,x,n)),((x + 1) -' 1)) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (k,x,n)),((x + 1) -' 1))),n) is V11() V12() integer ext-real set
1 + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
n is V6() V10() V11() V12() integer ext-real non negative set
k is V6() V10() V11() V12() integer ext-real non negative set
DecSD (k,1,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like V60() V61() V62() FinSequence of n -SD
n -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
Radix n is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
(Radix n) - 1 is V11() V12() integer ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix n) - 1 & (- (Radix n)) + 1 <= b1 ) } is set
SD2SDSub (DecSD (k,1,n)) is V15() V18( NAT ) V19(n -SD_Sub ) Function-like V35(1 + 1) FinSequence-like V60() V61() V62() FinSequence of n -SD_Sub
n -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
DigA_SDSub ((SD2SDSub (DecSD (k,1,n))),(1 + 1)) is V11() V12() integer ext-real set
SDSub_Add_Carry (k,n) is V11() V12() integer ext-real set
DigA ((DecSD (k,1,n)),1) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (k,1,n)),1)),n) is V11() V12() integer ext-real set
x is V6() V10() V11() V12() integer ext-real non negative set
n is V6() V10() V11() V12() integer ext-real non negative set
x + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
k is V6() V10() V11() V12() integer ext-real non negative set
Radix n is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
(Radix n) |^ x is V6() V10() V11() V12() integer ext-real non negative set
k mod ((Radix n) |^ x) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DecSD ((k mod ((Radix n) |^ x)),x,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(x) FinSequence-like V60() V61() V62() FinSequence of n -SD
n -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
(Radix n) - 1 is V11() V12() integer ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix n) - 1 & (- (Radix n)) + 1 <= b1 ) } is set
SD2SDSub (DecSD ((k mod ((Radix n) |^ x)),x,n)) is V15() V18( NAT ) V19(n -SD_Sub ) Function-like V35(x + 1) FinSequence-like V60() V61() V62() FinSequence of n -SD_Sub
n -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
DigA_SDSub ((SD2SDSub (DecSD ((k mod ((Radix n) |^ x)),x,n))),(x + 1)) is V11() V12() integer ext-real set
DecSD (k,x,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(x) FinSequence-like V60() V61() V62() FinSequence of n -SD
DigA ((DecSD (k,x,n)),x) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (k,x,n)),x)),n) is V11() V12() integer ext-real set
Seg (x + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
SD2SDSubDigitS ((DecSD ((k mod ((Radix n) |^ x)),x,n)),(x + 1),n) is V11() V12() integer V43() ext-real Element of n -SD_Sub
SD2SDSubDigit ((DecSD ((k mod ((Radix n) |^ x)),x,n)),(x + 1),n) is V11() V12() integer ext-real set
(x + 1) -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigA ((DecSD ((k mod ((Radix n) |^ x)),x,n)),((x + 1) -' 1)) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD ((k mod ((Radix n) |^ x)),x,n)),((x + 1) -' 1))),n) is V11() V12() integer ext-real set
x + 0 is V6() V10() V11() V12() integer ext-real non negative set
DigA ((DecSD ((k mod ((Radix n) |^ x)),x,n)),(x + 0)) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD ((k mod ((Radix n) |^ x)),x,n)),(x + 0))),n) is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer ext-real non negative set
Radix n is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
k is V6() V10() V11() V12() integer ext-real non negative set
DecSD (k,1,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(1) FinSequence-like V60() V61() V62() FinSequence of n -SD
n -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
(Radix n) - 1 is V11() V12() integer ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix n) - 1 & (- (Radix n)) + 1 <= b1 ) } is set
SD2SDSub (DecSD (k,1,n)) is V15() V18( NAT ) V19(n -SD_Sub ) Function-like V35(1 + 1) FinSequence-like V60() V61() V62() FinSequence of n -SD_Sub
n -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
DigA_SDSub ((SD2SDSub (DecSD (k,1,n))),1) is V11() V12() integer ext-real set
SDSub_Add_Carry (k,n) is V11() V12() integer ext-real set
(SDSub_Add_Carry (k,n)) * (Radix n) is V11() V12() integer ext-real set
k - ((SDSub_Add_Carry (k,n)) * (Radix n)) is V11() V12() integer ext-real set
Seg 1 is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
Seg (1 + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
SD2SDSubDigitS ((DecSD (k,1,n)),1,n) is V11() V12() integer V43() ext-real Element of n -SD_Sub
SD2SDSubDigit ((DecSD (k,1,n)),1,n) is V11() V12() integer ext-real set
DigA ((DecSD (k,1,n)),1) is V11() V12() integer ext-real set
SDSub_Add_Data ((DigA ((DecSD (k,1,n)),1)),n) is V11() V12() integer ext-real set
1 -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigA ((DecSD (k,1,n)),(1 -' 1)) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (k,1,n)),(1 -' 1))),n) is V11() V12() integer ext-real set
(SDSub_Add_Data ((DigA ((DecSD (k,1,n)),1)),n)) + (SDSub_Add_Carry ((DigA ((DecSD (k,1,n)),(1 -' 1))),n)) is V11() V12() integer ext-real set
DigA ((DecSD (k,1,n)),0) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (k,1,n)),0)),n) is V11() V12() integer ext-real set
(SDSub_Add_Data ((DigA ((DecSD (k,1,n)),1)),n)) + (SDSub_Add_Carry ((DigA ((DecSD (k,1,n)),0)),n)) is V11() V12() integer ext-real set
SDSub_Add_Carry (0,n) is V11() V12() integer ext-real set
(SDSub_Add_Data ((DigA ((DecSD (k,1,n)),1)),n)) + (SDSub_Add_Carry (0,n)) is V11() V12() integer ext-real set
SDSub_Add_Data (k,n) is V11() V12() integer ext-real set
(SDSub_Add_Data (k,n)) + (SDSub_Add_Carry (0,n)) is V11() V12() integer ext-real set
(SDSub_Add_Data (k,n)) + 0 is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer ext-real non negative set
Radix n is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
x is V6() V10() V11() V12() integer ext-real non negative set
(Radix n) |^ x is V6() V10() V11() V12() integer ext-real non negative set
x + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
(x + 1) + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
k is V6() V10() V11() V12() integer ext-real non negative set
DecSD (k,(x + 1),n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(x + 1) FinSequence-like V60() V61() V62() FinSequence of n -SD
n -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
(Radix n) - 1 is V11() V12() integer ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix n) - 1 & (- (Radix n)) + 1 <= b1 ) } is set
SD2SDSub (DecSD (k,(x + 1),n)) is V15() V18( NAT ) V19(n -SD_Sub ) Function-like V35((x + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of n -SD_Sub
n -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
DigA_SDSub ((SD2SDSub (DecSD (k,(x + 1),n))),(x + 1)) is V11() V12() integer ext-real set
((Radix n) |^ x) * (DigA_SDSub ((SD2SDSub (DecSD (k,(x + 1),n))),(x + 1))) is V11() V12() integer ext-real set
DigA ((DecSD (k,(x + 1),n)),(x + 1)) is V11() V12() integer ext-real set
((Radix n) |^ x) * (DigA ((DecSD (k,(x + 1),n)),(x + 1))) is V11() V12() integer ext-real set
(Radix n) |^ (x + 1) is V6() V10() V11() V12() integer ext-real non negative set
SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n) is V11() V12() integer ext-real set
((Radix n) |^ (x + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n)) is V11() V12() integer ext-real set
(((Radix n) |^ x) * (DigA ((DecSD (k,(x + 1),n)),(x + 1)))) - (((Radix n) |^ (x + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n))) is V11() V12() integer ext-real set
DigA ((DecSD (k,(x + 1),n)),x) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),x)),n) is V11() V12() integer ext-real set
((Radix n) |^ x) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),x)),n)) is V11() V12() integer ext-real set
((((Radix n) |^ x) * (DigA ((DecSD (k,(x + 1),n)),(x + 1)))) - (((Radix n) |^ (x + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n)))) + (((Radix n) |^ x) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),x)),n))) is V11() V12() integer ext-real set
Seg (x + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
Seg ((x + 1) + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
SD2SDSubDigitS ((DecSD (k,(x + 1),n)),(x + 1),n) is V11() V12() integer V43() ext-real Element of n -SD_Sub
((Radix n) |^ x) * (SD2SDSubDigitS ((DecSD (k,(x + 1),n)),(x + 1),n)) is V11() V12() integer ext-real set
SD2SDSubDigit ((DecSD (k,(x + 1),n)),(x + 1),n) is V11() V12() integer ext-real set
((Radix n) |^ x) * (SD2SDSubDigit ((DecSD (k,(x + 1),n)),(x + 1),n)) is V11() V12() integer ext-real set
SDSub_Add_Data ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n) is V11() V12() integer ext-real set
(x + 1) -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigA ((DecSD (k,(x + 1),n)),((x + 1) -' 1)) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),((x + 1) -' 1))),n) is V11() V12() integer ext-real set
(SDSub_Add_Data ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n)) + (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),((x + 1) -' 1))),n)) is V11() V12() integer ext-real set
((Radix n) |^ x) * ((SDSub_Add_Data ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n)) + (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),((x + 1) -' 1))),n))) is V11() V12() integer ext-real set
(SDSub_Add_Data ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n)) + (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),x)),n)) is V11() V12() integer ext-real set
((Radix n) |^ x) * ((SDSub_Add_Data ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n)) + (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),x)),n))) is V11() V12() integer ext-real set
(Radix n) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n)) is V11() V12() integer ext-real set
(DigA ((DecSD (k,(x + 1),n)),(x + 1))) - ((Radix n) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n))) is V11() V12() integer ext-real set
((DigA ((DecSD (k,(x + 1),n)),(x + 1))) - ((Radix n) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n)))) + (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),x)),n)) is V11() V12() integer ext-real set
((Radix n) |^ x) * (((DigA ((DecSD (k,(x + 1),n)),(x + 1))) - ((Radix n) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n)))) + (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),x)),n))) is V11() V12() integer ext-real set
((Radix n) |^ x) * (Radix n) is V6() V10() V11() V12() integer ext-real non negative set
(((Radix n) |^ x) * (Radix n)) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n)) is V11() V12() integer ext-real set
(((Radix n) |^ x) * (DigA ((DecSD (k,(x + 1),n)),(x + 1)))) - ((((Radix n) |^ x) * (Radix n)) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n))) is V11() V12() integer ext-real set
((((Radix n) |^ x) * (DigA ((DecSD (k,(x + 1),n)),(x + 1)))) - ((((Radix n) |^ x) * (Radix n)) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),(x + 1))),n)))) + (((Radix n) |^ x) * (SDSub_Add_Carry ((DigA ((DecSD (k,(x + 1),n)),x)),n))) is V11() V12() integer ext-real set
k is V6() V10() V11() V12() integer ext-real non negative set
x is V6() V10() V11() V12() integer ext-real non negative set
x -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
n is V6() V10() V11() V12() integer ext-real non negative set
Seg k is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
y is V15() V18( NAT ) V19(x -SD_Sub ) Function-like V35(k) FinSequence-like V60() V61() V62() FinSequence of x -SD_Sub
DigA_SDSub (y,n) is V11() V12() integer ext-real set
k is V15() V18( NAT ) V19(x -SD_Sub ) Function-like V35(k) FinSequence-like V60() V61() V62() FinSequence of x -SD_Sub
DigA_SDSub (k,n) is V11() V12() integer ext-real set
(DigA_SDSub (y,n)) + (DigA_SDSub (k,n)) is V11() V12() integer ext-real set
SDSub_Add_Data (((DigA_SDSub (y,n)) + (DigA_SDSub (k,n))),x) is V11() V12() integer ext-real set
n -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigA_SDSub (y,(n -' 1)) is V11() V12() integer ext-real set
DigA_SDSub (k,(n -' 1)) is V11() V12() integer ext-real set
(DigA_SDSub (y,(n -' 1))) + (DigA_SDSub (k,(n -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub (y,(n -' 1))) + (DigA_SDSub (k,(n -' 1)))),x) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub (y,n)) + (DigA_SDSub (k,n))),x)) + (SDSub_Add_Carry (((DigA_SDSub (y,(n -' 1))) + (DigA_SDSub (k,(n -' 1)))),x)) is V11() V12() integer ext-real set
x -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
Radix x is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power x is V11() V12() ext-real set
(Radix x) - 1 is V11() V12() integer ext-real set
- (Radix x) is V11() V12() integer ext-real non positive set
(- (Radix x)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix x) - 1 & (- (Radix x)) + 1 <= b1 ) } is set
x -SD_Sub_S is V1() V70() V71() V72() V73() V74() Element of K6(INT)
x -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (x -' 1) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (x -' 1) is V11() V12() ext-real set
- (Radix (x -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (x -' 1))) + (- 1) is V11() V12() integer ext-real non positive set
(Radix (x -' 1)) - 1 is V11() V12() integer ext-real set
((Radix (x -' 1)) - 1) + 1 is V11() V12() integer ext-real set
(- (Radix (x -' 1))) - 1 is V11() V12() integer ext-real non positive negative set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (x -' 1))) - 1 <= b1 & b1 <= Radix (x -' 1) ) } is set
n is V6() V10() V11() V12() integer ext-real non negative set
k is V6() V10() V11() V12() integer ext-real non negative set
k -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
Seg n is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
x is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
y is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
k is V15() V18( NAT ) V19(k -SD_Sub ) Function-like FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
len k is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom k is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
n -tuples_on (k -SD_Sub) is V1() functional FinSequence-membered FinSequenceSet of k -SD_Sub
x is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
y is V6() V10() V11() V12() integer ext-real non negative set
DigA_SDSub (x,y) is V11() V12() integer ext-real set
(y,n,k,x,y) is V11() V12() integer V43() ext-real Element of k -SD_Sub
x . y is V11() V12() ext-real set
k is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
x is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
len k is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom k is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
y is V6() V10() V11() V12() integer ext-real non negative set
k . y is V11() V12() ext-real set
DigA_SDSub (k,y) is V11() V12() integer ext-real set
(y,n,k,x,y) is V11() V12() integer V43() ext-real Element of k -SD_Sub
DigA_SDSub (x,y) is V11() V12() integer ext-real set
x . y is V11() V12() ext-real set
len x is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
n is V6() V10() V11() V12() integer ext-real non negative set
Seg n is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
n + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
(n + 1) + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
k is V6() V10() V11() V12() integer ext-real non negative set
Radix k is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
(Radix k) |^ n is V6() V10() V11() V12() integer ext-real non negative set
x is V6() V10() V11() V12() integer ext-real non negative set
DecSD (x,(n + 1),k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD
k -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
(Radix k) - 1 is V11() V12() integer ext-real set
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix k) - 1 & (- (Radix k)) + 1 <= b1 ) } is set
SD2SDSub (DecSD (x,(n + 1),k)) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35((n + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
k -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
x mod ((Radix k) |^ n) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DecSD ((x mod ((Radix k) |^ n)),n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of k -SD
SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
y is V6() V10() V11() V12() integer ext-real non negative set
DecSD (y,(n + 1),k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD
SD2SDSub (DecSD (y,(n + 1),k)) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35((n + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
y mod ((Radix k) |^ n) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DecSD ((y mod ((Radix k) |^ n)),n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of k -SD
SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
k is V6() V10() V11() V12() integer ext-real non negative set
(k,((n + 1) + 1),k,(SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k)))) is V11() V12() integer V43() ext-real Element of k -SD_Sub
(k,(n + 1),k,(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))) is V11() V12() integer V43() ext-real Element of k -SD_Sub
Seg (n + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
Seg ((n + 1) + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
X is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(X,((n + 1) + 1),k,(SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k)))) is V11() V12() integer V43() ext-real Element of k -SD_Sub
DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),X) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),X) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),X)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),X)) is V11() V12() integer ext-real set
SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),X)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),X))),k) is V11() V12() integer ext-real set
X -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(X -' 1)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(X -' 1)) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(X -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(X -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(X -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(X -' 1)))),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),X)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),X))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(X -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(X -' 1)))),k)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(X -' 1)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),0) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(X -' 1)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),0) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),0) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),0) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),X) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),X) is V11() V12() integer ext-real set
0 + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),X) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),X)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),X)) is V11() V12() integer ext-real set
SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),X)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),X))),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),X)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),X))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(X -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(X -' 1)))),k)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),X) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),X)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),X)) is V11() V12() integer ext-real set
SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),X)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),X))),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),X)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),X))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(X -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(X -' 1)))),k)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(X -' 1)) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(X -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(X -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(X -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(X -' 1)))),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),X)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),X))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(X -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(X -' 1)))),k)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(X -' 1)) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(X -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(X -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(X -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(X -' 1)))),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),X)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),X))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(X -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(X -' 1)))),k)) is V11() V12() integer ext-real set
(X,(n + 1),k,(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k)))) is V11() V12() integer V43() ext-real Element of k -SD_Sub
n is V6() V10() V11() V12() integer ext-real non negative set
n + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
k is V6() V10() V11() V12() integer ext-real non negative set
k + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
(k + 1) + 1 is V1() V6() V10() V11() V12() integer ext-real positive non negative set
x is V6() V10() V11() V12() integer ext-real non negative set
y is V6() V10() V11() V12() integer ext-real non negative set
k is V6() V10() V11() V12() integer ext-real non negative set
y + k is V6() V10() V11() V12() integer ext-real non negative set
DecSD (y,(k + 1),x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(k + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD
x -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
Radix x is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power x is V11() V12() ext-real set
(Radix x) - 1 is V11() V12() integer ext-real set
- (Radix x) is V11() V12() integer ext-real non positive set
(- (Radix x)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix x) - 1 & (- (Radix x)) + 1 <= b1 ) } is set
SD2SDSub (DecSD (y,(k + 1),x)) is V15() V18( NAT ) V19(x -SD_Sub ) Function-like V35((k + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD_Sub
x -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
DecSD (k,(k + 1),x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(k + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD
SD2SDSub (DecSD (k,(k + 1),x)) is V15() V18( NAT ) V19(x -SD_Sub ) Function-like V35((k + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD_Sub
(((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (k,(k + 1),x)))) is V15() V18( NAT ) V19(x -SD_Sub ) Function-like V35((k + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD_Sub
SDSub2IntOut (((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (k,(k + 1),x)))) is V11() V12() integer ext-real set
Seg ((k + 1) + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
x is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
y is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DecSD (y,(k + 1),x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(k + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD
x -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
Radix x is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power x is V11() V12() ext-real set
(Radix x) - 1 is V11() V12() integer ext-real set
- (Radix x) is V11() V12() integer ext-real non positive set
(- (Radix x)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix x) - 1 & (- (Radix x)) + 1 <= b1 ) } is set
SD2SDSub (DecSD (y,(k + 1),x)) is V15() V18( NAT ) V19(x -SD_Sub ) Function-like V35((k + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD_Sub
x -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1)) is V11() V12() integer ext-real set
SD2SDSubDigitS ((DecSD (y,(k + 1),x)),((k + 1) + 1),x) is V11() V12() integer V43() ext-real Element of x -SD_Sub
SD2SDSubDigit ((DecSD (y,(k + 1),x)),((k + 1) + 1),x) is V11() V12() integer ext-real set
((k + 1) + 1) -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigA ((DecSD (y,(k + 1),x)),(((k + 1) + 1) -' 1)) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (y,(k + 1),x)),(((k + 1) + 1) -' 1))),x) is V11() V12() integer ext-real set
DigA ((DecSD (y,(k + 1),x)),(k + 1)) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (y,(k + 1),x)),(k + 1))),x) is V11() V12() integer ext-real set
X is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DecSD (X,(k + 1),x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(k + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD
SD2SDSub (DecSD (X,(k + 1),x)) is V15() V18( NAT ) V19(x -SD_Sub ) Function-like V35((k + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD_Sub
DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)) is V11() V12() integer ext-real set
SD2SDSubDigitS ((DecSD (X,(k + 1),x)),((k + 1) + 1),x) is V11() V12() integer V43() ext-real Element of x -SD_Sub
SD2SDSubDigit ((DecSD (X,(k + 1),x)),((k + 1) + 1),x) is V11() V12() integer ext-real set
DigA ((DecSD (X,(k + 1),x)),(((k + 1) + 1) -' 1)) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (X,(k + 1),x)),(((k + 1) + 1) -' 1))),x) is V11() V12() integer ext-real set
DigA ((DecSD (X,(k + 1),x)),(k + 1)) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (X,(k + 1),x)),(k + 1))),x) is V11() V12() integer ext-real set
(Radix x) |^ k is V6() V10() V11() V12() integer ext-real non negative set
X mod ((Radix x) |^ k) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
y mod ((Radix x) |^ k) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DecSD ((y mod ((Radix x) |^ k)),k,x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(k) FinSequence-like V60() V61() V62() FinSequence of x -SD
SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x)) is V15() V18( NAT ) V19(x -SD_Sub ) Function-like V35(k + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD_Sub
DecSD ((X mod ((Radix x) |^ k)),k,x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(k) FinSequence-like V60() V61() V62() FinSequence of x -SD
SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)) is V15() V18( NAT ) V19(x -SD_Sub ) Function-like V35(k + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD_Sub
((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))) is V15() V18( NAT ) V19(x -SD_Sub ) Function-like V35(k + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD_Sub
RSDCX is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
len RSDCX is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom RSDCX is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
SDSub2INT ((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))) is V15() V18( NAT ) V19( INT ) Function-like V35(k + 1) FinSequence-like V60() V61() V62() FinSequence of INT
len (SDSub2INT ((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))))) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Seg k is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
SDSub2INTDigit (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1),x) is V11() V12() integer V43() ext-real Element of INT
<*(SDSub2INTDigit (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1),x))*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
RSDCX ^ <*(SDSub2INTDigit (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1),x))*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
RSDCY is V6() V10() V11() V12() integer ext-real non negative set
(SDSub2INT ((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))))) . RSDCY is V11() V12() integer ext-real set
(RSDCX ^ <*(SDSub2INTDigit (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1),x))*>) . RSDCY is V11() V12() integer ext-real set
Seg (k + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
dom (SDSub2INT ((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))))) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
RSDCX . RSDCY is V11() V12() integer ext-real set
SDSub2INTDigit (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),RSDCY,x) is V11() V12() integer V43() ext-real Element of INT
(SDSub2INT ((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))))) /. RSDCY is V11() V12() integer V43() ext-real Element of INT
(SDSub2INT ((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))))) /. (k + 1) is V11() V12() integer V43() ext-real Element of INT
len (RSDCX ^ <*(SDSub2INTDigit (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1),x))*>) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1))) is V11() V12() integer ext-real set
(((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))) is V15() V18( NAT ) V19(x -SD_Sub ) Function-like V35((k + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD_Sub
DIG2 is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
len DIG2 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom DIG2 is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
zp is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
len zp is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom zp is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
RN1 is V6() V10() V11() V12() integer ext-real non negative set
RSDCX . RN1 is V11() V12() integer ext-real set
DIG2 . RN1 is V11() V12() integer ext-real set
Seg (k + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),RN1,x) is V11() V12() integer V43() ext-real Element of INT
RN1 -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix x) |^ (RN1 -' 1) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigB_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),RN1) is V11() V12() integer V43() ext-real Element of INT
((Radix x) |^ (RN1 -' 1)) * (DigB_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),RN1)) is V11() V12() integer ext-real set
DigA_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),RN1) is V11() V12() integer ext-real set
((Radix x) |^ (RN1 -' 1)) * (DigA_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),RN1)) is V11() V12() integer ext-real set
(RN1,((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))) is V11() V12() integer V43() ext-real Element of x -SD_Sub
((Radix x) |^ (RN1 -' 1)) * (RN1,((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))) is V11() V12() integer ext-real set
(RN1,(k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))) is V11() V12() integer V43() ext-real Element of x -SD_Sub
((Radix x) |^ (RN1 -' 1)) * (RN1,(k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))) is V11() V12() integer ext-real set
DigA_SDSub (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),RN1) is V11() V12() integer ext-real set
((Radix x) |^ (RN1 -' 1)) * (DigA_SDSub (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),RN1)) is V11() V12() integer ext-real set
DigB_SDSub (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),RN1) is V11() V12() integer V43() ext-real Element of INT
((Radix x) |^ (RN1 -' 1)) * (DigB_SDSub (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),RN1)) is V11() V12() integer ext-real set
SDSub2INTDigit (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),RN1,x) is V11() V12() integer V43() ext-real Element of INT
(Radix x) |^ (k + 1) is V6() V10() V11() V12() integer ext-real non negative set
(DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1))) is V11() V12() integer ext-real set
SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x) is V11() V12() integer ext-real set
((Radix x) |^ (k + 1)) * (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x)) is V11() V12() integer ext-real set
((Radix x) |^ k) * (DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) is V11() V12() integer ext-real set
((Radix x) |^ k) * (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1))) is V11() V12() integer ext-real set
((Radix x) |^ (k + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (y,(k + 1),x)),(k + 1))),x)) is V11() V12() integer ext-real set
((Radix x) |^ (k + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (X,(k + 1),x)),(k + 1))),x)) is V11() V12() integer ext-real set
DigA ((DecSD (y,(k + 1),x)),k) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (y,(k + 1),x)),k)),x) is V11() V12() integer ext-real set
((Radix x) |^ k) * (SDSub_Add_Carry ((DigA ((DecSD (y,(k + 1),x)),k)),x)) is V11() V12() integer ext-real set
DigA ((DecSD (X,(k + 1),x)),k) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (X,(k + 1),x)),k)),x) is V11() V12() integer ext-real set
((Radix x) |^ k) * (SDSub_Add_Carry ((DigA ((DecSD (X,(k + 1),x)),k)),x)) is V11() V12() integer ext-real set
DecSD (y,k,x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(k) FinSequence-like V60() V61() V62() FinSequence of x -SD
DigA ((DecSD (y,k,x)),k) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x) is V11() V12() integer ext-real set
((Radix x) |^ k) * (SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) is V11() V12() integer ext-real set
DecSD (X,k,x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(k) FinSequence-like V60() V61() V62() FinSequence of x -SD
DigA ((DecSD (X,k,x)),k) is V11() V12() integer ext-real set
SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x) is V11() V12() integer ext-real set
((Radix x) |^ k) * (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k)) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x) is V11() V12() integer ext-real set
((Radix x) |^ k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x)) is V11() V12() integer ext-real set
SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),((k + 1) + 1),x) is V11() V12() integer V43() ext-real Element of INT
(Radix x) |^ (((k + 1) + 1) -' 1) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigB_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),((k + 1) + 1)) is V11() V12() integer V43() ext-real Element of INT
((Radix x) |^ (((k + 1) + 1) -' 1)) * (DigB_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),((k + 1) + 1))) is V11() V12() integer ext-real set
DigA_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),((k + 1) + 1)) is V11() V12() integer ext-real set
((Radix x) |^ (((k + 1) + 1) -' 1)) * (DigA_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),((k + 1) + 1))) is V11() V12() integer ext-real set
((Radix x) |^ (k + 1)) * (DigA_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),((k + 1) + 1))) is V11() V12() integer ext-real set
(((k + 1) + 1),((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))) is V11() V12() integer V43() ext-real Element of x -SD_Sub
((Radix x) |^ (k + 1)) * (((k + 1) + 1),((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(((k + 1) + 1) -' 1)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(((k + 1) + 1) -' 1)) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(((k + 1) + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(((k + 1) + 1) -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(((k + 1) + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(((k + 1) + 1) -' 1)))),x) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(((k + 1) + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(((k + 1) + 1) -' 1)))),x)) is V11() V12() integer ext-real set
((Radix x) |^ (k + 1)) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(((k + 1) + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(((k + 1) + 1) -' 1)))),x))) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(((k + 1) + 1) -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(((k + 1) + 1) -' 1)))),x) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(((k + 1) + 1) -' 1)))),x)) is V11() V12() integer ext-real set
((Radix x) |^ (k + 1)) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(((k + 1) + 1) -' 1)))),x))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)) is V11() V12() integer ext-real set
((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x))) + 0 is V11() V12() integer ext-real set
((Radix x) |^ (k + 1)) * (((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x))) + 0) is V11() V12() integer ext-real set
((Radix x) |^ (k + 1)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)) is V11() V12() integer ext-real set
(((Radix x) |^ (k + 1)) * (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x))) + (((Radix x) |^ (k + 1)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x) is V11() V12() integer ext-real set
(Radix x) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x)) is V11() V12() integer ext-real set
((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))) - ((Radix x) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x))) is V11() V12() integer ext-real set
((Radix x) |^ (k + 1)) * (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))) - ((Radix x) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x)))) is V11() V12() integer ext-real set
(Radix x) * 0 is V6() V10() V11() V12() integer ext-real non negative set
((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))) - ((Radix x) * 0) is V11() V12() integer ext-real set
((Radix x) |^ (k + 1)) * (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))) - ((Radix x) * 0)) is V11() V12() integer ext-real set
(SDSub_Add_Carry ((DigA ((DecSD (y,(k + 1),x)),(k + 1))),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,(k + 1),x)),(k + 1))),x)) is V11() V12() integer ext-real set
((Radix x) |^ (k + 1)) * ((SDSub_Add_Carry ((DigA ((DecSD (y,(k + 1),x)),(k + 1))),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,(k + 1),x)),(k + 1))),x))) is V11() V12() integer ext-real set
((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))) is V11() V12() integer ext-real set
y div ((Radix x) |^ k) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
((Radix x) |^ k) * (y div ((Radix x) |^ k)) is V6() V10() V11() V12() integer ext-real non negative set
(y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k)) is V6() V10() V11() V12() integer ext-real non negative set
SDSub2IntOut ((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))) is V11() V12() integer ext-real set
Sum (SDSub2INT ((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))))) is V11() V12() integer V43() ext-real Element of INT
((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + 0 is V6() V10() V11() V12() integer ext-real non negative set
Sum RSDCX is V11() V12() integer V43() ext-real Element of INT
(Sum RSDCX) + (SDSub2INTDigit (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1),x)) is V11() V12() integer ext-real set
(SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x)) is V11() V12() integer ext-real set
SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))),x) is V11() V12() integer ext-real set
SDSub_Add_Carry (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))),x) is V11() V12() integer ext-real set
(Radix x) * (SDSub_Add_Carry (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))),x)) is V11() V12() integer ext-real set
((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))) - ((Radix x) * (SDSub_Add_Carry (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))),x))) is V11() V12() integer ext-real set
((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))) - ((Radix x) * 0) is V11() V12() integer ext-real set
Seg (k + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),(k + 1),x) is V11() V12() integer V43() ext-real Element of INT
<*(SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),(k + 1),x))*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
DIG2 ^ <*(SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),(k + 1),x))*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
j is V6() V10() V11() V12() integer ext-real non negative set
zp . j is V11() V12() integer ext-real set
(DIG2 ^ <*(SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),(k + 1),x))*>) . j is V11() V12() integer ext-real set
DIG2 . j is V11() V12() integer ext-real set
SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),j,x) is V11() V12() integer V43() ext-real Element of INT
SDSub2INT (((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))) is V15() V18( NAT ) V19( INT ) Function-like V35((k + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of INT
len (SDSub2INT (((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x))))) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
<*(SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),((k + 1) + 1),x))*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
zp ^ <*(SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),((k + 1) + 1),x))*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
j is V6() V10() V11() V12() integer ext-real non negative set
(SDSub2INT (((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x))))) . j is V11() V12() integer ext-real set
(zp ^ <*(SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),((k + 1) + 1),x))*>) . j is V11() V12() integer ext-real set
dom (SDSub2INT (((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x))))) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
zp . j is V11() V12() integer ext-real set
SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),j,x) is V11() V12() integer V43() ext-real Element of INT
(SDSub2INT (((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x))))) /. j is V11() V12() integer V43() ext-real Element of INT
(SDSub2INT (((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x))))) /. ((k + 1) + 1) is V11() V12() integer V43() ext-real Element of INT
len (DIG2 ^ <*(SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),(k + 1),x))*>) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
len (zp ^ <*(SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),((k + 1) + 1),x))*>) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Sum (SDSub2INT (((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x))))) is V11() V12() integer V43() ext-real Element of INT
Sum zp is V11() V12() integer V43() ext-real Element of INT
(Sum zp) + (SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),((k + 1) + 1),x)) is V11() V12() integer ext-real set
(Sum RSDCX) + (SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),(k + 1),x)) is V11() V12() integer ext-real set
((Sum RSDCX) + (SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),(k + 1),x))) + (SDSub2INTDigit ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),((k + 1) + 1),x)) is V11() V12() integer ext-real set
(k + 1) -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix x) |^ ((k + 1) -' 1) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigB_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),(k + 1)) is V11() V12() integer V43() ext-real Element of INT
((Radix x) |^ ((k + 1) -' 1)) * (DigB_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),(k + 1))) is V11() V12() integer ext-real set
DigA_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),(k + 1)) is V11() V12() integer ext-real set
((Radix x) |^ ((k + 1) -' 1)) * (DigA_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),(k + 1))) is V11() V12() integer ext-real set
((Radix x) |^ k) * (DigA_SDSub ((((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))),(k + 1))) is V11() V12() integer ext-real set
((k + 1),((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))) is V11() V12() integer V43() ext-real Element of x -SD_Sub
((Radix x) |^ k) * ((k + 1),((k + 1) + 1),x,(SD2SDSub (DecSD (y,(k + 1),x))),(SD2SDSub (DecSD (X,(k + 1),x)))) is V11() V12() integer ext-real set
SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) -' 1)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) -' 1)) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) -' 1)))),x) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) -' 1)))),x)) is V11() V12() integer ext-real set
((Radix x) |^ k) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) -' 1)))),x))) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) -' 1)))),x) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) -' 1)))),x)) is V11() V12() integer ext-real set
((Radix x) |^ k) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) -' 1)))),x))) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x)) is V11() V12() integer ext-real set
((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x))) + 0 is V11() V12() integer ext-real set
((Radix x) |^ k) * (((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x))) + 0) is V11() V12() integer ext-real set
((Radix x) |^ k) * (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)) is V11() V12() integer ext-real set
(((Radix x) |^ k) * (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x))) + (((Radix x) |^ k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x))) is V11() V12() integer ext-real set
(Radix x) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)) is V11() V12() integer ext-real set
((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))) - ((Radix x) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x))) is V11() V12() integer ext-real set
((Radix x) |^ k) * (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))) - ((Radix x) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)))) is V11() V12() integer ext-real set
(((Radix x) |^ k) * (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))) - ((Radix x) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x))))) + (((Radix x) |^ k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x))) is V11() V12() integer ext-real set
((Radix x) |^ k) * ((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))) is V11() V12() integer ext-real set
((Radix x) |^ k) * (Radix x) is V6() V10() V11() V12() integer ext-real non negative set
(((Radix x) |^ k) * (Radix x)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)) is V11() V12() integer ext-real set
(((Radix x) |^ k) * ((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1))))) - ((((Radix x) |^ k) * (Radix x)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x))) is V11() V12() integer ext-real set
((((Radix x) |^ k) * ((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1))))) - ((((Radix x) |^ k) * (Radix x)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)))) + (((Radix x) |^ k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x))) is V11() V12() integer ext-real set
(((Radix x) |^ k) * ((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1))))) - (((Radix x) |^ (k + 1)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x))) is V11() V12() integer ext-real set
((((Radix x) |^ k) * ((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1))))) - (((Radix x) |^ (k + 1)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)))) + (((Radix x) |^ k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x))) is V11() V12() integer ext-real set
- (((Radix x) |^ (k + 1)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x))) is V11() V12() integer ext-real set
(((Radix x) |^ k) * ((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1))))) + (- (((Radix x) |^ (k + 1)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x)))) is V11() V12() integer ext-real set
((((Radix x) |^ k) * ((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1))))) + (- (((Radix x) |^ (k + 1)) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))),x))))) + (((Radix x) |^ k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x))) is V11() V12() integer ext-real set
((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * ((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1))))) is V11() V12() integer ext-real set
- (SDSub2INTDigit (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1),x)) is V11() V12() integer ext-real set
(- (SDSub2INTDigit (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1),x))) + (((Radix x) |^ k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x))) is V11() V12() integer ext-real set
(((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * ((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))))) + ((- (SDSub2INTDigit (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1),x))) + (((Radix x) |^ k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x)))) is V11() V12() integer ext-real set
((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * ((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),(k + 1)))))) + ((- (SDSub2INTDigit (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1),x))) + (((Radix x) |^ k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x))))) + (((Radix x) |^ (k + 1)) * (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),((k + 1) + 1))) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),((k + 1) + 1)))),x))) is V11() V12() integer ext-real set
DigB_SDSub (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1)) is V11() V12() integer V43() ext-real Element of INT
((Radix x) |^ ((k + 1) -' 1)) * (DigB_SDSub (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1))) is V11() V12() integer ext-real set
DigA_SDSub (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1)) is V11() V12() integer ext-real set
((Radix x) |^ ((k + 1) -' 1)) * (DigA_SDSub (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1))) is V11() V12() integer ext-real set
((Radix x) |^ k) * (DigA_SDSub (((k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))),(k + 1))) is V11() V12() integer ext-real set
((k + 1),(k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))) is V11() V12() integer V43() ext-real Element of x -SD_Sub
((Radix x) |^ k) * ((k + 1),(k + 1),x,(SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x)))) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(k + 1)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1)) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1))) is V11() V12() integer ext-real set
SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1)))),x) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1)) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1)))),x) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1)))),x)) is V11() V12() integer ext-real set
((Radix x) |^ k) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1)))),x))) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1)))),x) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1)))),x)) is V11() V12() integer ext-real set
((Radix x) |^ k) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),((k + 1) -' 1)))),x))) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k)) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k))),x) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k))),x)) is V11() V12() integer ext-real set
((Radix x) |^ k) * ((SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),(k + 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k))),x))) is V11() V12() integer ext-real set
(SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1))) is V11() V12() integer ext-real set
SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1)))),x) is V11() V12() integer ext-real set
(SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k))),x)) is V11() V12() integer ext-real set
((Radix x) |^ k) * ((SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),(k + 1)))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k))),x))) is V11() V12() integer ext-real set
(SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k))),x)) is V11() V12() integer ext-real set
((Radix x) |^ k) * ((SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix x) |^ k)),k,x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k))),x))) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k)) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k))),x) is V11() V12() integer ext-real set
(SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k))),x)) is V11() V12() integer ext-real set
((Radix x) |^ k) * ((SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD ((X mod ((Radix x) |^ k)),k,x))),k))),x))) is V11() V12() integer ext-real set
(SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x)) is V11() V12() integer ext-real set
((Radix x) |^ k) * ((SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))),x)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x))) is V11() V12() integer ext-real set
((Radix x) |^ k) * (SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))),x)) is V11() V12() integer ext-real set
(((Radix x) |^ k) * (SDSub_Add_Data (((SDSub_Add_Carry ((DigA ((DecSD (y,k,x)),k)),x)) + (SDSub_Add_Carry ((DigA ((DecSD (X,k,x)),k)),x))),x))) + (((Radix x) |^ k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (y,(k + 1),x))),k)) + (DigA_SDSub ((SD2SDSub (DecSD (X,(k + 1),x))),k))),x))) is V11() V12() integer ext-real set
RNDx11 is V11() V12() integer ext-real set
((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + RNDx11 is V11() V12() integer ext-real set
RNDy11 is V11() V12() integer ext-real set
(((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + RNDx11) + RNDy11 is V11() V12() integer ext-real set
RNCx is V11() V12() integer ext-real set
RNCy is V11() V12() integer ext-real set
RNCx + RNCy is V11() V12() integer ext-real set
- (RNCx + RNCy) is V11() V12() integer ext-real set
((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + RNDx11) + RNDy11) + (- (RNCx + RNCy)) is V11() V12() integer ext-real set
RN1Cx11 is V11() V12() integer ext-real set
RN1Cy11 is V11() V12() integer ext-real set
RN1Cx11 + RN1Cy11 is V11() V12() integer ext-real set
(((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + RNDx11) + RNDy11) + (- (RNCx + RNCy))) + (RN1Cx11 + RN1Cy11) is V11() V12() integer ext-real set
(((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1)))) - RN1Cx11 is V11() V12() integer ext-real set
RNCx1 is V11() V12() integer ext-real set
((((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1)))) - RN1Cx11) + RNCx1 is V11() V12() integer ext-real set
((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1)))) - RN1Cx11) + RNCx1) is V11() V12() integer ext-real set
(((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1)))) - RN1Cx11) + RNCx1)) + RNDy11 is V11() V12() integer ext-real set
((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1)))) - RN1Cx11) + RNCx1)) + RNDy11) + (- (RNCx + RNCy)) is V11() V12() integer ext-real set
(((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1)))) - RN1Cx11) + RNCx1)) + RNDy11) + (- (RNCx + RNCy))) + (RN1Cx11 + RN1Cy11) is V11() V12() integer ext-real set
((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1)))) is V11() V12() integer ext-real set
(((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1 is V11() V12() integer ext-real set
((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + RNDy11 is V11() V12() integer ext-real set
(((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + RNDy11) + RN1Cy11 is V11() V12() integer ext-real set
((((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + RNDy11) + RN1Cy11) - (RNCx + RNCy) is V11() V12() integer ext-real set
((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1))) is V11() V12() integer ext-real set
(((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1)))) - RN1Cy11 is V11() V12() integer ext-real set
RNCy1 is V11() V12() integer ext-real set
((((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1)))) - RN1Cy11) + RNCy1 is V11() V12() integer ext-real set
((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + (((((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1)))) - RN1Cy11) + RNCy1) is V11() V12() integer ext-real set
(((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + (((((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1)))) - RN1Cy11) + RNCy1)) + RN1Cy11 is V11() V12() integer ext-real set
((((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + (((((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1)))) - RN1Cy11) + RNCy1)) + RN1Cy11) - (RNCx + RNCy) is V11() V12() integer ext-real set
((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + (((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1)))) is V11() V12() integer ext-real set
- RN1Cy11 is V11() V12() integer ext-real set
(((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + (((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1))))) + (- RN1Cy11) is V11() V12() integer ext-real set
((((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + (((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1))))) + (- RN1Cy11)) + RNCy1 is V11() V12() integer ext-real set
(((((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + (((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1))))) + (- RN1Cy11)) + RNCy1) + RN1Cy11 is V11() V12() integer ext-real set
((((((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + (((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1))))) + (- RN1Cy11)) + RNCy1) + RN1Cy11) + (- (RNCx + RNCy)) is V11() V12() integer ext-real set
(((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + (((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1))))) + RNCy1 is V11() V12() integer ext-real set
RNCx1 + RNCy is V11() V12() integer ext-real set
- (RNCx1 + RNCy) is V11() V12() integer ext-real set
((((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + (((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1))))) + RNCy1) + (- (RNCx1 + RNCy)) is V11() V12() integer ext-real set
RNCx1 + RNCy1 is V11() V12() integer ext-real set
- (RNCx1 + RNCy1) is V11() V12() integer ext-real set
((((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + RNCx1) + (((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1))))) + RNCy1) + (- (RNCx1 + RNCy1)) is V11() V12() integer ext-real set
(((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + 0 is V11() V12() integer ext-real set
((((y mod ((Radix x) |^ k)) + (X mod ((Radix x) |^ k))) + (((Radix x) |^ k) * (DigA ((DecSD (y,(k + 1),x)),(k + 1))))) + 0) + (((Radix x) |^ k) * (DigA ((DecSD (X,(k + 1),x)),(k + 1)))) is V11() V12() integer ext-real set
X div ((Radix x) |^ k) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(X div ((Radix x) |^ k)) * ((Radix x) |^ k) is V6() V10() V11() V12() integer ext-real non negative set
((X div ((Radix x) |^ k)) * ((Radix x) |^ k)) + (X mod ((Radix x) |^ k)) is V6() V10() V11() V12() integer ext-real non negative set
(y div ((Radix x) |^ k)) * ((Radix x) |^ k) is V6() V10() V11() V12() integer ext-real non negative set
((y div ((Radix x) |^ k)) * ((Radix x) |^ k)) + (y mod ((Radix x) |^ k)) is V6() V10() V11() V12() integer ext-real non negative set
(X mod ((Radix x) |^ k)) + y is V6() V10() V11() V12() integer ext-real non negative set
((Radix x) |^ k) * (X div ((Radix x) |^ k)) is V6() V10() V11() V12() integer ext-real non negative set
((X mod ((Radix x) |^ k)) + y) + (((Radix x) |^ k) * (X div ((Radix x) |^ k))) is V6() V10() V11() V12() integer ext-real non negative set
k is V6() V10() V11() V12() integer ext-real non negative set
x is V6() V10() V11() V12() integer ext-real non negative set
y is V6() V10() V11() V12() integer ext-real non negative set
x + y is V6() V10() V11() V12() integer ext-real non negative set
DecSD (x,1,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(1) FinSequence-like V60() V61() V62() FinSequence of k -SD
k -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
Radix k is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
(Radix k) - 1 is V11() V12() integer ext-real set
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix k) - 1 & (- (Radix k)) + 1 <= b1 ) } is set
SD2SDSub (DecSD (x,1,k)) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(1 + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
k -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
DecSD (y,1,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(1) FinSequence-like V60() V61() V62() FinSequence of k -SD
SD2SDSub (DecSD (y,1,k)) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(1 + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(1 + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
SDSub2IntOut ((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))) is V11() V12() integer ext-real set
k is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
x is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DecSD (x,1,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(1) FinSequence-like V60() V61() V62() FinSequence of k -SD
k -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
Radix k is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
(Radix k) - 1 is V11() V12() integer ext-real set
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix k) - 1 & (- (Radix k)) + 1 <= b1 ) } is set
SD2SDSub (DecSD (x,1,k)) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(1 + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
k -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
y is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DecSD (y,1,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(1) FinSequence-like V60() V61() V62() FinSequence of k -SD
SD2SDSub (DecSD (y,1,k)) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(1 + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1)) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k) is V11() V12() integer ext-real set
((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(1 + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
DigA_SDSub (((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))),1) is V11() V12() integer ext-real set
SDSub_Add_Carry (x,k) is V11() V12() integer ext-real set
(Radix k) * (SDSub_Add_Carry (x,k)) is V11() V12() integer ext-real set
SDSub_Add_Carry (y,k) is V11() V12() integer ext-real set
(Radix k) * (SDSub_Add_Carry (y,k)) is V11() V12() integer ext-real set
(Radix k) * (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) is V11() V12() integer ext-real set
Seg (1 + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
SDSub2INT ((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))) is V15() V18( NAT ) V19( INT ) Function-like V35(1 + 1) FinSequence-like V60() V61() V62() FinSequence of INT
(SDSub2INT ((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k))))) /. 1 is V11() V12() integer V43() ext-real Element of INT
SDSub2INTDigit (((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))),1,k) is V11() V12() integer V43() ext-real Element of INT
1 -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix k) |^ (1 -' 1) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigB_SDSub (((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))),1) is V11() V12() integer V43() ext-real Element of INT
((Radix k) |^ (1 -' 1)) * (DigB_SDSub (((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))),1)) is V11() V12() integer ext-real set
(Radix k) |^ 0 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
((Radix k) |^ 0) * (DigB_SDSub (((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))),1)) is V11() V12() integer ext-real set
1 * (DigB_SDSub (((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))),1)) is V11() V12() integer ext-real set
len (SDSub2INT ((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k))))) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom (SDSub2INT ((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k))))) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
(SDSub2INT ((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k))))) . 1 is V11() V12() integer ext-real set
DIG1 is V11() V12() integer V43() ext-real Element of INT
2 - 1 is V11() V12() integer ext-real set
2 -' 1 is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(1,(1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))) is V11() V12() integer V43() ext-real Element of k -SD_Sub
SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),(1 -' 1)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(1 -' 1)) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),(1 -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(1 -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),(1 -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(1 -' 1)))),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),(1 -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(1 -' 1)))),k)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),0) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),0)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(1 -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),0)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(1 -' 1)))),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),0)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(1 -' 1)))),k)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),0) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),0)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),0)) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),0)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),0))),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),0)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),0))),k)) is V11() V12() integer ext-real set
0 + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),0)) is V11() V12() integer ext-real set
SDSub_Add_Carry ((0 + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),0))),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) + (SDSub_Add_Carry ((0 + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),0))),k)) is V11() V12() integer ext-real set
0 + 0 is V6() V10() V11() V12() integer ext-real non negative set
SDSub_Add_Carry ((0 + 0),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) + (SDSub_Add_Carry ((0 + 0),k)) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))),k)) + 0 is V11() V12() integer ext-real set
CRY1 is V11() V12() integer ext-real set
(Radix k) * CRY1 is V11() V12() integer ext-real set
((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))) - ((Radix k) * CRY1) is V11() V12() integer ext-real set
RSDCX is V11() V12() integer ext-real set
x - RSDCX is V11() V12() integer ext-real set
(x - RSDCX) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1)) is V11() V12() integer ext-real set
RCRY1 is V11() V12() integer ext-real set
((x - RSDCX) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),1))) - RCRY1 is V11() V12() integer ext-real set
RSDCY is V11() V12() integer ext-real set
y - RSDCY is V11() V12() integer ext-real set
(x - RSDCX) + (y - RSDCY) is V11() V12() integer ext-real set
((x - RSDCX) + (y - RSDCY)) - RCRY1 is V11() V12() integer ext-real set
x + y is V6() V10() V11() V12() integer ext-real non negative set
(x + y) - RSDCX is V11() V12() integer ext-real set
((x + y) - RSDCX) - RSDCY is V11() V12() integer ext-real set
(((x + y) - RSDCX) - RSDCY) - RCRY1 is V11() V12() integer ext-real set
DigA_SDSub (((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))),2) is V11() V12() integer ext-real set
(Radix k) * (DigA_SDSub (((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))),2)) is V11() V12() integer ext-real set
(SDSub2INT ((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k))))) /. 2 is V11() V12() integer V43() ext-real Element of INT
SDSub2INTDigit (((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))),2,k) is V11() V12() integer V43() ext-real Element of INT
(Radix k) |^ (2 -' 1) is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigB_SDSub (((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))),2) is V11() V12() integer V43() ext-real Element of INT
((Radix k) |^ (2 -' 1)) * (DigB_SDSub (((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))),2)) is V11() V12() integer ext-real set
(Radix k) * (DigB_SDSub (((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))),2)) is V11() V12() integer ext-real set
(SDSub2INT ((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k))))) . 2 is V11() V12() integer ext-real set
DIG2 is V11() V12() integer V43() ext-real Element of INT
<*DIG1,DIG2*> is set
Sum (SDSub2INT ((1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k))))) is V11() V12() integer V43() ext-real Element of INT
DIG1 + DIG2 is V11() V12() integer ext-real set
(2,(1 + 1),k,(SD2SDSub (DecSD (x,1,k))),(SD2SDSub (DecSD (y,1,k)))) is V11() V12() integer V43() ext-real Element of k -SD_Sub
DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),2) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),2) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),2)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),2)) is V11() V12() integer ext-real set
SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),2)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),2))),k) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),(2 -' 1)) is V11() V12() integer ext-real set
DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(2 -' 1)) is V11() V12() integer ext-real set
(DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),(2 -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(2 -' 1))) is V11() V12() integer ext-real set
SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),(2 -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(2 -' 1)))),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),2)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),2))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,1,k))),(2 -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),(2 -' 1)))),k)) is V11() V12() integer ext-real set
(SDSub_Add_Carry (x,k)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),2)) is V11() V12() integer ext-real set
SDSub_Add_Data (((SDSub_Add_Carry (x,k)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),2))),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((SDSub_Add_Carry (x,k)) + (DigA_SDSub ((SD2SDSub (DecSD (y,1,k))),2))),k)) + CRY1 is V11() V12() integer ext-real set
(SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k)) is V11() V12() integer ext-real set
SDSub_Add_Data (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k) is V11() V12() integer ext-real set
(SDSub_Add_Data (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k)) + CRY1 is V11() V12() integer ext-real set
SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k) is V11() V12() integer ext-real set
(Radix k) * (SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k)) is V11() V12() integer ext-real set
((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))) - ((Radix k) * (SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k))) is V11() V12() integer ext-real set
(((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))) - ((Radix k) * (SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k)))) + CRY1 is V11() V12() integer ext-real set
(Radix k) * 0 is V6() V10() V11() V12() integer ext-real non negative set
((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))) - ((Radix k) * 0) is V11() V12() integer ext-real set
(((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))) - ((Radix k) * 0)) + CRY1 is V11() V12() integer ext-real set
((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))) - 0 is V11() V12() integer ext-real set
(((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))) - 0) + CRY1 is V11() V12() integer ext-real set
k is V6() V10() V11() V12() integer ext-real non negative set
x is V6() V10() V11() V12() integer ext-real non negative set
y is V6() V10() V11() V12() integer ext-real non negative set
x + y is V6() V10() V11() V12() integer ext-real non negative set
DecSD (x,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of k -SD
k -SD is V1() V70() V71() V72() V73() V74() Element of K6(INT)
Radix k is V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
(Radix k) - 1 is V11() V12() integer ext-real set
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer V43() ext-real Element of INT : ( b1 <= (Radix k) - 1 & (- (Radix k)) + 1 <= b1 ) } is set
SD2SDSub (DecSD (x,n,k)) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
k -SD_Sub is V1() V70() V71() V72() V73() V74() Element of K6(INT)
DecSD (y,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of k -SD
SD2SDSub (DecSD (y,n,k)) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
((n + 1),k,(SD2SDSub (DecSD (x,n,k))),(SD2SDSub (DecSD (y,n,k)))) is V15() V18( NAT ) V19(k -SD_Sub ) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD_Sub
SDSub2IntOut ((n + 1),k,(SD2SDSub (DecSD (x,n,k))),(SD2SDSub (DecSD (y,n,k)))) is V11() V12() integer ext-real set