:: RADIX_6 semantic presentation

begin

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

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

begin

definition
let i, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let r be ( ( V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
assume i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) in Seg (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;
func M0Digit (r,i) -> ( ( ) ( ) Element of k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_6:def 1
r : ( ( ) ( ) set ) . i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) : ( ( ) ( ) set ) if i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) >= m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set )
otherwise 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

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

definition
let i, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let r be ( ( V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
assume that
k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) and
i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) in Seg (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;
func MmaxDigit (r,i) -> ( ( ) ( ) Element of k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_6:def 3
r : ( ( ) ( ) set ) . i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) : ( ( ) ( ) set ) if i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) >= m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set )
otherwise (Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) - 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;
end;

definition
let m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let r be ( ( V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
func Mmax r -> ( ( V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) means :: RADIX_6:def 4
 for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) in Seg (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
DigA (it : ( ( ) ( ) set ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = MmaxDigit (r : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( ) Element of k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let i, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let r be ( ( V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
assume that
k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) and
i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) in Seg (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;
func MminDigit (r,i) -> ( ( ) ( ) Element of k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_6:def 5
r : ( ( ) ( ) set ) . i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) : ( ( ) ( ) set ) if i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) >= m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set )
otherwise (- (Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V11() ) ( V11() V12() integer ext-real non positive ) set ) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;
end;

definition
let m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let r be ( ( V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
func Mmin r -> ( ( V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) means :: RADIX_6:def 6
 for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) in Seg (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
DigA (it : ( ( ) ( ) set ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = MminDigit (r : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( ) Element of k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

theorem :: RADIX_6:3
for m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds SDDec (Mmax r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) >= SDDec r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_6:4
for m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds SDDec r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) >= SDDec (Mmin r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

begin

definition
let n, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let x be ( ( integer ) ( V11() V12() integer ext-real ) Integer) ;
pred x needs_digits_of n,k means :: RADIX_6:def 7
( x : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) < (Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) & x : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) >= (Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ (n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -' 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) );
end;

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

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

theorem :: RADIX_6:7
for f, m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) needs_digits_of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= SDDec (Fmin ((m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) FinSequence of b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

begin

theorem :: RADIX_6:8
for mlow, mhigh, f being ( ( integer ) ( V11() V12() integer ext-real ) Integer) st mhigh : ( ( integer ) ( V11() V12() integer ext-real ) Integer) < mlow : ( ( integer ) ( V11() V12() integer ext-real ) Integer) + f : ( ( integer ) ( V11() V12() integer ext-real ) Integer) : ( ( ) ( V11() V12() integer ext-real ) set ) & f : ( ( integer ) ( V11() V12() integer ext-real ) Integer) > 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
ex s being ( ( integer ) ( V11() V12() integer ext-real ) Integer) st
( - f : ( ( integer ) ( V11() V12() integer ext-real ) Integer) : ( ( V11() ) ( V11() V12() integer ext-real ) set ) < mlow : ( ( integer ) ( V11() V12() integer ext-real ) Integer) - (s : ( ( integer ) ( V11() V12() integer ext-real ) Integer) * f : ( ( integer ) ( V11() V12() integer ext-real ) Integer) ) : ( ( ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) & mhigh : ( ( integer ) ( V11() V12() integer ext-real ) Integer) - (s : ( ( integer ) ( V11() V12() integer ext-real ) Integer) * f : ( ( integer ) ( V11() V12() integer ext-real ) Integer) ) : ( ( ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) < f : ( ( integer ) ( V11() V12() integer ext-real ) Integer) ) ;

theorem :: RADIX_6:9
for m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds (SDDec (Mmax r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDDec (DecSD (0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) = (SDDec (M0 r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDDec (SDMax ((m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_6:10
for m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds SDDec (Mmax r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) < (SDDec (M0 r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDDec (Fmin ((m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_6:11
for m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds (SDDec (Mmin r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDDec (DecSD (0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) = (SDDec (M0 r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDDec (SDMin ((m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_6:12
for m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
(SDDec (M0 r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDDec (DecSD (0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) = (SDDec (Mmin r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDDec (SDMax ((m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_6:13
for m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds SDDec (M0 r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) < (SDDec (Mmin r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDDec (Fmin ((m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_6:14
for m, k, f being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) needs_digits_of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
ex s being ( ( integer ) ( V11() V12() integer ext-real ) Integer) st
( - f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( V11() ) ( V11() V12() integer ext-real non positive ) set ) < (SDDec (M0 r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) - (s : ( ( integer ) ( V11() V12() integer ext-real ) Integer) * f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) & (SDDec (Mmax r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) - (s : ( ( integer ) ( V11() V12() integer ext-real ) Integer) * f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) < f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ;

theorem :: RADIX_6:15
for m, k, f being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) needs_digits_of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
ex s being ( ( integer ) ( V11() V12() integer ext-real ) Integer) st
( - f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( V11() ) ( V11() V12() integer ext-real non positive ) set ) < (SDDec (Mmin r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) - (s : ( ( integer ) ( V11() V12() integer ext-real ) Integer) * f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) & (SDDec (M0 r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) - (s : ( ( integer ) ( V11() V12() integer ext-real ) Integer) * f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) < f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ;

theorem :: RADIX_6:16
for m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
( not k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) or ( SDDec (M0 r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) <= SDDec r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) & SDDec r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) <= SDDec (Mmax r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) or ( SDDec (Mmin r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) <= SDDec r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) & SDDec r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) < SDDec (M0 r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) ) ;

begin

definition
let i, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let r be ( ( V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
assume i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) in Seg (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;
func MmaskDigit (r,i) -> ( ( ) ( ) Element of k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_6:def 8
r : ( ( ) ( ) set ) . i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) : ( ( ) ( ) set ) if i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) < m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set )
otherwise 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let r be ( ( V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
func Mmask r -> ( ( V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) means :: RADIX_6:def 9
 for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) in Seg (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
DigA (it : ( ( ) ( ) set ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = MmaskDigit (r : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( ) Element of k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

theorem :: RADIX_6:17
for m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
(SDDec (M0 r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDDec (Mmask r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) = (SDDec r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDDec (DecSD (0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) FinSequence of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_6:18
for m, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & SDDec (Mmask r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) > 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
SDDec r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) > SDDec (M0 r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

definition
let i, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
assume k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
func FSDMinDigit (m,k,i) -> ( ( ) ( ) Element of k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_6:def 10
 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) if i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) > m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set )
1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) if i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) = m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set )
otherwise (- (Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V11() ) ( V11() V12() integer ext-real non positive ) set ) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;
end;

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

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

definition
let n, m, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let r be ( ( V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
pred r is_Zero_over n means :: RADIX_6:def 12
 for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) > n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) holds
DigA (r : ( ( ) ( ) set ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

theorem :: RADIX_6:20
for m being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
for n, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for r being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) in Seg (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) : ( ( ) ( ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & Mmask r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) is_Zero_over n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) & DigA ((Mmask r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) > 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
SDDec (Mmask r : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 2 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() ) Element of K6(INT : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) > 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( V1() V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;