D
Dadd [lemma, in Dadd]
Datan_seq_Rabs [lemma, in Datan_seq_Rabs]
Datan_lim [lemma, in Datan_lim]
Datan_is_datan [lemma, in Datan_is_datan]
Datan_eq_DatanSeq_interv [lemma, in Datan_eq_DatanSeq_interv]
Datan_continuity [lemma, in Datan_continuity]
Datan_seq_decreasing [lemma, in Datan_seq_decreasing]
Datan_CVU_prelim [lemma, in Datan_CVU_prelim]
Datan_sum_eq [lemma, in Datan_sum_eq]
Datan_seq_CV_0 [lemma, in Datan_seq_CV_0]
Datan_seq_pos [lemma, in Datan_seq_pos]
Datan_seq [definition, in Datan_seq]
Datan_seq_increasing [lemma, in Datan_seq_increasing]
Datatypes [library]
Dcomp [lemma, in Dcomp]
Dcompare [lemma, in Dcompare]
Dcompare_inf [lemma, in Dcompare_inf]
Dconst [lemma, in Dconst]
dec [abbreviation, in dec]
DecBool [library]
decidability [section, in decidability]
decidability.x [variable, in x]
decidability.y [variable, in y]
decidable [definition, in decidable]
Decidable [library]
DecidableEqDep [module, in DecidableEqDep]
DecidableEqDepSet [module, in DecidableEqDepSet]
DecidableEqDepSet.eq_rect_eq [lemma, in eq_rect_eq]
DecidableEqDepSet.eq_dep_eq [lemma, in eq_dep_eq]
DecidableEqDepSet.inj_pair2 [lemma, in inj_pair2]
DecidableEqDepSet.inj_pairT2 [abbreviation, in inj_pairT2]
DecidableEqDepSet.inj_pairP2 [lemma, in inj_pairP2]
DecidableEqDepSet.N [module, in DecidableEqDepSet.N]
DecidableEqDepSet.Streicher_K [lemma, in Streicher_K]
DecidableEqDepSet.UIP [lemma, in UIP]
DecidableEqDepSet.UIP_refl [lemma, in UIP_refl]
DecidableEqDep.eq_rect_eq [lemma, in eq_rect_eq]
DecidableEqDep.eq_dep_eq [lemma, in eq_dep_eq]
DecidableEqDep.inj_pairT2 [lemma, in inj_pairT2]
DecidableEqDep.inj_pairP2 [lemma, in inj_pairP2]
DecidableEqDep.Streicher_K [lemma, in Streicher_K]
DecidableEqDep.UIP [lemma, in UIP]
DecidableEqDep.UIP_refl [lemma, in UIP_refl]
DecidableEquivalence [record, in DecidableEquivalence]
DecidableEquivalence [inductive, in DecidableEquivalence]
DecidableSet [module, in DecidableSet]
DecidableSetoid [record, in DecidableSetoid]
DecidableSetoid [inductive, in DecidableSetoid]
DecidableSet.eq_dec [axiom, in eq_dec]
DecidableSet.U [axiom, in U]
DecidableType [module, in DecidableType]
DecidableType [module, in DecidableType]
DecidableType [module, in DecidableType]
DecidableType [library]
DecidableTypeBoth [module, in DecidableTypeBoth]
DecidableTypeBoth' [module, in DecidableTypeBoth']
DecidableTypeEx [library]
DecidableTypeFull [module, in DecidableTypeFull]
DecidableTypeFull' [module, in DecidableTypeFull']
DecidableTypeOrig [module, in DecidableTypeOrig]
DecidableTypeOrig' [module, in DecidableTypeOrig']
DecidableType' [module, in DecidableType']
DecidableType.eq_dec [axiom, in eq_dec]
DecidableType.U [axiom, in U]
Decide [module, in Decide]
Decide [module, in Decide]
decide [lemma, in decide]
decide_left [lemma, in decide_left]
decide_right [lemma, in decide_right]
decimal_exp [definition, in decimal_exp]
decomp_sum [lemma, in decomp_sum]
decreasing [definition, in decreasing]
decreasing_ineq [lemma, in decreasing_ineq]
decreasing_prop [lemma, in decreasing_prop]
decreasing_growing [lemma, in decreasing_growing]
decreasing_cv [lemma, in decreasing_cv]
DecStrOrder [module, in DecStrOrder]
DecStrOrder' [module, in DecStrOrder']
dec_Zne [lemma, in dec_Zne]
dec_not [lemma, in dec_not]
dec_gt [lemma, in dec_gt]
dec_Zge [lemma, in dec_Zge]
dec_Zle [abbreviation, in dec_Zle]
dec_lt [lemma, in dec_lt]
dec_eq_nat [lemma, in dec_eq_nat]
dec_inh_nat_subset_has_unique_least_element [lemma, in dec_inh_nat_subset_has_unique_least_element]
dec_eq [abbreviation, in dec_eq]
dec_False [lemma, in dec_False]
dec_le [lemma, in dec_le]
dec_imp [lemma, in dec_imp]
dec_Zgt [lemma, in dec_Zgt]
dec_iff [lemma, in dec_iff]
dec_Zlt [abbreviation, in dec_Zlt]
dec_True [lemma, in dec_True]
dec_not_not [lemma, in dec_not_not]
dec_and [lemma, in dec_and]
dec_or [lemma, in dec_or]
dec_ge [lemma, in dec_ge]
Dec2Bool [module, in Dec2Bool]
DefaultRelation [record, in DefaultRelation]
default_relation [definition, in default_relation]
definition_of_noetherian [constructor, in definition_of_noetherian]
Definition_of_Directed [constructor, in Definition_of_Directed]
Definition_of_PER [constructor, in Definition_of_PER]
Definition_of_covers [constructor, in Definition_of_covers]
Definition_of_Power_set [constructor, in Definition_of_Power_set]
Definition_of_chain [constructor, in Definition_of_chain]
Definition_of_equivalence [constructor, in Definition_of_equivalence]
Definition_of_Conditionally_complete [constructor, in Definition_of_Conditionally_complete]
Definition_of_order [constructor, in Definition_of_order]
Definition_of_Complete [constructor, in Definition_of_Complete]
Definition_of_preorder [constructor, in Definition_of_preorder]
Definition_of_cpo [constructor, in Definition_of_cpo]
Definition_of_PO [constructor, in Definition_of_PO]
Defn_of_Approximant [constructor, in Defn_of_Approximant]
defs [section, in defs]
defs [section, in defs]
defs [section, in defs]
defs.A [variable, in A]
defs.A [variable, in A]
defs.A [variable, in A]
defs.emptyBag [variable, in emptyBag]
defs.eqA [variable, in eqA]
defs.eqA [variable, in eqA]
defs.eqA_dec [variable, in eqA_dec]
defs.eqA_dec [variable, in eqA_dec]
defs.gtA [variable, in gtA]
defs.leA [variable, in leA]
defs.leA_antisym [variable, in leA_antisym]
defs.leA_dec [variable, in leA_dec]
defs.leA_refl [variable, in leA_refl]
defs.leA_trans [variable, in leA_trans]
defs.R [variable, in R]
defs.singletonBag [variable, in singletonBag]
deg_rad [lemma, in deg_rad]
deletion [lemma, in deletion]
Delta [definition, in Delta]
Delta_is_pos [definition, in Delta_is_pos]
demorgan1 [abbreviation, in demorgan1]
demorgan2 [abbreviation, in demorgan2]
demorgan3 [abbreviation, in demorgan3]
demorgan4 [abbreviation, in demorgan4]
depair [definition, in depair]
depair_sanity [lemma, in depair_sanity]
DependentEliminationPackage [record, in DependentEliminationPackage]
DependentFunctionalChoice [abbreviation, in DependentFunctionalChoice]
DependentFunctionalChoice_on [definition, in DependentFunctionalChoice_on]
DependentFunctionalRelReification [abbreviation, in DependentFunctionalRelReification]
DependentFunctionalRelReification_on [definition, in DependentFunctionalRelReification_on]
DependentMemoFunction [section, in DependentMemoFunction]
DependentMemoFunction.A [variable, in A]
DependentMemoFunction.f [variable, in f]
DependentMemoFunction.g [variable, in g]
DependentMemoFunction.Hg_correct [variable, in Hg_correct]
DependentMemoFunction.mf [variable, in mf]
DependentMemoFunction.mg [variable, in mg]
Dependent_Equality.U [variable, in U]
Dependent_Equality.P [variable, in P]
dependent_description [definition, in dependent_description]
Dependent_Equality [section, in Dependent_Equality]
dependent_unique_choice [axiom, in dependent_unique_choice]
dependent_unique_choice [lemma, in dependent_unique_choice]
dependent_choice [lemma, in dependent_choice]
Dependent_choice_lemmas.R [variable, in R]
Dependent_choice_lemmas [section, in Dependent_choice_lemmas]
Dependent_choice_lemmas.X [variable, in X]
DepOfNodep [module, in DepOfNodep]
DepOfNodep.add [definition, in add]
DepOfNodep.Add [definition, in Add]
DepOfNodep.cardinal [definition, in cardinal]
DepOfNodep.choose [definition, in choose]
DepOfNodep.choose_ok1 [lemma, in choose_ok1]
DepOfNodep.choose_ok2 [lemma, in choose_ok2]
DepOfNodep.choose_aux [definition, in choose_aux]
DepOfNodep.choose_equal [lemma, in choose_equal]
DepOfNodep.compare [definition, in compare]
DepOfNodep.compat_P_aux [lemma, in compat_P_aux]
DepOfNodep.diff [definition, in diff]
DepOfNodep.E [module, in DepOfNodep.E]
DepOfNodep.elements [definition, in elements]
DepOfNodep.elt [definition, in elt]
DepOfNodep.empty [definition, in empty]
DepOfNodep.Empty [definition, in Empty]
DepOfNodep.eq [definition, in eq]
DepOfNodep.equal [definition, in equal]
DepOfNodep.Equal [definition, in Equal]
DepOfNodep.eq_refl [definition, in eq_refl]
DepOfNodep.eq_sym [definition, in eq_sym]
DepOfNodep.eq_trans [definition, in eq_trans]
DepOfNodep.eq_In [definition, in eq_In]
DepOfNodep.Exists [definition, in Exists]
DepOfNodep.exists_ [definition, in exists_]
DepOfNodep.fdec [definition, in fdec]
DepOfNodep.filter [definition, in filter]
DepOfNodep.fold [definition, in fold]
DepOfNodep.For_all [definition, in For_all]
DepOfNodep.for_all [definition, in for_all]
DepOfNodep.In [definition, in In]
DepOfNodep.inter [definition, in inter]
DepOfNodep.is_empty [definition, in is_empty]
DepOfNodep.lt [definition, in lt]
DepOfNodep.lt_not_eq [definition, in lt_not_eq]
DepOfNodep.lt_trans [definition, in lt_trans]
DepOfNodep.max_elt [definition, in max_elt]
DepOfNodep.mem [definition, in mem]
DepOfNodep.min_elt [definition, in min_elt]
DepOfNodep.partition [definition, in partition]
DepOfNodep.remove [definition, in remove]
DepOfNodep.singleton [definition, in singleton]
DepOfNodep.Subset [definition, in Subset]
DepOfNodep.subset [definition, in subset]
DepOfNodep.t [definition, in t]
DepOfNodep.union [definition, in union]
dep_iff_non_dep_functional_rel_reification [lemma, in dep_iff_non_dep_functional_rel_reification]
dep_non_dep_functional_choice [lemma, in dep_non_dep_functional_choice]
dep_non_dep_functional_rel_reification [lemma, in dep_non_dep_functional_rel_reification]
derivable [definition, in derivable]
derivable_pt [definition, in derivable_pt]
derivable_derive [lemma, in derivable_derive]
derivable_pt_lim_sin_0 [lemma, in derivable_pt_lim_sin_0]
derivable_pt_recip_interv_prelim0 [lemma, in derivable_pt_recip_interv_prelim0]
derivable_pt_sin [lemma, in derivable_pt_sin]
derivable_inv [lemma, in derivable_inv]
derivable_pt_tan [lemma, in derivable_pt_tan]
derivable_pt_id [lemma, in derivable_pt_id]
derivable_comp [lemma, in derivable_comp]
derivable_pt_minus [lemma, in derivable_pt_minus]
derivable_pt_sinh [lemma, in derivable_pt_sinh]
derivable_pt_lim_cos_0 [lemma, in derivable_pt_lim_cos_0]
derivable_pt_plus [lemma, in derivable_pt_plus]
derivable_pt_recip_interv [lemma, in derivable_pt_recip_interv]
derivable_continuous_pt [lemma, in derivable_continuous_pt]
derivable_pt_lim_recip_interv [lemma, in derivable_pt_lim_recip_interv]
derivable_pt_lim_sinh [lemma, in derivable_pt_lim_sinh]
derivable_pt_cos [lemma, in derivable_pt_cos]
derivable_pt_lim_pow_pos [lemma, in derivable_pt_lim_pow_pos]
derivable_scal [lemma, in derivable_scal]
derivable_sinh [lemma, in derivable_sinh]
derivable_pt_lim_minus [lemma, in derivable_pt_lim_minus]
derivable_pt_lim_pow [lemma, in derivable_pt_lim_pow]
derivable_pt_lim_D_in [lemma, in derivable_pt_lim_D_in]
derivable_pt_abs [definition, in derivable_pt_abs]
derivable_sin [lemma, in derivable_sin]
derivable_id [lemma, in derivable_id]
derivable_Rsqr [lemma, in derivable_Rsqr]
derivable_pt_comp [lemma, in derivable_pt_comp]
derivable_pt_lim_power [lemma, in derivable_pt_lim_power]
derivable_pt_lim_opp [lemma, in derivable_pt_lim_opp]
derivable_pt_finite_sum [lemma, in derivable_pt_finite_sum]
derivable_pt_lim [definition, in derivable_pt_lim]
derivable_pt_lim_exp_0 [lemma, in derivable_pt_lim_exp_0]
derivable_pt_atan [lemma, in derivable_pt_atan]
derivable_pt_id_interv [lemma, in derivable_pt_id_interv]
derivable_pt_lim_ps_atan [lemma, in derivable_pt_lim_ps_atan]
derivable_continuous [lemma, in derivable_continuous]
derivable_pt_recip_interv_prelim1 [lemma, in derivable_pt_recip_interv_prelim1]
derivable_pt_div [lemma, in derivable_pt_div]
derivable_pt_exp [lemma, in derivable_pt_exp]
derivable_opp [lemma, in derivable_opp]
derivable_pt_scal [lemma, in derivable_pt_scal]
derivable_pt_lim_const [lemma, in derivable_pt_lim_const]
derivable_pt_lim_ln [lemma, in derivable_pt_lim_ln]
derivable_div [lemma, in derivable_div]
derivable_pt_ps_atan [lemma, in derivable_pt_ps_atan]
derivable_exp [lemma, in derivable_exp]
derivable_cos [lemma, in derivable_cos]
derivable_pt_lim_cos [lemma, in derivable_pt_lim_cos]
derivable_pt_lim_sin [lemma, in derivable_pt_lim_sin]
derivable_pt_Rsqr [lemma, in derivable_pt_Rsqr]
derivable_pt_lim_exp [lemma, in derivable_pt_lim_exp]
derivable_pt_lim_div [lemma, in derivable_pt_lim_div]
derivable_pow [lemma, in derivable_pow]
derivable_minus [lemma, in derivable_minus]
derivable_pt_const [lemma, in derivable_pt_const]
derivable_pt_mult [lemma, in derivable_pt_mult]
derivable_pt_opp [lemma, in derivable_pt_opp]
derivable_pt_inv [lemma, in derivable_pt_inv]
derivable_pt_lim_id [lemma, in derivable_pt_lim_id]
derivable_pt_lim_mult [lemma, in derivable_pt_lim_mult]
derivable_pt_lim_plus [lemma, in derivable_pt_lim_plus]
derivable_plus [lemma, in derivable_plus]
derivable_pt_lim_finite_sum [lemma, in derivable_pt_lim_finite_sum]
derivable_pt_lim_sqrt [lemma, in derivable_pt_lim_sqrt]
derivable_pt_sqrt [lemma, in derivable_pt_sqrt]
derivable_pt_cosh [lemma, in derivable_pt_cosh]
derivable_pt_lim_CVU [lemma, in derivable_pt_lim_CVU]
derivable_cosh [lemma, in derivable_cosh]
derivable_pt_lim_comp [lemma, in derivable_pt_lim_comp]
derivable_pt_lim_scal [lemma, in derivable_pt_lim_scal]
derivable_const [lemma, in derivable_const]
derivable_pt_lim_cosh [lemma, in derivable_pt_lim_cosh]
derivable_pt_lim_Rsqr [lemma, in derivable_pt_lim_Rsqr]
derivable_pt_lim_fs [lemma, in derivable_pt_lim_fs]
derivable_pt_pow [lemma, in derivable_pt_pow]
derivable_mult [lemma, in derivable_mult]
derivable_finite_sum [lemma, in derivable_finite_sum]
derive [definition, in derive]
derive_pt_eq [lemma, in derive_pt_eq]
derive_pt_recip_interv_prelim0 [lemma, in derive_pt_recip_interv_prelim0]
derive_pt_plus [lemma, in derive_pt_plus]
derive_pt_minus [lemma, in derive_pt_minus]
derive_pt_Rsqr [lemma, in derive_pt_Rsqr]
derive_pt_id [lemma, in derive_pt_id]
derive_pt_cosh [lemma, in derive_pt_cosh]
derive_pt_opp [lemma, in derive_pt_opp]
derive_pt_pow [lemma, in derive_pt_pow]
derive_pt_eq_0 [lemma, in derive_pt_eq_0]
derive_pt_recip_interv_prelim1_0 [lemma, in derive_pt_recip_interv_prelim1_0]
derive_increasing_interv_var [lemma, in derive_increasing_interv_var]
derive_pt_inv [lemma, in derive_pt_inv]
derive_pt_sinh [lemma, in derive_pt_sinh]
derive_pt_mult [lemma, in derive_pt_mult]
derive_pt_D_in [lemma, in derive_pt_D_in]
derive_pt_const [lemma, in derive_pt_const]
derive_pt_sin [lemma, in derive_pt_sin]
derive_increasing_interv [lemma, in derive_increasing_interv]
derive_increasing_interv [lemma, in derive_increasing_interv]
derive_increasing_interv_ax [lemma, in derive_increasing_interv_ax]
derive_pt_recip_interv_prelim1_1 [lemma, in derive_pt_recip_interv_prelim1_1]
derive_pt_scal [lemma, in derive_pt_scal]
derive_pt_comp [lemma, in derive_pt_comp]
derive_pt_sqrt [lemma, in derive_pt_sqrt]
derive_pt_recip_interv [lemma, in derive_pt_recip_interv]
derive_pt [definition, in derive_pt]
derive_pt_atan [lemma, in derive_pt_atan]
derive_pt_exp [lemma, in derive_pt_exp]
derive_pt_div [lemma, in derive_pt_div]
derive_pt_cos [lemma, in derive_pt_cos]
derive_pt_eq_1 [lemma, in derive_pt_eq_1]
derive_pt_tan [lemma, in derive_pt_tan]
deriv_maximum [lemma, in deriv_maximum]
deriv_constant2 [lemma, in deriv_constant2]
deriv_minimum [lemma, in deriv_minimum]
Desc [inductive, in Desc]
Descl [abbreviation, in Descl]
description [definition, in description]
Description [library]
description_rel_choice_imp_funct_choice [lemma, in description_rel_choice_imp_funct_choice]
desc_prefix [lemma, in desc_prefix]
desc_end [lemma, in desc_end]
desc_tail [lemma, in desc_tail]
destruct_list [lemma, in destruct_list]
Dgf [definition, in Dgf]
Diaconescu [library]
Dichotomy_ub [definition, in Dichotomy_ub]
Dichotomy_lb [definition, in Dichotomy_lb]
dicho_lb_maj_y [lemma, in dicho_lb_maj_y]
dicho_up_cv [lemma, in dicho_up_cv]
dicho_comp [lemma, in dicho_comp]
dicho_up [definition, in dicho_up]
dicho_up_decreasing [lemma, in dicho_up_decreasing]
dicho_up_min [lemma, in dicho_up_min]
dicho_lb_cv [lemma, in dicho_lb_cv]
dicho_up_min_x [lemma, in dicho_up_min_x]
dicho_lb [definition, in dicho_lb]
dicho_lb_growing [lemma, in dicho_lb_growing]
dicho_lb_car [lemma, in dicho_lb_car]
dicho_lb_dicho_up [lemma, in dicho_lb_dicho_up]
dicho_up_car [lemma, in dicho_up_car]
dicho_lb_maj [lemma, in dicho_lb_maj]
did_normalization [constructor, in did_normalization]
diff [definition, in diff]
Differential [record, in Differential]
Differential_D2 [record, in Differential_D2]
diff_r [definition, in diff_r]
diff_false_true [lemma, in diff_false_true]
diff_true_false [lemma, in diff_true_false]
diff_l [definition, in diff_l]
diff0 [projection, in diff0]
digits [inductive, in digits]
digits_zop [lemma, in digits_zop]
digits_kzop [lemma, in digits_kzop]
digits31 [definition, in digits31]
dimemo_get_correct [lemma, in dimemo_get_correct]
dimemo_list [definition, in dimemo_list]
Directed [inductive, in Directed]
disc [definition, in disc]
discrete_nat [lemma, in discrete_nat]
DiscrR [library]
disc_P1 [lemma, in disc_P1]
Disjoint [inductive, in Disjoint]
Disjoint_Union.leA [variable, in leA]
Disjoint_Union.B [variable, in B]
Disjoint_Union [section, in Disjoint_Union]
Disjoint_intro [constructor, in Disjoint_intro]
Disjoint_Union.A [variable, in A]
Disjoint_Union.leB [variable, in leB]
Disjoint_Union [library]
dist [projection, in dist]
distance_refl [lemma, in distance_refl]
distance_symm [lemma, in distance_symm]
Distributivity [lemma, in Distributivity]
Distributivity' [lemma, in Distributivity']
distr_rev [abbreviation, in distr_rev]
dist_sym [projection, in dist_sym]
dist_aux [lemma, in dist_aux]
dist_Desc_concat [lemma, in dist_Desc_concat]
dist_pos [projection, in dist_pos]
dist_euc [definition, in dist_euc]
dist_refl [projection, in dist_refl]
dist_tri [projection, in dist_tri]
div [definition, in div]
div [definition, in div]
divers [section, in divers]
diveucl [inductive, in diveucl]
divex [constructor, in divex]
divide [definition, in divide]
DivideNotation [module, in DivideNotation]
( _ | _ ) [notation, in ::'('_x_'|'_x_')']
divmod [definition, in divmod]
DivMod [module, in DivMod]
DivModNotation [module, in DivModNotation]
_ / _ [notation, in ::x_'/'_x]
_ mod _ [notation, in ::x_'mod'_x]
divmod_spec [lemma, in divmod_spec]
DivMod' [module, in DivMod']
DivMod.div [axiom, in div]
DivMod.modulo [axiom, in modulo]
div_real_fct [definition, in div_real_fct]
div_gt [definition, in div_gt]
div_eq_inv [lemma, in div_eq_inv]
div_Zdiv [lemma, in div_Zdiv]
div_lt [lemma, in div_lt]
div_le_0 [lemma, in div_le_0]
div_mod [lemma, in div_mod]
div_fct [definition, in div_fct]
div2 [definition, in div2]
Div2 [library]
div2_double [lemma, in div2_double]
div2_double [lemma, in div2_double]
div2_S_double [lemma, in div2_S_double]
div2_double_plus_one [lemma, in div2_double_plus_one]
div2_not_R0 [lemma, in div2_not_R0]
div2_even [lemma, in div2_even]
div2_decr [lemma, in div2_decr]
div2_bitwise [lemma, in div2_bitwise]
div2_odd [lemma, in div2_odd]
div21 [definition, in div21]
div31 [definition, in div31]
div31_phi [lemma, in div31_phi]
div312_phi [lemma, in div312_phi]
div3121 [definition, in div3121]
Dln [lemma, in Dln]
dmemo_list [definition, in dmemo_list]
dmemo_get_correct [lemma, in dmemo_get_correct]
dmemo_get [definition, in dmemo_get]
Dminus [lemma, in Dminus]
Dmult [lemma, in Dmult]
Dmult_const [lemma, in Dmult_const]
domain_P1 [lemma, in domain_P1]
domain_finite [definition, in domain_finite]
Dopp [lemma, in Dopp]
double [lemma, in double]
double [definition, in double]
DoubleAdd [section, in DoubleAdd]
DoubleAdd [library]
DoubleAdd.Cont [section, in Cont]
DoubleAdd.Cont.P [variable, in P]
DoubleAdd.Cont.spec_f0 [variable, in spec_f0]
DoubleAdd.Cont.spec_f1 [variable, in spec_f1]
DoubleAdd.Cont.x [variable, in x]
DoubleAdd.Cont.y [variable, in y]
DoubleAdd.f0 [variable, in f0]
DoubleAdd.f1 [variable, in f1]
DoubleAdd.R [variable, in R]
DoubleAdd.spec_w_0 [variable, in spec_w_0]
DoubleAdd.spec_ww_1 [variable, in spec_ww_1]
DoubleAdd.spec_w_W0 [variable, in spec_w_W0]
DoubleAdd.spec_w_add_carry [variable, in spec_w_add_carry]
DoubleAdd.spec_w_add_carry_c [variable, in spec_w_add_carry_c]
DoubleAdd.spec_w_add [variable, in spec_w_add]
DoubleAdd.spec_w_add_c [variable, in spec_w_add_c]
DoubleAdd.spec_w_WW [variable, in spec_w_WW]
DoubleAdd.spec_to_Z [variable, in spec_to_Z]
DoubleAdd.spec_w_succ [variable, in spec_w_succ]
DoubleAdd.spec_w_succ_c [variable, in spec_w_succ_c]
DoubleAdd.spec_w_1 [variable, in spec_w_1]
DoubleAdd.w [variable, in w]
DoubleAdd.ww_1 [variable, in ww_1]
DoubleAdd.w_digits [variable, in w_digits]
DoubleAdd.w_add_carry_c [variable, in w_add_carry_c]
DoubleAdd.w_succ [variable, in w_succ]
DoubleAdd.w_add_c [variable, in w_add_c]
DoubleAdd.w_add [variable, in w_add]
DoubleAdd.w_1 [variable, in w_1]
DoubleAdd.w_succ_c [variable, in w_succ_c]
DoubleAdd.w_to_Z [variable, in w_to_Z]
DoubleAdd.w_add_carry [variable, in w_add_carry]
DoubleAdd.w_WW [variable, in w_WW]
DoubleAdd.w_0 [variable, in w_0]
DoubleAdd.w_W0 [variable, in w_W0]
[+[ _ ]] [notation, in ::'[+['_x_']]']
[+| _ |] [notation, in ::'[+|'_x_'|]']
[-[ _ ]] [notation, in ::'[-['_x_']]']
[-| _ |] [notation, in ::'[-|'_x_'|]']
[[ _ ]] [notation, in ::'[['_x_']]']
[| _ |] [notation, in ::'[|'_x_'|]']
DoubleBase [section, in DoubleBase]
DoubleBase [library]
DoubleBase.DoubleProof [section, in DoubleProof]
DoubleBase.DoubleProof.spec_w_Bm1 [variable, in spec_w_Bm1]
DoubleBase.DoubleProof.spec_w_0 [variable, in spec_w_0]
DoubleBase.DoubleProof.spec_w_WW [variable, in spec_w_WW]
DoubleBase.DoubleProof.spec_w_compare [variable, in spec_w_compare]
DoubleBase.DoubleProof.spec_to_Z [variable, in spec_to_Z]
DoubleBase.DoubleProof.spec_w_1 [variable, in spec_w_1]
DoubleBase.DoubleProof.spec_w_0W [variable, in spec_w_0W]
[! _ | _ !] [notation, in ::'[!'_x_'|'_x_'!]']
[+[ _ ]] [notation, in ::'[+['_x_']]']
[-[ _ ]] [notation, in ::'[-['_x_']]']
[[ _ ]] [notation, in ::'[['_x_']]']
[| _ |] [notation, in ::'[|'_x_'|]']
DoubleBase.w [variable, in w]
DoubleBase.w_digits [variable, in w_digits]
DoubleBase.w_compare [variable, in w_compare]
DoubleBase.w_add [variable, in w_add]
DoubleBase.w_1 [variable, in w_1]
DoubleBase.w_to_Z [variable, in w_to_Z]
DoubleBase.w_Bm1 [variable, in w_Bm1]
DoubleBase.w_WW [variable, in w_WW]
DoubleBase.w_0 [variable, in w_0]
DoubleBase.w_0W [variable, in w_0W]
DoubleBase.w_zdigits [variable, in w_zdigits]
DoubleCyclic [module, in DoubleCyclic]
DoubleCyclic [library]
DoubleCyclicKaratsuba [module, in DoubleCyclicKaratsuba]
DoubleCyclicKaratsuba.ops [definition, in ops]
DoubleCyclicKaratsuba.specs [definition, in specs]
DoubleCyclicKaratsuba.t [definition, in t]
DoubleCyclic.ops [instance, in ops]
DoubleCyclic.specs [instance, in specs]
DoubleCyclic.t [definition, in t]
DoubleDiv [section, in DoubleDiv]
DoubleDiv [library]
DoubleDivGt [section, in DoubleDivGt]
DoubleDivGt.spec_add_mul_div [variable, in spec_add_mul_div]
DoubleDivGt.spec_eq0 [variable, in spec_eq0]
DoubleDivGt.spec_div21 [variable, in spec_div21]
DoubleDivGt.spec_to_w_Z [variable, in spec_to_w_Z]
DoubleDivGt.spec_w_0 [variable, in spec_w_0]
DoubleDivGt.spec_ww_1 [variable, in spec_ww_1]
DoubleDivGt.spec_ww_add_mul_div [variable, in spec_ww_add_mul_div]
DoubleDivGt.spec_mod_gt [variable, in spec_mod_gt]
DoubleDivGt.spec_head0 [variable, in spec_head0]
DoubleDivGt.spec_opp_c [variable, in spec_opp_c]
DoubleDivGt.spec_ww_digits_ [variable, in spec_ww_digits_]
DoubleDivGt.spec_sub_carry [variable, in spec_sub_carry]
DoubleDivGt.spec_w_WW [variable, in spec_w_WW]
DoubleDivGt.spec_compare [variable, in spec_compare]
DoubleDivGt.spec_to_Z [variable, in spec_to_Z]
DoubleDivGt.spec_sub [variable, in spec_sub]
DoubleDivGt.spec_gcd_gt [variable, in spec_gcd_gt]
DoubleDivGt.spec_opp_carry [variable, in spec_opp_carry]
DoubleDivGt.spec_opp [variable, in spec_opp]
DoubleDivGt.spec_sub_c [variable, in spec_sub_c]
DoubleDivGt.spec_w_zdigits [variable, in spec_w_zdigits]
DoubleDivGt.spec_w_0W [variable, in spec_w_0W]
DoubleDivGt.spec_w_div32 [variable, in spec_w_div32]
DoubleDivGt.spec_div_gt [variable, in spec_div_gt]
DoubleDivGt.w [variable, in w]
DoubleDivGt.ww_add_mul_div [variable, in ww_add_mul_div]
DoubleDivGt.ww_1 [variable, in ww_1]
DoubleDivGt.w_opp [variable, in w_opp]
DoubleDivGt.w_mod_gt [variable, in w_mod_gt]
DoubleDivGt.w_div21 [variable, in w_div21]
DoubleDivGt.w_gcd_gt [variable, in w_gcd_gt]
DoubleDivGt.w_eq0 [variable, in w_eq0]
DoubleDivGt.w_digits [variable, in w_digits]
DoubleDivGt.w_head0 [variable, in w_head0]
DoubleDivGt.w_sub [variable, in w_sub]
DoubleDivGt.w_compare [variable, in w_compare]
DoubleDivGt.w_sub_c [variable, in w_sub_c]
DoubleDivGt.w_opp_c [variable, in w_opp_c]
DoubleDivGt.w_div32 [variable, in w_div32]
DoubleDivGt.w_div_gt [variable, in w_div_gt]
DoubleDivGt.w_to_Z [variable, in w_to_Z]
DoubleDivGt.w_sub_carry [variable, in w_sub_carry]
DoubleDivGt.w_opp_carry [variable, in w_opp_carry]
DoubleDivGt.w_WW [variable, in w_WW]
DoubleDivGt.w_add_mul_div [variable, in w_add_mul_div]
DoubleDivGt.w_0 [variable, in w_0]
DoubleDivGt.w_0W [variable, in w_0W]
DoubleDivGt.w_zdigits [variable, in w_zdigits]
DoubleDivGt._ww_zdigits [variable, in _ww_zdigits]
[-| _ |] [notation, in ::'[-|'_x_'|]']
[[ _ ]] [notation, in ::'[['_x_']]']
[| _ |] [notation, in ::'[|'_x_'|]']
DoubleDivn1 [library]
DoubleDiv.cont [variable, in cont]
DoubleDiv.spec_gcd_gt_fix [variable, in spec_gcd_gt_fix]
DoubleDiv.spec_eq0 [variable, in spec_eq0]
DoubleDiv.spec_w_0 [variable, in spec_w_0]
DoubleDiv.spec_cont [variable, in spec_cont]
DoubleDiv.spec_ww_1 [variable, in spec_ww_1]
DoubleDiv.spec_ww_digits_ [variable, in spec_ww_digits_]
DoubleDiv.spec_ww_div_gt [variable, in spec_ww_div_gt]
DoubleDiv.spec_compare [variable, in spec_compare]
DoubleDiv.spec_ww_compare [variable, in spec_ww_compare]
DoubleDiv.spec_to_Z [variable, in spec_to_Z]
DoubleDiv.spec_gcd_gt [variable, in spec_gcd_gt]
DoubleDiv.spec_w_1 [variable, in spec_w_1]
DoubleDiv.spec_ww_mod_gt [variable, in spec_ww_mod_gt]
DoubleDiv.w [variable, in w]
DoubleDiv.ww_gcd_gt_fix [variable, in ww_gcd_gt_fix]
DoubleDiv.ww_mod_gt [variable, in ww_mod_gt]
DoubleDiv.ww_div_gt [variable, in ww_div_gt]
DoubleDiv.ww_compare [variable, in ww_compare]
DoubleDiv.ww_1 [variable, in ww_1]
DoubleDiv.w_gcd_gt [variable, in w_gcd_gt]
DoubleDiv.w_eq0 [variable, in w_eq0]
DoubleDiv.w_digits [variable, in w_digits]
DoubleDiv.w_compare [variable, in w_compare]
DoubleDiv.w_1 [variable, in w_1]
DoubleDiv.w_to_Z [variable, in w_to_Z]
DoubleDiv.w_0 [variable, in w_0]
DoubleDiv._ww_digits [variable, in _ww_digits]
[[ _ ]] [notation, in ::'[['_x_']]']
[| _ |] [notation, in ::'[|'_x_'|]']
DoubleDiv21 [section, in DoubleDiv21]
DoubleDiv21.spec_w_0 [variable, in spec_w_0]
DoubleDiv21.spec_ww_sub [variable, in spec_ww_sub]
DoubleDiv21.spec_ww_1 [variable, in spec_ww_1]
DoubleDiv21.spec_ww_compare [variable, in spec_ww_compare]
DoubleDiv21.spec_to_Z [variable, in spec_to_Z]
DoubleDiv21.spec_w_0W [variable, in spec_w_0W]
DoubleDiv21.spec_w_div32 [variable, in spec_w_div32]
DoubleDiv21.w [variable, in w]
DoubleDiv21.ww_compare [variable, in ww_compare]
DoubleDiv21.ww_1 [variable, in ww_1]
DoubleDiv21.ww_sub [variable, in ww_sub]
DoubleDiv21.w_digits [variable, in w_digits]
DoubleDiv21.w_div32 [variable, in w_div32]
DoubleDiv21.w_to_Z [variable, in w_to_Z]
DoubleDiv21.w_0 [variable, in w_0]
DoubleDiv21.w_0W [variable, in w_0W]
[-[ _ ]] [notation, in ::'[-['_x_']]']
[[ _ ]] [notation, in ::'[['_x_']]']
[| _ |] [notation, in ::'[|'_x_'|]']
DoubleDiv32 [section, in DoubleDiv32]
DoubleDiv32.spec_w_Bm1 [variable, in spec_w_Bm1]
DoubleDiv32.spec_div21 [variable, in spec_div21]
DoubleDiv32.spec_pred [variable, in spec_pred]
DoubleDiv32.spec_w_0 [variable, in spec_w_0]
DoubleDiv32.spec_w_add_carry [variable, in spec_w_add_carry]
DoubleDiv32.spec_w_add_carry_c [variable, in spec_w_add_carry_c]
DoubleDiv32.spec_w_add [variable, in spec_w_add]
DoubleDiv32.spec_w_add_c [variable, in spec_w_add_c]
DoubleDiv32.spec_w_WW [variable, in spec_w_WW]
DoubleDiv32.spec_compare [variable, in spec_compare]
DoubleDiv32.spec_to_Z [variable, in spec_to_Z]
DoubleDiv32.spec_ww_sub_c [variable, in spec_ww_sub_c]
DoubleDiv32.spec_sub [variable, in spec_sub]
DoubleDiv32.spec_w_Bm2 [variable, in spec_w_Bm2]
DoubleDiv32.spec_mul_c [variable, in spec_mul_c]
DoubleDiv32.w [variable, in w]
DoubleDiv32.ww_sub_c [variable, in ww_sub_c]
DoubleDiv32.w_div21 [variable, in w_div21]
DoubleDiv32.w_digits [variable, in w_digits]
DoubleDiv32.w_mul_c [variable, in w_mul_c]
DoubleDiv32.w_add_carry_c [variable, in w_add_carry_c]
DoubleDiv32.w_sub [variable, in w_sub]
DoubleDiv32.w_compare [variable, in w_compare]
DoubleDiv32.w_add_c [variable, in w_add_c]
DoubleDiv32.w_add [variable, in w_add]
DoubleDiv32.w_to_Z [variable, in w_to_Z]
DoubleDiv32.w_Bm1 [variable, in w_Bm1]
DoubleDiv32.w_add_carry [variable, in w_add_carry]
DoubleDiv32.w_WW [variable, in w_WW]
DoubleDiv32.w_pred [variable, in w_pred]
DoubleDiv32.w_0 [variable, in w_0]
DoubleDiv32.w_Bm2 [variable, in w_Bm2]
[+| _ |] [notation, in ::'[+|'_x_'|]']
[-[ _ ]] [notation, in ::'[-['_x_']]']
[-| _ |] [notation, in ::'[-|'_x_'|]']
[[ _ ]] [notation, in ::'[['_x_']]']
[| _ |] [notation, in ::'[|'_x_'|]']
DoubleLift [section, in DoubleLift]
DoubleLift [library]
DoubleLift.DoubleProof [section, in DoubleProof]
DoubleLift.DoubleProof.spec_ww_digits [variable, in spec_ww_digits]
DoubleLift.DoubleProof.spec_low [variable, in spec_low]
DoubleLift.DoubleProof.spec_to_w_Z [variable, in spec_to_w_Z]
DoubleLift.DoubleProof.spec_w_0 [variable, in spec_w_0]
DoubleLift.DoubleProof.spec_ww_sub [variable, in spec_ww_sub]
DoubleLift.DoubleProof.spec_zdigits [variable, in spec_zdigits]
DoubleLift.DoubleProof.spec_w_head00 [variable, in spec_w_head00]
DoubleLift.DoubleProof.spec_w_W0 [variable, in spec_w_W0]
DoubleLift.DoubleProof.spec_w_head0 [variable, in spec_w_head0]
DoubleLift.DoubleProof.spec_w_add [variable, in spec_w_add]
DoubleLift.DoubleProof.spec_w_WW [variable, in spec_w_WW]
DoubleLift.DoubleProof.spec_compare [variable, in spec_compare]
DoubleLift.DoubleProof.spec_w_tail0 [variable, in spec_w_tail0]
DoubleLift.DoubleProof.spec_w_tail00 [variable, in spec_w_tail00]
DoubleLift.DoubleProof.spec_ww_zdigits [variable, in spec_ww_zdigits]
DoubleLift.DoubleProof.spec_ww_compare [variable, in spec_ww_compare]
DoubleLift.DoubleProof.spec_to_Z [variable, in spec_to_Z]
DoubleLift.DoubleProof.spec_w_add_mul_div [variable, in spec_w_add_mul_div]
DoubleLift.DoubleProof.spec_w_0W [variable, in spec_w_0W]
DoubleLift.DoubleProof.w_to_Z [variable, in w_to_Z]
[[ _ ]] [notation, in ::'[['_x_']]']
[| _ |] [notation, in ::'[|'_x_'|]']
DoubleLift.low [variable, in low]
DoubleLift.w [variable, in w]
DoubleLift.ww_zdigits [variable, in ww_zdigits]
DoubleLift.ww_Digits [variable, in ww_Digits]
DoubleLift.ww_compare [variable, in ww_compare]
DoubleLift.ww_sub [variable, in ww_sub]
DoubleLift.w_digits [variable, in w_digits]
DoubleLift.w_head0 [variable, in w_head0]
DoubleLift.w_compare [variable, in w_compare]
DoubleLift.w_add [variable, in w_add]
DoubleLift.w_WW [variable, in w_WW]
DoubleLift.w_add_mul_div [variable, in w_add_mul_div]
DoubleLift.w_0 [variable, in w_0]
DoubleLift.w_W0 [variable, in w_W0]
DoubleLift.w_0W [variable, in w_0W]
DoubleLift.w_zdigits [variable, in w_zdigits]
DoubleLift.w_tail0 [variable, in w_tail0]
DoubleMul [section, in DoubleMul]
DoubleMul [library]
DoubleMul.DoubleMulAddmn1 [section, in DoubleMulAddmn1]
DoubleMul.DoubleMulAddmn1.extend_n [variable, in extend_n]
DoubleMul.DoubleMulAddmn1.wn [variable, in wn]
DoubleMul.DoubleMulAddmn1.wn_WW [variable, in wn_WW]
DoubleMul.DoubleMulAddmn1.wn_0W [variable, in wn_0W]
DoubleMul.DoubleMulAddmn1.w_mul_add_n1 [variable, in w_mul_add_n1]
DoubleMul.DoubleMulAddn1 [section, in DoubleMulAddn1]
DoubleMul.DoubleMulAddn1Proof [section, in DoubleMulAddn1Proof]
DoubleMul.DoubleMulAddn1Proof.spec_w_mul_add [variable, in spec_w_mul_add]
DoubleMul.DoubleMulAddn1Proof.w_mul_add [variable, in w_mul_add]
DoubleMul.DoubleMulAddn1.w_mul_add [variable, in w_mul_add]
DoubleMul.spec_w_0 [variable, in spec_w_0]
DoubleMul.spec_w_square_c [variable, in spec_w_square_c]
DoubleMul.spec_ww_sub [variable, in spec_ww_sub]
DoubleMul.spec_ww_add_c [variable, in spec_ww_add_c]
DoubleMul.spec_w_W0 [variable, in spec_w_W0]
DoubleMul.spec_w_sub [variable, in spec_w_sub]
DoubleMul.spec_w_mul [variable, in spec_w_mul]
DoubleMul.spec_w_add [variable, in spec_w_add]
DoubleMul.spec_w_add_c [variable, in spec_w_add_c]
DoubleMul.spec_w_WW [variable, in spec_w_WW]
DoubleMul.spec_ww_add [variable, in spec_ww_add]
DoubleMul.spec_w_compare [variable, in spec_w_compare]
DoubleMul.spec_to_Z [variable, in spec_to_Z]
DoubleMul.spec_ww_sub_c [variable, in spec_ww_sub_c]
DoubleMul.spec_ww_add_carry [variable, in spec_ww_add_carry]
DoubleMul.spec_w_succ [variable, in spec_w_succ]
DoubleMul.spec_w_mul_c [variable, in spec_w_mul_c]
DoubleMul.spec_w_1 [variable, in spec_w_1]
DoubleMul.spec_w_0W [variable, in spec_w_0W]
DoubleMul.spec_more_than_1_digit [variable, in spec_more_than_1_digit]
DoubleMul.w [variable, in w]
DoubleMul.ww_add [variable, in ww_add]
DoubleMul.ww_add_c [variable, in ww_add_c]
DoubleMul.ww_sub_c [variable, in ww_sub_c]
DoubleMul.ww_add_carry [variable, in ww_add_carry]
DoubleMul.ww_sub [variable, in ww_sub]
DoubleMul.w_digits [variable, in w_digits]
DoubleMul.w_mul_c [variable, in w_mul_c]
DoubleMul.w_sub [variable, in w_sub]
DoubleMul.w_compare [variable, in w_compare]
DoubleMul.w_succ [variable, in w_succ]
DoubleMul.w_add_c [variable, in w_add_c]
DoubleMul.w_add [variable, in w_add]
DoubleMul.w_1 [variable, in w_1]
DoubleMul.w_mul [variable, in w_mul]
DoubleMul.w_to_Z [variable, in w_to_Z]
DoubleMul.w_WW [variable, in w_WW]
DoubleMul.w_0 [variable, in w_0]
DoubleMul.w_W0 [variable, in w_W0]
DoubleMul.w_square_c [variable, in w_square_c]
DoubleMul.w_0W [variable, in w_0W]
[! _ | _ !] [notation, in ::'[!'_x_'|'_x_'!]']
[+[ _ ]] [notation, in ::'[+['_x_']]']
[+| _ |] [notation, in ::'[+|'_x_'|]']
[-[ _ ]] [notation, in ::'[-['_x_']]']
[-| _ |] [notation, in ::'[-|'_x_'|]']
[[ _ ]] [notation, in ::'[['_x_']]']
[| _ |] [notation, in ::'[|'_x_'|]']
[|| _ ||] [notation, in ::'[||'_x_'||]']
DoubleQuote [definition, in DoubleQuote]
DoubleSqrt [section, in DoubleSqrt]
DoubleSqrt [library]
DoubleSqrt.low [variable, in low]
DoubleSqrt.spec_w_Bm1 [variable, in spec_w_Bm1]
DoubleSqrt.spec_ww_head0 [variable, in spec_ww_head0]
DoubleSqrt.spec_pred [variable, in spec_pred]
DoubleSqrt.spec_low [variable, in spec_low]
DoubleSqrt.spec_to_w_Z [variable, in spec_to_w_Z]
DoubleSqrt.spec_w_0 [variable, in spec_w_0]
DoubleSqrt.spec_w_square_c [variable, in spec_w_square_c]
DoubleSqrt.spec_ww_add_c [variable, in spec_ww_add_c]
DoubleSqrt.spec_ww_add_mul_div [variable, in spec_ww_add_mul_div]
DoubleSqrt.spec_ww_Bm1 [variable, in spec_ww_Bm1]
DoubleSqrt.spec_w_W0 [variable, in spec_w_W0]
DoubleSqrt.spec_w_sub [variable, in spec_w_sub]
DoubleSqrt.spec_ww_pred [variable, in spec_ww_pred]
DoubleSqrt.spec_w_div21 [variable, in spec_w_div21]
DoubleSqrt.spec_w_add_c [variable, in spec_w_add_c]
DoubleSqrt.spec_w_is_even [variable, in spec_w_is_even]
DoubleSqrt.spec_w_WW [variable, in spec_w_WW]
DoubleSqrt.spec_ww_add [variable, in spec_ww_add]
DoubleSqrt.spec_w_compare [variable, in spec_w_compare]
DoubleSqrt.spec_w_sqrt2 [variable, in spec_w_sqrt2]
DoubleSqrt.spec_ww_zdigits [variable, in spec_ww_zdigits]
DoubleSqrt.spec_ww_compare [variable, in spec_ww_compare]
DoubleSqrt.spec_to_Z [variable, in spec_to_Z]
DoubleSqrt.spec_ww_sub_c [variable, in spec_ww_sub_c]
DoubleSqrt.spec_w_add_mul_div [variable, in spec_w_add_mul_div]
DoubleSqrt.spec_w_1 [variable, in spec_w_1]
DoubleSqrt.spec_ww_pred_c [variable, in spec_ww_pred_c]
DoubleSqrt.spec_w_zdigits [variable, in spec_w_zdigits]
DoubleSqrt.spec_w_0W [variable, in spec_w_0W]
DoubleSqrt.spec_more_than_1_digit [variable, in spec_more_than_1_digit]
DoubleSqrt.w [variable, in w]
DoubleSqrt.wwBm1 [variable, in wwBm1]
DoubleSqrt.ww_add [variable, in ww_add]
DoubleSqrt.ww_add_c [variable, in ww_add_c]
DoubleSqrt.ww_zdigits [variable, in ww_zdigits]
DoubleSqrt.ww_head0 [variable, in ww_head0]
DoubleSqrt.ww_sub_c [variable, in ww_sub_c]
DoubleSqrt.ww_add_mul_div [variable, in ww_add_mul_div]
DoubleSqrt.ww_pred_c [variable, in ww_pred_c]
DoubleSqrt.ww_pred [variable, in ww_pred]
DoubleSqrt.ww_compare [variable, in ww_compare]
DoubleSqrt.w_is_even [variable, in w_is_even]
DoubleSqrt.w_div21 [variable, in w_div21]
DoubleSqrt.w_digits [variable, in w_digits]
DoubleSqrt.w_sub [variable, in w_sub]
DoubleSqrt.w_compare [variable, in w_compare]
DoubleSqrt.w_div2s [variable, in w_div2s]
DoubleSqrt.w_sub_c [variable, in w_sub_c]
DoubleSqrt.w_add_c [variable, in w_add_c]
DoubleSqrt.w_1 [variable, in w_1]
DoubleSqrt.w_to_Z [variable, in w_to_Z]
DoubleSqrt.w_Bm1 [variable, in w_Bm1]
DoubleSqrt.w_WW [variable, in w_WW]
DoubleSqrt.w_div21c [variable, in w_div21c]
DoubleSqrt.w_add_mul_div [variable, in w_add_mul_div]
DoubleSqrt.w_pred [variable, in w_pred]
DoubleSqrt.w_0 [variable, in w_0]
DoubleSqrt.w_sqrt2 [variable, in w_sqrt2]
DoubleSqrt.w_W0 [variable, in w_W0]
DoubleSqrt.w_square_c [variable, in w_square_c]
DoubleSqrt.w_0W [variable, in w_0W]
DoubleSqrt.w_zdigits [variable, in w_zdigits]
[! _ | _ !] [notation, in ::'[!'_x_'|'_x_'!]']
[+[ _ ]] [notation, in ::'[+['_x_']]']
[+| _ |] [notation, in ::'[+|'_x_'|]']
[-[ _ ]] [notation, in ::'[-['_x_']]']
[-| _ |] [notation, in ::'[-|'_x_'|]']
[[ _ ]] [notation, in ::'[['_x_']]']
[| _ |] [notation, in ::'[|'_x_'|]']
[|| _ ||] [notation, in ::'[||'_x_'||]']
DoubleSub [section, in DoubleSub]
DoubleSub [library]
DoubleSub.spec_pred_c [variable, in spec_pred_c]
DoubleSub.spec_w_Bm1 [variable, in spec_w_Bm1]
DoubleSub.spec_pred [variable, in spec_pred]
DoubleSub.spec_w_0 [variable, in spec_w_0]
DoubleSub.spec_ww_Bm1 [variable, in spec_ww_Bm1]
DoubleSub.spec_opp_c [variable, in spec_opp_c]
DoubleSub.spec_sub_carry [variable, in spec_sub_carry]
DoubleSub.spec_w_WW [variable, in spec_w_WW]
DoubleSub.spec_to_Z [variable, in spec_to_Z]
DoubleSub.spec_sub [variable, in spec_sub]
DoubleSub.spec_opp_carry [variable, in spec_opp_carry]
DoubleSub.spec_opp [variable, in spec_opp]
DoubleSub.spec_sub_c [variable, in spec_sub_c]
DoubleSub.spec_sub_carry_c [variable, in spec_sub_carry_c]
DoubleSub.w [variable, in w]
DoubleSub.ww_Bm1 [variable, in ww_Bm1]
DoubleSub.w_opp [variable, in w_opp]
DoubleSub.w_sub_carry_c [variable, in w_sub_carry_c]
DoubleSub.w_digits [variable, in w_digits]
DoubleSub.w_sub [variable, in w_sub]
DoubleSub.w_sub_c [variable, in w_sub_c]
DoubleSub.w_opp_c [variable, in w_opp_c]
DoubleSub.w_to_Z [variable, in w_to_Z]
DoubleSub.w_Bm1 [variable, in w_Bm1]
DoubleSub.w_sub_carry [variable, in w_sub_carry]
DoubleSub.w_opp_carry [variable, in w_opp_carry]
DoubleSub.w_WW [variable, in w_WW]
DoubleSub.w_pred_c [variable, in w_pred_c]
DoubleSub.w_pred [variable, in w_pred]
DoubleSub.w_0 [variable, in w_0]
[+[ _ ]] [notation, in ::'[+['_x_']]']
[+| _ |] [notation, in ::'[+|'_x_'|]']
[-[ _ ]] [notation, in ::'[-['_x_']]']
[-| _ |] [notation, in ::'[-|'_x_'|]']
[[ _ ]] [notation, in ::'[['_x_']]']
[| _ |] [notation, in ::'[|'_x_'|]']
DoubleType [library]
double_modn1 [definition, in double_modn1]
double_twice [lemma, in double_twice]
double_modn1_0_aux [definition, in double_modn1_0_aux]
double_wB_wwB [lemma, in double_wB_wwB]
double_mul_c [definition, in double_mul_c]
double_var [lemma, in double_var]
double_twice_firstl [lemma, in double_twice_firstl]
double_divn1_0 [definition, in double_divn1_0]
double_split [definition, in double_split]
double_plus [lemma, in double_plus]
double_wB_pos [lemma, in double_wB_pos]
double_twice_plus_one_firstl [lemma, in double_twice_plus_one_firstl]
double_to_Z [definition, in double_to_Z]
double_divn1_p [definition, in double_divn1_p]
double_odd [lemma, in double_odd]
double_modn1_p [definition, in double_modn1_p]
double_WW [definition, in double_WW]
double_moins_un_xO_discr [abbreviation, in double_moins_un_xO_discr]
double_divn1 [definition, in double_divn1]
double_mul_add_mn1 [definition, in double_mul_add_mn1]
double_wB_more_digits [lemma, in double_wB_more_digits]
double_wB [definition, in double_wB]
double_modn1_p_aux [definition, in double_modn1_p_aux]
double_even [lemma, in double_even]
double_modn1_0 [definition, in double_modn1_0]
double_divn1_0_aux [definition, in double_divn1_0_aux]
double_divn1_p_aux [definition, in double_divn1_p_aux]
double_0 [definition, in double_0]
double_S [lemma, in double_S]
double_mul_add_n1 [definition, in double_mul_add_n1]
do_subrelation [constructor, in do_subrelation]
Dpower [lemma, in Dpower]
DrinkerParadox [definition, in DrinkerParadox]
DSO_to_OT [module, in DSO_to_OT]
Dx [lemma, in Dx]
Dx_pow_n [lemma, in Dx_pow_n]
D_in [definition, in D_in]
d_nil [constructor, in d_nil]
d_one [constructor, in d_one]
D_pow_n [lemma, in D_pow_n]
D_in_imp [lemma, in D_in_imp]
D_x_no_cond [lemma, in D_x_no_cond]
D_x [definition, in D_x]
D_in_ext [lemma, in D_in_ext]
d_conc [constructor, in d_conc]
D0 [constructor, in D0]
d1 [projection, in d1]
D1 [constructor, in D1]
d2 [projection, in d2]