:: RADIX_5 semantic presentation

begin

theorem :: RADIX_5:1
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) - 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() V13() ext-real ) set ) in k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: RADIX_5:2
for i, n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) > 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) & i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -' 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) in Seg n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: RADIX_5:3
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) holds
4 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) <= Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_5:4
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat)
for tx being ( ( V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) Tuple of 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds SDDec tx : ( ( V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) Tuple of 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = DigA (tx : ( ( V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) Tuple of 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) ;

begin

theorem :: RADIX_5:5
for i, k, n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
DigA ((DecSD (0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_5:6
for n, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
SDDec (DecSD (0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_5:7
for k, n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) in Seg n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
DigA ((DecSD (1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) FinSequence of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_5:8
for i, k, n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) > 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
DigA ((DecSD (1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_5:9
for n, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
SDDec (DecSD (1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_5:10
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
SD_Add_Carry (Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_5:11
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
SD_Add_Data ((Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;

begin

theorem :: RADIX_5:12
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat)
for tx, ty being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) st ( for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
DigA (tx : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = DigA (ty : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) ) holds
SDDec tx : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = SDDec ty : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) ;

theorem :: RADIX_5:13
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat)
for tx, ty being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) st ( for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
DigA (tx : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) >= DigA (ty : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) ) holds
SDDec tx : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) >= SDDec ty : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) ;

theorem :: RADIX_5:14
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for tx, ty, tz, tw being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) st ( for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) holds
( not i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) or ( DigA (tx : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = DigA (tz : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) & DigA (ty : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = DigA (tw : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) ) or ( DigA (ty : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = DigA (tz : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) & DigA (tx : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = DigA (tw : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) ) ) ) holds
(SDDec tz : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) + (SDDec tw : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) : ( ( ) ( V11() V12() V13() ext-real ) set ) = (SDDec tx : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) + (SDDec ty : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) : ( ( ) ( V11() V12() V13() ext-real ) set ) ;

theorem :: RADIX_5:15
for n, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for tx, ty, tz being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) st ( for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) holds
( not i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) or ( DigA (tx : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = DigA (tz : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) & DigA (ty : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) or ( DigA (ty : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = DigA (tz : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) & DigA (tx : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ) holds
(SDDec tz : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) + (SDDec (DecSD (0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) : ( ( ) ( V11() V12() V13() ext-real ) set ) = (SDDec tx : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) + (SDDec ty : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) : ( ( ) ( V11() V12() V13() ext-real ) set ) ;

begin

definition
let i, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ;
assume k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func SDMinDigit (m,k,i) -> ( ( ) ( ) Element of k : ( ( ) ( ) Element of i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_5:def 1
(- (Radix k : ( ( ) ( ) Element of i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V11() ) ( V11() V12() V13() ext-real non positive ) set ) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() V13() ext-real ) set ) if ( 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) & i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) < m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) set ) )
otherwise 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let n, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ;
func SDMin (n,m,k) -> ( ( V35(n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) FinSequence-like ) Tuple of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ,k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) means :: RADIX_5:def 2
 for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
DigA (it : ( ( ) ( ) set ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = SDMinDigit (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) set ) ,k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( ) ( ) Element of k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let i, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ;
assume k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func SDMaxDigit (m,k,i) -> ( ( ) ( ) Element of k : ( ( ) ( ) Element of i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_5:def 3
(Radix k : ( ( ) ( ) Element of i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) - 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() V13() ext-real ) set ) if ( 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) & i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) < m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) set ) )
otherwise 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let n, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ;
func SDMax (n,m,k) -> ( ( V35(n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) FinSequence-like ) Tuple of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ,k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) means :: RADIX_5:def 4
 for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
DigA (it : ( ( ) ( ) set ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = SDMaxDigit (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) set ) ,k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( ) ( ) Element of k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let i, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ;
assume k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func FminDigit (m,k,i) -> ( ( ) ( ) Element of k : ( ( ) ( ) Element of i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_5:def 5
1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) if i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) = m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) set )
otherwise 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let n, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ;
func Fmin (n,m,k) -> ( ( V35(n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) FinSequence-like ) Tuple of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ,k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) means :: RADIX_5:def 6
 for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
DigA (it : ( ( ) ( ) set ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = FminDigit (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) set ) ,k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( ) ( ) Element of k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let i, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ;
assume k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func FmaxDigit (m,k,i) -> ( ( ) ( ) Element of k : ( ( ) ( ) Element of i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_5:def 7
(Radix k : ( ( ) ( ) Element of i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) - 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() V13() ext-real ) set ) if i : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) = m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) set )
otherwise 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let n, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ;
func Fmax (n,m,k) -> ( ( V35(n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) FinSequence-like ) Tuple of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ,k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) means :: RADIX_5:def 8
 for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
DigA (it : ( ( ) ( ) set ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = FmaxDigit (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) set ) ,k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) : ( ( ) ( ) Element of k : ( ( ) ( ) Element of n : ( ( ) ( V15() Function-like FinSequence-like ) FinSequence of INT : ( ( ) ( V1() V28() ) set ) ) ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

begin

theorem :: RADIX_5:16
for n, m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
(DigA ((SDMax (n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) + (DigA ((SDMin (n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) : ( ( ) ( V11() V12() V13() ext-real ) set ) = 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_5:17
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(SDDec (SDMax (n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) + (SDDec (SDMin (n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) : ( ( ) ( V11() V12() V13() ext-real ) set ) = SDDec (DecSD (0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() V13() ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) FinSequence of b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) ;

theorem :: RADIX_5:18
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
SDDec (Fmin (n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = (SDDec (SDMax (n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) + (SDDec (DecSD (1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ) FinSequence-like ) FinSequence of b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) : ( ( ) ( V11() V12() V13() ext-real ) set ) ;

theorem :: RADIX_5:19
for n, m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) holds
SDDec (Fmin ((n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ,(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) = (SDDec (Fmin ((n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) + (SDDec (Fmax ((n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() V13() ext-real positive non negative ) set ) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() V13() ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( V1() V28() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V13() ) ( V11() V12() V13() ext-real ) set ) : ( ( ) ( V11() V12() V13() ext-real ) set ) ;