:: RADIX_2 semantic presentation

begin

theorem :: RADIX_2:1
for a being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) holds a : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) mod 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer functional FinSequence-membered V43() ext-real non positive non negative V82() V83() V84() V85() V86() V87() V88() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_2:2
for a, b being ( ( integer ) ( V11() V12() integer ext-real ) Integer)
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) > 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer functional FinSequence-membered V43() ext-real non positive non negative V82() V83() V84() V85() V86() V87() V88() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds
((a : ( ( integer ) ( V11() V12() integer ext-real ) Integer) mod n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (b : ( ( integer ) ( V11() V12() integer ext-real ) Integer) mod n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) mod n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = (a : ( ( integer ) ( V11() V12() integer ext-real ) Integer) + (b : ( ( integer ) ( V11() V12() integer ext-real ) Integer) mod n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) mod n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_2:3
for a, b being ( ( integer ) ( V11() V12() integer ext-real ) Integer)
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) > 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer functional FinSequence-membered V43() ext-real non positive non negative V82() V83() V84() V85() V86() V87() V88() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( integer ) ( V11() V12() integer ext-real ) Integer) * b : ( ( integer ) ( V11() V12() integer ext-real ) Integer) ) : ( ( ) ( V11() V12() integer ext-real ) set ) mod n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = (a : ( ( integer ) ( V11() V12() integer ext-real ) Integer) * (b : ( ( integer ) ( V11() V12() integer ext-real ) Integer) mod n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) mod n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_2:4
for a, b, i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) & 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer functional FinSequence-membered V43() ext-real non positive non negative V82() V83() V84() V85() V86() V87() V88() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) < b : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
(a : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) mod (b : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) |^ i : ( ( 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 ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) div (b : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) |^ (i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -' 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = (a : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) div (b : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) |^ (i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -' 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) mod b : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_2:5
for i, n 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) : ( ( ) ( V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) V82() V83() V84() V85() V86() V87() ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) in Seg (n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) V82() V83() V84() V85() V86() V87() ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

begin

theorem :: RADIX_2:6
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) holds Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer functional FinSequence-membered V43() ext-real non positive non negative V82() V83() V84() V85() V86() V87() V88() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_2:7
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for x being ( ( V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds SDDec x : ( ( V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) = DigA (x : ( ( V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_2:8
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for x being ( ( integer ) ( V11() V12() integer ext-real ) Integer) holds (SD_Add_Data (x : ( ( integer ) ( V11() V12() integer ext-real ) Integer) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + ((SD_Add_Carry x : ( ( integer ) ( V11() V12() integer ext-real ) Integer) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) * (Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) = x : ( ( integer ) ( V11() V12() integer ext-real ) Integer) ;

theorem :: RADIX_2:9
for k, n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for x being ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) )
for xn being ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) st ( 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 ) Nat) : ( ( ) ( V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) V82() V83() V84() V85() V86() V87() ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
x : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) . i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) = xn : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) . i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) ) holds
Sum (DigitSD x : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) FinSequence of INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( V11() V12() integer V43() ext-real ) Element of INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) = Sum ((DigitSD xn : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) FinSequence of INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) ^ <*(SubDigit (x : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( ) ( V11() V12() integer V43() ext-real ) Element of INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) *> : ( ( ) ( V1() V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) Function-like V28() V35(1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) FinSequence of INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) ) : ( ( ) ( V1() V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) FinSequence of INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( V11() V12() integer V43() ext-real ) Element of INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) ;

theorem :: RADIX_2:10
for k, n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for x being ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) )
for xn being ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) st ( 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 ) Nat) : ( ( ) ( V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) V82() V83() V84() V85() V86() V87() ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
x : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) . i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) = xn : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) . i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) ) holds
(SDDec xn : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (((Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) |^ 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 ) * (DigA (x : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) = SDDec x : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_2:11
for k, 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 V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for x, y being ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) 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 V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(SDDec (x : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) '+' y : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) FinSequence of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + ((SD_Add_Carry ((DigA (x : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (DigA (y : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) * ((Radix k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) |^ 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 ) ) : ( ( ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) = (SDDec x : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) + (SDDec y : ( ( V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) : ( ( ) ( V11() V12() integer ext-real ) set ) ;

begin

definition
let i, k, n be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let x be ( ( V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func SubDigit2 (x,i,k) -> ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_2:def 1
((Radix k : ( ( ) ( ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) |^ (i : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) -' 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) * (x : ( ( V35(i : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(i : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) . i : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let n, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let x be ( ( V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func DigitSD2 (x,k) -> ( ( V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) means :: RADIX_2: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 n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) : ( ( ) ( V82() V83() V84() V85() V86() V87() ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
it : ( ( V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) /. i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = SubDigit2 (x : ( ( V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( ) ( ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let n, k be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let x be ( ( V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func SDDec2 (x,k) -> ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_2:def 3
 Sum (DigitSD2 (x : ( ( V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( ) ( ) set ) )) : ( ( V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let i, k, x be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
func DigitDC2 (x,i,k) -> ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_2:def 4
(x : ( ( V35(i : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(i : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) mod ((Radix k : ( ( ) ( ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) |^ i : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) div ((Radix k : ( ( ) ( ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) |^ (i : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) -' 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let k, n, x be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
func DecSD2 (x,n,k) -> ( ( V35(n : ( ( ) ( ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( ) ( ) set ) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of n : ( ( ) ( ) set ) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) means :: RADIX_2:def 5
 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 : ( ( ) ( ) set ) : ( ( ) ( V82() V83() V84() V85() V86() V87() ) Element of K6(NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
it : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(n : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of n : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) . i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = DigitDC2 (x : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(n : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of n : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

theorem :: RADIX_2:12
for n, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for x being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) )
for y being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) st x : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = y : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds
DigitSD2 (x : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) 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) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = DigitSD y : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) FinSequence of INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) ;

theorem :: RADIX_2:13
for n, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat)
for x being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) )
for y being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) st x : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = y : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds
SDDec2 (x : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = SDDec y : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

theorem :: RADIX_2:14
for x, n, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) holds DecSD2 (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() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = 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() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) FinSequence of b3 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RADIX_2:15
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 V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) 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) is_represented_by 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
m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) = SDDec2 ((DecSD2 (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) ,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() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;

begin

definition
let q be ( ( integer ) ( V11() V12() integer ext-real ) Integer) ;
let f, j, k, n be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let c be ( ( V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func Table1 (q,c,f,j) -> ( ( integer ) ( V11() V12() integer ext-real ) Integer) equals :: RADIX_2:def 6
(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) * (DigA (c : ( ( Function-like ) ( V15() V18(j : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) V19(k : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) Function-like ) Element of K6(K7(j : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,k : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,j : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) : ( ( ) ( ) set ) mod f : ( ( ) ( ) set ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;
end;

definition
let q be ( ( integer ) ( V11() V12() integer ext-real ) Integer) ;
let k, f, n be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let c be ( ( V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
assume n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func Mul_mod (q,c,f,k) -> ( ( V35(n : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) Function-like V28() V35(n : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of n : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) , INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) means :: RADIX_2:def 7
( it : ( ( Function-like ) ( V15() V18(f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) V19(n : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) Function-like ) Element of K6(K7(f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) = Table1 (q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ,c : ( ( V35(f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) Integer) & ( for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) & i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) <= n : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) - 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) holds
ex I1, I2 being ( ( integer ) ( V11() V12() integer ext-real ) Integer) st
( I1 : ( ( integer ) ( V11() V12() integer ext-real ) Integer) = it : ( ( Function-like ) ( V15() V18(f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) V19(n : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) Function-like ) Element of K6(K7(f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) & I2 : ( ( integer ) ( V11() V12() integer ext-real ) Integer) = it : ( ( Function-like ) ( V15() V18(f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) V19(n : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) Function-like ) Element of K6(K7(f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . (i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) & I2 : ( ( integer ) ( V11() V12() integer ext-real ) Integer) = (((Radix k : ( ( ) ( ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) * I1 : ( ( integer ) ( V11() V12() integer ext-real ) Integer) ) : ( ( ) ( V11() V12() integer ext-real ) set ) + (Table1 (q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ,c : ( ( V35(f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,(n : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) -' i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( integer ) ( V11() V12() integer ext-real ) Integer) ) : ( ( ) ( V11() V12() integer ext-real ) set ) mod f : ( ( V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(q : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ) ) );
end;

theorem :: RADIX_2:16
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 V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for q being ( ( integer ) ( V11() V12() integer ext-real ) Integer)
for ic, f, k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st ic : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) is_represented_by 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) & f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) > 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer functional FinSequence-membered V43() ext-real non positive non negative V82() V83() V84() V85() V86() V87() V88() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for c being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b5 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple 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) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) st c : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b5 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,b5 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = DecSD (ic : ( ( 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() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b5 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) FinSequence of b5 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(Mul_mod (q : ( ( integer ) ( V11() V12() integer ext-real ) Integer) ,c : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(b5 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,b5 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,f : ( ( 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() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) . n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V11() V12() integer ext-real ) Element of REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) = (q : ( ( integer ) ( V11() V12() integer ext-real ) Integer) * ic : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V11() V12() integer ext-real ) set ) mod f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;

begin

definition
let n, f, j, m be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let e be ( ( V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func Table2 (m,e,f,j) -> ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) equals :: RADIX_2:def 8
(m : ( ( V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) |^ (e : ( ( V35(j : ( ( V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(j : ( ( V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) /. j : ( ( V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) mod f : ( ( ) ( ) set ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let k, f, m, n be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
let e be ( ( V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
assume n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func Pow_mod (m,e,f,k) -> ( ( V35(n : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(n : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of n : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) means :: RADIX_2:def 9
( it : ( ( Function-like ) ( V15() V18(m : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) V19(n : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) Function-like ) Element of K6(K7(m : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = Table2 (m : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,e : ( ( V35(m : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(m : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,f : ( ( ) ( ) set ) ,n : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for i being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) & i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) <= n : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) - 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) holds
ex i1, i2 being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st
( i1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) = it : ( ( Function-like ) ( V15() V18(m : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) V19(n : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) Function-like ) Element of K6(K7(m : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) & i2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) = it : ( ( Function-like ) ( V15() V18(m : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) V19(n : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) Function-like ) Element of K6(K7(m : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . (i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4() V5() V6() V10() V11() V12() integer V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) & i2 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) = (((i1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) |^ (Radix k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) mod f : ( ( ) ( ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) * (Table2 (m : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,e : ( ( V35(m : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(m : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,f : ( ( ) ( ) set ) ,(n : ( ( V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19(f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(k : ( ( V15() Function-like V75() ) ( V15() V19( RAT : ( ( ) ( V1() V28() V82() V83() V84() V85() V88() ) set ) ) Function-like V72() V73() V74() V75() ) set ) ) FinSequence-like FinSubsequence-like ) FinSequence of f : ( ( ) ( ) set ) -SD : ( ( V1() ) ( V1() V82() V83() V84() V85() V86() ) Element of K6(INT : ( ( ) ( V1() V28() V82() V83() V84() V85() V86() V88() ) set ) ) : ( ( ) ( ) set ) ) ) -' i : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) mod f : ( ( ) ( ) set ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) );
end;

theorem :: RADIX_2:17
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 V43() ext-real positive non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for m, k, f, ie being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st ie : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) is_represented_by 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) & f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) > 0 : ( ( ) ( V1() V4() V5() V6() V8() V9() V10() V11() V12() integer functional FinSequence-membered V43() ext-real non positive non negative V82() V83() V84() V85() V86() V87() V88() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for e being ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) st e : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = DecSD2 (ie : ( ( 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() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(Pow_mod (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ,e : ( ( V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ( V15() V18( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ,f : ( ( 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() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) V19( NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V28() V35(b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) FinSequence-like FinSubsequence-like V72() V73() V74() V75() ) Tuple of b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) , NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) . n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) = (m : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) |^ ie : ( ( 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 ) mod f : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V43() ext-real non negative V82() V83() V84() V85() V86() V87() ) Element of NAT : ( ( ) ( V1() V4() V5() V6() V82() V83() V84() V85() V86() V87() V88() ) Element of K6(REAL : ( ( ) ( V1() V28() V82() V83() V84() V88() ) set ) ) : ( ( ) ( ) set ) ) ) ;