N (axiom)
NAbstract.destr_t [in destr_t]
NAbstract.digits_dom_op [in digits_dom_op]
NAbstract.dom_t [in dom_t]
NAbstract.iter_t [in iter_t]
NAbstract.iter_mk_t [in iter_mk_t]
NAbstract.mk_t_S_level [in mk_t_S_level]
NAbstract.mk_t [in mk_t]
NAbstract.mk_t_S [in mk_t_S]
NAbstract.reduce [in reduce]
NAbstract.same_level [in same_level]
NAbstract.spec_mk_t [in spec_mk_t]
NAbstract.spec_same_level_dep [in spec_same_level_dep]
NAbstract.spec_mk_t_S [in spec_mk_t_S]
NAbstract.spec_reduce [in spec_reduce]
NAbstract.t [in t]
NAbstract.to_Z [in to_Z]
NAxiomsRec.recursion [in recursion]
NAxiomsRec.recursion_0 [in recursion_0]
NAxiomsRec.recursion_succ [in recursion_succ]
NAxiom.pred_0 [in pred_0]
NDivSpecific.mod_upper_bound [in mod_upper_bound]
NType_ZType.Zabs_N [in Zabs_N]
NType_ZType.spec_Zabs_N [in spec_Zabs_N]
NType_ZType.Z_of_N [in Z_of_N]
NType_ZType.spec_Z_of_N [in spec_Z_of_N]
NType.add [in add]
NType.compare [in compare]
NType.div [in div]
NType.div_eucl [in div_eucl]
NType.div2 [in div2]
NType.eqb [in eqb]
NType.even [in even]
NType.gcd [in gcd]
NType.land [in land]
NType.ldiff [in ldiff]
NType.leb [in leb]
NType.log2 [in log2]
NType.lor [in lor]
NType.ltb [in ltb]
NType.lxor [in lxor]
NType.max [in max]
NType.min [in min]
NType.modulo [in modulo]
NType.mul [in mul]
NType.odd [in odd]
NType.of_N [in of_N]
NType.one [in one]
NType.pow [in pow]
NType.pow_N [in pow_N]
NType.pow_pos [in pow_pos]
NType.pred [in pred]
NType.shiftl [in shiftl]
NType.shiftr [in shiftr]
NType.spec_ltb [in spec_ltb]
NType.spec_shiftl [in spec_shiftl]
NType.spec_pos [in spec_pos]
NType.spec_pred [in spec_pred]
NType.spec_max [in spec_max]
NType.spec_leb [in spec_leb]
NType.spec_add [in spec_add]
NType.spec_land [in spec_land]
NType.spec_odd [in spec_odd]
NType.spec_shiftr [in spec_shiftr]
NType.spec_2 [in spec_2]
NType.spec_div2 [in spec_div2]
NType.spec_mul [in spec_mul]
NType.spec_testbit [in spec_testbit]
NType.spec_1 [in spec_1]
NType.spec_eqb [in spec_eqb]
NType.spec_lxor [in spec_lxor]
NType.spec_modulo [in spec_modulo]
NType.spec_compare [in spec_compare]
NType.spec_pow [in spec_pow]
NType.spec_even [in spec_even]
NType.spec_ldiff [in spec_ldiff]
NType.spec_div [in spec_div]
NType.spec_div_eucl [in spec_div_eucl]
NType.spec_pow_pos [in spec_pow_pos]
NType.spec_lor [in spec_lor]
NType.spec_sub [in spec_sub]
NType.spec_succ [in spec_succ]
NType.spec_sqrt [in spec_sqrt]
NType.spec_min [in spec_min]
NType.spec_log2 [in spec_log2]
NType.spec_gcd [in spec_gcd]
NType.spec_pow_N [in spec_pow_N]
NType.spec_square [in spec_square]
NType.spec_of_N [in spec_of_N]
NType.spec_0 [in spec_0]
NType.sqrt [in sqrt]
NType.square [in square]
NType.sub [in sub]
NType.succ [in succ]
NType.t [in t]
NType.testbit [in testbit]
NType.to_Z [in to_Z]
NType.two [in two]
NType.zero [in zero]
NZBitsSpec.div2_spec [in div2_spec]
NZBitsSpec.land_spec [in land_spec]
NZBitsSpec.ldiff_spec [in ldiff_spec]
NZBitsSpec.lor_spec [in lor_spec]
NZBitsSpec.lxor_spec [in lxor_spec]
NZBitsSpec.shiftl_spec_low [in shiftl_spec_low]
NZBitsSpec.shiftl_spec_high [in shiftl_spec_high]
NZBitsSpec.shiftr_spec [in shiftr_spec]
NZBitsSpec.testbit_even_0 [in testbit_even_0]
NZBitsSpec.testbit_neg_r [in testbit_neg_r]
NZBitsSpec.testbit_even_succ [in testbit_even_succ]
NZBitsSpec.testbit_odd_0 [in testbit_odd_0]
NZBitsSpec.testbit_odd_succ [in testbit_odd_succ]
NZDivSpec.div_mod [in div_mod]
NZDivSpec.mod_bound_pos [in mod_bound_pos]
NZGcdSpec.gcd_nonneg [in gcd_nonneg]
NZGcdSpec.gcd_greatest [in gcd_greatest]
NZGcdSpec.gcd_divide_r [in gcd_divide_r]
NZGcdSpec.gcd_divide_l [in gcd_divide_l]
NZLog2Spec.log2_spec [in log2_spec]
NZLog2Spec.log2_nonpos [in log2_nonpos]
NZParity.even [in even]
NZParity.even_spec [in even_spec]
NZParity.odd [in odd]
NZParity.odd_spec [in odd_spec]
NZPowSpec.pow_0_r [in pow_0_r]
NZPowSpec.pow_succ_r [in pow_succ_r]
NZPowSpec.pow_neg_r [in pow_neg_r]
NZSqrtSpec.sqrt_spec [in sqrt_spec]
NZSqrtSpec.sqrt_neg [in sqrt_neg]
NZSquare.square [in square]
NZSquare.square_spec [in square_spec]