| 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 | (877 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 | (6 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 | (35 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 | (479 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 | (157 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 | (16 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 | (73 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 | (4 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 | (107 entries) |
Global Index
A
above_equiv_del_above [lemma, in IPC.AvlTrees]above_above_avl [lemma, in IPC.AvlTrees]
above_avl_trans [lemma, in IPC.AvlTrees]
Above_Avl_Node [constructor, in IPC.AvlTrees]
Above_Avl_Nil [constructor, in IPC.AvlTrees]
above_trans [lemma, in IPC.AvlTrees]
Above_Node [constructor, in IPC.AvlTrees]
Above_Nil [constructor, in IPC.AvlTrees]
Abs [constructor, in IPC.Derivations]
AImp [constructor, in IPC.Normal_Forms]
AI_Nil [definition, in IPC.In_NGamma]
all_ref_rev_app_nil [lemma, in IPC.Cons_Counter_Model]
AndF [constructor, in IPC.Forms]
AndFElimL [constructor, in IPC.Derivations]
AndFElimR [constructor, in IPC.Derivations]
AndFIntro [constructor, in IPC.Derivations]
ANil [definition, in IPC.Kripke_Trees]
App [constructor, in IPC.Derivations]
Atms [definition, in IPC.Kripke_Trees]
Atom [constructor, in IPC.Forms]
atomic_imps [definition, in IPC.In_NGamma]
atoms [definition, in IPC.Kripke_Trees]
AVL [inductive, in IPC.AvlTrees]
AvlTrees [library]
AVL_NIL [definition, in IPC.AvlTrees]
AVL_intro [constructor, in IPC.AvlTrees]
Avl_Ins_Spec_Intro [constructor, in IPC.AvlTrees]
avl_ins_spec [inductive, in IPC.AvlTrees]
avl_ins_eq [lemma, in IPC.AvlTrees]
avl_height_avl_height [lemma, in IPC.AvlTrees]
Avl_Node [constructor, in IPC.AvlTrees]
Avl_Nil [constructor, in IPC.AvlTrees]
avl_tree [inductive, in IPC.AvlTrees]
avl_trees.B [variable, in IPC.AvlTrees]
avl_trees [section, in IPC.AvlTrees]
a_goal_disj [definition, in IPC.Disjunct]
a_ai_disj [definition, in IPC.Disjunct]
B
bal [inductive, in IPC.AvlTrees]Balanced [constructor, in IPC.AvlTrees]
Balanced_shrunk_left_balanced_shift [lemma, in IPC.AvlTrees]
balance_shrunk_right [lemma, in IPC.AvlTrees]
Balance_Shrunk_Right_Spec_Intro [constructor, in IPC.AvlTrees]
balance_shrunk_left [lemma, in IPC.AvlTrees]
Balance_Shrunk_Left_Spec_Intro [constructor, in IPC.AvlTrees]
balance_right [lemma, in IPC.AvlTrees]
Balance_Grow_Right_Spec_Intro [constructor, in IPC.AvlTrees]
balance_left [lemma, in IPC.AvlTrees]
Balance_Grow_Left_Spec_Intro [constructor, in IPC.AvlTrees]
bal_shrunk_right_spec [inductive, in IPC.AvlTrees]
bal_shrunk_left_spec [inductive, in IPC.AvlTrees]
bal_grow_right_spec [inductive, in IPC.AvlTrees]
bal_grow_left_spec [inductive, in IPC.AvlTrees]
below_vimp_tail [lemma, in IPC.Forms]
below_vimp_split [lemma, in IPC.Forms]
below_vimp_head [lemma, in IPC.Forms]
below_vimp2 [lemma, in IPC.Forms]
below_vimp [lemma, in IPC.Forms]
below_list_weak2 [lemma, in IPC.Forms]
below_list_weak [lemma, in IPC.Forms]
below_cons_list [lemma, in IPC.Forms]
below_cons_list_tail [lemma, in IPC.Forms]
below_cons_list_head [lemma, in IPC.Forms]
below_list_less_below_list [lemma, in IPC.Forms]
below_form_less_below_form [lemma, in IPC.Forms]
below_list [definition, in IPC.Forms]
below_form [definition, in IPC.Forms]
below_equiv_del_below [lemma, in IPC.AvlTrees]
below_equiv_below [lemma, in IPC.AvlTrees]
below_below_avl [lemma, in IPC.AvlTrees]
below_avl_trans [lemma, in IPC.AvlTrees]
Below_Avl_Node [constructor, in IPC.AvlTrees]
Below_Avl_Nil [constructor, in IPC.AvlTrees]
below_trans [lemma, in IPC.AvlTrees]
Below_Node [constructor, in IPC.AvlTrees]
Below_Nil [constructor, in IPC.AvlTrees]
ByAbsurdity [constructor, in IPC.Derivations]
ByAssumption [constructor, in IPC.Derivations]
C
Cas [constructor, in IPC.Derivations]cons_counter_model [lemma, in IPC.Cons_Counter_Model]
cons_counter_model_intro [constructor, in IPC.Cons_Counter_Model]
Cons_Counter_Model_Spec [inductive, in IPC.Cons_Counter_Model]
cons_counter_model_mon [lemma, in IPC.Cons_Counter_Model]
cons_counter_model_suc [lemma, in IPC.Cons_Counter_Model]
Cons_Forest [constructor, in IPC.Trees]
Cons_Counter_Model [library]
contradiction_atoms [lemma, in IPC.NRules]
count_undecs_rev_app [lemma, in IPC.Lt_Ks]
count_undecs [definition, in IPC.Lt_Ks]
D
Decorated [constructor, in IPC.In_NGamma]decorated_nested_imp2form [definition, in IPC.Rev_App]
decorated_nested_imp2k [definition, in IPC.Rev_App]
decorated_nested_imp2nimp [definition, in IPC.Rev_App]
decorated_nested_imps [definition, in IPC.Rev_App]
decorated_nested_imp [definition, in IPC.Rev_App]
deco_sound_in_forest_forces [lemma, in IPC.Cons_Counter_Model]
deco_sound_filter_deco [lemma, in IPC.NDeco_Sound]
deco_sound_inf [lemma, in IPC.NDeco_Sound]
deco_sound_shift_work_ai_strength [lemma, in IPC.NDeco_Sound]
deco_sound_shift_work_ai_weak [lemma, in IPC.NDeco_Sound]
deco_sound_cons_work_strength [lemma, in IPC.NDeco_Sound]
deco_sound_cons_work_weak2 [lemma, in IPC.NDeco_Sound]
deco_sound_cons_work_weak [lemma, in IPC.NDeco_Sound]
deco_sound_le [lemma, in IPC.NDeco_Sound]
deco_sound_shift_work_nirni [lemma, in IPC.NDeco_Sound]
deco_sound_shift_work_ninni [lemma, in IPC.NDeco_Sound]
deco_sound_shift_ni_x_ni_work [lemma, in IPC.NDeco_Sound]
deco_sound_shift_work_a [lemma, in IPC.NDeco_Sound]
deco_sound_shift_a_work [lemma, in IPC.NDeco_Sound]
deco_sound_shift_work_ai [lemma, in IPC.NDeco_Sound]
deco_sound_shift_ai_work_old [lemma, in IPC.NDeco_Sound]
deco_sound_shift_ai_work_new [lemma, in IPC.NDeco_Sound]
deco_sound_shift_work_ni0 [lemma, in IPC.NDeco_Sound]
deco_sound_shift_ni_work [lemma, in IPC.NDeco_Sound]
deco_sound_shift_work_ds [lemma, in IPC.NDeco_Sound]
deco_sound_shift_ds_work [lemma, in IPC.NDeco_Sound]
deco_sound_cons_ni_tail [lemma, in IPC.NDeco_Sound]
deco_sound_cons_ds_tail [lemma, in IPC.NDeco_Sound]
deco_sound_cons_work_tail [lemma, in IPC.NDeco_Sound]
deco_sound [definition, in IPC.NDeco_Sound]
DELETE_AVL [lemma, in IPC.AvlTrees]
DELETE_Spec [definition, in IPC.AvlTrees]
delete_avl [lemma, in IPC.AvlTrees]
Delete_Spec_Intro [constructor, in IPC.AvlTrees]
delete_spec [inductive, in IPC.AvlTrees]
delete_max [lemma, in IPC.AvlTrees]
delete_max_spec [inductive, in IPC.AvlTrees]
Del_Max_Spec_Intro [constructor, in IPC.AvlTrees]
Derivable [inductive, in IPC.Derivable_Def_dont_compute_derivations]
Derivable [inductive, in IPC.Derivable_Def_compute_derivations]
derivable [constructor, in IPC.Search]
derivable [constructor, in IPC.Rules]
Derivable_Intro [constructor, in IPC.Derivable_Def_dont_compute_derivations]
Derivable_Intro [constructor, in IPC.Derivable_Def_compute_derivations]
derivable_vimp0 [lemma, in IPC.Derivable_Tools]
derivable_vimp2 [lemma, in IPC.Derivable_Tools]
derivable_vimp [lemma, in IPC.Derivable_Tools]
derivable_a_context_b__derivable_a_imp_b [lemma, in IPC.Derivable_Tools]
derivable_a_a_imp_b__derivable_b [lemma, in IPC.Derivable_Tools]
derivable_b__derivable_a_imp_b [lemma, in IPC.Derivable_Tools]
derivable_falsum_imp_b_imp_c__derivable_c [lemma, in IPC.Derivable_Tools]
derivable_a0_or_a1_imp_b__derivable_a1_imp_b [lemma, in IPC.Derivable_Tools]
derivable_a0_or_a1_imp_b__derivable_a0_imp_b [lemma, in IPC.Derivable_Tools]
derivable_a0_and_a1_imp_b__derivable_a0_imp_a1_imp_b [lemma, in IPC.Derivable_Tools]
derivable_a_imp_b_or_falsum__derivable_a_imp_b [lemma, in IPC.Derivable_Tools]
derivable_a_imp_falsum_or_b__derivable_a_imp_b [lemma, in IPC.Derivable_Tools]
derivable_a_or_falsum__derivable_a [lemma, in IPC.Derivable_Tools]
derivable_falsum_or_a__derivable_a [lemma, in IPC.Derivable_Tools]
derivable_a_and_b__derivable_b [lemma, in IPC.Derivable_Tools]
derivable_a_and_b__derivable_a [lemma, in IPC.Derivable_Tools]
derivable_a_imp_a [lemma, in IPC.Derivable_Tools]
derivable_cut_merge [lemma, in IPC.Derivable_Tools]
derivable_cut [lemma, in IPC.Derivable_Tools]
derivable_cut_aux [lemma, in IPC.Derivable_Tools]
derivable_weak_list [lemma, in IPC.Derivable_Tools]
derivable_weak [lemma, in IPC.Derivable_Tools]
derivable_subst [lemma, in IPC.Derivable_Tools]
derivable_eq [lemma, in IPC.Derivable_Tools]
Derivable_Def [library]
Derivable_Tools [library]
Derivable_Def_compute_derivations [library]
Derivable_Def_dont_compute_derivations [library]
Derivable2 [inductive, in IPC.Derivable_Def_dont_compute_derivations]
Derivable2 [inductive, in IPC.Derivable_Def_compute_derivations]
Derivable2_Intro [constructor, in IPC.Derivable_Def_dont_compute_derivations]
Derivable2_Intro [constructor, in IPC.Derivable_Def_compute_derivations]
Derivations [library]
derives [inductive, in IPC.Derivations]
derives_rec [lemma, in IPC.Derivations]
disj [definition, in IPC.In_NGamma]
disjs [definition, in IPC.In_NGamma]
disjs_insert_a [lemma, in IPC.Disjunct]
disjs_delete_ai [lemma, in IPC.Disjunct]
disjs_insert_ai [lemma, in IPC.Disjunct]
disjs2forms [definition, in IPC.In_NGamma]
disjs2nforms [definition, in IPC.In_NGamma]
Disjunct [library]
disj2form [definition, in IPC.In_NGamma]
disj2nform [definition, in IPC.In_NGamma]
DNil [definition, in IPC.In_NGamma]
DNI_NIL [definition, in IPC.Rev_App]
E
Efq [constructor, in IPC.Derivations]Equal [axiom, in IPC.ML_Int]
equal_dec_refl [lemma, in IPC.ML_Int]
equal_eq [axiom, in IPC.ML_Int]
equal_refl [axiom, in IPC.ML_Int]
equal_trans [axiom, in IPC.ML_Int]
equal_sym [axiom, in IPC.ML_Int]
equal_less_less [axiom, in IPC.ML_Int]
equal_dec [axiom, in IPC.ML_Int]
equiv [inductive, in IPC.AvlTrees]
EQUIV_DEL [definition, in IPC.AvlTrees]
EQUIV_INS [definition, in IPC.AvlTrees]
equiv_del_trans_right [lemma, in IPC.AvlTrees]
equiv_del_trans_left [lemma, in IPC.AvlTrees]
equiv_del_equal [lemma, in IPC.AvlTrees]
equiv_del_right_semi_leave [lemma, in IPC.AvlTrees]
equiv_del_nil [lemma, in IPC.AvlTrees]
equiv_del_right [lemma, in IPC.AvlTrees]
equiv_del_above [lemma, in IPC.AvlTrees]
equiv_del_semi_leave [lemma, in IPC.AvlTrees]
equiv_del_equiv_equiv_del [lemma, in IPC.AvlTrees]
equiv_del_intro [constructor, in IPC.AvlTrees]
equiv_del [inductive, in IPC.AvlTrees]
equiv_ins_right [lemma, in IPC.AvlTrees]
equiv_ins_left [lemma, in IPC.AvlTrees]
equiv_ins_eq [lemma, in IPC.AvlTrees]
equiv_ins_nil [lemma, in IPC.AvlTrees]
equiv_ins_above [lemma, in IPC.AvlTrees]
equiv_ins_below [lemma, in IPC.AvlTrees]
equiv_ins_equiv_equiv_ins [lemma, in IPC.AvlTrees]
equiv_ins_intro [constructor, in IPC.AvlTrees]
equiv_ins [inductive, in IPC.AvlTrees]
equiv_refl [lemma, in IPC.AvlTrees]
equiv_sym [lemma, in IPC.AvlTrees]
equiv_intro [constructor, in IPC.AvlTrees]
eqv_nimps_eq [lemma, in IPC.Le_Ks]
eqv_ni_rec [lemma, in IPC.Le_Ks]
eqv_sym [lemma, in IPC.Le_Ks]
eqv_ni_trans [lemma, in IPC.Le_Ks]
Eqv_NI_Cons_ND [constructor, in IPC.Le_Ks]
Eqv_NI_Cons_DD [constructor, in IPC.Le_Ks]
Eqv_NI_Cons_DN [constructor, in IPC.Le_Ks]
Eqv_NI_Cons_NN [constructor, in IPC.Le_Ks]
Eqv_NI_Nil [constructor, in IPC.Le_Ks]
eqv_ni [inductive, in IPC.Le_Ks]
eq_lt_trans [lemma, in IPC.My_Arith]
Extr [library]
F
fail [lemma, in IPC.NRules]Falsum [constructor, in IPC.Forms]
filter_deco [lemma, in IPC.Le_Ks]
Filter_Deco_Spec_Intro [constructor, in IPC.Le_Ks]
filter_deco_spec [inductive, in IPC.Le_Ks]
flist [definition, in IPC.Forms]
fnil [definition, in IPC.Forms]
fold_right_perm [lemma, in IPC.My_Arith]
forces [definition, in IPC.Kripke_Trees]
forces_ngamma_shift_work_ai_strength [lemma, in IPC.Forces_NGamma]
forces_ngamma_shift_work_ai_weak [lemma, in IPC.Forces_NGamma]
forces_ngamma_cons_work_weak2 [lemma, in IPC.Forces_NGamma]
forces_ngamma_cons_work_weak [lemma, in IPC.Forces_NGamma]
forces_ngamma_shift_ni_x_ni_work [lemma, in IPC.Forces_NGamma]
forces_ngamma_shift_work_ni_x_ni [lemma, in IPC.Forces_NGamma]
forces_ngamma_shift_work_a [lemma, in IPC.Forces_NGamma]
forces_ngamma_shift_a_work [lemma, in IPC.Forces_NGamma]
forces_ngamma_shift_work_ai [lemma, in IPC.Forces_NGamma]
forces_ngamma_shift_ai_work_old [lemma, in IPC.Forces_NGamma]
forces_ngamma_shift_ai_work_new [lemma, in IPC.Forces_NGamma]
forces_ngamma_shift_work_ni [lemma, in IPC.Forces_NGamma]
forces_ngamma_shift_ni_work [lemma, in IPC.Forces_NGamma]
forces_ngamma_shift_work_ds [lemma, in IPC.Forces_NGamma]
forces_ngamma_shift_ds_work [lemma, in IPC.Forces_NGamma]
forces_ngamma_eqv [lemma, in IPC.Forces_NGamma]
forces_ngamma_del_ai_rev [lemma, in IPC.Forces_NGamma]
forces_ngamma_del_ai [lemma, in IPC.Forces_NGamma]
forces_ngamma_cons_ni_tail [lemma, in IPC.Forces_NGamma]
forces_ngamma_cons_ds_tail [lemma, in IPC.Forces_NGamma]
forces_ngamma_app_work_tail [lemma, in IPC.Forces_NGamma]
forces_ngamma_app_work [lemma, in IPC.Forces_NGamma]
forces_ngamma_cons_work_tail [lemma, in IPC.Forces_NGamma]
forces_ngamma_cons_work [lemma, in IPC.Forces_NGamma]
forces_ngamma [definition, in IPC.Forces_NGamma]
forces_gamma_cons_gamma_weak2 [lemma, in IPC.Forces_Gamma]
forces_gamma_cons_gamma_weak [lemma, in IPC.Forces_Gamma]
forces_gamma_shift_work_gamma [lemma, in IPC.Forces_Gamma]
forces_gamma_shift_gamma_work [lemma, in IPC.Forces_Gamma]
forces_gamma_cons_gamma_head [lemma, in IPC.Forces_Gamma]
forces_gamma_cons_gamma_tail [lemma, in IPC.Forces_Gamma]
forces_gamma_cons_gamma [lemma, in IPC.Forces_Gamma]
forces_gamma [definition, in IPC.Forces_Gamma]
forces_a_imp_b_imp_c__forces_a_imp_falsum_imp_c_t2 [lemma, in IPC.Kripke_Trees]
forces_vimp0 [lemma, in IPC.Kripke_Trees]
forces_vimp2 [lemma, in IPC.Kripke_Trees]
forces_vimp [lemma, in IPC.Kripke_Trees]
forces_a_imp_b_imp_c__forces_a_imp_falsum_imp_c [lemma, in IPC.Kripke_Trees]
forces_a_imp_falsum_imp_b1_t [lemma, in IPC.Kripke_Trees]
forces_a_imp_b__forces_a_imp_b_or_falsum [lemma, in IPC.Kripke_Trees]
forces_a_imp_b__forces_a_imp_falsum_or_b [lemma, in IPC.Kripke_Trees]
forces_a_imp_b0_a_imp_b1__forces_a_imp_a0_and_a1 [lemma, in IPC.Kripke_Trees]
forces_a_a_imp_b__forces_b_t [lemma, in IPC.Kripke_Trees]
forces_a1_imp_b__forces_a0_and_a1_imp_b_t [lemma, in IPC.Kripke_Trees]
forces_a0_imp_b__forces_a0_and_a1_imp_b_t [lemma, in IPC.Kripke_Trees]
forces_a0_imp_a1_imp_b__forces_a1_imp_b_t [lemma, in IPC.Kripke_Trees]
forces_a1_imp_b__forces_a0_imp_a1_imp_b_t [lemma, in IPC.Kripke_Trees]
forces_a0_imp_c_and_a1_imp_c_and_c_imp_b__forces_a0_or_a1_imp_b_t [lemma, in IPC.Kripke_Trees]
forces_a0_imp_a1_imp_b__forces_a0_and_a1_imp_b_t [lemma, in IPC.Kripke_Trees]
forces_b__forces_a_imp_b_t [lemma, in IPC.Kripke_Trees]
forces_t_mon [lemma, in IPC.Kripke_Trees]
forces_t_imp [lemma, in IPC.Kripke_Trees]
forces_t [definition, in IPC.Kripke_Trees]
forces_t2_is_local [lemma, in IPC.Kripke_Trees]
forces_t2 [definition, in IPC.Kripke_Trees]
forces_a1_imp_b__forces_a0_and_a1_imp_b [lemma, in IPC.Kripke_Trees]
forces_a0_imp_b__forces_a0_and_a1_imp_b [lemma, in IPC.Kripke_Trees]
forces_a0_imp_a1_imp_b__forces_a1_imp_b [lemma, in IPC.Kripke_Trees]
forces_a1_imp_b__forces_a0_imp_a1_imp_b [lemma, in IPC.Kripke_Trees]
forces_a0_imp_b_and_a1_imp_b__forces_a0_or_a1_imp_b [lemma, in IPC.Kripke_Trees]
forces_a0_imp_c_and_a1_imp_c_and_c_imp_b__forces_a0_or_a1_imp_b [lemma, in IPC.Kripke_Trees]
forces_a0_imp_a1_imp_b__forces_a0_and_a1_imp_b [lemma, in IPC.Kripke_Trees]
forces_b__forces_a_imp_b [lemma, in IPC.Kripke_Trees]
forces_mon [lemma, in IPC.Kripke_Trees]
Forces_Gamma [library]
Forces_NGamma [library]
forces0_t [definition, in IPC.Kripke_Trees]
Forest [inductive, in IPC.Trees]
form [inductive, in IPC.Forms]
Forms [library]
G
ge_eqv [lemma, in IPC.Le_Ks]goal_disj_insert_a [lemma, in IPC.Disjunct]
H
Hasnot_Shrunk_Right_Shift_Right [constructor, in IPC.AvlTrees]Hasnot_Shrunk_Right_Shift_Balanced [constructor, in IPC.AvlTrees]
Hasnot_Shrunk_Right_Bal [constructor, in IPC.AvlTrees]
hasnot_shrunk_right [inductive, in IPC.AvlTrees]
Hasnot_Shrunk_Left_Shift_Balanced [constructor, in IPC.AvlTrees]
Hasnot_Shrunk_Left_Shift_Left [constructor, in IPC.AvlTrees]
Hasnot_Shrunk_Left_Bal [constructor, in IPC.AvlTrees]
hasnot_shrunk_left [inductive, in IPC.AvlTrees]
Hasnot_Grown_Right_Shift_Right [constructor, in IPC.AvlTrees]
Hasnot_Grown_Right_Shift_Left [constructor, in IPC.AvlTrees]
Hasnot_Grown_Right_Bal [constructor, in IPC.AvlTrees]
hasnot_grown_right [inductive, in IPC.AvlTrees]
Hasnot_Grown_Left_Shift_Right [constructor, in IPC.AvlTrees]
Hasnot_Grown_Left_Shift_Left [constructor, in IPC.AvlTrees]
Hasnot_Grown_Left_Bal [constructor, in IPC.AvlTrees]
hasnot_grown_left [inductive, in IPC.AvlTrees]
hasnot_grown_right__preserves_is_balanced_avl [lemma, in IPC.AvlTrees]
hasnot_grown_left__preserves_is_balanced_avl [lemma, in IPC.AvlTrees]
Has_Shrunk_Right_Shift_Right [constructor, in IPC.AvlTrees]
Has_Shrunk_Right_Shift_Left [constructor, in IPC.AvlTrees]
has_shrunk_right [inductive, in IPC.AvlTrees]
Has_Shrunk_Left_Shift_Right [constructor, in IPC.AvlTrees]
Has_Shrunk_Left_Shift_Left [constructor, in IPC.AvlTrees]
has_shrunk_left [inductive, in IPC.AvlTrees]
Has_Grown_Right_Shift_Right [constructor, in IPC.AvlTrees]
Has_Grown_Right_Shift_Balanced [constructor, in IPC.AvlTrees]
has_grown_right [inductive, in IPC.AvlTrees]
Has_Grown_Left_Shift_Balanced [constructor, in IPC.AvlTrees]
Has_Grown_Left_Shift_Left [constructor, in IPC.AvlTrees]
has_grown_left [inductive, in IPC.AvlTrees]
height [definition, in IPC.AvlTrees]
height_in_le [lemma, in IPC.Trees]
height_forest [definition, in IPC.Trees]
height_tree [definition, in IPC.Trees]
height_avl_O_nil [lemma, in IPC.AvlTrees]
height_avl [definition, in IPC.AvlTrees]
height_O_nil [lemma, in IPC.AvlTrees]
I
Imp [constructor, in IPC.Forms]ImpElim [constructor, in IPC.Derivations]
ImpIntro [constructor, in IPC.Derivations]
inf_deco [lemma, in IPC.Le_Ks]
Inf_Deco_Spec_Intro [constructor, in IPC.Le_Ks]
inf_deco_spec [inductive, in IPC.Le_Ks]
insert_avl [lemma, in IPC.AvlTrees]
INSRT_AVL [lemma, in IPC.AvlTrees]
INSRT_Spec [definition, in IPC.AvlTrees]
Int [axiom, in IPC.ML_Int]
int_null [axiom, in IPC.ML_Int]
int_succ [axiom, in IPC.ML_Int]
inv_equiv_del_notequal1 [lemma, in IPC.AvlTrees]
inv_equiv_del_notequal0 [lemma, in IPC.AvlTrees]
inv_equiv_del_equal [lemma, in IPC.AvlTrees]
inv_equiv_ins_notequal1 [lemma, in IPC.AvlTrees]
inv_equiv_ins_notequal0 [lemma, in IPC.AvlTrees]
inv_equiv_ins_equal1 [lemma, in IPC.AvlTrees]
inv_equiv_ins_equal0 [lemma, in IPC.AvlTrees]
inv_equiv_t1_t0 [lemma, in IPC.AvlTrees]
inv_equiv_t0_t1 [lemma, in IPC.AvlTrees]
inv_is_avl_is_is_above_avl [lemma, in IPC.AvlTrees]
inv_is_avl_is_is_below_avl [lemma, in IPC.AvlTrees]
inv_is_avl_is_balanced_avl [lemma, in IPC.AvlTrees]
inv_is_avl_right [lemma, in IPC.AvlTrees]
inv_is_avl_left [lemma, in IPC.AvlTrees]
inv_right_balanced_avl [lemma, in IPC.AvlTrees]
inv_fully_balanced_avl [lemma, in IPC.AvlTrees]
inv_left_balanced_avl [lemma, in IPC.AvlTrees]
inv_above_avl_left [lemma, in IPC.AvlTrees]
inv_above_avl_key [lemma, in IPC.AvlTrees]
inv_below_avl_right [lemma, in IPC.AvlTrees]
inv_below_avl_key [lemma, in IPC.AvlTrees]
inv_lookup [lemma, in IPC.AvlTrees]
inv_lookup_nil [lemma, in IPC.AvlTrees]
inv_right_balanced [lemma, in IPC.AvlTrees]
inv_fully_balanced [lemma, in IPC.AvlTrees]
inv_left_balanced [lemma, in IPC.AvlTrees]
inv_above_right [lemma, in IPC.AvlTrees]
inv_above_left [lemma, in IPC.AvlTrees]
inv_above_key [lemma, in IPC.AvlTrees]
inv_below_right [lemma, in IPC.AvlTrees]
inv_below_left [lemma, in IPC.AvlTrees]
inv_below_key [lemma, in IPC.AvlTrees]
inv_nth_app [lemma, in IPC.My_Nth]
Inv_Nth_App1 [constructor, in IPC.My_Nth]
Inv_Nth_App0 [constructor, in IPC.My_Nth]
inv_my_nth_app [inductive, in IPC.My_Nth]
inv_nthS [lemma, in IPC.My_Nth]
inv_nthO [lemma, in IPC.My_Nth]
inv_nth_nil [lemma, in IPC.My_Nth]
in_ngamma_ge [lemma, in IPC.Le_Ks]
in_ngamma_le [lemma, in IPC.Le_Ks]
in_ngamma_eqv [lemma, in IPC.Le_Ks]
in_k_le [lemma, in IPC.Le_Ks]
in_ni_x_ni_tail [lemma, in IPC.Rev_App]
in_ni_x_ni_rev [lemma, in IPC.Rev_App]
in_ni1_in_nini [lemma, in IPC.Rev_App]
in_ni0_in_nini [lemma, in IPC.Rev_App]
in_app_or_ni [lemma, in IPC.Rev_App]
in_forest_ex_a0a1b [lemma, in IPC.Cons_Counter_Model]
in_successor_in [lemma, in IPC.Trees]
in_succs [constructor, in IPC.Trees]
in_leave [constructor, in IPC.Trees]
In_tree [inductive, in IPC.Trees]
in_forest_tail [constructor, in IPC.Trees]
in_forest_head [constructor, in IPC.Trees]
In_Forest [inductive, in IPC.Trees]
in_gamma_shift_work_gamma [lemma, in IPC.In_Gamma]
in_gamma_shift_gamma_work [lemma, in IPC.In_Gamma]
in_gamma_cons_work_rev [lemma, in IPC.In_Gamma]
in_gamma_cons_work_head [lemma, in IPC.In_Gamma]
in_gamma_cons_work_tail [lemma, in IPC.In_Gamma]
in_gamma_cons_gamma_rev [lemma, in IPC.In_Gamma]
in_gamma_cons_gamma_head [lemma, in IPC.In_Gamma]
in_gamma_cons_gamma_tail [lemma, in IPC.In_Gamma]
In_Work1 [constructor, in IPC.In_Gamma]
In_Gamma [constructor, in IPC.In_Gamma]
in_gamma [inductive, in IPC.In_Gamma]
in_ngamma_shift_a_work [lemma, in IPC.In_NGamma]
in_ngamma_shift_work_a [lemma, in IPC.In_NGamma]
in_ngamma_shift_ai_work [lemma, in IPC.In_NGamma]
in_ngamma_shift_work_ai_old [lemma, in IPC.In_NGamma]
in_ngamma_shift_work_ai_new [lemma, in IPC.In_NGamma]
in_ngamma_shift_ni_x_ni_work [lemma, in IPC.In_NGamma]
in_ngamma_shift_work_ni_x_ni [lemma, in IPC.In_NGamma]
in_ngamma_shift_ni_work [lemma, in IPC.In_NGamma]
in_ngamma_shift_work_ni [lemma, in IPC.In_NGamma]
in_ngamma_shift_ds_work [lemma, in IPC.In_NGamma]
in_ngamma_shift_work_ds [lemma, in IPC.In_NGamma]
in_ngamma_ins_a_rev [lemma, in IPC.In_NGamma]
in_ngamma_ins_a_head [lemma, in IPC.In_NGamma]
in_ngamma_ins_a_tail [lemma, in IPC.In_NGamma]
in_ngamma_del_ai_rev [lemma, in IPC.In_NGamma]
In_NGamma_Del_AI_Rev_Spec_Intro [constructor, in IPC.In_NGamma]
in_ngamma_del_ai_rev_spec [inductive, in IPC.In_NGamma]
in_ngamma_del_ai_tail [lemma, in IPC.In_NGamma]
in_ngamma_ins_ai_rev [lemma, in IPC.In_NGamma]
in_ngamma_ins_ai_head_old [lemma, in IPC.In_NGamma]
in_ngamma_ins_ai_head_new [lemma, in IPC.In_NGamma]
in_ngamma_ins_ai_tail [lemma, in IPC.In_NGamma]
in_ngamma_ni_eq [lemma, in IPC.In_NGamma]
in_ngamma_ni_x_ni_rev [lemma, in IPC.In_NGamma]
in_ngamma_ni_x_ni_tail [lemma, in IPC.In_NGamma]
in_ngamma_ni_x_ni_head [lemma, in IPC.In_NGamma]
in_ngamma_cons_ni_rev [lemma, in IPC.In_NGamma]
in_ngamma_cons_ni_head [lemma, in IPC.In_NGamma]
in_ngamma_cons_ni_tail [lemma, in IPC.In_NGamma]
in_ngamma_cons_ds_rev [lemma, in IPC.In_NGamma]
in_ngamma_cons_ds_head [lemma, in IPC.In_NGamma]
in_ngamma_cons_ds_tail [lemma, in IPC.In_NGamma]
in_ngamma_cons_work_rev [lemma, in IPC.In_NGamma]
in_ngamma_work_app_rev [lemma, in IPC.In_NGamma]
in_ngamma_work_app1 [lemma, in IPC.In_NGamma]
in_ngamma_cons_work_head [lemma, in IPC.In_NGamma]
in_ngamma_cons_work_tail [lemma, in IPC.In_NGamma]
In_Atoms [constructor, in IPC.In_NGamma]
In_Atomic_Imps [constructor, in IPC.In_NGamma]
In_Nested_Imps [constructor, in IPC.In_NGamma]
In_Disjs [constructor, in IPC.In_NGamma]
In_Work [constructor, in IPC.In_NGamma]
in_ngamma [inductive, in IPC.In_NGamma]
in_nth [lemma, in IPC.My_Nth]
In_NGamma [library]
In_Gamma [library]
is_monotone_tree_is_monotone [lemma, in IPC.Trees]
is_monotone_successor [lemma, in IPC.Trees]
is_monotone_intro [constructor, in IPC.Trees]
Is_Monotone [inductive, in IPC.Trees]
is_monotone_tree_successor [lemma, in IPC.Trees]
is_monotone_forest_cons [constructor, in IPC.Trees]
is_monotone_forest_nil [constructor, in IPC.Trees]
Is_Monotone_Forest [inductive, in IPC.Trees]
is_monotone_tree_intro [constructor, in IPC.Trees]
Is_Monotone_Tree [inductive, in IPC.Trees]
Is_Monotone_Kripke_Forest [definition, in IPC.Kripke_Trees]
Is_Monotone_kripke_tree [definition, in IPC.Kripke_Trees]
is_balanced_is_balanced_right_shift [lemma, in IPC.AvlTrees]
is_balanced_avl_is_balanced_avl_right_shift_left [lemma, in IPC.AvlTrees]
is_balanced_avl_is_balanced_avl_right_shift_false [lemma, in IPC.AvlTrees]
is_balanced_avl_is_balanced_avl_right_shift [lemma, in IPC.AvlTrees]
Is_Right_Balanced_Avl_Right_Shift [constructor, in IPC.AvlTrees]
Is_Fully_Balanced_Avl_Right_Shift [constructor, in IPC.AvlTrees]
Is_Left_Balanced_Avl_Right_Shift [constructor, in IPC.AvlTrees]
is_balanced_avl_right_shift [inductive, in IPC.AvlTrees]
is_balanced_is_balanced_left_shift_false [lemma, in IPC.AvlTrees]
is_left_balanced_is_left_balanced_left_shift [lemma, in IPC.AvlTrees]
Is_Right_Balanced_Avl_Left_Shift [constructor, in IPC.AvlTrees]
Is_Fully_Balanced_Avl_Left_Shift [constructor, in IPC.AvlTrees]
Is_Left_Balanced_Avl_Left_Shift [constructor, in IPC.AvlTrees]
is_balanced_avl_left_shift [inductive, in IPC.AvlTrees]
is_above_avl_is_above [lemma, in IPC.AvlTrees]
is_below_avl_is_below [lemma, in IPC.AvlTrees]
is_avl_is_balanced [lemma, in IPC.AvlTrees]
is_balanced_avl_is_balanced [lemma, in IPC.AvlTrees]
is_avl_rec [lemma, in IPC.AvlTrees]
is_avl [inductive, in IPC.AvlTrees]
Is_Right_Balanced_Avl [constructor, in IPC.AvlTrees]
Is_Fully_Balanced_Avl [constructor, in IPC.AvlTrees]
Is_Left_Balanced_Avl [constructor, in IPC.AvlTrees]
is_balanced_avl [inductive, in IPC.AvlTrees]
is_above_avl [inductive, in IPC.AvlTrees]
is_below_avl [inductive, in IPC.AvlTrees]
Is_Right_Balanced [constructor, in IPC.AvlTrees]
Is_Fully_Balanced [constructor, in IPC.AvlTrees]
Is_Left_Balanced [constructor, in IPC.AvlTrees]
is_balanced [inductive, in IPC.AvlTrees]
is_above [inductive, in IPC.AvlTrees]
is_below [inductive, in IPC.AvlTrees]
K
kripke_tree_succ [lemma, in IPC.Kripke_Trees]kripke_tree_kripke_model [lemma, in IPC.Kripke_Trees]
Kripke_Forest [definition, in IPC.Kripke_Trees]
kripke_tree [definition, in IPC.Kripke_Trees]
kripke_model [constructor, in IPC.Kripke_Trees]
Kripke_Model [inductive, in IPC.Kripke_Trees]
Kripke_Trees [library]
k_deco_sound_intro [constructor, in IPC.NDeco_Sound]
k_deco_sound [inductive, in IPC.NDeco_Sound]
L
leave_is_avl [lemma, in IPC.AvlTrees]left_nimp [lemma, in IPC.NRules]
left_disj [lemma, in IPC.NRules]
left_p_imp_ai [lemma, in IPC.NRules]
left_p_imp_work [lemma, in IPC.NRules]
Left_Balanced [constructor, in IPC.AvlTrees]
Less [axiom, in IPC.ML_Int]
less_irrefl [axiom, in IPC.ML_Int]
less_equal_less [axiom, in IPC.ML_Int]
less_trans [axiom, in IPC.ML_Int]
less_dec [axiom, in IPC.ML_Int]
le_ni_app_dd [lemma, in IPC.Le_Ks]
le_ni_app_dn [lemma, in IPC.Le_Ks]
le_ni_app_nn [lemma, in IPC.Le_Ks]
le_app0 [lemma, in IPC.Le_Ks]
Le_App_Spec_Intro [constructor, in IPC.Le_Ks]
le_app_spec [inductive, in IPC.Le_Ks]
le_eqv [lemma, in IPC.Le_Ks]
le_ni_trans [lemma, in IPC.Le_Ks]
le_ni_refl [lemma, in IPC.Le_Ks]
Le_NI_Cons_DD [constructor, in IPC.Le_Ks]
Le_NI_Cons_DN [constructor, in IPC.Le_Ks]
Le_NI_Cons_NN [constructor, in IPC.Le_Ks]
Le_NI_Nil [constructor, in IPC.Le_Ks]
le_ni [inductive, in IPC.Le_Ks]
le_ks_le_count_undecs [lemma, in IPC.Lt_Ks]
le_ni_le_count_undecs [lemma, in IPC.Lt_Ks]
le_n_max2 [lemma, in IPC.My_Arith]
le_n_max1 [lemma, in IPC.My_Arith]
le_reg [lemma, in IPC.My_Arith]
Le_Ks [library]
LIN_DEL [definition, in IPC.AvlTrees]
LIN_INS [definition, in IPC.AvlTrees]
LIN_AVL [definition, in IPC.AvlTrees]
Lin_Del_Spec_Intro [constructor, in IPC.AvlTrees]
lin_del_spec [inductive, in IPC.AvlTrees]
Lin_Ins_Update [constructor, in IPC.AvlTrees]
Lin_Ins_New [constructor, in IPC.AvlTrees]
lin_ins_spec [inductive, in IPC.AvlTrees]
lin_avl [definition, in IPC.AvlTrees]
list2vlist [definition, in IPC.Search]
LOOKUP [definition, in IPC.AvlTrees]
Lookup [constructor, in IPC.AvlTrees]
lookup [inductive, in IPC.AvlTrees]
LOOKUP_DEC [lemma, in IPC.AvlTrees]
LOOKUP_Dec_Spec [definition, in IPC.AvlTrees]
lookup_dec [lemma, in IPC.AvlTrees]
lookup_dec_spec [inductive, in IPC.AvlTrees]
lookup_avl_equal [lemma, in IPC.AvlTrees]
lookup_avl_inv_greater [lemma, in IPC.AvlTrees]
lookup_avl_inv_less [lemma, in IPC.AvlTrees]
lookup_avl_inv_equal [lemma, in IPC.AvlTrees]
lookup_above_false [lemma, in IPC.AvlTrees]
lookup_below_false [lemma, in IPC.AvlTrees]
lookup_below_lookup [lemma, in IPC.AvlTrees]
lookup_above_lookup [lemma, in IPC.AvlTrees]
lookup_greater_above [lemma, in IPC.AvlTrees]
lookup_less_below [lemma, in IPC.AvlTrees]
lookup_above_greater [lemma, in IPC.AvlTrees]
lookup_below_less [lemma, in IPC.AvlTrees]
Lookup_Right [constructor, in IPC.AvlTrees]
Lookup_Left [constructor, in IPC.AvlTrees]
Lookup_Equal [constructor, in IPC.AvlTrees]
lt_ks_shift_dd [lemma, in IPC.Lt_Ks]
lt_ks_shift_nd [lemma, in IPC.Lt_Ks]
lt_ks_length [constructor, in IPC.Lt_Ks]
lt_ks_count_undecs [constructor, in IPC.Lt_Ks]
Lt_Ks [inductive, in IPC.Lt_Ks]
lt_plus_assoc_l [lemma, in IPC.My_Arith]
Lt_Ks [library]
M
max [definition, in IPC.My_Arith]max_int_of_list [lemma, in IPC.Forms]
max_int_of_form [lemma, in IPC.Forms]
max_n_O [lemma, in IPC.My_Arith]
max_n_Sn [lemma, in IPC.My_Arith]
max_Sn_n [lemma, in IPC.My_Arith]
max_n_n [lemma, in IPC.My_Arith]
max_int [lemma, in IPC.ML_Int]
Max_Int_Intro [constructor, in IPC.ML_Int]
max_int_spec [inductive, in IPC.ML_Int]
minimal [definition, in IPC.Minimal]
Minimal [library]
minimal_cons_gamma_weak2 [lemma, in IPC.Minimal]
minimal_cons_gamma_weak [lemma, in IPC.Minimal]
minimal_cons_gamma_cons_context [lemma, in IPC.Minimal]
minimal_shift_work_gamma [lemma, in IPC.Minimal]
minimal_shift_gamma_work [lemma, in IPC.Minimal]
minimal_derivable_forces [lemma, in IPC.Minimal]
ML_Int [library]
My_Lt_Ks_rec [lemma, in IPC.Lt_Ks]
My_Tree_rec [lemma, in IPC.Trees]
My_Tree_ind [lemma, in IPC.Trees]
my_lt_weak [lemma, in IPC.My_Arith]
my_nth_split [lemma, in IPC.My_Nth]
my_nth_rec [lemma, in IPC.My_Nth]
My_NthS [constructor, in IPC.My_Nth]
My_NthO [constructor, in IPC.My_Nth]
my_nth [inductive, in IPC.My_Nth]
My_Nth.B [variable, in IPC.My_Nth]
My_Nth [section, in IPC.My_Nth]
My_Nth [library]
My_Arith [library]
N
NAtom [constructor, in IPC.Normal_Forms]nax [lemma, in IPC.NRules]
NDeco_Sound [library]
NDerivable [constructor, in IPC.NRules]
NDisj [constructor, in IPC.Normal_Forms]
nefq [lemma, in IPC.NRules]
nested_imps2nimps_length [lemma, in IPC.In_NGamma]
nested_imps2nimps_app [lemma, in IPC.In_NGamma]
nested_imps2nimps [definition, in IPC.In_NGamma]
nested_imps2nforms [definition, in IPC.In_NGamma]
nested_imps2forms [definition, in IPC.In_NGamma]
nested_imps [definition, in IPC.In_NGamma]
nested_imp2nform [definition, in IPC.In_NGamma]
nested_imp2form [definition, in IPC.In_NGamma]
nested_imp2nimp [definition, in IPC.In_NGamma]
nested_imp [inductive, in IPC.In_NGamma]
NFalsum [constructor, in IPC.Normal_Forms]
nf_nil [definition, in IPC.Normal_Forms]
nf_list [definition, in IPC.Normal_Forms]
nf2form [definition, in IPC.Normal_Forms]
Nil_Forest [constructor, in IPC.Trees]
Nil_Is_Avl [constructor, in IPC.AvlTrees]
NImp [constructor, in IPC.Normal_Forms]
nimp [inductive, in IPC.Normal_Forms]
NImp_NF [constructor, in IPC.Normal_Forms]
nimp2form [definition, in IPC.Normal_Forms]
nminimal [definition, in IPC.NMinimal]
NMinimal [library]
nminimal_cons_work_cons_context [lemma, in IPC.NMinimal]
nminimal_shift_ds_work_context [lemma, in IPC.NMinimal]
nminimal_shift_work_ai_weak [lemma, in IPC.NMinimal]
nminimal_cons_work_weak [lemma, in IPC.NMinimal]
nminimal_cons_work_strength [lemma, in IPC.NMinimal]
nminimal_shift_ni_x_ni_work [lemma, in IPC.NMinimal]
nminimal_shift_work_ni_x_ni [lemma, in IPC.NMinimal]
nminimal_shift_work_a [lemma, in IPC.NMinimal]
nminimal_shift_work_ai_old [lemma, in IPC.NMinimal]
nminimal_shift_work_ai_new [lemma, in IPC.NMinimal]
nminimal_shift_work_ni [lemma, in IPC.NMinimal]
nminimal_shift_work_ds [lemma, in IPC.NMinimal]
nminimal_eqv [lemma, in IPC.NMinimal]
nminimal_derivable_forces [lemma, in IPC.NMinimal]
NNil [definition, in IPC.In_NGamma]
node [constructor, in IPC.Trees]
Node_Is_Avl [constructor, in IPC.AvlTrees]
normal_form [inductive, in IPC.Normal_Forms]
Normal_Forms [library]
notequal_notless_greater [axiom, in IPC.ML_Int]
Not_Lookup [constructor, in IPC.AvlTrees]
NRefutable [constructor, in IPC.NRules]
NRules [library]
nsearch [lemma, in IPC.NSearch]
NSearch [library]
nsearch_spec [definition, in IPC.NRules]
NSearch_Res [constructor, in IPC.NRules]
nsearch_spec_result [inductive, in IPC.NRules]
nsearch_spec_result_aux [inductive, in IPC.NRules]
nsearch_aux [lemma, in IPC.NSearch]
nsearch_invariant [definition, in IPC.NSearch]
nsound [definition, in IPC.NSound]
NSound [library]
nsound_shift_work_ai_strength [lemma, in IPC.NSound]
nsound_cons_work_weak [lemma, in IPC.NSound]
nsound_cons_work_cons_context [lemma, in IPC.NSound]
nsound_del_ai [lemma, in IPC.NSound]
nsound_cons_ds_tail [lemma, in IPC.NSound]
nsound_app_work [lemma, in IPC.NSound]
nsound_shift_ni_x_ni_work [lemma, in IPC.NSound]
nsound_shift_work_ni_x_ni [lemma, in IPC.NSound]
nsound_shift_work_a [lemma, in IPC.NSound]
nsound_shift_work_ai [lemma, in IPC.NSound]
nsound_shift_work_ni [lemma, in IPC.NSound]
nsound_shift_work_ds [lemma, in IPC.NSound]
nsound_ge [lemma, in IPC.NSound]
nsound_le [lemma, in IPC.NSound]
nsound_eqv [lemma, in IPC.NSound]
nth_nimp__nth_nested_imp [lemma, in IPC.Cons_Counter_Model]
Nth_Split_Intro [constructor, in IPC.My_Nth]
nth_split [inductive, in IPC.My_Nth]
nth_app1 [lemma, in IPC.My_Nth]
nth_app0 [lemma, in IPC.My_Nth]
nth_in [lemma, in IPC.My_Nth]
nvimp [definition, in IPC.Normal_Forms]
nweight [definition, in IPC.NWeight]
NWeight [library]
nweight_sequent_left_disj_right [lemma, in IPC.NWeight]
nweight_sequent_left_disj_left [lemma, in IPC.NWeight]
nweight_sequent_nimp_right [lemma, in IPC.NWeight]
nweight_sequent_nimp_left [lemma, in IPC.NWeight]
nweight_sequent_eqv [lemma, in IPC.NWeight]
nweight_shift_ai_work [lemma, in IPC.NWeight]
nweight_shift_work_ai [lemma, in IPC.NWeight]
nweight_shift_work_ds [lemma, in IPC.NWeight]
nweight_shift_work_ni0 [lemma, in IPC.NWeight]
nweight_Sequent [definition, in IPC.NWeight]
nweight_rev_app [lemma, in IPC.NWeight]
nweight_eqv_ni [lemma, in IPC.NWeight]
nweight_ai_del [lemma, in IPC.NWeight]
nweight_ai_ins [lemma, in IPC.NWeight]
nweight_ai_perm [lemma, in IPC.NWeight]
nweight_ai [definition, in IPC.NWeight]
nweight_ibs [definition, in IPC.NWeight]
nweight_bs [definition, in IPC.NWeight]
nweight_atomicimp [definition, in IPC.NWeight]
nweight_dni [definition, in IPC.NWeight]
nweight_decoratednestedimp [definition, in IPC.NWeight]
nweight_ni [definition, in IPC.NWeight]
nweight_nestedimp [definition, in IPC.NWeight]
nweight_ds [definition, in IPC.NWeight]
nweight_disj [definition, in IPC.NWeight]
nweight_work_app [lemma, in IPC.NWeight]
nweight_work [definition, in IPC.NWeight]
n_Sn_false [lemma, in IPC.My_Arith]
n2forest [definition, in IPC.Cons_Counter_Model]
O
OrF [constructor, in IPC.Forms]OrFElim [constructor, in IPC.Derivations]
OrFIntroL [constructor, in IPC.Derivations]
OrFIntroR [constructor, in IPC.Derivations]
OrFL [constructor, in IPC.Derivations]
OrFR [constructor, in IPC.Derivations]
P
Pair [constructor, in IPC.Derivations]plus_reg [lemma, in IPC.My_Arith]
plus_O [lemma, in IPC.My_Arith]
PrL [constructor, in IPC.Derivations]
proof_term [inductive, in IPC.Derivations]
PrR [constructor, in IPC.Derivations]
R
rebalance_right [lemma, in IPC.AvlTrees]rebalance_right_spec [definition, in IPC.AvlTrees]
rebalance_left [lemma, in IPC.AvlTrees]
rebalance_left_spec [definition, in IPC.AvlTrees]
refutable [constructor, in IPC.Search]
refutable [constructor, in IPC.Rules]
REGULAR [definition, in IPC.Regular_Avl]
Regular [definition, in IPC.Regular_Avl]
regular_EQUIV_INS [lemma, in IPC.Regular_Avl]
regular_EQUIV_DEL [lemma, in IPC.Regular_Avl]
regular_AVL_NIL [lemma, in IPC.Regular_Avl]
regular_equiv_ins [lemma, in IPC.Regular_Avl]
regular_equiv_del [lemma, in IPC.Regular_Avl]
regular_nil [lemma, in IPC.Regular_Avl]
Regular_Avl.A [variable, in IPC.Regular_Avl]
Regular_Avl [section, in IPC.Regular_Avl]
Regular_Avl [library]
rev_app_lemma2 [lemma, in IPC.Rev_App]
rev_app_lemma1 [lemma, in IPC.Rev_App]
Rev_App_Spec_Intro [constructor, in IPC.Rev_App]
rev_app_spec [inductive, in IPC.Rev_App]
rev_app_lemma0 [lemma, in IPC.Rev_App]
rev_app_app [lemma, in IPC.Rev_App]
rev_app [definition, in IPC.Rev_App]
Rev_App [library]
Right_Balanced [constructor, in IPC.AvlTrees]
root [definition, in IPC.Trees]
Rules [library]
rule_shift_work_a [lemma, in IPC.NRules]
rule_shift_work_ai_old [lemma, in IPC.NRules]
rule_shift_work_ai_new [lemma, in IPC.NRules]
rule_shift_work_ni0 [lemma, in IPC.NRules]
rule_shift_work_ds [lemma, in IPC.NRules]
rule_a_imp_b_imp_c_gamma [lemma, in IPC.Rules]
rule_atom_imp_b_imp_c_gamma [lemma, in IPC.Rules]
rule_atom_imp_atom_imp_c_gamma [lemma, in IPC.Rules]
rule_vimp_imp_falsum_imp_gamma [lemma, in IPC.Rules]
rule_vimp_falsum_imp_imp_gamma [lemma, in IPC.Rules]
rule_vimp_or_imp_gamma_new [lemma, in IPC.Rules]
rule_vimp_or_imp_gamma [lemma, in IPC.Rules]
rule_vimp_and_imp_gamma [lemma, in IPC.Rules]
rule_vimp_atom_imp_b_gamma [lemma, in IPC.Rules]
rule_vimp_falsum_imp_b_gamma [lemma, in IPC.Rules]
rule_vimp_a_or_b_gamma [lemma, in IPC.Rules]
rule_vimp_atom_or_a_gamma [lemma, in IPC.Rules]
rule_vimp_a_or_falsum_gamma [lemma, in IPC.Rules]
rule_vimp_falsum_or_a_gamma [lemma, in IPC.Rules]
rule_vimp_conj_gamma_new [lemma, in IPC.Rules]
rule_vimp_conj_gamma [lemma, in IPC.Rules]
rule_gamma_a [lemma, in IPC.Rules]
rule_gamma_a_imp_b [lemma, in IPC.Rules]
rule_gamma_falsum [lemma, in IPC.Rules]
rule_vimp_imp_gamma [lemma, in IPC.Rules]
rule_vimp_a_gamma [lemma, in IPC.Rules]
rule_shift_gamma_work [lemma, in IPC.Rules]
S
search [lemma, in IPC.Search]Search [library]
search_spec [inductive, in IPC.Search]
search_goal_invariant [lemma, in IPC.Search]
search_atom_aux [lemma, in IPC.Search]
search_atom_invariant [definition, in IPC.Search]
search_spec_subst_gamma_pos [lemma, in IPC.Rules]
search_spec [definition, in IPC.Rules]
search_spec_aux [inductive, in IPC.Rules]
Shift [constructor, in IPC.Derivations]
ShiftIntro [constructor, in IPC.Derivations]
shift_ni_dni [lemma, in IPC.NRules]
snd_order_inst [lemma, in IPC.Derivable_Tools]
sound [definition, in IPC.Sound]
Sound [library]
soundness [lemma, in IPC.Kripke_Trees]
soundness_t [lemma, in IPC.Kripke_Trees]
sound_cons_gamma_weak2 [lemma, in IPC.Sound]
sound_cons_gamma_weak [lemma, in IPC.Sound]
sound_cons_gamma_cons_context [lemma, in IPC.Sound]
sound_shift_work_gamma [lemma, in IPC.Sound]
sound_shift_gamma_work [lemma, in IPC.Sound]
sound_cons_gamma_head [lemma, in IPC.Sound]
sound_cons_gamma_tail [lemma, in IPC.Sound]
sound_cons_gamma [lemma, in IPC.Sound]
subst_vimp_head [lemma, in IPC.Forms]
subst_list_below [lemma, in IPC.Forms]
subst_form_below [lemma, in IPC.Forms]
subst_nth [lemma, in IPC.Forms]
subst_list [definition, in IPC.Forms]
subst_form [definition, in IPC.Forms]
Suc [definition, in IPC.Kripke_Trees]
Successor [inductive, in IPC.Trees]
successors [definition, in IPC.Trees]
successor_trans [constructor, in IPC.Trees]
successor_refl [constructor, in IPC.Trees]
Succs [definition, in IPC.Kripke_Trees]
Succs_Tree_ind [lemma, in IPC.Trees]
succs_refl [lemma, in IPC.Trees]
succs_trans [lemma, in IPC.Trees]
S_reg [lemma, in IPC.My_Arith]
T
Tree [inductive, in IPC.Trees]Trees [section, in IPC.Trees]
Trees [library]
Trees.A [variable, in IPC.Trees]
Trees.I [variable, in IPC.Trees]
Trees.P [variable, in IPC.Trees]
U
Undecorated [constructor, in IPC.In_NGamma]V
Var [constructor, in IPC.Derivations]vimp [definition, in IPC.Forms]
vimp_eq_nvimp [lemma, in IPC.Normal_Forms]
vimp2nform [lemma, in IPC.Normal_Forms]
vimp2nvimp [lemma, in IPC.Normal_Forms]
vlist [definition, in IPC.Search]
vlist_eq [lemma, in IPC.Search]
vlist2hlist [definition, in IPC.Search]
vlist2list [definition, in IPC.Search]
W
weight [definition, in IPC.Weight]Weight [library]
weight_gamma_weak3' [lemma, in IPC.Weight]
weight_gamma_weak3 [lemma, in IPC.Weight]
weight_gamma_weak2' [lemma, in IPC.Weight]
weight_gamma_weak2 [lemma, in IPC.Weight]
weight_gamma_weak' [lemma, in IPC.Weight]
weight_gamma_weak [lemma, in IPC.Weight]
weight_vimp [lemma, in IPC.Weight]
weight_neg_le [lemma, in IPC.Weight]
weight_ge_1 [lemma, in IPC.Weight]
weight_gamma [definition, in IPC.Weight]
weight_goal [definition, in IPC.Weight]
weight_neg [definition, in IPC.Weight]
Variable Index
A
avl_trees.B [in IPC.AvlTrees]M
My_Nth.B [in IPC.My_Nth]R
Regular_Avl.A [in IPC.Regular_Avl]T
Trees.A [in IPC.Trees]Trees.I [in IPC.Trees]
Trees.P [in IPC.Trees]
Library Index
A
AvlTreesC
Cons_Counter_ModelD
Derivable_DefDerivable_Tools
Derivable_Def_compute_derivations
Derivable_Def_dont_compute_derivations
Derivations
Disjunct
E
ExtrF
Forces_GammaForces_NGamma
Forms
I
In_NGammaIn_Gamma
K
Kripke_TreesL
Le_KsLt_Ks
M
MinimalML_Int
My_Nth
My_Arith
N
NDeco_SoundNMinimal
Normal_Forms
NRules
NSearch
NSound
NWeight
R
Regular_AvlRev_App
Rules
S
SearchSound
T
TreesW
WeightLemma Index
A
above_equiv_del_above [in IPC.AvlTrees]above_above_avl [in IPC.AvlTrees]
above_avl_trans [in IPC.AvlTrees]
above_trans [in IPC.AvlTrees]
all_ref_rev_app_nil [in IPC.Cons_Counter_Model]
avl_ins_eq [in IPC.AvlTrees]
avl_height_avl_height [in IPC.AvlTrees]
B
Balanced_shrunk_left_balanced_shift [in IPC.AvlTrees]balance_shrunk_right [in IPC.AvlTrees]
balance_shrunk_left [in IPC.AvlTrees]
balance_right [in IPC.AvlTrees]
balance_left [in IPC.AvlTrees]
below_vimp_tail [in IPC.Forms]
below_vimp_split [in IPC.Forms]
below_vimp_head [in IPC.Forms]
below_vimp2 [in IPC.Forms]
below_vimp [in IPC.Forms]
below_list_weak2 [in IPC.Forms]
below_list_weak [in IPC.Forms]
below_cons_list [in IPC.Forms]
below_cons_list_tail [in IPC.Forms]
below_cons_list_head [in IPC.Forms]
below_list_less_below_list [in IPC.Forms]
below_form_less_below_form [in IPC.Forms]
below_equiv_del_below [in IPC.AvlTrees]
below_equiv_below [in IPC.AvlTrees]
below_below_avl [in IPC.AvlTrees]
below_avl_trans [in IPC.AvlTrees]
below_trans [in IPC.AvlTrees]
C
cons_counter_model [in IPC.Cons_Counter_Model]cons_counter_model_mon [in IPC.Cons_Counter_Model]
cons_counter_model_suc [in IPC.Cons_Counter_Model]
contradiction_atoms [in IPC.NRules]
count_undecs_rev_app [in IPC.Lt_Ks]
D
deco_sound_in_forest_forces [in IPC.Cons_Counter_Model]deco_sound_filter_deco [in IPC.NDeco_Sound]
deco_sound_inf [in IPC.NDeco_Sound]
deco_sound_shift_work_ai_strength [in IPC.NDeco_Sound]
deco_sound_shift_work_ai_weak [in IPC.NDeco_Sound]
deco_sound_cons_work_strength [in IPC.NDeco_Sound]
deco_sound_cons_work_weak2 [in IPC.NDeco_Sound]
deco_sound_cons_work_weak [in IPC.NDeco_Sound]
deco_sound_le [in IPC.NDeco_Sound]
deco_sound_shift_work_nirni [in IPC.NDeco_Sound]
deco_sound_shift_work_ninni [in IPC.NDeco_Sound]
deco_sound_shift_ni_x_ni_work [in IPC.NDeco_Sound]
deco_sound_shift_work_a [in IPC.NDeco_Sound]
deco_sound_shift_a_work [in IPC.NDeco_Sound]
deco_sound_shift_work_ai [in IPC.NDeco_Sound]
deco_sound_shift_ai_work_old [in IPC.NDeco_Sound]
deco_sound_shift_ai_work_new [in IPC.NDeco_Sound]
deco_sound_shift_work_ni0 [in IPC.NDeco_Sound]
deco_sound_shift_ni_work [in IPC.NDeco_Sound]
deco_sound_shift_work_ds [in IPC.NDeco_Sound]
deco_sound_shift_ds_work [in IPC.NDeco_Sound]
deco_sound_cons_ni_tail [in IPC.NDeco_Sound]
deco_sound_cons_ds_tail [in IPC.NDeco_Sound]
deco_sound_cons_work_tail [in IPC.NDeco_Sound]
DELETE_AVL [in IPC.AvlTrees]
delete_avl [in IPC.AvlTrees]
delete_max [in IPC.AvlTrees]
derivable_vimp0 [in IPC.Derivable_Tools]
derivable_vimp2 [in IPC.Derivable_Tools]
derivable_vimp [in IPC.Derivable_Tools]
derivable_a_context_b__derivable_a_imp_b [in IPC.Derivable_Tools]
derivable_a_a_imp_b__derivable_b [in IPC.Derivable_Tools]
derivable_b__derivable_a_imp_b [in IPC.Derivable_Tools]
derivable_falsum_imp_b_imp_c__derivable_c [in IPC.Derivable_Tools]
derivable_a0_or_a1_imp_b__derivable_a1_imp_b [in IPC.Derivable_Tools]
derivable_a0_or_a1_imp_b__derivable_a0_imp_b [in IPC.Derivable_Tools]
derivable_a0_and_a1_imp_b__derivable_a0_imp_a1_imp_b [in IPC.Derivable_Tools]
derivable_a_imp_b_or_falsum__derivable_a_imp_b [in IPC.Derivable_Tools]
derivable_a_imp_falsum_or_b__derivable_a_imp_b [in IPC.Derivable_Tools]
derivable_a_or_falsum__derivable_a [in IPC.Derivable_Tools]
derivable_falsum_or_a__derivable_a [in IPC.Derivable_Tools]
derivable_a_and_b__derivable_b [in IPC.Derivable_Tools]
derivable_a_and_b__derivable_a [in IPC.Derivable_Tools]
derivable_a_imp_a [in IPC.Derivable_Tools]
derivable_cut_merge [in IPC.Derivable_Tools]
derivable_cut [in IPC.Derivable_Tools]
derivable_cut_aux [in IPC.Derivable_Tools]
derivable_weak_list [in IPC.Derivable_Tools]
derivable_weak [in IPC.Derivable_Tools]
derivable_subst [in IPC.Derivable_Tools]
derivable_eq [in IPC.Derivable_Tools]
derives_rec [in IPC.Derivations]
disjs_insert_a [in IPC.Disjunct]
disjs_delete_ai [in IPC.Disjunct]
disjs_insert_ai [in IPC.Disjunct]
E
equal_dec_refl [in IPC.ML_Int]equiv_del_trans_right [in IPC.AvlTrees]
equiv_del_trans_left [in IPC.AvlTrees]
equiv_del_equal [in IPC.AvlTrees]
equiv_del_right_semi_leave [in IPC.AvlTrees]
equiv_del_nil [in IPC.AvlTrees]
equiv_del_right [in IPC.AvlTrees]
equiv_del_above [in IPC.AvlTrees]
equiv_del_semi_leave [in IPC.AvlTrees]
equiv_del_equiv_equiv_del [in IPC.AvlTrees]
equiv_ins_right [in IPC.AvlTrees]
equiv_ins_left [in IPC.AvlTrees]
equiv_ins_eq [in IPC.AvlTrees]
equiv_ins_nil [in IPC.AvlTrees]
equiv_ins_above [in IPC.AvlTrees]
equiv_ins_below [in IPC.AvlTrees]
equiv_ins_equiv_equiv_ins [in IPC.AvlTrees]
equiv_refl [in IPC.AvlTrees]
equiv_sym [in IPC.AvlTrees]
eqv_nimps_eq [in IPC.Le_Ks]
eqv_ni_rec [in IPC.Le_Ks]
eqv_sym [in IPC.Le_Ks]
eqv_ni_trans [in IPC.Le_Ks]
eq_lt_trans [in IPC.My_Arith]
F
fail [in IPC.NRules]filter_deco [in IPC.Le_Ks]
fold_right_perm [in IPC.My_Arith]
forces_ngamma_shift_work_ai_strength [in IPC.Forces_NGamma]
forces_ngamma_shift_work_ai_weak [in IPC.Forces_NGamma]
forces_ngamma_cons_work_weak2 [in IPC.Forces_NGamma]
forces_ngamma_cons_work_weak [in IPC.Forces_NGamma]
forces_ngamma_shift_ni_x_ni_work [in IPC.Forces_NGamma]
forces_ngamma_shift_work_ni_x_ni [in IPC.Forces_NGamma]
forces_ngamma_shift_work_a [in IPC.Forces_NGamma]
forces_ngamma_shift_a_work [in IPC.Forces_NGamma]
forces_ngamma_shift_work_ai [in IPC.Forces_NGamma]
forces_ngamma_shift_ai_work_old [in IPC.Forces_NGamma]
forces_ngamma_shift_ai_work_new [in IPC.Forces_NGamma]
forces_ngamma_shift_work_ni [in IPC.Forces_NGamma]
forces_ngamma_shift_ni_work [in IPC.Forces_NGamma]
forces_ngamma_shift_work_ds [in IPC.Forces_NGamma]
forces_ngamma_shift_ds_work [in IPC.Forces_NGamma]
forces_ngamma_eqv [in IPC.Forces_NGamma]
forces_ngamma_del_ai_rev [in IPC.Forces_NGamma]
forces_ngamma_del_ai [in IPC.Forces_NGamma]
forces_ngamma_cons_ni_tail [in IPC.Forces_NGamma]
forces_ngamma_cons_ds_tail [in IPC.Forces_NGamma]
forces_ngamma_app_work_tail [in IPC.Forces_NGamma]
forces_ngamma_app_work [in IPC.Forces_NGamma]
forces_ngamma_cons_work_tail [in IPC.Forces_NGamma]
forces_ngamma_cons_work [in IPC.Forces_NGamma]
forces_gamma_cons_gamma_weak2 [in IPC.Forces_Gamma]
forces_gamma_cons_gamma_weak [in IPC.Forces_Gamma]
forces_gamma_shift_work_gamma [in IPC.Forces_Gamma]
forces_gamma_shift_gamma_work [in IPC.Forces_Gamma]
forces_gamma_cons_gamma_head [in IPC.Forces_Gamma]
forces_gamma_cons_gamma_tail [in IPC.Forces_Gamma]
forces_gamma_cons_gamma [in IPC.Forces_Gamma]
forces_a_imp_b_imp_c__forces_a_imp_falsum_imp_c_t2 [in IPC.Kripke_Trees]
forces_vimp0 [in IPC.Kripke_Trees]
forces_vimp2 [in IPC.Kripke_Trees]
forces_vimp [in IPC.Kripke_Trees]
forces_a_imp_b_imp_c__forces_a_imp_falsum_imp_c [in IPC.Kripke_Trees]
forces_a_imp_falsum_imp_b1_t [in IPC.Kripke_Trees]
forces_a_imp_b__forces_a_imp_b_or_falsum [in IPC.Kripke_Trees]
forces_a_imp_b__forces_a_imp_falsum_or_b [in IPC.Kripke_Trees]
forces_a_imp_b0_a_imp_b1__forces_a_imp_a0_and_a1 [in IPC.Kripke_Trees]
forces_a_a_imp_b__forces_b_t [in IPC.Kripke_Trees]
forces_a1_imp_b__forces_a0_and_a1_imp_b_t [in IPC.Kripke_Trees]
forces_a0_imp_b__forces_a0_and_a1_imp_b_t [in IPC.Kripke_Trees]
forces_a0_imp_a1_imp_b__forces_a1_imp_b_t [in IPC.Kripke_Trees]
forces_a1_imp_b__forces_a0_imp_a1_imp_b_t [in IPC.Kripke_Trees]
forces_a0_imp_c_and_a1_imp_c_and_c_imp_b__forces_a0_or_a1_imp_b_t [in IPC.Kripke_Trees]
forces_a0_imp_a1_imp_b__forces_a0_and_a1_imp_b_t [in IPC.Kripke_Trees]
forces_b__forces_a_imp_b_t [in IPC.Kripke_Trees]
forces_t_mon [in IPC.Kripke_Trees]
forces_t_imp [in IPC.Kripke_Trees]
forces_t2_is_local [in IPC.Kripke_Trees]
forces_a1_imp_b__forces_a0_and_a1_imp_b [in IPC.Kripke_Trees]
forces_a0_imp_b__forces_a0_and_a1_imp_b [in IPC.Kripke_Trees]
forces_a0_imp_a1_imp_b__forces_a1_imp_b [in IPC.Kripke_Trees]
forces_a1_imp_b__forces_a0_imp_a1_imp_b [in IPC.Kripke_Trees]
forces_a0_imp_b_and_a1_imp_b__forces_a0_or_a1_imp_b [in IPC.Kripke_Trees]
forces_a0_imp_c_and_a1_imp_c_and_c_imp_b__forces_a0_or_a1_imp_b [in IPC.Kripke_Trees]
forces_a0_imp_a1_imp_b__forces_a0_and_a1_imp_b [in IPC.Kripke_Trees]
forces_b__forces_a_imp_b [in IPC.Kripke_Trees]
forces_mon [in IPC.Kripke_Trees]
G
ge_eqv [in IPC.Le_Ks]goal_disj_insert_a [in IPC.Disjunct]
H
hasnot_grown_right__preserves_is_balanced_avl [in IPC.AvlTrees]hasnot_grown_left__preserves_is_balanced_avl [in IPC.AvlTrees]
height_in_le [in IPC.Trees]
height_avl_O_nil [in IPC.AvlTrees]
height_O_nil [in IPC.AvlTrees]
I
inf_deco [in IPC.Le_Ks]insert_avl [in IPC.AvlTrees]
INSRT_AVL [in IPC.AvlTrees]
inv_equiv_del_notequal1 [in IPC.AvlTrees]
inv_equiv_del_notequal0 [in IPC.AvlTrees]
inv_equiv_del_equal [in IPC.AvlTrees]
inv_equiv_ins_notequal1 [in IPC.AvlTrees]
inv_equiv_ins_notequal0 [in IPC.AvlTrees]
inv_equiv_ins_equal1 [in IPC.AvlTrees]
inv_equiv_ins_equal0 [in IPC.AvlTrees]
inv_equiv_t1_t0 [in IPC.AvlTrees]
inv_equiv_t0_t1 [in IPC.AvlTrees]
inv_is_avl_is_is_above_avl [in IPC.AvlTrees]
inv_is_avl_is_is_below_avl [in IPC.AvlTrees]
inv_is_avl_is_balanced_avl [in IPC.AvlTrees]
inv_is_avl_right [in IPC.AvlTrees]
inv_is_avl_left [in IPC.AvlTrees]
inv_right_balanced_avl [in IPC.AvlTrees]
inv_fully_balanced_avl [in IPC.AvlTrees]
inv_left_balanced_avl [in IPC.AvlTrees]
inv_above_avl_left [in IPC.AvlTrees]
inv_above_avl_key [in IPC.AvlTrees]
inv_below_avl_right [in IPC.AvlTrees]
inv_below_avl_key [in IPC.AvlTrees]
inv_lookup [in IPC.AvlTrees]
inv_lookup_nil [in IPC.AvlTrees]
inv_right_balanced [in IPC.AvlTrees]
inv_fully_balanced [in IPC.AvlTrees]
inv_left_balanced [in IPC.AvlTrees]
inv_above_right [in IPC.AvlTrees]
inv_above_left [in IPC.AvlTrees]
inv_above_key [in IPC.AvlTrees]
inv_below_right [in IPC.AvlTrees]
inv_below_left [in IPC.AvlTrees]
inv_below_key [in IPC.AvlTrees]
inv_nth_app [in IPC.My_Nth]
inv_nthS [in IPC.My_Nth]
inv_nthO [in IPC.My_Nth]
inv_nth_nil [in IPC.My_Nth]
in_ngamma_ge [in IPC.Le_Ks]
in_ngamma_le [in IPC.Le_Ks]
in_ngamma_eqv [in IPC.Le_Ks]
in_k_le [in IPC.Le_Ks]
in_ni_x_ni_tail [in IPC.Rev_App]
in_ni_x_ni_rev [in IPC.Rev_App]
in_ni1_in_nini [in IPC.Rev_App]
in_ni0_in_nini [in IPC.Rev_App]
in_app_or_ni [in IPC.Rev_App]
in_forest_ex_a0a1b [in IPC.Cons_Counter_Model]
in_successor_in [in IPC.Trees]
in_gamma_shift_work_gamma [in IPC.In_Gamma]
in_gamma_shift_gamma_work [in IPC.In_Gamma]
in_gamma_cons_work_rev [in IPC.In_Gamma]
in_gamma_cons_work_head [in IPC.In_Gamma]
in_gamma_cons_work_tail [in IPC.In_Gamma]
in_gamma_cons_gamma_rev [in IPC.In_Gamma]
in_gamma_cons_gamma_head [in IPC.In_Gamma]
in_gamma_cons_gamma_tail [in IPC.In_Gamma]
in_ngamma_shift_a_work [in IPC.In_NGamma]
in_ngamma_shift_work_a [in IPC.In_NGamma]
in_ngamma_shift_ai_work [in IPC.In_NGamma]
in_ngamma_shift_work_ai_old [in IPC.In_NGamma]
in_ngamma_shift_work_ai_new [in IPC.In_NGamma]
in_ngamma_shift_ni_x_ni_work [in IPC.In_NGamma]
in_ngamma_shift_work_ni_x_ni [in IPC.In_NGamma]
in_ngamma_shift_ni_work [in IPC.In_NGamma]
in_ngamma_shift_work_ni [in IPC.In_NGamma]
in_ngamma_shift_ds_work [in IPC.In_NGamma]
in_ngamma_shift_work_ds [in IPC.In_NGamma]
in_ngamma_ins_a_rev [in IPC.In_NGamma]
in_ngamma_ins_a_head [in IPC.In_NGamma]
in_ngamma_ins_a_tail [in IPC.In_NGamma]
in_ngamma_del_ai_rev [in IPC.In_NGamma]
in_ngamma_del_ai_tail [in IPC.In_NGamma]
in_ngamma_ins_ai_rev [in IPC.In_NGamma]
in_ngamma_ins_ai_head_old [in IPC.In_NGamma]
in_ngamma_ins_ai_head_new [in IPC.In_NGamma]
in_ngamma_ins_ai_tail [in IPC.In_NGamma]
in_ngamma_ni_eq [in IPC.In_NGamma]
in_ngamma_ni_x_ni_rev [in IPC.In_NGamma]
in_ngamma_ni_x_ni_tail [in IPC.In_NGamma]
in_ngamma_ni_x_ni_head [in IPC.In_NGamma]
in_ngamma_cons_ni_rev [in IPC.In_NGamma]
in_ngamma_cons_ni_head [in IPC.In_NGamma]
in_ngamma_cons_ni_tail [in IPC.In_NGamma]
in_ngamma_cons_ds_rev [in IPC.In_NGamma]
in_ngamma_cons_ds_head [in IPC.In_NGamma]
in_ngamma_cons_ds_tail [in IPC.In_NGamma]
in_ngamma_cons_work_rev [in IPC.In_NGamma]
in_ngamma_work_app_rev [in IPC.In_NGamma]
in_ngamma_work_app1 [in IPC.In_NGamma]
in_ngamma_cons_work_head [in IPC.In_NGamma]
in_ngamma_cons_work_tail [in IPC.In_NGamma]
in_nth [in IPC.My_Nth]
is_monotone_tree_is_monotone [in IPC.Trees]
is_monotone_successor [in IPC.Trees]
is_monotone_tree_successor [in IPC.Trees]
is_balanced_is_balanced_right_shift [in IPC.AvlTrees]
is_balanced_avl_is_balanced_avl_right_shift_left [in IPC.AvlTrees]
is_balanced_avl_is_balanced_avl_right_shift_false [in IPC.AvlTrees]
is_balanced_avl_is_balanced_avl_right_shift [in IPC.AvlTrees]
is_balanced_is_balanced_left_shift_false [in IPC.AvlTrees]
is_left_balanced_is_left_balanced_left_shift [in IPC.AvlTrees]
is_above_avl_is_above [in IPC.AvlTrees]
is_below_avl_is_below [in IPC.AvlTrees]
is_avl_is_balanced [in IPC.AvlTrees]
is_balanced_avl_is_balanced [in IPC.AvlTrees]
is_avl_rec [in IPC.AvlTrees]
K
kripke_tree_succ [in IPC.Kripke_Trees]kripke_tree_kripke_model [in IPC.Kripke_Trees]
L
leave_is_avl [in IPC.AvlTrees]left_nimp [in IPC.NRules]
left_disj [in IPC.NRules]
left_p_imp_ai [in IPC.NRules]
left_p_imp_work [in IPC.NRules]
le_ni_app_dd [in IPC.Le_Ks]
le_ni_app_dn [in IPC.Le_Ks]
le_ni_app_nn [in IPC.Le_Ks]
le_app0 [in IPC.Le_Ks]
le_eqv [in IPC.Le_Ks]
le_ni_trans [in IPC.Le_Ks]
le_ni_refl [in IPC.Le_Ks]
le_ks_le_count_undecs [in IPC.Lt_Ks]
le_ni_le_count_undecs [in IPC.Lt_Ks]
le_n_max2 [in IPC.My_Arith]
le_n_max1 [in IPC.My_Arith]
le_reg [in IPC.My_Arith]
LOOKUP_DEC [in IPC.AvlTrees]
lookup_dec [in IPC.AvlTrees]
lookup_avl_equal [in IPC.AvlTrees]
lookup_avl_inv_greater [in IPC.AvlTrees]
lookup_avl_inv_less [in IPC.AvlTrees]
lookup_avl_inv_equal [in IPC.AvlTrees]
lookup_above_false [in IPC.AvlTrees]
lookup_below_false [in IPC.AvlTrees]
lookup_below_lookup [in IPC.AvlTrees]
lookup_above_lookup [in IPC.AvlTrees]
lookup_greater_above [in IPC.AvlTrees]
lookup_less_below [in IPC.AvlTrees]
lookup_above_greater [in IPC.AvlTrees]
lookup_below_less [in IPC.AvlTrees]
lt_ks_shift_dd [in IPC.Lt_Ks]
lt_ks_shift_nd [in IPC.Lt_Ks]
lt_plus_assoc_l [in IPC.My_Arith]
M
max_int_of_list [in IPC.Forms]max_int_of_form [in IPC.Forms]
max_n_O [in IPC.My_Arith]
max_n_Sn [in IPC.My_Arith]
max_Sn_n [in IPC.My_Arith]
max_n_n [in IPC.My_Arith]
max_int [in IPC.ML_Int]
minimal_cons_gamma_weak2 [in IPC.Minimal]
minimal_cons_gamma_weak [in IPC.Minimal]
minimal_cons_gamma_cons_context [in IPC.Minimal]
minimal_shift_work_gamma [in IPC.Minimal]
minimal_shift_gamma_work [in IPC.Minimal]
minimal_derivable_forces [in IPC.Minimal]
My_Lt_Ks_rec [in IPC.Lt_Ks]
My_Tree_rec [in IPC.Trees]
My_Tree_ind [in IPC.Trees]
my_lt_weak [in IPC.My_Arith]
my_nth_split [in IPC.My_Nth]
my_nth_rec [in IPC.My_Nth]
N
nax [in IPC.NRules]nefq [in IPC.NRules]
nested_imps2nimps_length [in IPC.In_NGamma]
nested_imps2nimps_app [in IPC.In_NGamma]
nminimal_cons_work_cons_context [in IPC.NMinimal]
nminimal_shift_ds_work_context [in IPC.NMinimal]
nminimal_shift_work_ai_weak [in IPC.NMinimal]
nminimal_cons_work_weak [in IPC.NMinimal]
nminimal_cons_work_strength [in IPC.NMinimal]
nminimal_shift_ni_x_ni_work [in IPC.NMinimal]
nminimal_shift_work_ni_x_ni [in IPC.NMinimal]
nminimal_shift_work_a [in IPC.NMinimal]
nminimal_shift_work_ai_old [in IPC.NMinimal]
nminimal_shift_work_ai_new [in IPC.NMinimal]
nminimal_shift_work_ni [in IPC.NMinimal]
nminimal_shift_work_ds [in IPC.NMinimal]
nminimal_eqv [in IPC.NMinimal]
nminimal_derivable_forces [in IPC.NMinimal]
nsearch [in IPC.NSearch]
nsearch_aux [in IPC.NSearch]
nsound_shift_work_ai_strength [in IPC.NSound]
nsound_cons_work_weak [in IPC.NSound]
nsound_cons_work_cons_context [in IPC.NSound]
nsound_del_ai [in IPC.NSound]
nsound_cons_ds_tail [in IPC.NSound]
nsound_app_work [in IPC.NSound]
nsound_shift_ni_x_ni_work [in IPC.NSound]
nsound_shift_work_ni_x_ni [in IPC.NSound]
nsound_shift_work_a [in IPC.NSound]
nsound_shift_work_ai [in IPC.NSound]
nsound_shift_work_ni [in IPC.NSound]
nsound_shift_work_ds [in IPC.NSound]
nsound_ge [in IPC.NSound]
nsound_le [in IPC.NSound]
nsound_eqv [in IPC.NSound]
nth_nimp__nth_nested_imp [in IPC.Cons_Counter_Model]
nth_app1 [in IPC.My_Nth]
nth_app0 [in IPC.My_Nth]
nth_in [in IPC.My_Nth]
nweight_sequent_left_disj_right [in IPC.NWeight]
nweight_sequent_left_disj_left [in IPC.NWeight]
nweight_sequent_nimp_right [in IPC.NWeight]
nweight_sequent_nimp_left [in IPC.NWeight]
nweight_sequent_eqv [in IPC.NWeight]
nweight_shift_ai_work [in IPC.NWeight]
nweight_shift_work_ai [in IPC.NWeight]
nweight_shift_work_ds [in IPC.NWeight]
nweight_shift_work_ni0 [in IPC.NWeight]
nweight_rev_app [in IPC.NWeight]
nweight_eqv_ni [in IPC.NWeight]
nweight_ai_del [in IPC.NWeight]
nweight_ai_ins [in IPC.NWeight]
nweight_ai_perm [in IPC.NWeight]
nweight_work_app [in IPC.NWeight]
n_Sn_false [in IPC.My_Arith]
P
plus_reg [in IPC.My_Arith]plus_O [in IPC.My_Arith]
R
rebalance_right [in IPC.AvlTrees]rebalance_left [in IPC.AvlTrees]
regular_EQUIV_INS [in IPC.Regular_Avl]
regular_EQUIV_DEL [in IPC.Regular_Avl]
regular_AVL_NIL [in IPC.Regular_Avl]
regular_equiv_ins [in IPC.Regular_Avl]
regular_equiv_del [in IPC.Regular_Avl]
regular_nil [in IPC.Regular_Avl]
rev_app_lemma2 [in IPC.Rev_App]
rev_app_lemma1 [in IPC.Rev_App]
rev_app_lemma0 [in IPC.Rev_App]
rev_app_app [in IPC.Rev_App]
rule_shift_work_a [in IPC.NRules]
rule_shift_work_ai_old [in IPC.NRules]
rule_shift_work_ai_new [in IPC.NRules]
rule_shift_work_ni0 [in IPC.NRules]
rule_shift_work_ds [in IPC.NRules]
rule_a_imp_b_imp_c_gamma [in IPC.Rules]
rule_atom_imp_b_imp_c_gamma [in IPC.Rules]
rule_atom_imp_atom_imp_c_gamma [in IPC.Rules]
rule_vimp_imp_falsum_imp_gamma [in IPC.Rules]
rule_vimp_falsum_imp_imp_gamma [in IPC.Rules]
rule_vimp_or_imp_gamma_new [in IPC.Rules]
rule_vimp_or_imp_gamma [in IPC.Rules]
rule_vimp_and_imp_gamma [in IPC.Rules]
rule_vimp_atom_imp_b_gamma [in IPC.Rules]
rule_vimp_falsum_imp_b_gamma [in IPC.Rules]
rule_vimp_a_or_b_gamma [in IPC.Rules]
rule_vimp_atom_or_a_gamma [in IPC.Rules]
rule_vimp_a_or_falsum_gamma [in IPC.Rules]
rule_vimp_falsum_or_a_gamma [in IPC.Rules]
rule_vimp_conj_gamma_new [in IPC.Rules]
rule_vimp_conj_gamma [in IPC.Rules]
rule_gamma_a [in IPC.Rules]
rule_gamma_a_imp_b [in IPC.Rules]
rule_gamma_falsum [in IPC.Rules]
rule_vimp_imp_gamma [in IPC.Rules]
rule_vimp_a_gamma [in IPC.Rules]
rule_shift_gamma_work [in IPC.Rules]
S
search [in IPC.Search]search_goal_invariant [in IPC.Search]
search_atom_aux [in IPC.Search]
search_spec_subst_gamma_pos [in IPC.Rules]
shift_ni_dni [in IPC.NRules]
snd_order_inst [in IPC.Derivable_Tools]
soundness [in IPC.Kripke_Trees]
soundness_t [in IPC.Kripke_Trees]
sound_cons_gamma_weak2 [in IPC.Sound]
sound_cons_gamma_weak [in IPC.Sound]
sound_cons_gamma_cons_context [in IPC.Sound]
sound_shift_work_gamma [in IPC.Sound]
sound_shift_gamma_work [in IPC.Sound]
sound_cons_gamma_head [in IPC.Sound]
sound_cons_gamma_tail [in IPC.Sound]
sound_cons_gamma [in IPC.Sound]
subst_vimp_head [in IPC.Forms]
subst_list_below [in IPC.Forms]
subst_form_below [in IPC.Forms]
subst_nth [in IPC.Forms]
Succs_Tree_ind [in IPC.Trees]
succs_refl [in IPC.Trees]
succs_trans [in IPC.Trees]
S_reg [in IPC.My_Arith]
V
vimp_eq_nvimp [in IPC.Normal_Forms]vimp2nform [in IPC.Normal_Forms]
vimp2nvimp [in IPC.Normal_Forms]
vlist_eq [in IPC.Search]
W
weight_gamma_weak3' [in IPC.Weight]weight_gamma_weak3 [in IPC.Weight]
weight_gamma_weak2' [in IPC.Weight]
weight_gamma_weak2 [in IPC.Weight]
weight_gamma_weak' [in IPC.Weight]
weight_gamma_weak [in IPC.Weight]
weight_vimp [in IPC.Weight]
weight_neg_le [in IPC.Weight]
weight_ge_1 [in IPC.Weight]
Constructor Index
A
Above_Avl_Node [in IPC.AvlTrees]Above_Avl_Nil [in IPC.AvlTrees]
Above_Node [in IPC.AvlTrees]
Above_Nil [in IPC.AvlTrees]
Abs [in IPC.Derivations]
AImp [in IPC.Normal_Forms]
AndF [in IPC.Forms]
AndFElimL [in IPC.Derivations]
AndFElimR [in IPC.Derivations]
AndFIntro [in IPC.Derivations]
App [in IPC.Derivations]
Atom [in IPC.Forms]
AVL_intro [in IPC.AvlTrees]
Avl_Ins_Spec_Intro [in IPC.AvlTrees]
Avl_Node [in IPC.AvlTrees]
Avl_Nil [in IPC.AvlTrees]
B
Balanced [in IPC.AvlTrees]Balance_Shrunk_Right_Spec_Intro [in IPC.AvlTrees]
Balance_Shrunk_Left_Spec_Intro [in IPC.AvlTrees]
Balance_Grow_Right_Spec_Intro [in IPC.AvlTrees]
Balance_Grow_Left_Spec_Intro [in IPC.AvlTrees]
Below_Avl_Node [in IPC.AvlTrees]
Below_Avl_Nil [in IPC.AvlTrees]
Below_Node [in IPC.AvlTrees]
Below_Nil [in IPC.AvlTrees]
ByAbsurdity [in IPC.Derivations]
ByAssumption [in IPC.Derivations]
C
Cas [in IPC.Derivations]cons_counter_model_intro [in IPC.Cons_Counter_Model]
Cons_Forest [in IPC.Trees]
D
Decorated [in IPC.In_NGamma]Delete_Spec_Intro [in IPC.AvlTrees]
Del_Max_Spec_Intro [in IPC.AvlTrees]
derivable [in IPC.Search]
derivable [in IPC.Rules]
Derivable_Intro [in IPC.Derivable_Def_dont_compute_derivations]
Derivable_Intro [in IPC.Derivable_Def_compute_derivations]
Derivable2_Intro [in IPC.Derivable_Def_dont_compute_derivations]
Derivable2_Intro [in IPC.Derivable_Def_compute_derivations]
E
Efq [in IPC.Derivations]equiv_del_intro [in IPC.AvlTrees]
equiv_ins_intro [in IPC.AvlTrees]
equiv_intro [in IPC.AvlTrees]
Eqv_NI_Cons_ND [in IPC.Le_Ks]
Eqv_NI_Cons_DD [in IPC.Le_Ks]
Eqv_NI_Cons_DN [in IPC.Le_Ks]
Eqv_NI_Cons_NN [in IPC.Le_Ks]
Eqv_NI_Nil [in IPC.Le_Ks]
F
Falsum [in IPC.Forms]Filter_Deco_Spec_Intro [in IPC.Le_Ks]
H
Hasnot_Shrunk_Right_Shift_Right [in IPC.AvlTrees]Hasnot_Shrunk_Right_Shift_Balanced [in IPC.AvlTrees]
Hasnot_Shrunk_Right_Bal [in IPC.AvlTrees]
Hasnot_Shrunk_Left_Shift_Balanced [in IPC.AvlTrees]
Hasnot_Shrunk_Left_Shift_Left [in IPC.AvlTrees]
Hasnot_Shrunk_Left_Bal [in IPC.AvlTrees]
Hasnot_Grown_Right_Shift_Right [in IPC.AvlTrees]
Hasnot_Grown_Right_Shift_Left [in IPC.AvlTrees]
Hasnot_Grown_Right_Bal [in IPC.AvlTrees]
Hasnot_Grown_Left_Shift_Right [in IPC.AvlTrees]
Hasnot_Grown_Left_Shift_Left [in IPC.AvlTrees]
Hasnot_Grown_Left_Bal [in IPC.AvlTrees]
Has_Shrunk_Right_Shift_Right [in IPC.AvlTrees]
Has_Shrunk_Right_Shift_Left [in IPC.AvlTrees]
Has_Shrunk_Left_Shift_Right [in IPC.AvlTrees]
Has_Shrunk_Left_Shift_Left [in IPC.AvlTrees]
Has_Grown_Right_Shift_Right [in IPC.AvlTrees]
Has_Grown_Right_Shift_Balanced [in IPC.AvlTrees]
Has_Grown_Left_Shift_Balanced [in IPC.AvlTrees]
Has_Grown_Left_Shift_Left [in IPC.AvlTrees]
I
Imp [in IPC.Forms]ImpElim [in IPC.Derivations]
ImpIntro [in IPC.Derivations]
Inf_Deco_Spec_Intro [in IPC.Le_Ks]
Inv_Nth_App1 [in IPC.My_Nth]
Inv_Nth_App0 [in IPC.My_Nth]
in_succs [in IPC.Trees]
in_leave [in IPC.Trees]
in_forest_tail [in IPC.Trees]
in_forest_head [in IPC.Trees]
In_Work1 [in IPC.In_Gamma]
In_Gamma [in IPC.In_Gamma]
In_NGamma_Del_AI_Rev_Spec_Intro [in IPC.In_NGamma]
In_Atoms [in IPC.In_NGamma]
In_Atomic_Imps [in IPC.In_NGamma]
In_Nested_Imps [in IPC.In_NGamma]
In_Disjs [in IPC.In_NGamma]
In_Work [in IPC.In_NGamma]
is_monotone_intro [in IPC.Trees]
is_monotone_forest_cons [in IPC.Trees]
is_monotone_forest_nil [in IPC.Trees]
is_monotone_tree_intro [in IPC.Trees]
Is_Right_Balanced_Avl_Right_Shift [in IPC.AvlTrees]
Is_Fully_Balanced_Avl_Right_Shift [in IPC.AvlTrees]
Is_Left_Balanced_Avl_Right_Shift [in IPC.AvlTrees]
Is_Right_Balanced_Avl_Left_Shift [in IPC.AvlTrees]
Is_Fully_Balanced_Avl_Left_Shift [in IPC.AvlTrees]
Is_Left_Balanced_Avl_Left_Shift [in IPC.AvlTrees]
Is_Right_Balanced_Avl [in IPC.AvlTrees]
Is_Fully_Balanced_Avl [in IPC.AvlTrees]
Is_Left_Balanced_Avl [in IPC.AvlTrees]
Is_Right_Balanced [in IPC.AvlTrees]
Is_Fully_Balanced [in IPC.AvlTrees]
Is_Left_Balanced [in IPC.AvlTrees]
K
kripke_model [in IPC.Kripke_Trees]k_deco_sound_intro [in IPC.NDeco_Sound]
L
Left_Balanced [in IPC.AvlTrees]Le_App_Spec_Intro [in IPC.Le_Ks]
Le_NI_Cons_DD [in IPC.Le_Ks]
Le_NI_Cons_DN [in IPC.Le_Ks]
Le_NI_Cons_NN [in IPC.Le_Ks]
Le_NI_Nil [in IPC.Le_Ks]
Lin_Del_Spec_Intro [in IPC.AvlTrees]
Lin_Ins_Update [in IPC.AvlTrees]
Lin_Ins_New [in IPC.AvlTrees]
Lookup [in IPC.AvlTrees]
Lookup_Right [in IPC.AvlTrees]
Lookup_Left [in IPC.AvlTrees]
Lookup_Equal [in IPC.AvlTrees]
lt_ks_length [in IPC.Lt_Ks]
lt_ks_count_undecs [in IPC.Lt_Ks]
M
Max_Int_Intro [in IPC.ML_Int]My_NthS [in IPC.My_Nth]
My_NthO [in IPC.My_Nth]
N
NAtom [in IPC.Normal_Forms]NDerivable [in IPC.NRules]
NDisj [in IPC.Normal_Forms]
NFalsum [in IPC.Normal_Forms]
Nil_Forest [in IPC.Trees]
Nil_Is_Avl [in IPC.AvlTrees]
NImp [in IPC.Normal_Forms]
NImp_NF [in IPC.Normal_Forms]
node [in IPC.Trees]
Node_Is_Avl [in IPC.AvlTrees]
Not_Lookup [in IPC.AvlTrees]
NRefutable [in IPC.NRules]
NSearch_Res [in IPC.NRules]
Nth_Split_Intro [in IPC.My_Nth]
O
OrF [in IPC.Forms]OrFElim [in IPC.Derivations]
OrFIntroL [in IPC.Derivations]
OrFIntroR [in IPC.Derivations]
OrFL [in IPC.Derivations]
OrFR [in IPC.Derivations]
P
Pair [in IPC.Derivations]PrL [in IPC.Derivations]
PrR [in IPC.Derivations]
R
refutable [in IPC.Search]refutable [in IPC.Rules]
Rev_App_Spec_Intro [in IPC.Rev_App]
Right_Balanced [in IPC.AvlTrees]
S
Shift [in IPC.Derivations]ShiftIntro [in IPC.Derivations]
successor_trans [in IPC.Trees]
successor_refl [in IPC.Trees]
U
Undecorated [in IPC.In_NGamma]V
Var [in IPC.Derivations]Axiom Index
E
Equal [in IPC.ML_Int]equal_eq [in IPC.ML_Int]
equal_refl [in IPC.ML_Int]
equal_trans [in IPC.ML_Int]
equal_sym [in IPC.ML_Int]
equal_less_less [in IPC.ML_Int]
equal_dec [in IPC.ML_Int]
I
Int [in IPC.ML_Int]int_null [in IPC.ML_Int]
int_succ [in IPC.ML_Int]
L
Less [in IPC.ML_Int]less_irrefl [in IPC.ML_Int]
less_equal_less [in IPC.ML_Int]
less_trans [in IPC.ML_Int]
less_dec [in IPC.ML_Int]
N
notequal_notless_greater [in IPC.ML_Int]Inductive Index
A
AVL [in IPC.AvlTrees]avl_ins_spec [in IPC.AvlTrees]
avl_tree [in IPC.AvlTrees]
B
bal [in IPC.AvlTrees]bal_shrunk_right_spec [in IPC.AvlTrees]
bal_shrunk_left_spec [in IPC.AvlTrees]
bal_grow_right_spec [in IPC.AvlTrees]
bal_grow_left_spec [in IPC.AvlTrees]
C
Cons_Counter_Model_Spec [in IPC.Cons_Counter_Model]D
delete_spec [in IPC.AvlTrees]delete_max_spec [in IPC.AvlTrees]
Derivable [in IPC.Derivable_Def_dont_compute_derivations]
Derivable [in IPC.Derivable_Def_compute_derivations]
Derivable2 [in IPC.Derivable_Def_dont_compute_derivations]
Derivable2 [in IPC.Derivable_Def_compute_derivations]
derives [in IPC.Derivations]
E
equiv [in IPC.AvlTrees]equiv_del [in IPC.AvlTrees]
equiv_ins [in IPC.AvlTrees]
eqv_ni [in IPC.Le_Ks]
F
filter_deco_spec [in IPC.Le_Ks]Forest [in IPC.Trees]
form [in IPC.Forms]
H
hasnot_shrunk_right [in IPC.AvlTrees]hasnot_shrunk_left [in IPC.AvlTrees]
hasnot_grown_right [in IPC.AvlTrees]
hasnot_grown_left [in IPC.AvlTrees]
has_shrunk_right [in IPC.AvlTrees]
has_shrunk_left [in IPC.AvlTrees]
has_grown_right [in IPC.AvlTrees]
has_grown_left [in IPC.AvlTrees]
I
inf_deco_spec [in IPC.Le_Ks]inv_my_nth_app [in IPC.My_Nth]
In_tree [in IPC.Trees]
In_Forest [in IPC.Trees]
in_gamma [in IPC.In_Gamma]
in_ngamma_del_ai_rev_spec [in IPC.In_NGamma]
in_ngamma [in IPC.In_NGamma]
Is_Monotone [in IPC.Trees]
Is_Monotone_Forest [in IPC.Trees]
Is_Monotone_Tree [in IPC.Trees]
is_balanced_avl_right_shift [in IPC.AvlTrees]
is_balanced_avl_left_shift [in IPC.AvlTrees]
is_avl [in IPC.AvlTrees]
is_balanced_avl [in IPC.AvlTrees]
is_above_avl [in IPC.AvlTrees]
is_below_avl [in IPC.AvlTrees]
is_balanced [in IPC.AvlTrees]
is_above [in IPC.AvlTrees]
is_below [in IPC.AvlTrees]
K
Kripke_Model [in IPC.Kripke_Trees]k_deco_sound [in IPC.NDeco_Sound]
L
le_app_spec [in IPC.Le_Ks]le_ni [in IPC.Le_Ks]
lin_del_spec [in IPC.AvlTrees]
lin_ins_spec [in IPC.AvlTrees]
lookup [in IPC.AvlTrees]
lookup_dec_spec [in IPC.AvlTrees]
Lt_Ks [in IPC.Lt_Ks]
M
max_int_spec [in IPC.ML_Int]my_nth [in IPC.My_Nth]
N
nested_imp [in IPC.In_NGamma]nimp [in IPC.Normal_Forms]
normal_form [in IPC.Normal_Forms]
nsearch_spec_result [in IPC.NRules]
nsearch_spec_result_aux [in IPC.NRules]
nth_split [in IPC.My_Nth]
P
proof_term [in IPC.Derivations]R
rev_app_spec [in IPC.Rev_App]S
search_spec [in IPC.Search]search_spec_aux [in IPC.Rules]
Successor [in IPC.Trees]
T
Tree [in IPC.Trees]Section Index
A
avl_trees [in IPC.AvlTrees]M
My_Nth [in IPC.My_Nth]R
Regular_Avl [in IPC.Regular_Avl]T
Trees [in IPC.Trees]Definition Index
A
AI_Nil [in IPC.In_NGamma]ANil [in IPC.Kripke_Trees]
Atms [in IPC.Kripke_Trees]
atomic_imps [in IPC.In_NGamma]
atoms [in IPC.Kripke_Trees]
AVL_NIL [in IPC.AvlTrees]
a_goal_disj [in IPC.Disjunct]
a_ai_disj [in IPC.Disjunct]
B
below_list [in IPC.Forms]below_form [in IPC.Forms]
C
count_undecs [in IPC.Lt_Ks]D
decorated_nested_imp2form [in IPC.Rev_App]decorated_nested_imp2k [in IPC.Rev_App]
decorated_nested_imp2nimp [in IPC.Rev_App]
decorated_nested_imps [in IPC.Rev_App]
decorated_nested_imp [in IPC.Rev_App]
deco_sound [in IPC.NDeco_Sound]
DELETE_Spec [in IPC.AvlTrees]
disj [in IPC.In_NGamma]
disjs [in IPC.In_NGamma]
disjs2forms [in IPC.In_NGamma]
disjs2nforms [in IPC.In_NGamma]
disj2form [in IPC.In_NGamma]
disj2nform [in IPC.In_NGamma]
DNil [in IPC.In_NGamma]
DNI_NIL [in IPC.Rev_App]
E
EQUIV_DEL [in IPC.AvlTrees]EQUIV_INS [in IPC.AvlTrees]
F
flist [in IPC.Forms]fnil [in IPC.Forms]
forces [in IPC.Kripke_Trees]
forces_ngamma [in IPC.Forces_NGamma]
forces_gamma [in IPC.Forces_Gamma]
forces_t [in IPC.Kripke_Trees]
forces_t2 [in IPC.Kripke_Trees]
forces0_t [in IPC.Kripke_Trees]
H
height [in IPC.AvlTrees]height_forest [in IPC.Trees]
height_tree [in IPC.Trees]
height_avl [in IPC.AvlTrees]
I
INSRT_Spec [in IPC.AvlTrees]Is_Monotone_Kripke_Forest [in IPC.Kripke_Trees]
Is_Monotone_kripke_tree [in IPC.Kripke_Trees]
K
Kripke_Forest [in IPC.Kripke_Trees]kripke_tree [in IPC.Kripke_Trees]
L
LIN_DEL [in IPC.AvlTrees]LIN_INS [in IPC.AvlTrees]
LIN_AVL [in IPC.AvlTrees]
lin_avl [in IPC.AvlTrees]
list2vlist [in IPC.Search]
LOOKUP [in IPC.AvlTrees]
LOOKUP_Dec_Spec [in IPC.AvlTrees]
M
max [in IPC.My_Arith]minimal [in IPC.Minimal]
N
nested_imps2nimps [in IPC.In_NGamma]nested_imps2nforms [in IPC.In_NGamma]
nested_imps2forms [in IPC.In_NGamma]
nested_imps [in IPC.In_NGamma]
nested_imp2nform [in IPC.In_NGamma]
nested_imp2form [in IPC.In_NGamma]
nested_imp2nimp [in IPC.In_NGamma]
nf_nil [in IPC.Normal_Forms]
nf_list [in IPC.Normal_Forms]
nf2form [in IPC.Normal_Forms]
nimp2form [in IPC.Normal_Forms]
nminimal [in IPC.NMinimal]
NNil [in IPC.In_NGamma]
nsearch_spec [in IPC.NRules]
nsearch_invariant [in IPC.NSearch]
nsound [in IPC.NSound]
nvimp [in IPC.Normal_Forms]
nweight [in IPC.NWeight]
nweight_Sequent [in IPC.NWeight]
nweight_ai [in IPC.NWeight]
nweight_ibs [in IPC.NWeight]
nweight_bs [in IPC.NWeight]
nweight_atomicimp [in IPC.NWeight]
nweight_dni [in IPC.NWeight]
nweight_decoratednestedimp [in IPC.NWeight]
nweight_ni [in IPC.NWeight]
nweight_nestedimp [in IPC.NWeight]
nweight_ds [in IPC.NWeight]
nweight_disj [in IPC.NWeight]
nweight_work [in IPC.NWeight]
n2forest [in IPC.Cons_Counter_Model]
R
rebalance_right_spec [in IPC.AvlTrees]rebalance_left_spec [in IPC.AvlTrees]
REGULAR [in IPC.Regular_Avl]
Regular [in IPC.Regular_Avl]
rev_app [in IPC.Rev_App]
root [in IPC.Trees]
S
search_atom_invariant [in IPC.Search]search_spec [in IPC.Rules]
sound [in IPC.Sound]
subst_list [in IPC.Forms]
subst_form [in IPC.Forms]
Suc [in IPC.Kripke_Trees]
successors [in IPC.Trees]
Succs [in IPC.Kripke_Trees]
V
vimp [in IPC.Forms]vlist [in IPC.Search]
vlist2hlist [in IPC.Search]
vlist2list [in IPC.Search]
W
weight [in IPC.Weight]weight_gamma [in IPC.Weight]
weight_goal [in IPC.Weight]
weight_neg [in IPC.Weight]
| 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 | (877 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 | (6 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 | (35 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 | (479 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 | (157 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 | (16 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 | (73 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 | (4 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 | (107 entries) |