:: RADIX_4 semantic presentation

begin

theorem :: RADIX_4:1
for k being ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) st 2 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
2 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) < Radix k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ;

begin

theorem :: RADIX_4:2
for x, y being ( ( integer ) ( V11() V12() integer ext-real ) Integer)
for k being ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) st 3 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
SDSub_Add_Carry (((SDSub_Add_Carry (x : ( ( integer ) ( V11() V12() integer ext-real ) Integer) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDSub_Add_Carry (y : ( ( integer ) ( V11() V12() integer ext-real ) Integer) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = 0 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_4:3
for k, m, n being ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) st 2 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
DigA_SDSub ((SD2SDSub (DecSD (m : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = SDSub_Add_Carry ((DigA ((DecSD (m : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_4:4
for k, m being ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) st 2 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) & m : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) is_represented_by 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
DigA_SDSub ((SD2SDSub (DecSD (m : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,(1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = SDSub_Add_Carry (m : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_4:5
for k, x, n being ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) st n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 3 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) & x : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) is_represented_by n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
DigA_SDSub ((SD2SDSub (DecSD ((x : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) mod ((Radix k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) |^ n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = SDSub_Add_Carry ((DigA ((DecSD (x : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_4:6
for k, m being ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) st 2 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) & m : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) is_represented_by 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
DigA_SDSub ((SD2SDSub (DecSD (m : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = m : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) - ((SDSub_Add_Carry (m : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) * (Radix k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_4:7
for k, x, n being ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) st k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) holds
((Radix k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) |^ n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) * (DigA_SDSub ((SD2SDSub (DecSD (x : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35((b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35((b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) = ((((Radix k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) |^ n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) * (DigA ((DecSD (x : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) - (((Radix k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) |^ (n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) : ( ( ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) * (SDSub_Add_Carry ((DigA ((DecSD (x : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) + (((Radix k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) |^ n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) * (SDSub_Add_Carry ((DigA ((DecSD (x : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b3 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;

begin

definition
let i, n, k be ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let x, y be ( ( V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like V60() V61() V62() ) Tuple of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ;
assume that
i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V70() V71() V72() V73() V74() V75() ) Element of K6(NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) and
k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 2 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func SDSubAddDigit (x,y,i,k) -> ( ( ) ( V11() V12() integer V43() ext-real ) Element of k : ( ( V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_4:def 1
(SDSub_Add_Data (((DigA_SDSub (x : ( ( V35(k : ( ( V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() Function-like V35(k : ( ( V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (DigA_SDSub (y : ( ( V35(k : ( ( V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() Function-like V35(k : ( ( V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) FinSequence of i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) ,k : ( ( V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDSub_Add_Carry (((DigA_SDSub (x : ( ( V35(k : ( ( V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() Function-like V35(k : ( ( V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -' 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (DigA_SDSub (y : ( ( V35(k : ( ( V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() Function-like V35(k : ( ( V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) FinSequence of i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -' 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) ,k : ( ( V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;
end;

definition
let n, k be ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let x, y be ( ( V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like V60() V61() V62() ) Tuple of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func x '+' y -> ( ( V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like V60() V61() V62() ) Tuple of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) means :: RADIX_4:def 2
 for i being ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) st i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) : ( ( ) ( V70() V71() V72() V73() V74() V75() ) Element of K6(NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
DigA_SDSub (it : ( ( V35(x : ( ( V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() Function-like V35(x : ( ( V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) FinSequence of n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = SDSubAddDigit (x : ( ( V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,y : ( ( V35(x : ( ( V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() Function-like V35(x : ( ( V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) ) ( V15() Function-like V35(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) FinSequence-like ) FinSequence of k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) FinSequence of k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) : ( ( ) ( V11() V12() integer V43() ext-real ) Element of k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

theorem :: RADIX_4:8
for n, k, x, y, i being ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) st i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) in Seg n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V70() V71() V72() V73() V74() V75() ) Element of K6(NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & 2 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
SDSubAddDigit ((SD2SDSub (DecSD (x : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35((b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35((b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,(SD2SDSub (DecSD (y : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,(n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35((b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35((b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V11() V12() integer V43() ext-real ) Element of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) = SDSubAddDigit ((SD2SDSub (DecSD ((x : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) mod ((Radix k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) |^ n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like V60() V61() V62() ) FinSequence of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,(SD2SDSub (DecSD ((y : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) mod ((Radix k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) |^ n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) ) : ( ( ) ( V6() V10() V11() V12() integer V43() ext-real non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like V60() V61() V62() ) FinSequence of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V11() V12() integer V43() ext-real ) Element of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_4:9
for n being ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) st n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for k, x, y being ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) st k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 3 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) & x : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) is_represented_by n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) & y : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) is_represented_by n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
x : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + y : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V6() V10() V11() V12() integer ext-real non negative ) set ) = SDSub2IntOut ((SD2SDSub (DecSD (x : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like V60() V61() V62() ) FinSequence of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) '+' (SD2SDSub (DecSD (y : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,n : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like V60() V61() V62() ) FinSequence of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) FinSequence of b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V35(b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ) FinSequence-like V60() V61() V62() ) Tuple of b1 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V6() V10() V11() V12() integer V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( V1() V28() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V6() V10() V11() V12() integer ext-real positive non negative ) set ) ,b2 : ( ( V10() ) ( V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD_Sub : ( ( V1() ) ( V1() V70() V71() V72() V73() V74() ) Element of K6(INT : ( ( ) ( V1() V28() V70() V71() V72() V73() V74() V76() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;