| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (980 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (93 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (634 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (53 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (154 entries) |
Global Index
A
aapp [definition, in Mapiter]aapp_length [lemma, in Lsort]
acons [definition, in Mapiter]
Action [inductive, in SetChecker]
ad [definition, in Map]
AdAlloc [section, in Adalloc]
Adalloc [library]
AdAlloc.A [variable, in Adalloc]
add_ICNF_unsat [lemma, in SetChecker]
add_ICNF [definition, in SetChecker]
ad_comp_double_plus_un_inj [lemma, in Mapiter]
ad_comp_double_inj [lemma, in Mapiter]
ad_inj [definition, in Mapiter]
ad_alloc_opt_optimal [lemma, in Adalloc]
ad_alloc_opt_optimal_1 [lemma, in Adalloc]
ad_alloc_opt_allocates [lemma, in Adalloc]
ad_alloc_opt_allocates_1 [lemma, in Adalloc]
ad_alloc_opt [definition, in Adalloc]
ad_list_of_dom_Dom [lemma, in Maplists]
ad_list_of_dom_Dom_1 [lemma, in Maplists]
ad_list_of_dom_not_stutters [lemma, in Maplists]
ad_list_of_dom_card [lemma, in Maplists]
ad_list_of_dom_card_1 [lemma, in Maplists]
ad_in_list_of_dom_in_dom [lemma, in Maplists]
ad_list_of_dom [definition, in Maplists]
ad_list_app_rev [lemma, in Maplists]
ad_list_stutters_rev [lemma, in Maplists]
ad_list_rev_length [lemma, in Maplists]
ad_list_stutters_permute [lemma, in Maplists]
ad_list_app_length [lemma, in Maplists]
ad_list_Elems [lemma, in Maplists]
ad_list_stutters_prev_conv_r [lemma, in Maplists]
ad_list_stutters_prev_r [lemma, in Maplists]
ad_list_stutters_prev_conv_l [lemma, in Maplists]
ad_list_stutters_prev_l [lemma, in Maplists]
ad_list_has_circuit_stutters [lemma, in Maplists]
ad_in_list_rev [lemma, in Maplists]
ad_in_list_app [lemma, in Maplists]
ad_in_list_app_1 [lemma, in Maplists]
ad_list_stutters_app_conv_r [lemma, in Maplists]
ad_list_stutters_app_conv_l [lemma, in Maplists]
ad_list_stutters_app_r [lemma, in Maplists]
ad_in_list_r [lemma, in Maplists]
ad_list_stutters_app_l [lemma, in Maplists]
ad_in_list_l [lemma, in Maplists]
ad_list_stutters_card_conv [lemma, in Maplists]
ad_list_not_stutters_card_conv [lemma, in Maplists]
ad_list_stutters_card [lemma, in Maplists]
ad_list_card [lemma, in Maplists]
ad_list_not_stutters_card [lemma, in Maplists]
ad_in_elems_in_list [lemma, in Maplists]
ad_list_stutters_has_circuit [lemma, in Maplists]
ad_in_list_forms_circuit [lemma, in Maplists]
ad_list_stutters [definition, in Maplists]
ad_in_list [definition, in Maplists]
ad_comp_double_plus_un_monotonic [lemma, in Lsort]
ad_comp_double_monotonic [lemma, in Lsort]
ad_comp_monotonic [lemma, in Lsort]
ad_monotonic [definition, in Lsort]
alist [definition, in Mapiter]
alist_semantics_disjoint_comm [lemma, in Mapiter]
alist_MapMerge_semantics_disjoint [lemma, in Mapiter]
alist_MapMerge_semantics [lemma, in Mapiter]
alist_of_Map_of_alist [lemma, in Mapiter]
alist_of_Map_semantics [lemma, in Mapiter]
alist_of_Map_semantics_1 [lemma, in Mapiter]
alist_of_Map_semantics_1_1 [lemma, in Mapiter]
alist_semantics_app [lemma, in Mapiter]
alist_semantics [definition, in Mapiter]
alist_of_Map [definition, in Mapiter]
alist_of_Map_of_alist_c [lemma, in Mapc]
alist_canonical [lemma, in Lsort]
alist_sorted_tail [lemma, in Lsort]
alist_semantics_same_tail [lemma, in Lsort]
alist_semantics_tail [lemma, in Lsort]
alist_semantics_nth_ad [lemma, in Lsort]
alist_too_low [lemma, in Lsort]
alist_of_Map_sorts2 [lemma, in Lsort]
alist_of_Map_sorts1 [lemma, in Lsort]
alist_of_Map_sorts [lemma, in Lsort]
alist_of_Map_sorts_1 [lemma, in Lsort]
alist_of_Map_nth_ad [lemma, in Lsort]
alist_nth_ad_semantics [lemma, in Lsort]
alist_conc_sorted [lemma, in Lsort]
alist_nth_ad_aapp_2 [lemma, in Lsort]
alist_nth_ad_aapp_1 [lemma, in Lsort]
alist_sorted_2_imp [lemma, in Lsort]
alist_sorted_1_imp_2 [lemma, in Lsort]
alist_sorted_2 [definition, in Lsort]
alist_sorted_imp_1 [lemma, in Lsort]
alist_sorted_1 [definition, in Lsort]
alist_nth_ad [definition, in Lsort]
alist_sorted [definition, in Lsort]
Allmaps [library]
anil [definition, in Mapiter]
Answer [definition, in SetChecker]
app_length [lemma, in Lsort]
B
balanced [definition, in BinaryTrees]Basic [library]
BinaryTree [inductive, in BinaryTrees]
BinaryTrees [library]
BPT_formula_sat [lemma, in Generate]
BPT_formula [definition, in Generate]
BPT_list [definition, in Generate]
BT_map_in [lemma, in BinaryTrees]
BT_map [definition, in BinaryTrees]
BT_in_add_all [lemma, in BinaryTrees]
BT_add_all_in [lemma, in BinaryTrees]
BT_add_all_mon [lemma, in BinaryTrees]
BT_add_all_wf_rev [lemma, in BinaryTrees]
BT_wf_add_all [lemma, in BinaryTrees]
BT_add_all [definition, in BinaryTrees]
BT_size_split [lemma, in BinaryTrees]
BT_size [definition, in BinaryTrees]
BT_nought_diff [lemma, in BinaryTrees]
BT_diff_nought [lemma, in BinaryTrees]
BT_diff_out' [lemma, in BinaryTrees]
BT_diff_out [lemma, in BinaryTrees]
BT_diff_in_rev [lemma, in BinaryTrees]
BT_diff_in [lemma, in BinaryTrees]
BT_diff_wf [lemma, in BinaryTrees]
BT_diff [definition, in BinaryTrees]
BT_remove_out [lemma, in BinaryTrees]
BT_in_remove [lemma, in BinaryTrees]
BT_remove_in_rev [lemma, in BinaryTrees]
BT_remove_wf [lemma, in BinaryTrees]
BT_remove_in [lemma, in BinaryTrees]
BT_remove [definition, in BinaryTrees]
BT_all_in_dec [lemma, in BinaryTrees]
BT_in_dec [lemma, in BinaryTrees]
BT_split_compare [lemma, in BinaryTrees]
BT_split_in [lemma, in BinaryTrees]
BT_split_in_l [lemma, in BinaryTrees]
BT_split_wf [lemma, in BinaryTrees]
BT_split_in_r [lemma, in BinaryTrees]
BT_split [definition, in BinaryTrees]
BT_add_wf_rev [lemma, in BinaryTrees]
BT_add_mon [lemma, in BinaryTrees]
BT_wf_add [lemma, in BinaryTrees]
BT_in_add [lemma, in BinaryTrees]
BT_add_in [lemma, in BinaryTrees]
BT_add [definition, in BinaryTrees]
BT_in_balance [lemma, in BinaryTrees]
BT_balance_in [lemma, in BinaryTrees]
BT_balance_wf [lemma, in BinaryTrees]
BT_balance [definition, in BinaryTrees]
BT_in_rot_RR [lemma, in BinaryTrees]
BT_rot_RR_in [lemma, in BinaryTrees]
BT_rot_RR_wf [lemma, in BinaryTrees]
BT_rot_RR [definition, in BinaryTrees]
BT_in_rot_LL [lemma, in BinaryTrees]
BT_rot_LL_in [lemma, in BinaryTrees]
BT_rot_LL_wf [lemma, in BinaryTrees]
BT_rot_LL [definition, in BinaryTrees]
BT_rot_R_wf_rev [lemma, in BinaryTrees]
BT_in_rot_R [lemma, in BinaryTrees]
BT_rot_R_in [lemma, in BinaryTrees]
BT_rot_R_wf [lemma, in BinaryTrees]
BT_rot_R [definition, in BinaryTrees]
BT_rot_L_wf_rev [lemma, in BinaryTrees]
BT_in_rot_L [lemma, in BinaryTrees]
BT_rot_L_in [lemma, in BinaryTrees]
BT_rot_L_wf [lemma, in BinaryTrees]
BT_rot_L [definition, in BinaryTrees]
BT_singleton_char [lemma, in BinaryTrees]
BT_nought_char [lemma, in BinaryTrees]
BT_wf [definition, in BinaryTrees]
BT_In [definition, in BinaryTrees]
C
change_val_p' [lemma, in Generate]change_val_p [lemma, in Generate]
change_val [definition, in Generate]
Clause [definition, in CNF]
Clauses [section, in CNF]
Clauses.Compare [section, in CNF]
Clause_compare_sym_Lt [lemma, in CNF]
Clause_compare_sym_Gt [lemma, in CNF]
Clause_compare_trans [lemma, in CNF]
Clause_compare_eq [lemma, in CNF]
Clause_compare [definition, in CNF]
clause_eq_nil_cons [lemma, in CNF]
clause_eq_dec [lemma, in CNF]
Clause_to_SetClause [definition, in SetChecker]
CNF [definition, in CNF]
CNF [section, in CNF]
CNF [library]
CNF_equiv [definition, in CNF]
CNF_empty [lemma, in CNF]
CNF_eq_dec [lemma, in CNF]
colorful [definition, in Generate]
colorful_simplify [lemma, in Generate]
colorful_remove_singleton [lemma, in Generate]
colorful_add [lemma, in Generate]
colorful_gives_val [lemma, in Generate]
coloring [definition, in Generate]
Compare [section, in Basic]
compare_Eq_dec [lemma, in Basic]
compare_Gt_dec [lemma, in Basic]
compare_Lt_dec [lemma, in Basic]
Cube [definition, in CubeAndConquer]
CubeAndConquer [library]
CubeAndConquer_lemma [lemma, in CubeAndConquer]
Cubed_CNF_satisfies [lemma, in CubeAndConquer]
Cubed_CNF [definition, in CubeAndConquer]
C_sat_clause [lemma, in CNF]
C_unsat_empty [lemma, in CNF]
C_unsat [definition, in CNF]
C_satisfies_dec [lemma, in CNF]
C_satisfies_exists [lemma, in CNF]
C_satisfies [definition, in CNF]
C_to_C_satisfies_2 [lemma, in SetChecker]
C_to_C_satisfies_1 [lemma, in SetChecker]
C_to_SC_In_2 [lemma, in SetChecker]
C_to_SC_In_1 [lemma, in SetChecker]
C_to_SC_wf [lemma, in SetChecker]
D
D [constructor, in SetChecker]del_ICNF_in [lemma, in SetChecker]
del_ICNF [definition, in SetChecker]
DMerge [definition, in Mapfold]
DMergeDef [section, in Mapfold]
DMergeDef.A [variable, in Mapfold]
Dom [section, in Fset]
Dom.A [variable, in Fset]
Dom.B [variable, in Fset]
E
Elems [definition, in Maplists]Elems_of_list_of_dom_c [lemma, in Maplists]
Elems_of_list_of_dom [lemma, in Maplists]
Elems_rev [lemma, in Maplists]
Elems_app [lemma, in Maplists]
Elems_canon [lemma, in Maplists]
empty_ICNF [definition, in SetChecker]
entails [definition, in CNF]
eqm [definition, in Map]
eqmap [definition, in Mapaxioms]
eqmap_trans [lemma, in Mapaxioms]
eqmap_refl [lemma, in Mapaxioms]
eqmap_sym [lemma, in Mapaxioms]
eqm_trans [lemma, in Mapaxioms]
eqm_refl [lemma, in Mapaxioms]
eqm_sym [lemma, in Mapaxioms]
eq_Clause_compare [lemma, in CNF]
eq_Lit_compare [lemma, in CNF]
exists_C_satisfies [lemma, in CNF]
exists_SC_satisfies [lemma, in SetChecker]
ExtractionChecker [library]
ExtractionCubes [library]
ExtractionNoCubes [library]
F
fix_one_color [lemma, in Generate]fold_right_aapp [lemma, in Mapiter]
force [definition, in SetChecker]
Formula [section, in Generate]
for_all_satisfies [lemma, in CNF]
fromVal [definition, in SetChecker]
FSet [definition, in Fset]
Fset [library]
FSetCanon [section, in Mapcanon]
FSetCanon.A [variable, in Mapcanon]
FSetDefs [section, in Fset]
FSetDefs.A [variable, in Fset]
FSetDelta [definition, in Fset]
FSetDelta_assoc [lemma, in Mapaxioms]
FSetDelta_assoc_c [lemma, in Mapc]
FSetDiff [definition, in Fset]
FSetInter [definition, in Fset]
FSetInter_Union_r [lemma, in Mapaxioms]
FSetInter_Union_l [lemma, in Mapaxioms]
FSetInter_idempotent [lemma, in Mapaxioms]
FSetInter_s_M0 [lemma, in Mapaxioms]
FSetInter_M0_s [lemma, in Mapaxioms]
FSetInter_assoc [lemma, in Mapaxioms]
FSetInter_comm [lemma, in Mapaxioms]
FSetInter_Union_r [lemma, in Mapc]
FSetInter_Union_l_c [lemma, in Mapc]
FSetInter_idempotent [lemma, in Mapc]
FSetInter_s_M0_c [lemma, in Mapc]
FSetInter_M0_s_c [lemma, in Mapc]
FSetInter_assoc_c [lemma, in Mapc]
FSetInter_comm_c [lemma, in Mapc]
FSetUnion [definition, in Fset]
FSetUnion_Inter_r [lemma, in Mapaxioms]
FSetUnion_Inter_l [lemma, in Mapaxioms]
FSetUnion_idempotent [lemma, in Mapaxioms]
FSetUnion_s_M0 [lemma, in Mapaxioms]
FSetUnion_M0_s [lemma, in Mapaxioms]
FSetUnion_assoc [lemma, in Mapaxioms]
FSetUnion_comm [lemma, in Mapaxioms]
FSetUnion_Inter_r [lemma, in Mapc]
FSetUnion_Inter_l_c [lemma, in Mapc]
FSetUnion_idempotent [lemma, in Mapc]
FSetUnion_s_M0_c [lemma, in Mapc]
FSetUnion_M0_s_c [lemma, in Mapc]
FSetUnion_assoc_c [lemma, in Mapc]
FSetUnion_comm_c [lemma, in Mapc]
FSet_Dom [lemma, in Fset]
FSet_ext [lemma, in Mapaxioms]
FSet_ext_c [lemma, in Mapc]
FSubsetOrder [section, in Mapsubset]
FSubset_trans [lemma, in Mapsubset]
FSubset_antisym [lemma, in Mapsubset]
FSubset_refl [lemma, in Mapsubset]
FSubset_antisym_c [lemma, in Mapc]
G
Generate [library]get_ICNF_in_or_default [lemma, in SetChecker]
get_ICNF [definition, in SetChecker]
H
height [definition, in BinaryTrees]I
ICNF [definition, in SetChecker]ICNF [section, in SetChecker]
ICNF_get_del [lemma, in SetChecker]
ICNF_get_in [lemma, in SetChecker]
ICNF_to_TCNF_wf [lemma, in SetChecker]
ICNF_to_TCNF [definition, in SetChecker]
InDom [section, in Fset]
InDom.A [variable, in Fset]
InDom.B [variable, in Fset]
inner_cycle_okl [lemma, in Generate]
inner_cycle [definition, in Generate]
interval_split [lemma, in Lsort]
in_dom_DMerge_3 [lemma, in Mapfold]
in_dom_DMerge_2 [lemma, in Mapfold]
in_dom_DMerge_1 [lemma, in Mapfold]
In_remove [lemma, in Basic]
in_remove [lemma, in Basic]
in_simplify [lemma, in Generate]
in_BTree_list [lemma, in BinaryTrees]
in_list_BTree [lemma, in BinaryTrees]
in_FSet_delta [lemma, in Fset]
in_FSet_diff [lemma, in Fset]
in_FSet_inter [lemma, in Fset]
in_FSet_union [lemma, in Fset]
in_FSet [definition, in Fset]
in_dom_restrby [lemma, in Fset]
in_dom_restrto [lemma, in Fset]
in_dom_delta [lemma, in Fset]
in_dom_merge [lemma, in Fset]
in_dom_remove [lemma, in Fset]
in_dom_put_behind [lemma, in Fset]
in_dom_put [lemma, in Fset]
in_dom_none [lemma, in Fset]
in_dom_some [lemma, in Fset]
in_dom_M1_2 [lemma, in Fset]
in_dom_M1_1 [lemma, in Fset]
in_dom_M1 [lemma, in Fset]
in_dom_M0 [lemma, in Fset]
in_dom [definition, in Fset]
in_ICNF_get' [lemma, in SetChecker]
in_ICNF_get [lemma, in SetChecker]
In_TCNF [lemma, in SetChecker]
In_TCNF' [lemma, in SetChecker]
L
LazyT [definition, in SetChecker]lazy_list [inductive, in SetChecker]
lcons [constructor, in SetChecker]
length_as_fold_2 [lemma, in Mapcard]
length_as_fold [lemma, in Mapcard]
Lists_of_Clauses [section, in Generate]
Lists_and_Stuff [section, in Generate]
list_subset [definition, in Basic]
list_to_BTree_wf [lemma, in BinaryTrees]
list_to_BTree [definition, in BinaryTrees]
list_append_split [lemma, in SetChecker]
Literal [inductive, in CNF]
Literal [section, in CNF]
Literal_neg_neg [lemma, in CubeAndConquer]
Literal_compare [definition, in CNF]
literal_eq_dec [lemma, in CNF]
Literal.Compare [section, in CNF]
Lit_compare_sym_Lt [lemma, in CNF]
Lit_compare_sym_Gt [lemma, in CNF]
Lit_compare_trans [lemma, in CNF]
Lit_compare_eq [lemma, in CNF]
lnil [constructor, in SetChecker]
LSort [section, in Lsort]
Lsort [library]
LSort.A [variable, in Lsort]
L_satisfies_dec [lemma, in CNF]
L_satisfies_neg_neg [lemma, in CNF]
L_satisfies_neg [lemma, in CNF]
L_satisfies [definition, in CNF]
M
makeM2 [definition, in Map]makeM2_M2 [lemma, in Map]
makeM2_canon [lemma, in Mapcanon]
make_TCNF_wf [lemma, in SetChecker]
make_TCNF [definition, in SetChecker]
Map [inductive, in Map]
Map [library]
MapAxioms [section, in Mapaxioms]
Mapaxioms [library]
MapAxioms.A [variable, in Mapaxioms]
MapAxioms.B [variable, in Mapaxioms]
MapAxioms.C [variable, in Mapaxioms]
MapC [section, in Mapc]
Mapc [library]
mapcanon [inductive, in Mapcanon]
MapCanon [section, in Mapcanon]
Mapcanon [library]
MapCanonicalize [definition, in Mapcanon]
mapcanon_exists [lemma, in Mapcanon]
mapcanon_exists_2 [lemma, in Mapcanon]
mapcanon_exists_1 [lemma, in Mapcanon]
mapcanon_unique [lemma, in Mapcanon]
mapcanon_M2_2 [lemma, in Mapcanon]
mapcanon_M2_1 [lemma, in Mapcanon]
mapcanon_M2 [lemma, in Mapcanon]
MapCanon.A [variable, in Mapcanon]
MapCanon.B [variable, in Mapcanon]
MapCard [definition, in Map]
MapCard [section, in Mapcard]
Mapcard [library]
MapCard_is_Sn [lemma, in Mapcard]
MapCard_Remove_2_conv [lemma, in Mapcard]
MapCard_Remove_1_conv [lemma, in Mapcard]
MapCard_Remove_2 [lemma, in Mapcard]
MapCard_Remove_1 [lemma, in Mapcard]
MapCard_Remove_lb [lemma, in Mapcard]
MapCard_Remove_ub [lemma, in Mapcard]
MapCard_Remove_sum [lemma, in Mapcard]
MapCard_makeM2 [lemma, in Mapcard]
MapCard_Put_behind_sum [lemma, in Mapcard]
MapCard_Put_behind_Put [lemma, in Mapcard]
MapCard_Dom_Put_behind [lemma, in Mapcard]
MapCard_Dom [lemma, in Mapcard]
MapCard_ext [lemma, in Mapcard]
MapCard_Put_2_conv [lemma, in Mapcard]
MapCard_Put_1_conv [lemma, in Mapcard]
MapCard_Put_2 [lemma, in Mapcard]
MapCard_Put_1 [lemma, in Mapcard]
MapCard_Put_ub [lemma, in Mapcard]
MapCard_Put_lb [lemma, in Mapcard]
MapCard_Put_sum [lemma, in Mapcard]
MapCard_Put1_equals_2 [lemma, in Mapcard]
MapCard_as_length [lemma, in Mapcard]
MapCard_as_Fold [lemma, in Mapcard]
MapCard_as_Fold_1 [lemma, in Mapcard]
MapCard_is_one_unique [lemma, in Mapcard]
MapCard_is_one [lemma, in Mapcard]
MapCard_is_not_O [lemma, in Mapcard]
MapCard_is_O [lemma, in Mapcard]
MapCard_M1 [lemma, in Mapcard]
MapCard_M0 [lemma, in Mapcard]
MapCard.A [variable, in Mapcard]
MapCard.B [variable, in Mapcard]
MapCard2 [section, in Mapcard]
MapCard2.A [variable, in Mapcard]
MapCard2.B [variable, in Mapcard]
MapCard3 [section, in Mapcard]
MapCard3.A [variable, in Mapcard]
MapCard3.B [variable, in Mapcard]
MapCollect [definition, in Mapiter]
MapCollect_as_Fold [lemma, in Mapiter]
MapCollect_canon [lemma, in Mapcanon]
MapCollect1 [definition, in Mapiter]
MapC.A [variable, in Mapc]
MapC.B [variable, in Mapc]
MapC.C [variable, in Mapc]
MapDefs [section, in Map]
MapDefs.A [variable, in Map]
MapDelta [definition, in Map]
MapDelta_RestrTo_disjoint_2 [lemma, in Mapsubset]
MapDelta_RestrTo_disjoint [lemma, in Mapsubset]
MapDelta_disjoint [lemma, in Mapsubset]
MapDelta_semantics [lemma, in Map]
MapDelta_semantics_3 [lemma, in Map]
MapDelta_semantics_3_1 [lemma, in Map]
MapDelta_semantics_2 [lemma, in Map]
MapDelta_semantics_2_2 [lemma, in Map]
MapDelta_semantics_2_1 [lemma, in Map]
MapDelta_semantics_1 [lemma, in Map]
MapDelta_semantics_1_1 [lemma, in Map]
MapDelta_semantics_comm [lemma, in Map]
MapDelta_ext_r [lemma, in Mapaxioms]
MapDelta_ext_l [lemma, in Mapaxioms]
MapDelta_ext [lemma, in Mapaxioms]
MapDelta_sym [lemma, in Mapaxioms]
MapDelta_as_DomRestrBy_2 [lemma, in Mapaxioms]
MapDelta_as_DomRestrBy [lemma, in Mapaxioms]
MapDelta_as_Merge [lemma, in Mapaxioms]
MapDelta_nilpotent [lemma, in Mapaxioms]
MapDelta_m_empty [lemma, in Mapaxioms]
MapDelta_m_empty_1 [lemma, in Mapaxioms]
MapDelta_empty_m [lemma, in Mapaxioms]
MapDelta_empty_m_1 [lemma, in Mapaxioms]
MapDelta_canon [lemma, in Mapcanon]
MapDelta_disjoint_c [lemma, in Mapc]
MapDelta_sym_c [lemma, in Mapc]
MapDelta_as_DomRestrBy_2_c [lemma, in Mapc]
MapDelta_as_DomRestrBy_c [lemma, in Mapc]
MapDelta_as_Merge_c [lemma, in Mapc]
MapDelta_nilpotent_c [lemma, in Mapc]
MapDisjoint [definition, in Mapsubset]
MapDisjointDef [section, in Mapsubset]
MapDisjointDef.A [variable, in Mapsubset]
MapDisjointDef.B [variable, in Mapsubset]
MapDisjointExtra [section, in Mapsubset]
MapDisjointExtra.A [variable, in Mapsubset]
MapDisjointExtra.B [variable, in Mapsubset]
MapDisjointExtra.C [variable, in Mapsubset]
MapDisjointExtra.D [variable, in Mapsubset]
MapDisjoint_empty [lemma, in Mapsubset]
MapDisjoint_sym [lemma, in Mapsubset]
MapDisjoint_M1_conv_r [lemma, in Mapsubset]
MapDisjoint_M1_conv_l [lemma, in Mapsubset]
MapDisjoint_M1_r [lemma, in Mapsubset]
MapDisjoint_M1_l [lemma, in Mapsubset]
MapDisjoint_M2 [lemma, in Mapsubset]
MapDisjoint_M2_r [lemma, in Mapsubset]
MapDisjoint_M2_l [lemma, in Mapsubset]
MapDisjoint_ext [lemma, in Mapsubset]
MapDisjoint_2_imp [lemma, in Mapsubset]
MapDisjoint_imp_2 [lemma, in Mapsubset]
MapDisjoint_1_imp [lemma, in Mapsubset]
MapDisjoint_imp_1 [lemma, in Mapsubset]
MapDisjoint_2 [definition, in Mapsubset]
MapDisjoint_1 [definition, in Mapsubset]
MapDisjoint_empty_c [lemma, in Mapc]
MapDom [definition, in Fset]
MapDomRestrBy [definition, in Fset]
MapDomRestrBy_Card_lb [lemma, in Mapcard]
MapDomRestrBy_Card_ub_l [lemma, in Mapcard]
MapDomRestrBy_semantics [lemma, in Fset]
MapDomRestrBy_m_m [lemma, in Mapaxioms]
MapDomRestrBy_ext_r [lemma, in Mapaxioms]
MapDomRestrBy_ext_l [lemma, in Mapaxioms]
MapDomRestrBy_ext [lemma, in Mapaxioms]
MapDomRestrBy_To_comm [lemma, in Mapaxioms]
MapDomRestrBy_To [lemma, in Mapaxioms]
MapDomRestrBy_By_comm [lemma, in Mapaxioms]
MapDomRestrBy_By [lemma, in Mapaxioms]
MapDomRestrBy_m_m_1 [lemma, in Mapaxioms]
MapDomRestrBy_Dom [lemma, in Mapaxioms]
MapDomRestrBy_m_empty [lemma, in Mapaxioms]
MapDomRestrBy_m_empty_1 [lemma, in Mapaxioms]
MapDomRestrBy_empty_m [lemma, in Mapaxioms]
MapDomRestrBy_empty_m_1 [lemma, in Mapaxioms]
MapDomRestrBy_canon [lemma, in Mapcanon]
MapDomRestrBy_To_comm_c [lemma, in Mapc]
MapDomRestrBy_To_c [lemma, in Mapc]
MapDomRestrBy_By_comm_c [lemma, in Mapc]
MapDomRestrBy_By_c [lemma, in Mapc]
MapDomRestrBy_Dom_c [lemma, in Mapc]
MapDomRestrTo [definition, in Fset]
MapDomRestrTo_Card_ub_r [lemma, in Mapcard]
MapDomRestrTo_Card_ub_l [lemma, in Mapcard]
MapDomRestrTo_semantics [lemma, in Fset]
MapDomRestrTo_ext_r [lemma, in Mapaxioms]
MapDomRestrTo_ext_l [lemma, in Mapaxioms]
MapDomRestrTo_ext [lemma, in Mapaxioms]
MapDomRestrTo_To_comm [lemma, in Mapaxioms]
MapDomRestrTo_By_comm [lemma, in Mapaxioms]
MapDomRestrTo_By [lemma, in Mapaxioms]
MapDomRestrTo_Dom [lemma, in Mapaxioms]
MapDomRestrTo_idempotent [lemma, in Mapaxioms]
MapDomRestrTo_assoc [lemma, in Mapaxioms]
MapDomRestrTo_m_empty [lemma, in Mapaxioms]
MapDomRestrTo_m_empty_1 [lemma, in Mapaxioms]
MapDomRestrTo_empty_m [lemma, in Mapaxioms]
MapDomRestrTo_empty_m_1 [lemma, in Mapaxioms]
MapDomRestrTo_canon [lemma, in Mapcanon]
MapDomRestrTo_To_comm_c [lemma, in Mapc]
MapDomRestrTo_By_comm_c [lemma, in Mapc]
MapDomRestrTo_By_c [lemma, in Mapc]
MapDomRestrTo_Dom_c [lemma, in Mapc]
MapDomRestrTo_idempotent_c [lemma, in Mapc]
MapDomRestrTo_assoc_c [lemma, in Mapc]
MapDomRestr_disjoint [lemma, in Mapsubset]
MapDom_Dom [lemma, in Fset]
MapDom_semantics_4 [lemma, in Fset]
MapDom_semantics_3 [lemma, in Fset]
MapDom_semantics_2 [lemma, in Fset]
MapDom_semantics_1 [lemma, in Fset]
MapDom_Split_3 [lemma, in Mapaxioms]
MapDom_Split_2 [lemma, in Mapaxioms]
MapDom_Split_1 [lemma, in Mapaxioms]
MapDom_canon [lemma, in Mapcanon]
MapDom_Split_3_c [lemma, in Mapc]
MapDom_Split_2_c [lemma, in Mapc]
MapDom_Split_1_c [lemma, in Mapc]
MapEmptyp [definition, in Map]
MapEmptyp_complete [lemma, in Map]
MapEmptyp_correct [lemma, in Map]
MapFold [definition, in Mapiter]
Mapfold [library]
MapFoldCanon [section, in Mapcanon]
MapFoldCanon.A [variable, in Mapcanon]
MapFoldCanon.B [variable, in Mapcanon]
MapFoldDistr [section, in Mapfold]
MapFoldDistrL [section, in Mapfold]
MapFoldDistrL.A [variable, in Mapfold]
MapFoldDistrL.absorb [variable, in Mapfold]
MapFoldDistrL.distr [variable, in Mapfold]
MapFoldDistrL.M [variable, in Mapfold]
MapFoldDistrL.M' [variable, in Mapfold]
MapFoldDistrL.N [variable, in Mapfold]
MapFoldDistrL.neutral [variable, in Mapfold]
MapFoldDistrL.neutral' [variable, in Mapfold]
MapFoldDistrL.op [variable, in Mapfold]
MapFoldDistrL.op' [variable, in Mapfold]
MapFoldDistrL.times [variable, in Mapfold]
MapFoldDistr.A [variable, in Mapfold]
MapFoldDistr.absorb [variable, in Mapfold]
MapFoldDistr.distr [variable, in Mapfold]
MapFoldDistr.M [variable, in Mapfold]
MapFoldDistr.M' [variable, in Mapfold]
MapFoldDistr.N [variable, in Mapfold]
MapFoldDistr.neutral [variable, in Mapfold]
MapFoldDistr.neutral' [variable, in Mapfold]
MapFoldDistr.op [variable, in Mapfold]
MapFoldDistr.op' [variable, in Mapfold]
MapFoldDistr.times [variable, in Mapfold]
MapFoldExists [section, in Mapfold]
MapFoldExists.A [variable, in Mapfold]
MapFoldResults [section, in Mapfold]
MapFoldResults.A [variable, in Mapfold]
MapFoldResults.assoc [variable, in Mapfold]
MapFoldResults.comm [variable, in Mapfold]
MapFoldResults.M [variable, in Mapfold]
MapFoldResults.neutral [variable, in Mapfold]
MapFoldResults.nleft [variable, in Mapfold]
MapFoldResults.nright [variable, in Mapfold]
MapFoldResults.op [variable, in Mapfold]
MapFold_orb [lemma, in Mapfold]
MapFold_orb_1 [lemma, in Mapfold]
MapFold_distr_l [lemma, in Mapfold]
MapFold_distr_r [lemma, in Mapfold]
MapFold_distr_r_1 [lemma, in Mapfold]
MapFold_Merge_disjoint [lemma, in Mapfold]
MapFold_Merge_disjoint_1 [lemma, in Mapfold]
MapFold_Put_behind_disjoint [lemma, in Mapfold]
MapFold_Put_behind_disjoint_2 [lemma, in Mapfold]
MapFold_Put_disjoint [lemma, in Mapfold]
MapFold_Put_disjoint_2 [lemma, in Mapfold]
MapFold_Put_disjoint_1 [lemma, in Mapfold]
MapFold_ext_f [lemma, in Mapfold]
MapFold_ext_f_1 [lemma, in Mapfold]
MapFold_ext [lemma, in Mapfold]
MapFold_as_fold [lemma, in Mapiter]
MapFold_as_fold_1 [lemma, in Mapiter]
MapFold_state_stateless [lemma, in Mapiter]
MapFold_state_stateless_1 [lemma, in Mapiter]
MapFold_state [definition, in Mapiter]
MapFold_M1 [lemma, in Mapiter]
MapFold_empty [lemma, in Mapiter]
MapFold_canon [lemma, in Mapcanon]
MapFold_canon_1 [lemma, in Mapcanon]
MapFold1 [definition, in Mapiter]
MapFold1_ext [lemma, in Mapfold]
MapFold1_as_Fold [lemma, in Mapfold]
MapFold1_as_Fold_1 [lemma, in Mapfold]
MapFold1_state [definition, in Mapiter]
MapGet [definition, in Map]
MapGet_M2_both_None [lemma, in Map]
MapGet_M2_bit_0_2 [lemma, in Map]
MapGet_if_same [lemma, in Map]
MapGet_if_commute [lemma, in Map]
MapGet_M2_bit_0 [lemma, in Map]
MapGet_M2_bit_0_if [lemma, in Map]
MapGet_M2_bit_0_1 [lemma, in Map]
MapGet_M2_bit_0_0 [lemma, in Map]
MapIter [section, in Mapiter]
Mapiter [library]
MapIter.A [variable, in Mapiter]
MapIter.B [variable, in Mapiter]
MapIter.MapFoldDef [section, in Mapiter]
MapIter.MapFoldDef.f [variable, in Mapiter]
MapIter.MapFoldDef.M [variable, in Mapiter]
MapIter.MapFoldDef.neutral [variable, in Mapiter]
MapIter.MapFoldDef.op [variable, in Mapiter]
MapIter.MapFoldDef.State [variable, in Mapiter]
MapIter.MapSweepDef [section, in Mapiter]
MapIter.MapSweepDef.f [variable, in Mapiter]
MapLists [section, in Maplists]
Maplists [library]
MapLists.ListOfDomDef [section, in Maplists]
MapLists.ListOfDomDef.A [variable, in Maplists]
MapMerge [definition, in Map]
MapMerge_disjoint [lemma, in Mapsubset]
MapMerge_semantics [lemma, in Map]
MapMerge_Card_lb_r [lemma, in Mapcard]
MapMerge_Card_lb_l [lemma, in Mapcard]
MapMerge_Card_disjoint [lemma, in Mapcard]
MapMerge_Card_ub [lemma, in Mapcard]
MapMerge_disjoint_Card [lemma, in Mapcard]
MapMerge_Restr_Card [lemma, in Mapcard]
MapMerge_DomRestrBy [lemma, in Mapaxioms]
MapMerge_DomRestrTo [lemma, in Mapaxioms]
MapMerge_RestrTo_l [lemma, in Mapaxioms]
MapMerge_ext_r [lemma, in Mapaxioms]
MapMerge_ext_l [lemma, in Mapaxioms]
MapMerge_ext [lemma, in Mapaxioms]
MapMerge_idempotent [lemma, in Mapaxioms]
MapMerge_assoc [lemma, in Mapaxioms]
MapMerge_empty_r [lemma, in Mapaxioms]
MapMerge_empty_l [lemma, in Mapaxioms]
MapMerge_m_empty [lemma, in Mapaxioms]
MapMerge_m_empty_1 [lemma, in Mapaxioms]
MapMerge_empty_m [lemma, in Mapaxioms]
MapMerge_empty_m_1 [lemma, in Mapaxioms]
MapMerge_canon [lemma, in Mapcanon]
MapMerge_DomRestrBy_c [lemma, in Mapc]
MapMerge_DomRestrTo_c [lemma, in Mapc]
MapMerge_RestrTo_l_c [lemma, in Mapc]
MapMerge_idempotent_c [lemma, in Mapc]
MapMerge_assoc_c [lemma, in Mapc]
MapMerge_empty_m_c [lemma, in Mapc]
MapPut [definition, in Map]
MapPut_behind_semantics [lemma, in Map]
MapPut_behind_new [lemma, in Map]
MapPut_behind_as_before [lemma, in Map]
MapPut_behind_as_before_1 [lemma, in Map]
MapPut_behind_semantics_3_1 [lemma, in Map]
MapPut_behind [definition, in Map]
MapPut_semantics [lemma, in Map]
MapPut_semantics_3_1 [lemma, in Map]
MapPut_semantics_2 [lemma, in Map]
MapPut_semantics_2_2 [lemma, in Map]
MapPut_semantics_2_1 [lemma, in Map]
MapPut_semantics_1 [lemma, in Map]
MapPut_behind_ext [lemma, in Mapaxioms]
MapPut_behind_as_Merge [lemma, in Mapaxioms]
MapPut_ext [lemma, in Mapaxioms]
MapPut_as_Merge [lemma, in Mapaxioms]
MapPut_behind_canon [lemma, in Mapcanon]
MapPut_canon [lemma, in Mapcanon]
MapPut_behind_as_Merge_c [lemma, in Mapc]
MapPut_as_Merge_c [lemma, in Mapc]
MapPut_in [lemma, in SetChecker]
MapPut1 [definition, in Map]
MapPut1_semantics' [lemma, in Map]
MapPut1_semantics [lemma, in Map]
MapPut1_semantics_3 [lemma, in Map]
MapPut1_semantics_2 [lemma, in Map]
MapPut1_semantics_1 [lemma, in Map]
MapPut1_canon [lemma, in Mapcanon]
MapPut1_in [lemma, in SetChecker]
MapRemove [definition, in Map]
MapRemove_semantics [lemma, in Map]
MapRemove_ext [lemma, in Mapaxioms]
MapRemove_as_RestrBy [lemma, in Mapaxioms]
MapRemove_canon [lemma, in Mapcanon]
MapRemove_as_RestrBy_c [lemma, in Mapc]
MapRemove_in [lemma, in SetChecker]
MapSingleton [definition, in Map]
MapSingleton_semantics [lemma, in Map]
MapSplit_Card [lemma, in Mapcard]
MapSubset [definition, in Mapsubset]
Mapsubset [library]
MapSubsetDef [section, in Mapsubset]
MapSubsetDef.A [variable, in Mapsubset]
MapSubsetDef.B [variable, in Mapsubset]
MapSubsetExtra [section, in Mapsubset]
MapSubsetExtra.A [variable, in Mapsubset]
MapSubsetExtra.B [variable, in Mapsubset]
MapSubsetExtra.C [variable, in Mapsubset]
MapSubsetExtra.D [variable, in Mapsubset]
MapSubsetOrder [section, in Mapsubset]
MapSubsetOrder.A [variable, in Mapsubset]
MapSubsetOrder.B [variable, in Mapsubset]
MapSubsetOrder.C [variable, in Mapsubset]
MapSubset_Disjoint_r [lemma, in Mapsubset]
MapSubset_Disjoint_l [lemma, in Mapsubset]
MapSubset_Disjoint [lemma, in Mapsubset]
MapSubset_DomRestrBy_mono [lemma, in Mapsubset]
MapSubset_DomRestrBy_l [lemma, in Mapsubset]
MapSubset_DomRestrTo_mono [lemma, in Mapsubset]
MapSubset_ext [lemma, in Mapsubset]
MapSubset_DomRestrTo_r [lemma, in Mapsubset]
MapSubset_DomRestrTo_l [lemma, in Mapsubset]
MapSubset_Merge_mono [lemma, in Mapsubset]
MapSubset_Merge_r [lemma, in Mapsubset]
MapSubset_Merge_l [lemma, in Mapsubset]
MapSubset_Remove_mono [lemma, in Mapsubset]
MapSubset_Remove [lemma, in Mapsubset]
MapSubset_Put_behind_mono [lemma, in Mapsubset]
MapSubset_Put_behind [lemma, in Mapsubset]
MapSubset_Put_mono [lemma, in Mapsubset]
MapSubset_Put [lemma, in Mapsubset]
MapSubset_1_Dom [lemma, in Mapsubset]
MapSubset_Dom_2 [lemma, in Mapsubset]
MapSubset_Dom_1 [lemma, in Mapsubset]
MapSubset_trans [lemma, in Mapsubset]
MapSubset_antisym [lemma, in Mapsubset]
MapSubset_refl [lemma, in Mapsubset]
MapSubset_2_imp [lemma, in Mapsubset]
MapSubset_imp_2 [lemma, in Mapsubset]
MapSubset_1_imp [lemma, in Mapsubset]
MapSubset_imp_1 [lemma, in Mapsubset]
MapSubset_2 [definition, in Mapsubset]
MapSubset_1 [definition, in Mapsubset]
MapSubset_card_eq [lemma, in Mapcard]
MapSubset_Card_le [lemma, in Mapcard]
MapSubset_card_eq_1 [lemma, in Mapcard]
MapSubset_c_2 [lemma, in Mapcanon]
MapSubset_c_1 [lemma, in Mapcanon]
MapSubset_antisym_c [lemma, in Mapc]
MapSweep [definition, in Mapiter]
MapSweep_semantics_4 [lemma, in Mapiter]
MapSweep_semantics_4_1 [lemma, in Mapiter]
MapSweep_semantics_3 [lemma, in Mapiter]
MapSweep_semantics_3_1 [lemma, in Mapiter]
MapSweep_semantics_2 [lemma, in Mapiter]
MapSweep_semantics_2_2 [lemma, in Mapiter]
MapSweep_semantics_2_1 [lemma, in Mapiter]
MapSweep_semantics_1 [lemma, in Mapiter]
MapSweep_semantics_1_1 [lemma, in Mapiter]
MapSweep1 [definition, in Mapiter]
MapSweep2 [definition, in Mapiter]
Map_disjoint_M0 [lemma, in Mapsubset]
Map_M0_disjoint [lemma, in Mapsubset]
map_dom_empty_2 [lemma, in Mapsubset]
map_dom_empty_1 [lemma, in Mapsubset]
map_in [lemma, in Basic]
Map_of_alist_of_Map [lemma, in Mapiter]
Map_of_alist_semantics [lemma, in Mapiter]
Map_of_alist [definition, in Mapiter]
Map_of_alist_canon [lemma, in Mapcanon]
Map_of_alist_of_Map_c [lemma, in Mapc]
Map2_semantics_3_eq [lemma, in Map]
Map2_semantics_3 [lemma, in Map]
Map2_semantics_2_eq [lemma, in Map]
Map2_semantics_2 [lemma, in Map]
Map2_semantics_1_eq [lemma, in Map]
Map2_semantics_1 [lemma, in Map]
M0 [constructor, in Map]
M0_canon [constructor, in Mapcanon]
M1 [constructor, in Map]
M1_semantics_2 [lemma, in Map]
M1_semantics_1 [lemma, in Map]
M1_canon [constructor, in Mapcanon]
M2 [constructor, in Map]
M2_eqmap_2 [lemma, in Mapcanon]
M2_eqmap_1 [lemma, in Mapcanon]
M2_canon [constructor, in Mapcanon]
N
NatCompare [section, in Basic]nat_compare_trans [lemma, in Basic]
nat_compare_sym_gt [lemma, in Basic]
nat_compare_sym_lt [lemma, in Basic]
nat_compare_eq_rev [lemma, in Basic]
Ndouble_plus_one_monotonic [lemma, in Lsort]
Ndouble_monotonic [lemma, in Lsort]
neg [constructor, in CNF]
negate [definition, in CNF]
negF [definition, in Generate]
neg_cube [definition, in CubeAndConquer]
neg_in [lemma, in Generate]
newMap [definition, in Map]
newMap_semantics [lemma, in Map]
noCube [definition, in CubeAndConquer]
node [constructor, in BinaryTrees]
nought [constructor, in BinaryTrees]
no_occurrence_dec [lemma, in Generate]
no_occurrence_add [lemma, in Generate]
no_occurrence_char [lemma, in Generate]
no_occurrence [definition, in Generate]
no_pythagorean [lemma, in Generate]
O
O [constructor, in SetChecker]ok_list [definition, in Generate]
one_occurrence_dec [lemma, in Generate]
one_occurrence_find [lemma, in Generate]
one_occurrence [definition, in Generate]
option_sum [lemma, in Map]
Oracle [definition, in SetChecker]
Oracle_size [definition, in SetChecker]
outer_cycle_okl [lemma, in Generate]
outer_cycle [definition, in Generate]
P
pair_sp [lemma, in Mapiter]pos [constructor, in CNF]
posF [definition, in Generate]
pos_in [lemma, in Generate]
propagate [definition, in SetChecker]
propagate_sound [lemma, in SetChecker]
propagate_true [lemma, in SetChecker]
propagate_entails [lemma, in SetChecker]
propagate_empty [lemma, in SetChecker]
propagate_singleton [lemma, in SetChecker]
Propagation [section, in SetChecker]
Pythagoras [section, in Generate]
pythagorean [definition, in Generate]
Pythagorean_Theorem'' [lemma, in Generate]
Pythagorean_Theorem' [lemma, in Generate]
Pythagorean_Theorem [lemma, in Generate]
pythagorean_dec [lemma, in Generate]
pythagorean_lim_equiv [lemma, in Generate]
pythagorean_equiv [lemma, in Generate]
pythagorean_neg [definition, in Generate]
pythagorean_pos [definition, in Generate]
pythagorean_neq_1 [lemma, in Generate]
pythagorean_neq_2 [lemma, in Generate]
pythagorean_comm [lemma, in Generate]
pyth_lim_gen_neg [lemma, in Generate]
pyth_lim_gen [lemma, in Generate]
pyth_lim_neg [definition, in Generate]
pyth_lim_pos [definition, in Generate]
R
R [constructor, in SetChecker]reduces [definition, in Generate]
Refutation [section, in SetChecker]
refute [definition, in SetChecker]
refute_correct [lemma, in SetChecker]
refute_work_correct [lemma, in SetChecker]
RemoveAll [section, in Basic]
RemoveAll.A [variable, in Basic]
RemoveAll.A_dec [variable, in Basic]
remove_all_orig [lemma, in Basic]
remove_all [definition, in Basic]
remove_neq [lemma, in Basic]
remove_not_In [lemma, in Basic]
remove_in [lemma, in Generate]
remove_keep [lemma, in Generate]
remove_no_occurrence [lemma, in Generate]
remove_number [definition, in Generate]
S
satisfies [definition, in CNF]satisfies_Cubed_CNF [lemma, in CubeAndConquer]
satisfies_remove [lemma, in CNF]
satisfies_for_all [lemma, in CNF]
satisfies_to_T_satisfies' [lemma, in SetChecker]
satisfies_to_T_satisfies [lemma, in SetChecker]
SC_in_add [lemma, in SetChecker]
SC_satisfies_exists [lemma, in SetChecker]
SC_to_C_In_2 [lemma, in SetChecker]
SC_to_C_In_1 [lemma, in SetChecker]
SC_wf [definition, in SetChecker]
SC_diff [definition, in SetChecker]
SC_in [definition, in SetChecker]
SC_add [definition, in SetChecker]
SetChecker [library]
SetClause [definition, in SetChecker]
SetClauses [section, in SetChecker]
SetClause_eq_nil_cons [lemma, in SetChecker]
SetClause_eq_dec [lemma, in SetChecker]
SetClause_to_Clause_inv [lemma, in SetChecker]
SetClause_to_Clause [definition, in SetChecker]
Simplification [section, in Generate]
simplification_ok [lemma, in Generate]
simplified_BPT_formula [definition, in Generate]
simplify [definition, in Generate]
symbreak_ok [lemma, in Generate]
SymmetryBreak [section, in Generate]
T
target_formula_in [lemma, in Generate]target_formula [definition, in Generate]
target_list [definition, in Generate]
TCNF_In [lemma, in SetChecker]
TCNF_In' [lemma, in SetChecker]
TCNF_to_CNF [definition, in SetChecker]
TCNF_eq_dec [lemma, in SetChecker]
TCNF_add [definition, in SetChecker]
TCNF_join [definition, in SetChecker]
TCNF_wf [definition, in SetChecker]
TCNF_remove [definition, in SetChecker]
TCNF_in [definition, in SetChecker]
TheBreak [axiom, in Generate]
TheN [axiom, in Generate]
The_Asymmetric_CNF [definition, in Generate]
The_Simple_CNF [definition, in Generate]
The_List [axiom, in Generate]
The_CNF [definition, in Generate]
TreeCNF [definition, in SetChecker]
TreeCNF [section, in SetChecker]
Trees [section, in BinaryTrees]
Trees.Balancing [section, in BinaryTrees]
Trees.BT_Wf [variable, in BinaryTrees]
Trees.eq_T_compare [variable, in BinaryTrees]
Trees.Map [section, in BinaryTrees]
Trees.Map.f [variable, in BinaryTrees]
Trees.T [variable, in BinaryTrees]
Trees.T_dec [variable, in BinaryTrees]
Trees.T_compare_sym_Lt [variable, in BinaryTrees]
Trees.T_compare_sym_Gt [variable, in BinaryTrees]
Trees.T_compare_trans [variable, in BinaryTrees]
Trees.T_compare_eq [variable, in BinaryTrees]
Trees.T_compare [variable, in BinaryTrees]
true_C_true [lemma, in CNF]
true_C [definition, in CNF]
true_SC [definition, in SetChecker]
T_satisfies_to_satisfies' [lemma, in SetChecker]
T_satisfies_to_satisfies [lemma, in SetChecker]
T_satisfies [definition, in SetChecker]
U
unsat [definition, in CNF]unsat_subset [lemma, in CNF]
unsat_remove [lemma, in CNF]
V
Valuation [definition, in CNF]val_gives_colorful [lemma, in Generate]
Z
Zabs_diff_le_1 [lemma, in Basic]Zabs_le_1 [lemma, in Basic]
Z_stuff [section, in Basic]
Variable Index
A
AdAlloc.A [in Adalloc]D
DMergeDef.A [in Mapfold]Dom.A [in Fset]
Dom.B [in Fset]
F
FSetCanon.A [in Mapcanon]FSetDefs.A [in Fset]
I
InDom.A [in Fset]InDom.B [in Fset]
L
LSort.A [in Lsort]M
MapAxioms.A [in Mapaxioms]MapAxioms.B [in Mapaxioms]
MapAxioms.C [in Mapaxioms]
MapCanon.A [in Mapcanon]
MapCanon.B [in Mapcanon]
MapCard.A [in Mapcard]
MapCard.B [in Mapcard]
MapCard2.A [in Mapcard]
MapCard2.B [in Mapcard]
MapCard3.A [in Mapcard]
MapCard3.B [in Mapcard]
MapC.A [in Mapc]
MapC.B [in Mapc]
MapC.C [in Mapc]
MapDefs.A [in Map]
MapDisjointDef.A [in Mapsubset]
MapDisjointDef.B [in Mapsubset]
MapDisjointExtra.A [in Mapsubset]
MapDisjointExtra.B [in Mapsubset]
MapDisjointExtra.C [in Mapsubset]
MapDisjointExtra.D [in Mapsubset]
MapFoldCanon.A [in Mapcanon]
MapFoldCanon.B [in Mapcanon]
MapFoldDistrL.A [in Mapfold]
MapFoldDistrL.absorb [in Mapfold]
MapFoldDistrL.distr [in Mapfold]
MapFoldDistrL.M [in Mapfold]
MapFoldDistrL.M' [in Mapfold]
MapFoldDistrL.N [in Mapfold]
MapFoldDistrL.neutral [in Mapfold]
MapFoldDistrL.neutral' [in Mapfold]
MapFoldDistrL.op [in Mapfold]
MapFoldDistrL.op' [in Mapfold]
MapFoldDistrL.times [in Mapfold]
MapFoldDistr.A [in Mapfold]
MapFoldDistr.absorb [in Mapfold]
MapFoldDistr.distr [in Mapfold]
MapFoldDistr.M [in Mapfold]
MapFoldDistr.M' [in Mapfold]
MapFoldDistr.N [in Mapfold]
MapFoldDistr.neutral [in Mapfold]
MapFoldDistr.neutral' [in Mapfold]
MapFoldDistr.op [in Mapfold]
MapFoldDistr.op' [in Mapfold]
MapFoldDistr.times [in Mapfold]
MapFoldExists.A [in Mapfold]
MapFoldResults.A [in Mapfold]
MapFoldResults.assoc [in Mapfold]
MapFoldResults.comm [in Mapfold]
MapFoldResults.M [in Mapfold]
MapFoldResults.neutral [in Mapfold]
MapFoldResults.nleft [in Mapfold]
MapFoldResults.nright [in Mapfold]
MapFoldResults.op [in Mapfold]
MapIter.A [in Mapiter]
MapIter.B [in Mapiter]
MapIter.MapFoldDef.f [in Mapiter]
MapIter.MapFoldDef.M [in Mapiter]
MapIter.MapFoldDef.neutral [in Mapiter]
MapIter.MapFoldDef.op [in Mapiter]
MapIter.MapFoldDef.State [in Mapiter]
MapIter.MapSweepDef.f [in Mapiter]
MapLists.ListOfDomDef.A [in Maplists]
MapSubsetDef.A [in Mapsubset]
MapSubsetDef.B [in Mapsubset]
MapSubsetExtra.A [in Mapsubset]
MapSubsetExtra.B [in Mapsubset]
MapSubsetExtra.C [in Mapsubset]
MapSubsetExtra.D [in Mapsubset]
MapSubsetOrder.A [in Mapsubset]
MapSubsetOrder.B [in Mapsubset]
MapSubsetOrder.C [in Mapsubset]
R
RemoveAll.A [in Basic]RemoveAll.A_dec [in Basic]
T
Trees.BT_Wf [in BinaryTrees]Trees.eq_T_compare [in BinaryTrees]
Trees.Map.f [in BinaryTrees]
Trees.T [in BinaryTrees]
Trees.T_dec [in BinaryTrees]
Trees.T_compare_sym_Lt [in BinaryTrees]
Trees.T_compare_sym_Gt [in BinaryTrees]
Trees.T_compare_trans [in BinaryTrees]
Trees.T_compare_eq [in BinaryTrees]
Trees.T_compare [in BinaryTrees]
Library Index
A
AdallocAllmaps
B
BasicBinaryTrees
C
CNFCubeAndConquer
E
ExtractionCheckerExtractionCubes
ExtractionNoCubes
F
FsetG
GenerateL
LsortM
MapMapaxioms
Mapc
Mapcanon
Mapcard
Mapfold
Mapiter
Maplists
Mapsubset
S
SetCheckerLemma Index
A
aapp_length [in Lsort]add_ICNF_unsat [in SetChecker]
ad_comp_double_plus_un_inj [in Mapiter]
ad_comp_double_inj [in Mapiter]
ad_alloc_opt_optimal [in Adalloc]
ad_alloc_opt_optimal_1 [in Adalloc]
ad_alloc_opt_allocates [in Adalloc]
ad_alloc_opt_allocates_1 [in Adalloc]
ad_list_of_dom_Dom [in Maplists]
ad_list_of_dom_Dom_1 [in Maplists]
ad_list_of_dom_not_stutters [in Maplists]
ad_list_of_dom_card [in Maplists]
ad_list_of_dom_card_1 [in Maplists]
ad_in_list_of_dom_in_dom [in Maplists]
ad_list_app_rev [in Maplists]
ad_list_stutters_rev [in Maplists]
ad_list_rev_length [in Maplists]
ad_list_stutters_permute [in Maplists]
ad_list_app_length [in Maplists]
ad_list_Elems [in Maplists]
ad_list_stutters_prev_conv_r [in Maplists]
ad_list_stutters_prev_r [in Maplists]
ad_list_stutters_prev_conv_l [in Maplists]
ad_list_stutters_prev_l [in Maplists]
ad_list_has_circuit_stutters [in Maplists]
ad_in_list_rev [in Maplists]
ad_in_list_app [in Maplists]
ad_in_list_app_1 [in Maplists]
ad_list_stutters_app_conv_r [in Maplists]
ad_list_stutters_app_conv_l [in Maplists]
ad_list_stutters_app_r [in Maplists]
ad_in_list_r [in Maplists]
ad_list_stutters_app_l [in Maplists]
ad_in_list_l [in Maplists]
ad_list_stutters_card_conv [in Maplists]
ad_list_not_stutters_card_conv [in Maplists]
ad_list_stutters_card [in Maplists]
ad_list_card [in Maplists]
ad_list_not_stutters_card [in Maplists]
ad_in_elems_in_list [in Maplists]
ad_list_stutters_has_circuit [in Maplists]
ad_in_list_forms_circuit [in Maplists]
ad_comp_double_plus_un_monotonic [in Lsort]
ad_comp_double_monotonic [in Lsort]
ad_comp_monotonic [in Lsort]
alist_semantics_disjoint_comm [in Mapiter]
alist_MapMerge_semantics_disjoint [in Mapiter]
alist_MapMerge_semantics [in Mapiter]
alist_of_Map_of_alist [in Mapiter]
alist_of_Map_semantics [in Mapiter]
alist_of_Map_semantics_1 [in Mapiter]
alist_of_Map_semantics_1_1 [in Mapiter]
alist_semantics_app [in Mapiter]
alist_of_Map_of_alist_c [in Mapc]
alist_canonical [in Lsort]
alist_sorted_tail [in Lsort]
alist_semantics_same_tail [in Lsort]
alist_semantics_tail [in Lsort]
alist_semantics_nth_ad [in Lsort]
alist_too_low [in Lsort]
alist_of_Map_sorts2 [in Lsort]
alist_of_Map_sorts1 [in Lsort]
alist_of_Map_sorts [in Lsort]
alist_of_Map_sorts_1 [in Lsort]
alist_of_Map_nth_ad [in Lsort]
alist_nth_ad_semantics [in Lsort]
alist_conc_sorted [in Lsort]
alist_nth_ad_aapp_2 [in Lsort]
alist_nth_ad_aapp_1 [in Lsort]
alist_sorted_2_imp [in Lsort]
alist_sorted_1_imp_2 [in Lsort]
alist_sorted_imp_1 [in Lsort]
app_length [in Lsort]
B
BPT_formula_sat [in Generate]BT_map_in [in BinaryTrees]
BT_in_add_all [in BinaryTrees]
BT_add_all_in [in BinaryTrees]
BT_add_all_mon [in BinaryTrees]
BT_add_all_wf_rev [in BinaryTrees]
BT_wf_add_all [in BinaryTrees]
BT_size_split [in BinaryTrees]
BT_nought_diff [in BinaryTrees]
BT_diff_nought [in BinaryTrees]
BT_diff_out' [in BinaryTrees]
BT_diff_out [in BinaryTrees]
BT_diff_in_rev [in BinaryTrees]
BT_diff_in [in BinaryTrees]
BT_diff_wf [in BinaryTrees]
BT_remove_out [in BinaryTrees]
BT_in_remove [in BinaryTrees]
BT_remove_in_rev [in BinaryTrees]
BT_remove_wf [in BinaryTrees]
BT_remove_in [in BinaryTrees]
BT_all_in_dec [in BinaryTrees]
BT_in_dec [in BinaryTrees]
BT_split_compare [in BinaryTrees]
BT_split_in [in BinaryTrees]
BT_split_in_l [in BinaryTrees]
BT_split_wf [in BinaryTrees]
BT_split_in_r [in BinaryTrees]
BT_add_wf_rev [in BinaryTrees]
BT_add_mon [in BinaryTrees]
BT_wf_add [in BinaryTrees]
BT_in_add [in BinaryTrees]
BT_add_in [in BinaryTrees]
BT_in_balance [in BinaryTrees]
BT_balance_in [in BinaryTrees]
BT_balance_wf [in BinaryTrees]
BT_in_rot_RR [in BinaryTrees]
BT_rot_RR_in [in BinaryTrees]
BT_rot_RR_wf [in BinaryTrees]
BT_in_rot_LL [in BinaryTrees]
BT_rot_LL_in [in BinaryTrees]
BT_rot_LL_wf [in BinaryTrees]
BT_rot_R_wf_rev [in BinaryTrees]
BT_in_rot_R [in BinaryTrees]
BT_rot_R_in [in BinaryTrees]
BT_rot_R_wf [in BinaryTrees]
BT_rot_L_wf_rev [in BinaryTrees]
BT_in_rot_L [in BinaryTrees]
BT_rot_L_in [in BinaryTrees]
BT_rot_L_wf [in BinaryTrees]
BT_singleton_char [in BinaryTrees]
BT_nought_char [in BinaryTrees]
C
change_val_p' [in Generate]change_val_p [in Generate]
Clause_compare_sym_Lt [in CNF]
Clause_compare_sym_Gt [in CNF]
Clause_compare_trans [in CNF]
Clause_compare_eq [in CNF]
clause_eq_nil_cons [in CNF]
clause_eq_dec [in CNF]
CNF_empty [in CNF]
CNF_eq_dec [in CNF]
colorful_simplify [in Generate]
colorful_remove_singleton [in Generate]
colorful_add [in Generate]
colorful_gives_val [in Generate]
compare_Eq_dec [in Basic]
compare_Gt_dec [in Basic]
compare_Lt_dec [in Basic]
CubeAndConquer_lemma [in CubeAndConquer]
Cubed_CNF_satisfies [in CubeAndConquer]
C_sat_clause [in CNF]
C_unsat_empty [in CNF]
C_satisfies_dec [in CNF]
C_satisfies_exists [in CNF]
C_to_C_satisfies_2 [in SetChecker]
C_to_C_satisfies_1 [in SetChecker]
C_to_SC_In_2 [in SetChecker]
C_to_SC_In_1 [in SetChecker]
C_to_SC_wf [in SetChecker]
D
del_ICNF_in [in SetChecker]E
Elems_of_list_of_dom_c [in Maplists]Elems_of_list_of_dom [in Maplists]
Elems_rev [in Maplists]
Elems_app [in Maplists]
Elems_canon [in Maplists]
eqmap_trans [in Mapaxioms]
eqmap_refl [in Mapaxioms]
eqmap_sym [in Mapaxioms]
eqm_trans [in Mapaxioms]
eqm_refl [in Mapaxioms]
eqm_sym [in Mapaxioms]
eq_Clause_compare [in CNF]
eq_Lit_compare [in CNF]
exists_C_satisfies [in CNF]
exists_SC_satisfies [in SetChecker]
F
fix_one_color [in Generate]fold_right_aapp [in Mapiter]
for_all_satisfies [in CNF]
FSetDelta_assoc [in Mapaxioms]
FSetDelta_assoc_c [in Mapc]
FSetInter_Union_r [in Mapaxioms]
FSetInter_Union_l [in Mapaxioms]
FSetInter_idempotent [in Mapaxioms]
FSetInter_s_M0 [in Mapaxioms]
FSetInter_M0_s [in Mapaxioms]
FSetInter_assoc [in Mapaxioms]
FSetInter_comm [in Mapaxioms]
FSetInter_Union_r [in Mapc]
FSetInter_Union_l_c [in Mapc]
FSetInter_idempotent [in Mapc]
FSetInter_s_M0_c [in Mapc]
FSetInter_M0_s_c [in Mapc]
FSetInter_assoc_c [in Mapc]
FSetInter_comm_c [in Mapc]
FSetUnion_Inter_r [in Mapaxioms]
FSetUnion_Inter_l [in Mapaxioms]
FSetUnion_idempotent [in Mapaxioms]
FSetUnion_s_M0 [in Mapaxioms]
FSetUnion_M0_s [in Mapaxioms]
FSetUnion_assoc [in Mapaxioms]
FSetUnion_comm [in Mapaxioms]
FSetUnion_Inter_r [in Mapc]
FSetUnion_Inter_l_c [in Mapc]
FSetUnion_idempotent [in Mapc]
FSetUnion_s_M0_c [in Mapc]
FSetUnion_M0_s_c [in Mapc]
FSetUnion_assoc_c [in Mapc]
FSetUnion_comm_c [in Mapc]
FSet_Dom [in Fset]
FSet_ext [in Mapaxioms]
FSet_ext_c [in Mapc]
FSubset_trans [in Mapsubset]
FSubset_antisym [in Mapsubset]
FSubset_refl [in Mapsubset]
FSubset_antisym_c [in Mapc]
G
get_ICNF_in_or_default [in SetChecker]I
ICNF_get_del [in SetChecker]ICNF_get_in [in SetChecker]
ICNF_to_TCNF_wf [in SetChecker]
inner_cycle_okl [in Generate]
interval_split [in Lsort]
in_dom_DMerge_3 [in Mapfold]
in_dom_DMerge_2 [in Mapfold]
in_dom_DMerge_1 [in Mapfold]
In_remove [in Basic]
in_remove [in Basic]
in_simplify [in Generate]
in_BTree_list [in BinaryTrees]
in_list_BTree [in BinaryTrees]
in_FSet_delta [in Fset]
in_FSet_diff [in Fset]
in_FSet_inter [in Fset]
in_FSet_union [in Fset]
in_dom_restrby [in Fset]
in_dom_restrto [in Fset]
in_dom_delta [in Fset]
in_dom_merge [in Fset]
in_dom_remove [in Fset]
in_dom_put_behind [in Fset]
in_dom_put [in Fset]
in_dom_none [in Fset]
in_dom_some [in Fset]
in_dom_M1_2 [in Fset]
in_dom_M1_1 [in Fset]
in_dom_M1 [in Fset]
in_dom_M0 [in Fset]
in_ICNF_get' [in SetChecker]
in_ICNF_get [in SetChecker]
In_TCNF [in SetChecker]
In_TCNF' [in SetChecker]
L
length_as_fold_2 [in Mapcard]length_as_fold [in Mapcard]
list_to_BTree_wf [in BinaryTrees]
list_append_split [in SetChecker]
Literal_neg_neg [in CubeAndConquer]
literal_eq_dec [in CNF]
Lit_compare_sym_Lt [in CNF]
Lit_compare_sym_Gt [in CNF]
Lit_compare_trans [in CNF]
Lit_compare_eq [in CNF]
L_satisfies_dec [in CNF]
L_satisfies_neg_neg [in CNF]
L_satisfies_neg [in CNF]
M
makeM2_M2 [in Map]makeM2_canon [in Mapcanon]
make_TCNF_wf [in SetChecker]
mapcanon_exists [in Mapcanon]
mapcanon_exists_2 [in Mapcanon]
mapcanon_exists_1 [in Mapcanon]
mapcanon_unique [in Mapcanon]
mapcanon_M2_2 [in Mapcanon]
mapcanon_M2_1 [in Mapcanon]
mapcanon_M2 [in Mapcanon]
MapCard_is_Sn [in Mapcard]
MapCard_Remove_2_conv [in Mapcard]
MapCard_Remove_1_conv [in Mapcard]
MapCard_Remove_2 [in Mapcard]
MapCard_Remove_1 [in Mapcard]
MapCard_Remove_lb [in Mapcard]
MapCard_Remove_ub [in Mapcard]
MapCard_Remove_sum [in Mapcard]
MapCard_makeM2 [in Mapcard]
MapCard_Put_behind_sum [in Mapcard]
MapCard_Put_behind_Put [in Mapcard]
MapCard_Dom_Put_behind [in Mapcard]
MapCard_Dom [in Mapcard]
MapCard_ext [in Mapcard]
MapCard_Put_2_conv [in Mapcard]
MapCard_Put_1_conv [in Mapcard]
MapCard_Put_2 [in Mapcard]
MapCard_Put_1 [in Mapcard]
MapCard_Put_ub [in Mapcard]
MapCard_Put_lb [in Mapcard]
MapCard_Put_sum [in Mapcard]
MapCard_Put1_equals_2 [in Mapcard]
MapCard_as_length [in Mapcard]
MapCard_as_Fold [in Mapcard]
MapCard_as_Fold_1 [in Mapcard]
MapCard_is_one_unique [in Mapcard]
MapCard_is_one [in Mapcard]
MapCard_is_not_O [in Mapcard]
MapCard_is_O [in Mapcard]
MapCard_M1 [in Mapcard]
MapCard_M0 [in Mapcard]
MapCollect_as_Fold [in Mapiter]
MapCollect_canon [in Mapcanon]
MapDelta_RestrTo_disjoint_2 [in Mapsubset]
MapDelta_RestrTo_disjoint [in Mapsubset]
MapDelta_disjoint [in Mapsubset]
MapDelta_semantics [in Map]
MapDelta_semantics_3 [in Map]
MapDelta_semantics_3_1 [in Map]
MapDelta_semantics_2 [in Map]
MapDelta_semantics_2_2 [in Map]
MapDelta_semantics_2_1 [in Map]
MapDelta_semantics_1 [in Map]
MapDelta_semantics_1_1 [in Map]
MapDelta_semantics_comm [in Map]
MapDelta_ext_r [in Mapaxioms]
MapDelta_ext_l [in Mapaxioms]
MapDelta_ext [in Mapaxioms]
MapDelta_sym [in Mapaxioms]
MapDelta_as_DomRestrBy_2 [in Mapaxioms]
MapDelta_as_DomRestrBy [in Mapaxioms]
MapDelta_as_Merge [in Mapaxioms]
MapDelta_nilpotent [in Mapaxioms]
MapDelta_m_empty [in Mapaxioms]
MapDelta_m_empty_1 [in Mapaxioms]
MapDelta_empty_m [in Mapaxioms]
MapDelta_empty_m_1 [in Mapaxioms]
MapDelta_canon [in Mapcanon]
MapDelta_disjoint_c [in Mapc]
MapDelta_sym_c [in Mapc]
MapDelta_as_DomRestrBy_2_c [in Mapc]
MapDelta_as_DomRestrBy_c [in Mapc]
MapDelta_as_Merge_c [in Mapc]
MapDelta_nilpotent_c [in Mapc]
MapDisjoint_empty [in Mapsubset]
MapDisjoint_sym [in Mapsubset]
MapDisjoint_M1_conv_r [in Mapsubset]
MapDisjoint_M1_conv_l [in Mapsubset]
MapDisjoint_M1_r [in Mapsubset]
MapDisjoint_M1_l [in Mapsubset]
MapDisjoint_M2 [in Mapsubset]
MapDisjoint_M2_r [in Mapsubset]
MapDisjoint_M2_l [in Mapsubset]
MapDisjoint_ext [in Mapsubset]
MapDisjoint_2_imp [in Mapsubset]
MapDisjoint_imp_2 [in Mapsubset]
MapDisjoint_1_imp [in Mapsubset]
MapDisjoint_imp_1 [in Mapsubset]
MapDisjoint_empty_c [in Mapc]
MapDomRestrBy_Card_lb [in Mapcard]
MapDomRestrBy_Card_ub_l [in Mapcard]
MapDomRestrBy_semantics [in Fset]
MapDomRestrBy_m_m [in Mapaxioms]
MapDomRestrBy_ext_r [in Mapaxioms]
MapDomRestrBy_ext_l [in Mapaxioms]
MapDomRestrBy_ext [in Mapaxioms]
MapDomRestrBy_To_comm [in Mapaxioms]
MapDomRestrBy_To [in Mapaxioms]
MapDomRestrBy_By_comm [in Mapaxioms]
MapDomRestrBy_By [in Mapaxioms]
MapDomRestrBy_m_m_1 [in Mapaxioms]
MapDomRestrBy_Dom [in Mapaxioms]
MapDomRestrBy_m_empty [in Mapaxioms]
MapDomRestrBy_m_empty_1 [in Mapaxioms]
MapDomRestrBy_empty_m [in Mapaxioms]
MapDomRestrBy_empty_m_1 [in Mapaxioms]
MapDomRestrBy_canon [in Mapcanon]
MapDomRestrBy_To_comm_c [in Mapc]
MapDomRestrBy_To_c [in Mapc]
MapDomRestrBy_By_comm_c [in Mapc]
MapDomRestrBy_By_c [in Mapc]
MapDomRestrBy_Dom_c [in Mapc]
MapDomRestrTo_Card_ub_r [in Mapcard]
MapDomRestrTo_Card_ub_l [in Mapcard]
MapDomRestrTo_semantics [in Fset]
MapDomRestrTo_ext_r [in Mapaxioms]
MapDomRestrTo_ext_l [in Mapaxioms]
MapDomRestrTo_ext [in Mapaxioms]
MapDomRestrTo_To_comm [in Mapaxioms]
MapDomRestrTo_By_comm [in Mapaxioms]
MapDomRestrTo_By [in Mapaxioms]
MapDomRestrTo_Dom [in Mapaxioms]
MapDomRestrTo_idempotent [in Mapaxioms]
MapDomRestrTo_assoc [in Mapaxioms]
MapDomRestrTo_m_empty [in Mapaxioms]
MapDomRestrTo_m_empty_1 [in Mapaxioms]
MapDomRestrTo_empty_m [in Mapaxioms]
MapDomRestrTo_empty_m_1 [in Mapaxioms]
MapDomRestrTo_canon [in Mapcanon]
MapDomRestrTo_To_comm_c [in Mapc]
MapDomRestrTo_By_comm_c [in Mapc]
MapDomRestrTo_By_c [in Mapc]
MapDomRestrTo_Dom_c [in Mapc]
MapDomRestrTo_idempotent_c [in Mapc]
MapDomRestrTo_assoc_c [in Mapc]
MapDomRestr_disjoint [in Mapsubset]
MapDom_Dom [in Fset]
MapDom_semantics_4 [in Fset]
MapDom_semantics_3 [in Fset]
MapDom_semantics_2 [in Fset]
MapDom_semantics_1 [in Fset]
MapDom_Split_3 [in Mapaxioms]
MapDom_Split_2 [in Mapaxioms]
MapDom_Split_1 [in Mapaxioms]
MapDom_canon [in Mapcanon]
MapDom_Split_3_c [in Mapc]
MapDom_Split_2_c [in Mapc]
MapDom_Split_1_c [in Mapc]
MapEmptyp_complete [in Map]
MapEmptyp_correct [in Map]
MapFold_orb [in Mapfold]
MapFold_orb_1 [in Mapfold]
MapFold_distr_l [in Mapfold]
MapFold_distr_r [in Mapfold]
MapFold_distr_r_1 [in Mapfold]
MapFold_Merge_disjoint [in Mapfold]
MapFold_Merge_disjoint_1 [in Mapfold]
MapFold_Put_behind_disjoint [in Mapfold]
MapFold_Put_behind_disjoint_2 [in Mapfold]
MapFold_Put_disjoint [in Mapfold]
MapFold_Put_disjoint_2 [in Mapfold]
MapFold_Put_disjoint_1 [in Mapfold]
MapFold_ext_f [in Mapfold]
MapFold_ext_f_1 [in Mapfold]
MapFold_ext [in Mapfold]
MapFold_as_fold [in Mapiter]
MapFold_as_fold_1 [in Mapiter]
MapFold_state_stateless [in Mapiter]
MapFold_state_stateless_1 [in Mapiter]
MapFold_M1 [in Mapiter]
MapFold_empty [in Mapiter]
MapFold_canon [in Mapcanon]
MapFold_canon_1 [in Mapcanon]
MapFold1_ext [in Mapfold]
MapFold1_as_Fold [in Mapfold]
MapFold1_as_Fold_1 [in Mapfold]
MapGet_M2_both_None [in Map]
MapGet_M2_bit_0_2 [in Map]
MapGet_if_same [in Map]
MapGet_if_commute [in Map]
MapGet_M2_bit_0 [in Map]
MapGet_M2_bit_0_if [in Map]
MapGet_M2_bit_0_1 [in Map]
MapGet_M2_bit_0_0 [in Map]
MapMerge_disjoint [in Mapsubset]
MapMerge_semantics [in Map]
MapMerge_Card_lb_r [in Mapcard]
MapMerge_Card_lb_l [in Mapcard]
MapMerge_Card_disjoint [in Mapcard]
MapMerge_Card_ub [in Mapcard]
MapMerge_disjoint_Card [in Mapcard]
MapMerge_Restr_Card [in Mapcard]
MapMerge_DomRestrBy [in Mapaxioms]
MapMerge_DomRestrTo [in Mapaxioms]
MapMerge_RestrTo_l [in Mapaxioms]
MapMerge_ext_r [in Mapaxioms]
MapMerge_ext_l [in Mapaxioms]
MapMerge_ext [in Mapaxioms]
MapMerge_idempotent [in Mapaxioms]
MapMerge_assoc [in Mapaxioms]
MapMerge_empty_r [in Mapaxioms]
MapMerge_empty_l [in Mapaxioms]
MapMerge_m_empty [in Mapaxioms]
MapMerge_m_empty_1 [in Mapaxioms]
MapMerge_empty_m [in Mapaxioms]
MapMerge_empty_m_1 [in Mapaxioms]
MapMerge_canon [in Mapcanon]
MapMerge_DomRestrBy_c [in Mapc]
MapMerge_DomRestrTo_c [in Mapc]
MapMerge_RestrTo_l_c [in Mapc]
MapMerge_idempotent_c [in Mapc]
MapMerge_assoc_c [in Mapc]
MapMerge_empty_m_c [in Mapc]
MapPut_behind_semantics [in Map]
MapPut_behind_new [in Map]
MapPut_behind_as_before [in Map]
MapPut_behind_as_before_1 [in Map]
MapPut_behind_semantics_3_1 [in Map]
MapPut_semantics [in Map]
MapPut_semantics_3_1 [in Map]
MapPut_semantics_2 [in Map]
MapPut_semantics_2_2 [in Map]
MapPut_semantics_2_1 [in Map]
MapPut_semantics_1 [in Map]
MapPut_behind_ext [in Mapaxioms]
MapPut_behind_as_Merge [in Mapaxioms]
MapPut_ext [in Mapaxioms]
MapPut_as_Merge [in Mapaxioms]
MapPut_behind_canon [in Mapcanon]
MapPut_canon [in Mapcanon]
MapPut_behind_as_Merge_c [in Mapc]
MapPut_as_Merge_c [in Mapc]
MapPut_in [in SetChecker]
MapPut1_semantics' [in Map]
MapPut1_semantics [in Map]
MapPut1_semantics_3 [in Map]
MapPut1_semantics_2 [in Map]
MapPut1_semantics_1 [in Map]
MapPut1_canon [in Mapcanon]
MapPut1_in [in SetChecker]
MapRemove_semantics [in Map]
MapRemove_ext [in Mapaxioms]
MapRemove_as_RestrBy [in Mapaxioms]
MapRemove_canon [in Mapcanon]
MapRemove_as_RestrBy_c [in Mapc]
MapRemove_in [in SetChecker]
MapSingleton_semantics [in Map]
MapSplit_Card [in Mapcard]
MapSubset_Disjoint_r [in Mapsubset]
MapSubset_Disjoint_l [in Mapsubset]
MapSubset_Disjoint [in Mapsubset]
MapSubset_DomRestrBy_mono [in Mapsubset]
MapSubset_DomRestrBy_l [in Mapsubset]
MapSubset_DomRestrTo_mono [in Mapsubset]
MapSubset_ext [in Mapsubset]
MapSubset_DomRestrTo_r [in Mapsubset]
MapSubset_DomRestrTo_l [in Mapsubset]
MapSubset_Merge_mono [in Mapsubset]
MapSubset_Merge_r [in Mapsubset]
MapSubset_Merge_l [in Mapsubset]
MapSubset_Remove_mono [in Mapsubset]
MapSubset_Remove [in Mapsubset]
MapSubset_Put_behind_mono [in Mapsubset]
MapSubset_Put_behind [in Mapsubset]
MapSubset_Put_mono [in Mapsubset]
MapSubset_Put [in Mapsubset]
MapSubset_1_Dom [in Mapsubset]
MapSubset_Dom_2 [in Mapsubset]
MapSubset_Dom_1 [in Mapsubset]
MapSubset_trans [in Mapsubset]
MapSubset_antisym [in Mapsubset]
MapSubset_refl [in Mapsubset]
MapSubset_2_imp [in Mapsubset]
MapSubset_imp_2 [in Mapsubset]
MapSubset_1_imp [in Mapsubset]
MapSubset_imp_1 [in Mapsubset]
MapSubset_card_eq [in Mapcard]
MapSubset_Card_le [in Mapcard]
MapSubset_card_eq_1 [in Mapcard]
MapSubset_c_2 [in Mapcanon]
MapSubset_c_1 [in Mapcanon]
MapSubset_antisym_c [in Mapc]
MapSweep_semantics_4 [in Mapiter]
MapSweep_semantics_4_1 [in Mapiter]
MapSweep_semantics_3 [in Mapiter]
MapSweep_semantics_3_1 [in Mapiter]
MapSweep_semantics_2 [in Mapiter]
MapSweep_semantics_2_2 [in Mapiter]
MapSweep_semantics_2_1 [in Mapiter]
MapSweep_semantics_1 [in Mapiter]
MapSweep_semantics_1_1 [in Mapiter]
Map_disjoint_M0 [in Mapsubset]
Map_M0_disjoint [in Mapsubset]
map_dom_empty_2 [in Mapsubset]
map_dom_empty_1 [in Mapsubset]
map_in [in Basic]
Map_of_alist_of_Map [in Mapiter]
Map_of_alist_semantics [in Mapiter]
Map_of_alist_canon [in Mapcanon]
Map_of_alist_of_Map_c [in Mapc]
Map2_semantics_3_eq [in Map]
Map2_semantics_3 [in Map]
Map2_semantics_2_eq [in Map]
Map2_semantics_2 [in Map]
Map2_semantics_1_eq [in Map]
Map2_semantics_1 [in Map]
M1_semantics_2 [in Map]
M1_semantics_1 [in Map]
M2_eqmap_2 [in Mapcanon]
M2_eqmap_1 [in Mapcanon]
N
nat_compare_trans [in Basic]nat_compare_sym_gt [in Basic]
nat_compare_sym_lt [in Basic]
nat_compare_eq_rev [in Basic]
Ndouble_plus_one_monotonic [in Lsort]
Ndouble_monotonic [in Lsort]
neg_in [in Generate]
newMap_semantics [in Map]
no_occurrence_dec [in Generate]
no_occurrence_add [in Generate]
no_occurrence_char [in Generate]
no_pythagorean [in Generate]
O
one_occurrence_dec [in Generate]one_occurrence_find [in Generate]
option_sum [in Map]
outer_cycle_okl [in Generate]
P
pair_sp [in Mapiter]pos_in [in Generate]
propagate_sound [in SetChecker]
propagate_true [in SetChecker]
propagate_entails [in SetChecker]
propagate_empty [in SetChecker]
propagate_singleton [in SetChecker]
Pythagorean_Theorem'' [in Generate]
Pythagorean_Theorem' [in Generate]
Pythagorean_Theorem [in Generate]
pythagorean_dec [in Generate]
pythagorean_lim_equiv [in Generate]
pythagorean_equiv [in Generate]
pythagorean_neq_1 [in Generate]
pythagorean_neq_2 [in Generate]
pythagorean_comm [in Generate]
pyth_lim_gen_neg [in Generate]
pyth_lim_gen [in Generate]
R
refute_correct [in SetChecker]refute_work_correct [in SetChecker]
remove_all_orig [in Basic]
remove_neq [in Basic]
remove_not_In [in Basic]
remove_in [in Generate]
remove_keep [in Generate]
remove_no_occurrence [in Generate]
S
satisfies_Cubed_CNF [in CubeAndConquer]satisfies_remove [in CNF]
satisfies_for_all [in CNF]
satisfies_to_T_satisfies' [in SetChecker]
satisfies_to_T_satisfies [in SetChecker]
SC_in_add [in SetChecker]
SC_satisfies_exists [in SetChecker]
SC_to_C_In_2 [in SetChecker]
SC_to_C_In_1 [in SetChecker]
SetClause_eq_nil_cons [in SetChecker]
SetClause_eq_dec [in SetChecker]
SetClause_to_Clause_inv [in SetChecker]
simplification_ok [in Generate]
symbreak_ok [in Generate]
T
target_formula_in [in Generate]TCNF_In [in SetChecker]
TCNF_In' [in SetChecker]
TCNF_eq_dec [in SetChecker]
true_C_true [in CNF]
T_satisfies_to_satisfies' [in SetChecker]
T_satisfies_to_satisfies [in SetChecker]
U
unsat_subset [in CNF]unsat_remove [in CNF]
V
val_gives_colorful [in Generate]Z
Zabs_diff_le_1 [in Basic]Zabs_le_1 [in Basic]
Constructor Index
D
D [in SetChecker]L
lcons [in SetChecker]lnil [in SetChecker]
M
M0 [in Map]M0_canon [in Mapcanon]
M1 [in Map]
M1_canon [in Mapcanon]
M2 [in Map]
M2_canon [in Mapcanon]
N
neg [in CNF]node [in BinaryTrees]
nought [in BinaryTrees]
O
O [in SetChecker]P
pos [in CNF]R
R [in SetChecker]Axiom Index
T
TheBreak [in Generate]TheN [in Generate]
The_List [in Generate]
Inductive Index
A
Action [in SetChecker]B
BinaryTree [in BinaryTrees]L
lazy_list [in SetChecker]Literal [in CNF]
M
Map [in Map]mapcanon [in Mapcanon]
Section Index
A
AdAlloc [in Adalloc]C
Clauses [in CNF]Clauses.Compare [in CNF]
CNF [in CNF]
Compare [in Basic]
D
DMergeDef [in Mapfold]Dom [in Fset]
F
Formula [in Generate]FSetCanon [in Mapcanon]
FSetDefs [in Fset]
FSubsetOrder [in Mapsubset]
I
ICNF [in SetChecker]InDom [in Fset]
L
Lists_of_Clauses [in Generate]Lists_and_Stuff [in Generate]
Literal [in CNF]
Literal.Compare [in CNF]
LSort [in Lsort]
M
MapAxioms [in Mapaxioms]MapC [in Mapc]
MapCanon [in Mapcanon]
MapCard [in Mapcard]
MapCard2 [in Mapcard]
MapCard3 [in Mapcard]
MapDefs [in Map]
MapDisjointDef [in Mapsubset]
MapDisjointExtra [in Mapsubset]
MapFoldCanon [in Mapcanon]
MapFoldDistr [in Mapfold]
MapFoldDistrL [in Mapfold]
MapFoldExists [in Mapfold]
MapFoldResults [in Mapfold]
MapIter [in Mapiter]
MapIter.MapFoldDef [in Mapiter]
MapIter.MapSweepDef [in Mapiter]
MapLists [in Maplists]
MapLists.ListOfDomDef [in Maplists]
MapSubsetDef [in Mapsubset]
MapSubsetExtra [in Mapsubset]
MapSubsetOrder [in Mapsubset]
N
NatCompare [in Basic]P
Propagation [in SetChecker]Pythagoras [in Generate]
R
Refutation [in SetChecker]RemoveAll [in Basic]
S
SetClauses [in SetChecker]Simplification [in Generate]
SymmetryBreak [in Generate]
T
TreeCNF [in SetChecker]Trees [in BinaryTrees]
Trees.Balancing [in BinaryTrees]
Trees.Map [in BinaryTrees]
Z
Z_stuff [in Basic]Definition Index
A
aapp [in Mapiter]acons [in Mapiter]
ad [in Map]
add_ICNF [in SetChecker]
ad_inj [in Mapiter]
ad_alloc_opt [in Adalloc]
ad_list_of_dom [in Maplists]
ad_list_stutters [in Maplists]
ad_in_list [in Maplists]
ad_monotonic [in Lsort]
alist [in Mapiter]
alist_semantics [in Mapiter]
alist_of_Map [in Mapiter]
alist_sorted_2 [in Lsort]
alist_sorted_1 [in Lsort]
alist_nth_ad [in Lsort]
alist_sorted [in Lsort]
anil [in Mapiter]
Answer [in SetChecker]
B
balanced [in BinaryTrees]BPT_formula [in Generate]
BPT_list [in Generate]
BT_map [in BinaryTrees]
BT_add_all [in BinaryTrees]
BT_size [in BinaryTrees]
BT_diff [in BinaryTrees]
BT_remove [in BinaryTrees]
BT_split [in BinaryTrees]
BT_add [in BinaryTrees]
BT_balance [in BinaryTrees]
BT_rot_RR [in BinaryTrees]
BT_rot_LL [in BinaryTrees]
BT_rot_R [in BinaryTrees]
BT_rot_L [in BinaryTrees]
BT_wf [in BinaryTrees]
BT_In [in BinaryTrees]
C
change_val [in Generate]Clause [in CNF]
Clause_compare [in CNF]
Clause_to_SetClause [in SetChecker]
CNF [in CNF]
CNF_equiv [in CNF]
colorful [in Generate]
coloring [in Generate]
Cube [in CubeAndConquer]
Cubed_CNF [in CubeAndConquer]
C_unsat [in CNF]
C_satisfies [in CNF]
D
del_ICNF [in SetChecker]DMerge [in Mapfold]
E
Elems [in Maplists]empty_ICNF [in SetChecker]
entails [in CNF]
eqm [in Map]
eqmap [in Mapaxioms]
F
force [in SetChecker]fromVal [in SetChecker]
FSet [in Fset]
FSetDelta [in Fset]
FSetDiff [in Fset]
FSetInter [in Fset]
FSetUnion [in Fset]
G
get_ICNF [in SetChecker]H
height [in BinaryTrees]I
ICNF [in SetChecker]ICNF_to_TCNF [in SetChecker]
inner_cycle [in Generate]
in_FSet [in Fset]
in_dom [in Fset]
L
LazyT [in SetChecker]list_subset [in Basic]
list_to_BTree [in BinaryTrees]
Literal_compare [in CNF]
L_satisfies [in CNF]
M
makeM2 [in Map]make_TCNF [in SetChecker]
MapCanonicalize [in Mapcanon]
MapCard [in Map]
MapCollect [in Mapiter]
MapCollect1 [in Mapiter]
MapDelta [in Map]
MapDisjoint [in Mapsubset]
MapDisjoint_2 [in Mapsubset]
MapDisjoint_1 [in Mapsubset]
MapDom [in Fset]
MapDomRestrBy [in Fset]
MapDomRestrTo [in Fset]
MapEmptyp [in Map]
MapFold [in Mapiter]
MapFold_state [in Mapiter]
MapFold1 [in Mapiter]
MapFold1_state [in Mapiter]
MapGet [in Map]
MapMerge [in Map]
MapPut [in Map]
MapPut_behind [in Map]
MapPut1 [in Map]
MapRemove [in Map]
MapSingleton [in Map]
MapSubset [in Mapsubset]
MapSubset_2 [in Mapsubset]
MapSubset_1 [in Mapsubset]
MapSweep [in Mapiter]
MapSweep1 [in Mapiter]
MapSweep2 [in Mapiter]
Map_of_alist [in Mapiter]
N
negate [in CNF]negF [in Generate]
neg_cube [in CubeAndConquer]
newMap [in Map]
noCube [in CubeAndConquer]
no_occurrence [in Generate]
O
ok_list [in Generate]one_occurrence [in Generate]
Oracle [in SetChecker]
Oracle_size [in SetChecker]
outer_cycle [in Generate]
P
posF [in Generate]propagate [in SetChecker]
pythagorean [in Generate]
pythagorean_neg [in Generate]
pythagorean_pos [in Generate]
pyth_lim_neg [in Generate]
pyth_lim_pos [in Generate]
R
reduces [in Generate]refute [in SetChecker]
remove_all [in Basic]
remove_number [in Generate]
S
satisfies [in CNF]SC_wf [in SetChecker]
SC_diff [in SetChecker]
SC_in [in SetChecker]
SC_add [in SetChecker]
SetClause [in SetChecker]
SetClause_to_Clause [in SetChecker]
simplified_BPT_formula [in Generate]
simplify [in Generate]
T
target_formula [in Generate]target_list [in Generate]
TCNF_to_CNF [in SetChecker]
TCNF_add [in SetChecker]
TCNF_join [in SetChecker]
TCNF_wf [in SetChecker]
TCNF_remove [in SetChecker]
TCNF_in [in SetChecker]
The_Asymmetric_CNF [in Generate]
The_Simple_CNF [in Generate]
The_CNF [in Generate]
TreeCNF [in SetChecker]
true_C [in CNF]
true_SC [in SetChecker]
T_satisfies [in SetChecker]
U
unsat [in CNF]V
Valuation [in CNF]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (980 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (93 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (634 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (53 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (154 entries) |
This page has been generated by coqdoc