S
S [module, in S]
S [module, in S]
S [module, in S]
S [constructor, in S]
Same_set [definition, in Same_set]
same_relation_is_equivalence [lemma, in same_relation_is_equivalence]
same_relation [definition, in same_relation]
same_relation [definition, in same_relation]
sb [definition, in sb]
scal_sum [lemma, in scal_sum]
SCANNING [section, in SCANNING]
SCHEMES [section, in SCHEMES]
SCHEMES [section, in SCHEMES]
Sdep [module, in Sdep]
Sdep.add [axiom, in add]
Sdep.Add [definition, in Add]
Sdep.cardinal [axiom, in cardinal]
Sdep.choose [axiom, in choose]
Sdep.choose_equal [axiom, in choose_equal]
Sdep.compare [axiom, in compare]
Sdep.diff [axiom, in diff]
Sdep.E [module, in Sdep.E]
Sdep.elements [axiom, in elements]
Sdep.elt [definition, in elt]
Sdep.empty [axiom, in empty]
Sdep.Empty [definition, in Empty]
Sdep.eq [definition, in eq]
Sdep.equal [axiom, in equal]
Sdep.Equal [definition, in Equal]
Sdep.eq_refl [axiom, in eq_refl]
Sdep.eq_sym [axiom, in eq_sym]
Sdep.eq_trans [axiom, in eq_trans]
Sdep.eq_In [axiom, in eq_In]
Sdep.Exists [definition, in Exists]
Sdep.exists_ [axiom, in exists_]
Sdep.filter [axiom, in filter]
Sdep.fold [axiom, in fold]
Sdep.For_all [definition, in For_all]
Sdep.for_all [axiom, in for_all]
Sdep.In [axiom, in In]
Sdep.inter [axiom, in inter]
Sdep.is_empty [axiom, in is_empty]
Sdep.lt [axiom, in lt]
Sdep.lt_not_eq [axiom, in lt_not_eq]
Sdep.lt_trans [axiom, in lt_trans]
Sdep.max_elt [axiom, in max_elt]
Sdep.mem [axiom, in mem]
Sdep.min_elt [axiom, in min_elt]
Sdep.partition [axiom, in partition]
Sdep.remove [axiom, in remove]
Sdep.singleton [axiom, in singleton]
Sdep.Subset [definition, in Subset]
Sdep.subset [axiom, in subset]
Sdep.t [axiom, in t]
Sdep.union [axiom, in union]
_ [=] _ [notation, in ::x_'[=]'_x]
seq [definition, in seq]
seq [definition, in seq]
SeqProp [library]
SeqSeries [library]
sequence [section, in sequence]
sequence_lb [definition, in sequence_lb]
sequence_minorant [abbreviation, in sequence_minorant]
sequence_majorant [abbreviation, in sequence_majorant]
sequence_ub [definition, in sequence_ub]
sequence.Un [variable, in Un]
seq_nth [lemma, in seq_nth]
seq_refl [lemma, in seq_refl]
Seq_refl [definition, in Seq_refl]
Seq_sym [definition, in Seq_sym]
seq_right [lemma, in seq_right]
seq_left [lemma, in seq_left]
seq_congr [lemma, in seq_congr]
seq_shift [lemma, in seq_shift]
seq_sym [lemma, in seq_sym]
seq_length [lemma, in seq_length]
Seq_trans [definition, in Seq_trans]
seq_trans [lemma, in seq_trans]
set [definition, in set]
setcover_inv [lemma, in setcover_inv]
setcover_intro [lemma, in setcover_intro]
SetIncl [section, in SetIncl]
SetIncl.A [variable, in A]
SetIsType [library]
Setminus [definition, in Setminus]
Setminus_intro [lemma, in Setminus_intro]
Setoid [record, in Setoid]
Setoid [library]
SetoidClass [library]
SetoidDec [library]
SetoidList [library]
SetoidPermutation [library]
SetoidTactics [library]
setoid_refl [definition, in setoid_refl]
setoid_morphism [instance, in setoid_morphism]
setoid_equiv [projection, in setoid_equiv]
setoid_partial_app_morphism [instance, in setoid_partial_app_morphism]
Setoid_Theory [definition, in Setoid_Theory]
setoid_sym [definition, in setoid_sym]
setoid_trans [definition, in setoid_trans]
setoid_decidable [projection, in setoid_decidable]
setoid_decidable [constructor, in setoid_decidable]
setoid_decidable [projection, in setoid_decidable]
setoid_decidable [constructor, in setoid_decidable]
Sets [module, in Sets]
SetsOn [module, in SetsOn]
SetsOn.choose_spec3 [axiom, in choose_spec3]
SetsOn.compare_spec [axiom, in compare_spec]
SetsOn.elements_spec2 [axiom, in elements_spec2]
SetsOn.max_elt_spec3 [axiom, in max_elt_spec3]
SetsOn.max_elt_spec2 [axiom, in max_elt_spec2]
SetsOn.max_elt_spec1 [axiom, in max_elt_spec1]
SetsOn.min_elt_spec2 [axiom, in min_elt_spec2]
SetsOn.min_elt_spec3 [axiom, in min_elt_spec3]
SetsOn.min_elt_spec1 [axiom, in min_elt_spec1]
SetsOn.Spec [section, in Spec]
SetsOn.Spec.s [variable, in s]
SetsOn.Spec.s' [variable, in s']
SetsOn.Spec.x [variable, in x]
SetsOn.Spec.y [variable, in y]
Sets_as_an_algebra.U [variable, in U]
Sets_as_an_algebra.U [variable, in U]
Sets_as_an_algebra [section, in Sets_as_an_algebra]
Sets_as_an_algebra [section, in Sets_as_an_algebra]
Sets.E [module, in Sets.E]
set_fold_right [definition, in set_fold_right]
set_add_elim2 [lemma, in set_add_elim2]
set_union_intro1 [lemma, in set_union_intro1]
set_union [definition, in set_union]
set_union_intro [lemma, in set_union_intro]
set_map [definition, in set_map]
set_diff_intro [lemma, in set_diff_intro]
set_inter_elim2 [lemma, in set_inter_elim2]
set_mem_correct2 [lemma, in set_mem_correct2]
set_add_elim [lemma, in set_add_elim]
set_mem [definition, in set_mem]
set_diff [definition, in set_diff]
set_prod [definition, in set_prod]
set_add_intro2 [lemma, in set_add_intro2]
set_add_intro [lemma, in set_add_intro]
set_add_intro1 [lemma, in set_add_intro1]
set_union_elim [lemma, in set_union_elim]
set_mem_ind [lemma, in set_mem_ind]
set_In [definition, in set_In]
set_diff_elim2 [lemma, in set_diff_elim2]
set_In_dec [lemma, in set_In_dec]
set_mem_correct1 [lemma, in set_mem_correct1]
set_remove [definition, in set_remove]
set_diff_trivial [lemma, in set_diff_trivial]
set_power [definition, in set_power]
set_union_emptyR [lemma, in set_union_emptyR]
set_add [definition, in set_add]
set_diff_elim1 [lemma, in set_diff_elim1]
set_union_emptyL [lemma, in set_union_emptyL]
set_inter [definition, in set_inter]
set_fold_left [definition, in set_fold_left]
set_inter_elim1 [lemma, in set_inter_elim1]
set_add_not_empty [lemma, in set_add_not_empty]
set_inter_elim [lemma, in set_inter_elim]
set_mem_complete1 [lemma, in set_mem_complete1]
set_mem_ind2 [lemma, in set_mem_ind2]
set_union_intro2 [lemma, in set_union_intro2]
set_mem_complete2 [lemma, in set_mem_complete2]
set_inter_intro [lemma, in set_inter_intro]
SFL [definition, in SFL]
SFL_continuity [lemma, in SFL_continuity]
SFL_continuity_pt [lemma, in SFL_continuity_pt]
Sfun [module, in Sfun]
Sfun [module, in Sfun]
Sfun.choose_3 [axiom, in choose_3]
Sfun.compare [axiom, in compare]
Sfun.elements_3 [axiom, in elements_3]
Sfun.elements_3 [axiom, in elements_3]
Sfun.elt [section, in elt]
Sfun.elt.elt [variable, in elt]
Sfun.lt [axiom, in lt]
Sfun.lt_key [definition, in lt_key]
Sfun.lt_not_eq [axiom, in lt_not_eq]
Sfun.lt_trans [axiom, in lt_trans]
Sfun.max_elt [axiom, in max_elt]
Sfun.max_elt_1 [axiom, in max_elt_1]
Sfun.max_elt_3 [axiom, in max_elt_3]
Sfun.max_elt_2 [axiom, in max_elt_2]
Sfun.min_elt_3 [axiom, in min_elt_3]
Sfun.min_elt_2 [axiom, in min_elt_2]
Sfun.min_elt_1 [axiom, in min_elt_1]
Sfun.min_elt [axiom, in min_elt]
Sfun.Spec [section, in Spec]
Sfun.Spec.s [variable, in s]
Sfun.Spec.s' [variable, in s']
Sfun.Spec.s'' [variable, in s'']
Sfun.Spec.x [variable, in x]
Sfun.Spec.y [variable, in y]
shift [definition, in shift]
shift [definition, in shift]
shiftin [definition, in shiftin]
shiftin_nth [lemma, in shiftin_nth]
shiftin_last [lemma, in shiftin_last]
shiftl [definition, in shiftl]
shiftl [definition, in shiftl]
shiftl_spec_low [lemma, in shiftl_spec_low]
shiftl_spec_high [lemma, in shiftl_spec_high]
shiftout [definition, in shiftout]
shiftr [definition, in shiftr]
shiftr [definition, in shiftr]
shiftrepeat [definition, in shiftrepeat]
shiftrepeat_nth [lemma, in shiftrepeat_nth]
shiftrepeat_last [lemma, in shiftrepeat_last]
shiftr_spec [lemma, in shiftr_spec]
shift_pos_nat [lemma, in shift_pos_nat]
shift_equiv [lemma, in shift_equiv]
shift_pos [definition, in shift_pos]
shift_nat [definition, in shift_nat]
shift_nat_plus [lemma, in shift_nat_plus]
shift_pos_correct [lemma, in shift_pos_correct]
shift_unshift_mod [lemma, in shift_unshift_mod]
shift_nat_correct [lemma, in shift_nat_correct]
shift_unshift_mod_2 [lemma, in shift_unshift_mod_2]
shift_nat_equiv [lemma, in shift_nat_equiv]
shift_pos_equiv [lemma, in shift_pos_equiv]
sig [inductive, in sig]
sigma [definition, in sigma]
Sigma [section, in Sigma]
sigma_split [lemma, in sigma_split]
sigma_first [lemma, in sigma_first]
sigma_eq_arg [lemma, in sigma_eq_arg]
sigma_last [lemma, in sigma_last]
sigma_diff [lemma, in sigma_diff]
sigma_diff_neg [lemma, in sigma_diff_neg]
Sigma.f [variable, in f]
sigS [abbreviation, in sigS]
sigS_rect [abbreviation, in sigS_rect]
sigS_rec [abbreviation, in sigS_rec]
sigS_ind [abbreviation, in sigS_ind]
sigS2 [abbreviation, in sigS2]
sigS2_ind [abbreviation, in sigS2_ind]
sigS2_rect [abbreviation, in sigS2_rect]
sigS2_rec [abbreviation, in sigS2_rec]
sigT [inductive, in sigT]
sigT_of_sig [lemma, in sigT_of_sig]
sigT2 [inductive, in sigT2]
sig_of_sigT [lemma, in sig_of_sigT]
sig_forall_dec [lemma, in sig_forall_dec]
sig2 [inductive, in sig2]
SimpleMergeExample [definition, in SimpleMergeExample]
simplification_heq [lemma, in simplification_heq]
simplification_K [lemma, in simplification_K]
simplification_existT2 [lemma, in simplification_existT2]
simplification_existT1 [lemma, in simplification_existT1]
Simplify_add [lemma, in Simplify_add]
SimplOp [section, in SimplOp]
SimplOp.w [variable, in w]
simpl_fact [lemma, in simpl_fact]
simpl_sin_n [lemma, in simpl_sin_n]
simpl_cos_n [lemma, in simpl_cos_n]
SIN [lemma, in SIN]
sin [definition, in sin]
sincl_add_x [lemma, in sincl_add_x]
sind [definition, in sind]
Singleton [definition, in Singleton]
Singleton [inductive, in Singleton]
SingletonBag [definition, in SingletonBag]
Singleton_atomic [lemma, in Singleton_atomic]
Singleton_is_finite [lemma, in Singleton_is_finite]
singleton_choice [lemma, in singleton_choice]
Singleton_intro [lemma, in Singleton_intro]
Singleton_inv [lemma, in Singleton_inv]
single_limit [lemma, in single_limit]
single_z_r_R1 [lemma, in single_z_r_R1]
singlx [lemma, in singlx]
sinh [definition, in sinh]
sinh_0 [lemma, in sinh_0]
sin_0 [lemma, in sin_0]
sin_gt_0 [lemma, in sin_gt_0]
sin_n [definition, in sin_n]
sin_shift [lemma, in sin_shift]
sin_in [definition, in sin_in]
sin_pos_tech [lemma, in sin_pos_tech]
sin_lb_gt_0 [lemma, in sin_lb_gt_0]
sin_decr_0 [lemma, in sin_decr_0]
sin_bound [lemma, in sin_bound]
sin_2PI3 [lemma, in sin_2PI3]
sin_ub [definition, in sin_ub]
sin_no_R0 [lemma, in sin_no_R0]
sin_minus [lemma, in sin_minus]
sin_5PI4 [lemma, in sin_5PI4]
SIN_bound [lemma, in SIN_bound]
sin_approx [definition, in sin_approx]
sin_eq_0_1 [lemma, in sin_eq_0_1]
sin_incr_1 [lemma, in sin_incr_1]
sin_period [lemma, in sin_period]
sin_PI_x [lemma, in sin_PI_x]
sin_decreasing_0 [lemma, in sin_decreasing_0]
sin_lt_0 [lemma, in sin_lt_0]
sin_increasing_1 [lemma, in sin_increasing_1]
sin_PI [lemma, in sin_PI]
sin_PI6 [lemma, in sin_PI6]
sin_ge_0 [lemma, in sin_ge_0]
sin_lb_ge_0 [lemma, in sin_lb_ge_0]
sin_PI4 [lemma, in sin_PI4]
sin_PI2 [lemma, in sin_PI2]
sin_cos5PI4 [lemma, in sin_cos5PI4]
sin_eq_O_2PI_1 [lemma, in sin_eq_O_2PI_1]
sin_increasing_0 [lemma, in sin_increasing_0]
sin_term [definition, in sin_term]
sin_PI3_cos_PI6 [lemma, in sin_PI3_cos_PI6]
sin_neg [lemma, in sin_neg]
sin_PI3 [lemma, in sin_PI3]
sin_3PI2 [lemma, in sin_3PI2]
sin_lt_0_var [lemma, in sin_lt_0_var]
sin_cos [lemma, in sin_cos]
sin_lb [definition, in sin_lb]
sin_PI6_cos_PI3 [lemma, in sin_PI6_cos_PI3]
sin_cos_PI4 [lemma, in sin_cos_PI4]
sin_eq_O_2PI_0 [lemma, in sin_eq_O_2PI_0]
sin_plus [lemma, in sin_plus]
sin_gt_cos_7_8 [lemma, in sin_gt_cos_7_8]
sin_le_0 [lemma, in sin_le_0]
sin_decr_1 [lemma, in sin_decr_1]
sin_2PI [lemma, in sin_2PI]
sin_2a [lemma, in sin_2a]
sin_eq_0_0 [lemma, in sin_eq_0_0]
sin_antisym [lemma, in sin_antisym]
sin_incr_0 [lemma, in sin_incr_0]
sin_decreasing_1 [lemma, in sin_decreasing_1]
sin2 [lemma, in sin2]
sin2_cos2 [lemma, in sin2_cos2]
sin3PI4 [lemma, in sin3PI4]
size [definition, in size]
skipn [definition, in skipn]
SmallDrinker'sParadox [definition, in SmallDrinker'sParadox]
small_drinkers'_paradox [lemma, in small_drinkers'_paradox]
Snd [abbreviation, in Snd]
snd [definition, in snd]
SndRel_ProdRel [lemma, in SndRel_ProdRel]
SndRel_sub [instance, in SndRel_sub]
sndT [abbreviation, in sndT]
snd_compat [instance, in snd_compat]
snd_measure [instance, in snd_measure]
sneakl [definition, in sneakl]
sneakl_shiftr [lemma, in sneakl_shiftr]
sneakr [definition, in sneakr]
sneakr_shiftl [lemma, in sneakr_shiftl]
solution_right [lemma, in solution_right]
solution_left [lemma, in solution_left]
sol_x1 [definition, in sol_x1]
sol_x2 [definition, in sol_x2]
Some [constructor, in Some]
Sord [module, in Sord]
Sord.cmp [definition, in cmp]
Sord.compare [axiom, in compare]
Sord.Data [module, in Sord.Data]
Sord.eq [axiom, in eq]
Sord.eq_refl [axiom, in eq_refl]
Sord.eq_1 [axiom, in eq_1]
Sord.eq_2 [axiom, in eq_2]
Sord.eq_sym [axiom, in eq_sym]
Sord.eq_trans [axiom, in eq_trans]
Sord.lt [axiom, in lt]
Sord.lt_not_eq [axiom, in lt_not_eq]
Sord.lt_trans [axiom, in lt_trans]
Sord.MapS [module, in Sord.MapS]
Sord.t [definition, in t]
sort [abbreviation, in sort]
Sort [module, in Sort]
SortA [abbreviation, in SortA]
SortA_InfA_InA [lemma, in SortA_InfA_InA]
SortA_app [lemma, in SortA_app]
SortA_NoDupA [lemma, in SortA_NoDupA]
SortA_equivlistA_eqlistA [lemma, in SortA_equivlistA_eqlistA]
Sorted [inductive, in Sorted]
Sorted [library]
Sorted_cons [constructor, in Sorted_cons]
Sorted_rect [lemma, in Sorted_rect]
Sorted_inv [lemma, in Sorted_inv]
Sorted_nil [constructor, in Sorted_nil]
Sorted_extends [lemma, in Sorted_extends]
Sorted_LocallySorted_iff [lemma, in Sorted_LocallySorted_iff]
Sorted_StronglySorted [lemma, in Sorted_StronglySorted]
Sorting [library]
sort_inv [abbreviation, in sort_inv]
sort_rect [abbreviation, in sort_rect]
Sort.flatten_stack [definition, in flatten_stack]
Sort.iter_merge [definition, in iter_merge]
Sort.LocallySorted_sort [lemma, in LocallySorted_sort]
Sort.merge [definition, in merge]
Sort.merge_stack [definition, in merge_stack]
Sort.merge_list_to_stack [definition, in merge_list_to_stack]
Sort.Permuted_merge_stack [lemma, in Permuted_merge_stack]
Sort.Permuted_sort [lemma, in Permuted_sort]
Sort.Permuted_iter_merge [lemma, in Permuted_iter_merge]
Sort.Permuted_merge [lemma, in Permuted_merge]
Sort.Permuted_merge_list_to_stack [lemma, in Permuted_merge_list_to_stack]
Sort.sort [definition, in sort]
Sort.Sorted [abbreviation, in Sorted]
Sort.SortedStack [definition, in SortedStack]
Sort.Sorted_merge [lemma, in Sorted_merge]
Sort.Sorted_merge_list_to_stack [lemma, in Sorted_merge_list_to_stack]
Sort.Sorted_sort [lemma, in Sorted_sort]
Sort.Sorted_merge_stack [lemma, in Sorted_merge_stack]
Sort.Sorted_iter_merge [lemma, in Sorted_iter_merge]
Sort.StronglySorted_sort [lemma, in StronglySorted_sort]
SP [definition, in SP]
Space [definition, in Space]
Specif [library]
Specific_orders.U [variable, in U]
Specific_orders [section, in Specific_orders]
spec_ww_sqrt2 [lemma, in spec_ww_sqrt2]
spec_pred_c [lemma, in spec_pred_c]
spec_pred_c [lemma, in spec_pred_c]
spec_add_mul_div [lemma, in spec_add_mul_div]
spec_add_mul_div [lemma, in spec_add_mul_div]
spec_eq0 [lemma, in spec_eq0]
spec_eq0 [lemma, in spec_eq0]
spec_w_div2s [lemma, in spec_w_div2s]
spec_double_modn1_p [lemma, in spec_double_modn1_p]
spec_of_pos [lemma, in spec_of_pos]
spec_sqrt2 [lemma, in spec_sqrt2]
spec_sqrt2 [lemma, in spec_sqrt2]
spec_mul_aux [lemma, in spec_mul_aux]
spec_div21 [lemma, in spec_div21]
spec_div21 [lemma, in spec_div21]
spec_is_even [lemma, in spec_is_even]
spec_is_even [lemma, in spec_is_even]
spec_ww_opp [lemma, in spec_ww_opp]
spec_ww_head0 [lemma, in spec_ww_head0]
spec_pred [lemma, in spec_pred]
spec_pred [lemma, in spec_pred]
spec_head00 [lemma, in spec_head00]
spec_head00 [lemma, in spec_head00]
spec_double_to_Z [lemma, in spec_double_to_Z]
spec_to_N [lemma, in spec_to_N]
spec_w_div21c [lemma, in spec_w_div21c]
spec_ww_gcd [lemma, in spec_ww_gcd]
spec_double_divn1 [lemma, in spec_double_divn1]
spec_double_modn1_aux [lemma, in spec_double_modn1_aux]
spec_add [lemma, in spec_add]
spec_add [lemma, in spec_add]
spec_ww_pos_mod [lemma, in spec_ww_pos_mod]
spec_double_mul_add_n1 [lemma, in spec_double_mul_add_n1]
spec_compare_mn_1 [lemma, in spec_compare_mn_1]
spec_ww_sub [lemma, in spec_ww_sub]
spec_w_mod_gt_eq [lemma, in spec_w_mod_gt_eq]
spec_double_mul_c [lemma, in spec_double_mul_c]
spec_double_WW [lemma, in spec_double_WW]
spec_ww_add_c [lemma, in spec_ww_add_c]
spec_zdigits [lemma, in spec_zdigits]
spec_zdigits [lemma, in spec_zdigits]
spec_ww_1 [lemma, in spec_ww_1]
spec_succ_c [lemma, in spec_succ_c]
spec_succ_c [lemma, in spec_succ_c]
spec_ww_add_mul_div [lemma, in spec_ww_add_mul_div]
spec_ww_add_mul_div [lemma, in spec_ww_add_mul_div]
spec_ww_mul_c [lemma, in spec_ww_mul_c]
spec_ww_add_mul_div_aux [lemma, in spec_ww_add_mul_div_aux]
spec_ww_Bm1 [lemma, in spec_ww_Bm1]
spec_double_split [lemma, in spec_double_split]
spec_Bm1 [lemma, in spec_Bm1]
spec_ww_gcd_gt_aux_body [lemma, in spec_ww_gcd_gt_aux_body]
spec_ww_pred [lemma, in spec_ww_pred]
spec_double_modn1_0 [lemma, in spec_double_modn1_0]
spec_mul [lemma, in spec_mul]
spec_mul [lemma, in spec_mul]
spec_head0 [lemma, in spec_head0]
spec_head0 [lemma, in spec_head0]
spec_ww_square_c [lemma, in spec_ww_square_c]
spec_tail00 [lemma, in spec_tail00]
spec_tail00 [lemma, in spec_tail00]
spec_ww_mod_gt_aux [lemma, in spec_ww_mod_gt_aux]
spec_ww_sub_carry [lemma, in spec_ww_sub_carry]
spec_ww_opp_c [lemma, in spec_ww_opp_c]
spec_opp_c [lemma, in spec_opp_c]
spec_opp_c [lemma, in spec_opp_c]
spec_ww_is_even [lemma, in spec_ww_is_even]
spec_square_c [lemma, in spec_square_c]
spec_to_Z_1 [lemma, in spec_to_Z_1]
spec_square_c [lemma, in spec_square_c]
spec_ww_sqrt [lemma, in spec_ww_sqrt]
spec_sub_carry [lemma, in spec_sub_carry]
spec_sub_carry [lemma, in spec_sub_carry]
spec_ww_div [lemma, in spec_ww_div]
spec_1 [lemma, in spec_1]
spec_1 [lemma, in spec_1]
spec_ww_tail00 [lemma, in spec_ww_tail00]
spec_get_low [lemma, in spec_get_low]
spec_double_divn1_p [lemma, in spec_double_divn1_p]
spec_ww_to_Z_wBwB [lemma, in spec_ww_to_Z_wBwB]
spec_double_digits [lemma, in spec_double_digits]
spec_high [lemma, in spec_high]
spec_m1 [lemma, in spec_m1]
spec_ww_div_gt [lemma, in spec_ww_div_gt]
spec_ww_mod_gt_aux_eq [lemma, in spec_ww_mod_gt_aux_eq]
spec_tail0 [lemma, in spec_tail0]
spec_tail0 [lemma, in spec_tail0]
spec_ww_add [lemma, in spec_ww_add]
spec_ww_sub_carry_c [lemma, in spec_ww_sub_carry_c]
spec_modulo [lemma, in spec_modulo]
spec_extend [lemma, in spec_extend]
spec_compare [lemma, in spec_compare]
spec_compare [lemma, in spec_compare]
spec_ww_head1 [lemma, in spec_ww_head1]
spec_div [lemma, in spec_div]
spec_div [lemma, in spec_div]
spec_ww_compare [lemma, in spec_ww_compare]
spec_modulo_gt [lemma, in spec_modulo_gt]
spec_to_Z [lemma, in spec_to_Z]
spec_to_Z [lemma, in spec_to_Z]
spec_ww_gcd_gt [lemma, in spec_ww_gcd_gt]
spec_ww_sub_c [lemma, in spec_ww_sub_c]
spec_ww_add_carry [lemma, in spec_ww_add_carry]
spec_kara_prod [lemma, in spec_kara_prod]
spec_add_mul_divp [lemma, in spec_add_mul_divp]
spec_sub [lemma, in spec_sub]
spec_sub [lemma, in spec_sub]
spec_pos_mod [lemma, in spec_pos_mod]
spec_pos_mod [lemma, in spec_pos_mod]
spec_succ [lemma, in spec_succ]
spec_succ [lemma, in spec_succ]
spec_gcd_gt [lemma, in spec_gcd_gt]
spec_compare0_mn [lemma, in spec_compare0_mn]
spec_ww_mul [lemma, in spec_ww_mul]
spec_w_mul_add [lemma, in spec_w_mul_add]
spec_opp_carry [lemma, in spec_opp_carry]
spec_opp_carry [lemma, in spec_opp_carry]
spec_ww_karatsuba_c [lemma, in spec_ww_karatsuba_c]
spec_ww_mod [lemma, in spec_ww_mod]
spec_add_carry_c [lemma, in spec_add_carry_c]
spec_add_carry_c [lemma, in spec_add_carry_c]
spec_sqrt [lemma, in spec_sqrt]
spec_sqrt [lemma, in spec_sqrt]
spec_gcd_cont [lemma, in spec_gcd_cont]
spec_ww_is_zero [lemma, in spec_ww_is_zero]
spec_ww_gcd_gt_aux [lemma, in spec_ww_gcd_gt_aux]
spec_add_c [lemma, in spec_add_c]
spec_add_c [lemma, in spec_add_c]
spec_double_modn1 [lemma, in spec_double_modn1]
spec_ww_head00 [lemma, in spec_ww_head00]
spec_w_2 [lemma, in spec_w_2]
spec_opp [lemma, in spec_opp]
spec_opp [lemma, in spec_opp]
spec_sub_c [lemma, in spec_sub_c]
spec_sub_c [lemma, in spec_sub_c]
spec_double_0 [lemma, in spec_double_0]
spec_ww_mod_gt_eq [lemma, in spec_ww_mod_gt_eq]
spec_split [lemma, in spec_split]
spec_split [lemma, in spec_split]
spec_double_divn1_0 [lemma, in spec_double_divn1_0]
spec_add_carry [lemma, in spec_add_carry]
spec_add_carry [lemma, in spec_add_carry]
spec_gcd [lemma, in spec_gcd]
spec_gcd [lemma, in spec_gcd]
spec_ww_div_gt_aux [lemma, in spec_ww_div_gt_aux]
spec_to_Z_2 [lemma, in spec_to_Z_2]
spec_sub_carry_c [lemma, in spec_sub_carry_c]
spec_sub_carry_c [lemma, in spec_sub_carry_c]
spec_ww_tail0 [lemma, in spec_ww_tail0]
spec_ww_pred_c [lemma, in spec_ww_pred_c]
spec_ww_add_c_cont [lemma, in spec_ww_add_c_cont]
spec_ww_div21 [lemma, in spec_ww_div21]
spec_ww_opp_carry [lemma, in spec_ww_opp_carry]
spec_ww_add_carry_c [lemma, in spec_ww_add_carry_c]
spec_to_Z_pos [lemma, in spec_to_Z_pos]
spec_mul_add [lemma, in spec_mul_add]
spec_ww_succ [lemma, in spec_ww_succ]
spec_ww_mod_gt [lemma, in spec_ww_mod_gt]
spec_0 [lemma, in spec_0]
spec_0 [lemma, in spec_0]
spec_mul_c [lemma, in spec_mul_c]
spec_mul_c [lemma, in spec_mul_c]
spec_w_div32 [lemma, in spec_w_div32]
spec_mod [lemma, in spec_mod]
spec_ww_to_Z [lemma, in spec_ww_to_Z]
spec_ww_to_Z [lemma, in spec_ww_to_Z]
spec_div_gt [lemma, in spec_div_gt]
spec_more_than_1_digit [lemma, in spec_more_than_1_digit]
spec_more_than_1_digit [lemma, in spec_more_than_1_digit]
spec_extend_aux [lemma, in spec_extend_aux]
spec_ww_succ_c [lemma, in spec_ww_succ_c]
split [definition, in split]
split [definition, in split]
SplitAbsolu [library]
SplitRmult [library]
split_length_l [lemma, in split_length_l]
split_nth [lemma, in split_nth]
split_length_r [lemma, in split_length_r]
split_combine [lemma, in split_combine]
sp_swap [constructor, in sp_swap]
sp_noswap [constructor, in sp_noswap]
Sqrt [module, in Sqrt]
sqrt [definition, in sqrt]
sqrt [definition, in sqrt]
sqrt [definition, in sqrt]
SqrtNotation [module, in SqrtNotation]
√ _ [notation, in ::'√'_x]
sqrtrempos [definition, in sqrtrempos]
sqrt_main_trick [lemma, in sqrt_main_trick]
sqrt_more [lemma, in sqrt_more]
sqrt_sqrt [lemma, in sqrt_sqrt]
sqrt_le_0 [lemma, in sqrt_le_0]
sqrt_div_alt [lemma, in sqrt_div_alt]
sqrt_lem_1 [lemma, in sqrt_lem_1]
sqrt_positivity [lemma, in sqrt_positivity]
sqrt_continuity_pt_R1 [lemma, in sqrt_continuity_pt_R1]
sqrt_1 [lemma, in sqrt_1]
sqrt_iter_spec [lemma, in sqrt_iter_spec]
sqrt_0 [lemma, in sqrt_0]
sqrt_Rsqr [lemma, in sqrt_Rsqr]
sqrt_continuity_pt [lemma, in sqrt_continuity_pt]
sqrt_def [lemma, in sqrt_def]
sqrt_mult [lemma, in sqrt_mult]
sqrt_spec [lemma, in sqrt_spec]
sqrt_cauchy [lemma, in sqrt_cauchy]
sqrt_lt_0 [lemma, in sqrt_lt_0]
sqrt_lt_1 [lemma, in sqrt_lt_1]
sqrt_less_alt [lemma, in sqrt_less_alt]
sqrt_le_1_alt [lemma, in sqrt_le_1_alt]
sqrt_mult_alt [lemma, in sqrt_mult_alt]
sqrt_data [inductive, in sqrt_data]
sqrt_test_false [lemma, in sqrt_test_false]
sqrt_test_true [lemma, in sqrt_test_true]
sqrt_less [lemma, in sqrt_less]
sqrt_var_maj [lemma, in sqrt_var_maj]
sqrt_le_1 [lemma, in sqrt_le_1]
sqrt_main [lemma, in sqrt_main]
sqrt_lt_R0 [lemma, in sqrt_lt_R0]
sqrt_div [lemma, in sqrt_div]
sqrt_lem_0 [lemma, in sqrt_lem_0]
sqrt_Rsqr_abs [lemma, in sqrt_Rsqr_abs]
sqrt_iter [definition, in sqrt_iter]
sqrt_eq_0 [lemma, in sqrt_eq_0]
sqrt_init [lemma, in sqrt_init]
sqrt_lt_1_alt [lemma, in sqrt_lt_1_alt]
sqrt_inj [lemma, in sqrt_inj]
sqrt_square [lemma, in sqrt_square]
sqrt_lt_0_alt [lemma, in sqrt_lt_0_alt]
sqrt_pos [lemma, in sqrt_pos]
Sqrt_reg [library]
Sqrt' [module, in Sqrt']
Sqrt.sqrt [axiom, in sqrt]
sqrt2 [definition, in sqrt2]
sqrt2_neq_0 [lemma, in sqrt2_neq_0]
sqrt3_2_neq_0 [lemma, in sqrt3_2_neq_0]
sqrt31 [definition, in sqrt31]
sqrt31_step [definition, in sqrt31_step]
sqrt31_step_correct [lemma, in sqrt31_step_correct]
sqrt31_step_def [lemma, in sqrt31_step_def]
sqrt312 [definition, in sqrt312]
sqrt312_step_correct [lemma, in sqrt312_step_correct]
sqrt312_step_def [lemma, in sqrt312_step_def]
sqrt312_lower_bound [lemma, in sqrt312_lower_bound]
sqrt312_step [definition, in sqrt312_step]
sqr_pos [lemma, in sqr_pos]
square [definition, in square]
square_c [definition, in square_c]
square_spec [lemma, in square_spec]
square_not_prime [lemma, in square_not_prime]
SSorted_nil [constructor, in SSorted_nil]
SSorted_cons [constructor, in SSorted_cons]
Sstar_contains_Rstar [lemma, in Sstar_contains_Rstar]
star_monotone [lemma, in star_monotone]
Step [abbreviation, in Step]
StepFun [record, in StepFun]
StepFun_P45 [lemma, in StepFun_P45]
StepFun_P6 [lemma, in StepFun_P6]
StepFun_P44 [lemma, in StepFun_P44]
StepFun_P24 [lemma, in StepFun_P24]
StepFun_P9 [lemma, in StepFun_P9]
StepFun_P23 [lemma, in StepFun_P23]
StepFun_P1 [lemma, in StepFun_P1]
StepFun_P34 [lemma, in StepFun_P34]
StepFun_P13 [lemma, in StepFun_P13]
StepFun_P16 [lemma, in StepFun_P16]
StepFun_P17 [lemma, in StepFun_P17]
StepFun_P20 [lemma, in StepFun_P20]
StepFun_P14 [lemma, in StepFun_P14]
StepFun_P19 [lemma, in StepFun_P19]
StepFun_P32 [lemma, in StepFun_P32]
StepFun_P5 [lemma, in StepFun_P5]
StepFun_P38 [lemma, in StepFun_P38]
StepFun_P31 [lemma, in StepFun_P31]
StepFun_P8 [lemma, in StepFun_P8]
StepFun_P22 [lemma, in StepFun_P22]
StepFun_P11 [lemma, in StepFun_P11]
StepFun_P35 [lemma, in StepFun_P35]
StepFun_P28 [lemma, in StepFun_P28]
StepFun_P18 [lemma, in StepFun_P18]
StepFun_P3 [lemma, in StepFun_P3]
StepFun_P10 [lemma, in StepFun_P10]
StepFun_P33 [lemma, in StepFun_P33]
StepFun_P43 [lemma, in StepFun_P43]
StepFun_P12 [lemma, in StepFun_P12]
StepFun_P29 [lemma, in StepFun_P29]
StepFun_P21 [lemma, in StepFun_P21]
StepFun_P30 [lemma, in StepFun_P30]
StepFun_P26 [lemma, in StepFun_P26]
StepFun_P15 [lemma, in StepFun_P15]
StepFun_P46 [lemma, in StepFun_P46]
StepFun_P42 [lemma, in StepFun_P42]
StepFun_P2 [lemma, in StepFun_P2]
StepFun_P40 [lemma, in StepFun_P40]
StepFun_P4 [lemma, in StepFun_P4]
StepFun_P7 [lemma, in StepFun_P7]
StepFun_P36 [lemma, in StepFun_P36]
StepFun_P25 [lemma, in StepFun_P25]
StepFun_P37 [lemma, in StepFun_P37]
StepFun_P27 [lemma, in StepFun_P27]
StepFun_P41 [lemma, in StepFun_P41]
StepFun_P39 [lemma, in StepFun_P39]
stop [constructor, in stop]
Stream [inductive, in Stream]
StreamMemo [library]
Streams [section, in Streams]
Streams [library]
Streams.A [variable, in A]
Streams.Stream_Properties [section, in Stream_Properties]
Streams.Stream_Properties.P [variable, in P]
Streams.Stream_Properties.Co_Induction_ForAll [section, in Co_Induction_ForAll]
Streams.Stream_Properties.Co_Induction_ForAll.InvIsStable [variable, in InvIsStable]
Streams.Stream_Properties.Co_Induction_ForAll.InvThenP [variable, in InvThenP]
Streams.Stream_Properties.Co_Induction_ForAll.Inv [variable, in Inv]
Streicher_K__eq_rect_eq [lemma, in Streicher_K__eq_rect_eq]
Streicher_K_ [definition, in Streicher_K_]
strictincreasing_strictdecreasing_opp [lemma, in strictincreasing_strictdecreasing_opp]
StrictOrder [record, in StrictOrder]
StrictOrder_inverse [lemma, in StrictOrder_inverse]
StrictOrder_Transitive [projection, in StrictOrder_Transitive]
StrictOrder_PartialOrder [lemma, in StrictOrder_PartialOrder]
StrictOrder_PreOrder [lemma, in StrictOrder_PreOrder]
StrictOrder_Asymmetric [instance, in StrictOrder_Asymmetric]
StrictOrder_Irreflexive [projection, in StrictOrder_Irreflexive]
strict_increasing [definition, in strict_increasing]
Strict_Rel_Transitive [lemma, in Strict_Rel_Transitive]
Strict_super_set_contains_new_element [lemma, in Strict_super_set_contains_new_element]
strict_decreasing [definition, in strict_decreasing]
Strict_Included [definition, in Strict_Included]
Strict_Rel_Transitive_with_Rel_left [lemma, in Strict_Rel_Transitive_with_Rel_left]
Strict_Included_inv [lemma, in Strict_Included_inv]
Strict_Rel_Transitive_with_Rel [lemma, in Strict_Rel_Transitive_with_Rel]
Strict_Rel_is_Strict_Included [lemma, in Strict_Rel_is_Strict_Included]
Strict_inclusion_is_transitive_with_inclusion_left [lemma, in Strict_inclusion_is_transitive_with_inclusion_left]
Strict_Rel_of [definition, in Strict_Rel_of]
Strict_Included_strict [lemma, in Strict_Included_strict]
Strict_inclusion_is_transitive_with_inclusion [lemma, in Strict_inclusion_is_transitive_with_inclusion]
Strict_Included_intro [lemma, in Strict_Included_intro]
Strict_inclusion_is_transitive [lemma, in Strict_inclusion_is_transitive]
String [constructor, in String]
string [inductive, in string]
String [library]
string_dec [definition, in string_dec]
strip_commut [lemma, in strip_commut]
StronglySorted [inductive, in StronglySorted]
StronglySorted_rect [lemma, in StronglySorted_rect]
StronglySorted_Sorted [lemma, in StronglySorted_Sorted]
StronglySorted_rec [lemma, in StronglySorted_rec]
StronglySorted_inv [lemma, in StronglySorted_inv]
Strongly_confluent [definition, in Strongly_confluent]
Strong_confluence_direct [lemma, in Strong_confluence_direct]
Strong_confluence [lemma, in Strong_confluence]
StrOrder [module, in StrOrder]
StrOrder' [module, in StrOrder']
Str_nth_tl_plus [lemma, in Str_nth_tl_plus]
Str_nth_tl_zipWith [lemma, in Str_nth_tl_zipWith]
Str_nth_plus [lemma, in Str_nth_plus]
Str_nth [definition, in Str_nth]
Str_nth_tl [definition, in Str_nth_tl]
Str_nth_tl_map [lemma, in Str_nth_tl_map]
Str_nth_zipWith [lemma, in Str_nth_zipWith]
Str_nth_map [lemma, in Str_nth_map]
sub [definition, in sub]
subdivision [definition, in subdivision]
subdivision_val [definition, in subdivision_val]
SubEqui [definition, in SubEqui]
SubEquiN [definition, in SubEquiN]
SubEqui_P5 [lemma, in SubEqui_P5]
SubEqui_P7 [lemma, in SubEqui_P7]
SubEqui_P2 [lemma, in SubEqui_P2]
SubEqui_P6 [lemma, in SubEqui_P6]
SubEqui_P3 [lemma, in SubEqui_P3]
SubEqui_P4 [lemma, in SubEqui_P4]
SubEqui_P9 [lemma, in SubEqui_P9]
SubEqui_P8 [lemma, in SubEqui_P8]
SubEqui_P1 [lemma, in SubEqui_P1]
subfamily [definition, in subfamily]
subrelation [record, in subrelation]
subrelation [inductive, in subrelation]
subrelation [definition, in subrelation]
subrelation_pointwise [instance, in subrelation_pointwise]
subrelation_symmetric [lemma, in subrelation_symmetric]
subrelation_refl [lemma, in subrelation_refl]
subrelation_partial_order [instance, in subrelation_partial_order]
subrelation_respectful [lemma, in subrelation_respectful]
subrelation_proper [lemma, in subrelation_proper]
subrelation_id_proper [instance, in subrelation_id_proper]
subset [definition, in subset]
Subset [library]
Subset_projections.P [variable, in P]
subset_types_imp_guarded_rel_choice_iff_rel_choice [lemma, in subset_types_imp_guarded_rel_choice_iff_rel_choice]
subset_eq [lemma, in subset_eq]
Subset_projections.A [variable, in A]
Subset_projections [section, in Subset_projections]
substring [definition, in substring]
substring_correct2 [lemma, in substring_correct2]
substring_correct1 [lemma, in substring_correct1]
Subtract [definition, in Subtract]
Subtract_intro [lemma, in Subtract_intro]
Subtract_inv [lemma, in Subtract_inv]
Sub_Add_new [lemma, in Sub_Add_new]
sub_carry_c [definition, in sub_carry_c]
sub_c [definition, in sub_c]
sub_carry [definition, in sub_carry]
sub_carry [lemma, in sub_carry]
sub31 [definition, in sub31]
sub31c [definition, in sub31c]
sub31carryc [definition, in sub31carryc]
succ [definition, in succ]
SuccNat2Pos [module, in SuccNat2Pos]
SuccNat2Pos.id_succ [lemma, in id_succ]
SuccNat2Pos.inj [lemma, in inj]
SuccNat2Pos.inj_iff [lemma, in inj_iff]
SuccNat2Pos.inj_compare [lemma, in inj_compare]
SuccNat2Pos.inj_succ [lemma, in inj_succ]
SuccNat2Pos.inv [lemma, in inv]
SuccNat2Pos.pred_id [lemma, in pred_id]
succ_plus_discr [lemma, in succ_plus_discr]
succ_IZR [lemma, in succ_IZR]
succ_min_distr [definition, in succ_min_distr]
succ_pred [lemma, in succ_pred]
succ_max_distr [definition, in succ_max_distr]
succ_c [definition, in succ_c]
sum [inductive, in sum]
sumbool [inductive, in sumbool]
Sumbool [library]
sumbool_of_bool [definition, in sumbool_of_bool]
sumbool_or [definition, in sumbool_or]
sumbool_and [definition, in sumbool_and]
sumbool_not [definition, in sumbool_not]
sumor [inductive, in sumor]
sum_f_R0 [definition, in sum_f_R0]
sum_growing [lemma, in sum_growing]
sum_N_predN [lemma, in sum_N_predN]
sum_inequa_Rle_lt [lemma, in sum_inequa_Rle_lt]
sum_maj1 [lemma, in sum_maj1]
sum_eqdec [instance, in sum_eqdec]
sum_Rle [lemma, in sum_Rle]
sum_Ratan_seq_opp [lemma, in sum_Ratan_seq_opp]
sum_decomposition [lemma, in sum_decomposition]
sum_f_R0_triangle [lemma, in sum_f_R0_triangle]
sum_cv_maj [lemma, in sum_cv_maj]
sum_plus [lemma, in sum_plus]
sum_mul_carry [lemma, in sum_mul_carry]
sum_mul_carry [lemma, in sum_mul_carry]
sum_nat [definition, in sum_nat]
sum_nat_O [definition, in sum_nat_O]
sum_eq [lemma, in sum_eq]
sum_eq_R0 [lemma, in sum_eq_R0]
sum_cte [lemma, in sum_cte]
sum_nat_f_O [definition, in sum_nat_f_O]
sum_incr [lemma, in sum_incr]
sum_nat_f [definition, in sum_nat_f]
sum_f [definition, in sum_f]
sup [constructor, in sup]
surjective_pairing [lemma, in surjective_pairing]
Swap [section, in Swap]
Swap [section, in Swap]
SwapProd [abbreviation, in SwapProd]
swapprod [inductive, in swapprod]
swap_Acc [lemma, in swap_Acc]
swap_sumbool [definition, in swap_sumbool]
swap_sumbool [definition, in swap_sumbool]
Swap.A [variable, in A]
Swap.A [variable, in A]
Swap.R [variable, in R]
Swap.R [variable, in R]
SWithLeibniz [module, in SWithLeibniz]
SWithLeibniz.E [module, in SWithLeibniz.E]
SWithLeibniz.eq_leibniz [axiom, in eq_leibniz]
Symmetric [record, in Symmetric]
Symmetric [inductive, in Symmetric]
Symmetric [definition, in Symmetric]
symmetric [definition, in symmetric]
Symmetric_Product.leA [variable, in leA]
Symmetric_Product.B [variable, in B]
Symmetric_Product [section, in Symmetric_Product]
symmetric_equiv_inverse [lemma, in symmetric_equiv_inverse]
Symmetric_Product.A [variable, in A]
Symmetric_Product.leB [variable, in leB]
symmetry [projection, in symmetry]
symmetry [constructor, in symmetry]
symprod [inductive, in symprod]
Symprod [abbreviation, in Symprod]
sym_not_id [abbreviation, in sym_not_id]
sym_not_equal [abbreviation, in sym_not_equal]
sym_not_eq [abbreviation, in sym_not_eq]
sym_id [abbreviation, in sym_id]
sym_JMeq [abbreviation, in sym_JMeq]
sym_EqSt [lemma, in sym_EqSt]
sym_equal [abbreviation, in sym_equal]
sym_eq [abbreviation, in sym_eq]
SYM1 [abbreviation, in SYM1]
SYM2 [abbreviation, in SYM2]
SYM3 [abbreviation, in SYM3]
Syntax [library]
S_to_Finite_set [module, in S_to_Finite_set]
S_to_Finite_set [module, in S_to_Finite_set]
S_pred [lemma, in S_pred]
S_O_plus_INR [lemma, in S_O_plus_INR]
S_INR [lemma, in S_INR]
S.E [module, in S.E]
S.E [module, in S.E]