| 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 | (1232 entries) |
| Notation 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 | (17 entries) |
| Module 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 | (44 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 | (69 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 | (21 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 | (618 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 | (129 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 | (42 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 | (55 entries) |
| Projection 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 | (10 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 | (20 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 | (203 entries) |
| Record 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) |
Global Index
A
accElim3 [lemma, in Cantor.prelude.AccP]AccElim3 [lemma, in Cantor.prelude.AccP]
AccP [library]
acc_trans [lemma, in Cantor.prelude.closure]
Acc_iter_partial [definition, in Cantor.prelude.PartialFix]
acc_imp [lemma, in Cantor.prelude.not_decreasing]
ap [inductive, in Cantor.epsilon0.EPSILON0]
ap [inductive, in Cantor.gamma0.Gamma0_prelude]
app [definition, in Cantor.epsilon0.MSE0]
app_equiv_assoc [lemma, in Cantor.epsilon0.MSE0]
app_equiv_comm [lemma, in Cantor.epsilon0.MSE0]
ap_plusR [lemma, in Cantor.epsilon0.EPSILON0]
ap_plus [lemma, in Cantor.epsilon0.EPSILON0]
ap_phi0R [lemma, in Cantor.epsilon0.EPSILON0]
ap_phi0 [lemma, in Cantor.epsilon0.EPSILON0]
ap_intro [constructor, in Cantor.epsilon0.EPSILON0]
ap_intro [constructor, in Cantor.gamma0.Gamma0_prelude]
B
base [projection, in Cantor.misc.G4]big_number_eq [lemma, in Cantor.misc.G4]
C
Cantor_normal_form [lemma, in Cantor.epsilon0.EPSILON0]closure [library]
coeff_lt [constructor, in Cantor.epsilon0.EPSILON0]
coeff0 [projection, in Cantor.misc.G4]
coeff1 [projection, in Cantor.misc.G4]
coeff2 [projection, in Cantor.misc.G4]
compare [definition, in Cantor.epsilon0.EPSILON0]
compare [definition, in Cantor.gamma0.Gamma0]
compare_reflectR [lemma, in Cantor.epsilon0.EPSILON0]
compare_rw3 [lemma, in Cantor.epsilon0.EPSILON0]
compare_rw2 [lemma, in Cantor.epsilon0.EPSILON0]
compare_rw1 [lemma, in Cantor.epsilon0.EPSILON0]
compare_reflect [lemma, in Cantor.epsilon0.EPSILON0]
compare_ok_1 [lemma, in Cantor.epsilon0.EPSILON0]
compare_rw_gt [lemma, in Cantor.gamma0.Gamma0]
compare_rw_eq [lemma, in Cantor.gamma0.Gamma0]
compare_rw_lt [lemma, in Cantor.gamma0.Gamma0]
compare_gt_rw [lemma, in Cantor.gamma0.Gamma0]
compare_eq_rw [lemma, in Cantor.gamma0.Gamma0]
compare_lt_rw [lemma, in Cantor.gamma0.Gamma0]
compare_reflect [lemma, in Cantor.gamma0.Gamma0]
cons [constructor, in Cantor.epsilon0.EPSILON0]
cons [constructor, in Cantor.gamma0.Gamma0_prelude]
cons_unicity [lemma, in Cantor.epsilon0.EPSILON0]
cons_ambiguity [lemma, in Cantor.epsilon0.EPSILON0]
cons_nf [constructor, in Cantor.epsilon0.EPSILON0]
cons_lt_e0 [constructor, in Cantor.gamma0.Gamma0_prelude]
cons_nf [constructor, in Cantor.gamma0.Gamma0_prelude]
cons_lt_epsilon0 [lemma, in Cantor.gamma0.Gamma0]
cons_succ [constructor, in Cantor.gamma0.Gamma0]
cons_rw [lemma, in Cantor.gamma0.Gamma0]
Cons_correct [constructor, in Cantor.epsilon0.Goodstein]
correct [inductive, in Cantor.epsilon0.Goodstein]
correct_succ [lemma, in Cantor.epsilon0.Goodstein]
D
decidable_set [library]depth1 [constructor, in Cantor.epsilon0.Hydra]
depth2 [constructor, in Cantor.epsilon0.Hydra]
dickson [library]
E
epsilon [definition, in Cantor.gamma0.Gamma0_prelude]epsilon_fxp [lemma, in Cantor.gamma0.Gamma0]
epsilon0 [definition, in Cantor.gamma0.Gamma0_prelude]
EPSILON0 [library]
epsilon0_as_lub [lemma, in Cantor.gamma0.Gamma0]
Eps0_rpo [module, in Cantor.epsilon0.EPSILON0]
Eps0_alg [module, in Cantor.epsilon0.EPSILON0]
Eps0_prec.prec_transitive [lemma, in Cantor.epsilon0.EPSILON0]
Eps0_prec.prec_antisym [lemma, in Cantor.epsilon0.EPSILON0]
Eps0_prec.prec_dec [lemma, in Cantor.epsilon0.EPSILON0]
Eps0_prec.status [definition, in Cantor.epsilon0.EPSILON0]
Eps0_prec.Mul [constructor, in Cantor.epsilon0.EPSILON0]
Eps0_prec.Lex [constructor, in Cantor.epsilon0.EPSILON0]
Eps0_prec.status_type [inductive, in Cantor.epsilon0.EPSILON0]
Eps0_prec.prec [definition, in Cantor.epsilon0.EPSILON0]
Eps0_prec.A [definition, in Cantor.epsilon0.EPSILON0]
Eps0_prec [module, in Cantor.epsilon0.EPSILON0]
Eps0_sig.arity [definition, in Cantor.epsilon0.EPSILON0]
Eps0_sig.Free [constructor, in Cantor.epsilon0.EPSILON0]
Eps0_sig.C [constructor, in Cantor.epsilon0.EPSILON0]
Eps0_sig.AC [constructor, in Cantor.epsilon0.EPSILON0]
Eps0_sig.arity_type [inductive, in Cantor.epsilon0.EPSILON0]
Eps0_sig.eq_symbol_dec [lemma, in Cantor.epsilon0.EPSILON0]
Eps0_sig.symb [definition, in Cantor.epsilon0.EPSILON0]
Eps0_sig.ord_cons [constructor, in Cantor.epsilon0.EPSILON0]
Eps0_sig.ord_zero [constructor, in Cantor.epsilon0.EPSILON0]
Eps0_sig.nat_S [constructor, in Cantor.epsilon0.EPSILON0]
Eps0_sig.nat_0 [constructor, in Cantor.epsilon0.EPSILON0]
Eps0_sig.symb0 [inductive, in Cantor.epsilon0.EPSILON0]
Eps0_sig [module, in Cantor.epsilon0.EPSILON0]
equiv [definition, in Cantor.epsilon0.MSE0]
equiv_cong2 [lemma, in Cantor.epsilon0.MSE0]
equiv_cong1 [lemma, in Cantor.epsilon0.MSE0]
equiv_perm [lemma, in Cantor.epsilon0.MSE0]
equiv_tail [lemma, in Cantor.epsilon0.MSE0]
equiv_cons [lemma, in Cantor.epsilon0.MSE0]
equiv_trans [lemma, in Cantor.epsilon0.MSE0]
equiv_sym [lemma, in Cantor.epsilon0.MSE0]
equiv_refl [lemma, in Cantor.epsilon0.MSE0]
Euc1 [lemma, in Cantor.prelude.More_nat]
Euc2 [lemma, in Cantor.prelude.More_nat]
exists_map12_without_repetition [lemma, in Cantor.prelude.more_list]
exists_map_without_repetition [lemma, in Cantor.prelude.more_list]
exp [definition, in Cantor.epsilon0.EPSILON0]
exp_fin_omega [lemma, in Cantor.epsilon0.EPSILON0]
exp_compat [lemma, in Cantor.epsilon0.EPSILON0]
exp_F_compat [lemma, in Cantor.epsilon0.EPSILON0]
exp_F [definition, in Cantor.epsilon0.EPSILON0]
F
f [definition, in Cantor.misc.G4]Final [lemma, in Cantor.misc.G4]
final [inductive, in Cantor.misc.G4]
final_no_future [lemma, in Cantor.misc.G4]
final_intro [constructor, in Cantor.misc.G4]
find [definition, in Cantor.prelude.more_list]
find_not_mem [lemma, in Cantor.prelude.more_list]
finite [definition, in Cantor.epsilon0.EPSILON0]
finite [definition, in Cantor.gamma0.Gamma0_prelude]
finite_ltR [lemma, in Cantor.epsilon0.EPSILON0]
finite_lt [lemma, in Cantor.epsilon0.EPSILON0]
finite_succ [constructor, in Cantor.gamma0.Gamma0]
finite_is_finite [lemma, in Cantor.gamma0.Gamma0]
finite_lt_omega [lemma, in Cantor.gamma0.Gamma0]
fold_left2 [definition, in Cantor.prelude.more_list]
f_decreases [lemma, in Cantor.epsilon0.EPSILON0]
f_not_in_normal_form [lemma, in Cantor.epsilon0.EPSILON0]
f_Z [definition, in Cantor.misc.G4]
f_Sn [lemma, in Cantor.misc.G4]
F_not_lim [lemma, in Cantor.gamma0.Gamma0]
F1 [lemma, in Cantor.misc.G4]
F2 [lemma, in Cantor.misc.G4]
F27 [lemma, in Cantor.misc.G4]
F28 [lemma, in Cantor.misc.G4]
F3 [lemma, in Cantor.misc.G4]
F4 [lemma, in Cantor.misc.G4]
G
game [section, in Cantor.epsilon0.Hydra]game.str [variable, in Cantor.epsilon0.Hydra]
game.str_hy [variable, in Cantor.epsilon0.Hydra]
game.str_ok [variable, in Cantor.epsilon0.Hydra]
Gamma0 [library]
Gamma0_rpo [module, in Cantor.gamma0.Gamma0]
Gamma0_alg [module, in Cantor.gamma0.Gamma0]
Gamma0_prec.prec_transitive [lemma, in Cantor.gamma0.Gamma0]
Gamma0_prec.prec_antisym [lemma, in Cantor.gamma0.Gamma0]
Gamma0_prec.prec_dec [lemma, in Cantor.gamma0.Gamma0]
Gamma0_prec.status [definition, in Cantor.gamma0.Gamma0]
Gamma0_prec.Mul [constructor, in Cantor.gamma0.Gamma0]
Gamma0_prec.Lex [constructor, in Cantor.gamma0.Gamma0]
Gamma0_prec.status_type [inductive, in Cantor.gamma0.Gamma0]
Gamma0_prec.prec [definition, in Cantor.gamma0.Gamma0]
Gamma0_prec.A [definition, in Cantor.gamma0.Gamma0]
Gamma0_prec [module, in Cantor.gamma0.Gamma0]
Gamma0_sig.arity [definition, in Cantor.gamma0.Gamma0]
Gamma0_sig.Free [constructor, in Cantor.gamma0.Gamma0]
Gamma0_sig.C [constructor, in Cantor.gamma0.Gamma0]
Gamma0_sig.AC [constructor, in Cantor.gamma0.Gamma0]
Gamma0_sig.arity_type [inductive, in Cantor.gamma0.Gamma0]
Gamma0_sig.eq_symbol_dec [lemma, in Cantor.gamma0.Gamma0]
Gamma0_sig.symb [definition, in Cantor.gamma0.Gamma0]
Gamma0_sig.ord_cons [constructor, in Cantor.gamma0.Gamma0]
Gamma0_sig.ord_psi [constructor, in Cantor.gamma0.Gamma0]
Gamma0_sig.ord_zero [constructor, in Cantor.gamma0.Gamma0]
Gamma0_sig.nat_S [constructor, in Cantor.gamma0.Gamma0]
Gamma0_sig.nat_0 [constructor, in Cantor.gamma0.Gamma0]
Gamma0_sig.symb0 [inductive, in Cantor.gamma0.Gamma0]
Gamma0_sig [module, in Cantor.gamma0.Gamma0]
Gamma0_length [library]
Gamma0_prelude [library]
get_decomposition [definition, in Cantor.epsilon0.EPSILON0]
get_predecessor [lemma, in Cantor.prelude.More_nat]
Goodstein [library]
Goodstein_thm [lemma, in Cantor.epsilon0.Goodstein]
Goodstein_decrease [lemma, in Cantor.epsilon0.Goodstein]
goodstein_next_ord_correct [lemma, in Cantor.epsilon0.Goodstein]
goodstein_next_ord_nf [lemma, in Cantor.epsilon0.Goodstein]
goodstein_next_ord_lt [lemma, in Cantor.epsilon0.Goodstein]
goodstein_next_ord [definition, in Cantor.epsilon0.Goodstein]
goodstein_next [definition, in Cantor.epsilon0.Goodstein]
gpred [definition, in Cantor.epsilon0.Goodstein]
gpred_lt [lemma, in Cantor.epsilon0.Goodstein]
G4 [library]
G4_length [lemma, in Cantor.misc.G4]
H
hcons [constructor, in Cantor.epsilon0.Hydra]head [constructor, in Cantor.epsilon0.Hydra]
head_lt_cons [lemma, in Cantor.epsilon0.EPSILON0]
head_lt [constructor, in Cantor.epsilon0.EPSILON0]
head_at_l_S_cons [lemma, in Cantor.epsilon0.Hydra]
head_at_l_O_cons [lemma, in Cantor.epsilon0.Hydra]
head_at_l_S_nil [lemma, in Cantor.epsilon0.Hydra]
head_at_l_zero_nil [lemma, in Cantor.epsilon0.Hydra]
head_at_l_nil [lemma, in Cantor.epsilon0.Hydra]
head_at_S_cons [lemma, in Cantor.epsilon0.Hydra]
head_at_O_cons [lemma, in Cantor.epsilon0.Hydra]
head_at_S_nil [lemma, in Cantor.epsilon0.Hydra]
head_at_zero_nil [lemma, in Cantor.epsilon0.Hydra]
head_at_nil [lemma, in Cantor.epsilon0.Hydra]
head_at_l [definition, in Cantor.epsilon0.Hydra]
head_at [definition, in Cantor.epsilon0.Hydra]
Hercules_ok [definition, in Cantor.epsilon0.Hydra]
Hercules_wins [inductive, in Cantor.epsilon0.Hydra]
Hercules_strat [definition, in Cantor.epsilon0.Hydra]
Hydra [inductive, in Cantor.epsilon0.Hydra]
Hydra [library]
Hydrae [inductive, in Cantor.epsilon0.Hydra]
Hydrae_rect2 [definition, in Cantor.epsilon0.Hydra]
Hydra_strat [definition, in Cantor.epsilon0.Hydra]
Hydra_answers [lemma, in Cantor.epsilon0.Hydra]
Hydra_answers_nil [lemma, in Cantor.epsilon0.Hydra]
Hydra_rect2 [definition, in Cantor.epsilon0.Hydra]
h2o [definition, in Cantor.epsilon0.Hydra]
h2ol [definition, in Cantor.epsilon0.Hydra]
h2ol_nfs [lemma, in Cantor.epsilon0.Hydra]
h2o_nf [lemma, in Cantor.epsilon0.Hydra]
I
inj_monoR [lemma, in Cantor.gamma0.Gamma0]inj_mono [lemma, in Cantor.gamma0.Gamma0]
inv_trans [lemma, in Cantor.prelude.closure]
in_remove [lemma, in Cantor.prelude.more_list]
in_map_in [lemma, in Cantor.prelude.more_list]
in_in_map [lemma, in Cantor.prelude.more_list]
is_finite [inductive, in Cantor.gamma0.Gamma0_prelude]
is_limit_ab [lemma, in Cantor.gamma0.Gamma0]
is_limit_intro [lemma, in Cantor.gamma0.Gamma0]
is_limit_cons_inv [lemma, in Cantor.gamma0.Gamma0]
is_limit_not_succ [lemma, in Cantor.gamma0.Gamma0]
is_succ_not_lim [lemma, in Cantor.gamma0.Gamma0]
is_limit_cons [constructor, in Cantor.gamma0.Gamma0]
is_limit_0 [constructor, in Cantor.gamma0.Gamma0]
is_limit [inductive, in Cantor.gamma0.Gamma0]
is_successor [inductive, in Cantor.gamma0.Gamma0]
is_finite_finite [lemma, in Cantor.gamma0.Gamma0]
item [record, in Cantor.misc.G4]
L
Later [constructor, in Cantor.epsilon0.Hydra]le [definition, in Cantor.epsilon0.EPSILON0]
le [definition, in Cantor.gamma0.Gamma0_prelude]
Legend [lemma, in Cantor.epsilon0.Hydra]
lemmas_on_length [section, in Cantor.gamma0.Gamma0]
length [definition, in Cantor.gamma0.Gamma0_length]
length_abnc [lemma, in Cantor.gamma0.Gamma0_length]
length_ab [lemma, in Cantor.gamma0.Gamma0_length]
length_psi [lemma, in Cantor.gamma0.Gamma0_length]
length_n [lemma, in Cantor.gamma0.Gamma0_length]
length_c [lemma, in Cantor.gamma0.Gamma0_length]
length_b [lemma, in Cantor.gamma0.Gamma0_length]
length_a [lemma, in Cantor.gamma0.Gamma0_length]
length_aux [definition, in Cantor.gamma0.Gamma0_length]
length_map [lemma, in Cantor.prelude.more_list]
Lerne [definition, in Cantor.epsilon0.Hydra]
lex [definition, in Cantor.rpo.rpo]
lex_trans [lemma, in Cantor.rpo.rpo]
le_succ_succ [lemma, in Cantor.epsilon0.EPSILON0]
le_phi0_phi0 [lemma, in Cantor.epsilon0.EPSILON0]
le_tail [lemma, in Cantor.epsilon0.EPSILON0]
le_zero_inv [lemma, in Cantor.epsilon0.EPSILON0]
le_inv [lemma, in Cantor.epsilon0.EPSILON0]
le_lt_trans [lemma, in Cantor.epsilon0.EPSILON0]
le_trans [lemma, in Cantor.epsilon0.EPSILON0]
le_plus_l [lemma, in Cantor.gamma0.Gamma0]
le_plus_r [lemma, in Cantor.gamma0.Gamma0]
le_b_phi_ab [lemma, in Cantor.gamma0.Gamma0]
le_one_cons [lemma, in Cantor.gamma0.Gamma0]
le_cons_tail [lemma, in Cantor.gamma0.Gamma0]
le_trans [lemma, in Cantor.gamma0.Gamma0]
le_lt_trans [lemma, in Cantor.gamma0.Gamma0]
le_inv_nc [lemma, in Cantor.gamma0.Gamma0]
le_psi_term_le [lemma, in Cantor.gamma0.Gamma0]
le_zero_alpha [lemma, in Cantor.gamma0.Gamma0]
limit_plus_F_ok [lemma, in Cantor.gamma0.Gamma0]
limit_plus_F_inv0 [lemma, in Cantor.gamma0.Gamma0]
limit_plus_F_lim [lemma, in Cantor.gamma0.Gamma0]
limit_plus_F_plus [lemma, in Cantor.gamma0.Gamma0]
limit_plus_F_cons [constructor, in Cantor.gamma0.Gamma0]
limit_plus_F_0 [constructor, in Cantor.gamma0.Gamma0]
limit_plus_F [inductive, in Cantor.gamma0.Gamma0]
list_rec3 [definition, in Cantor.prelude.more_list]
list_rec2 [definition, in Cantor.prelude.more_list]
list_size_size_eq [lemma, in Cantor.prelude.more_list]
list_size_fold [lemma, in Cantor.prelude.more_list]
list_size_app [lemma, in Cantor.prelude.more_list]
list_size_tl_compat [lemma, in Cantor.prelude.more_list]
list_size [definition, in Cantor.prelude.more_list]
list_app_length [lemma, in Cantor.prelude.more_list]
list_permut [library]
list_set [library]
log [definition, in Cantor.epsilon0.EPSILON0]
log_nf [lemma, in Cantor.epsilon0.EPSILON0]
lt [inductive, in Cantor.epsilon0.EPSILON0]
lt [inductive, in Cantor.gamma0.Gamma0_prelude]
ltM [definition, in Cantor.epsilon0.MSE0]
ltM_head [lemma, in Cantor.epsilon0.MSE0]
ltM_tail [lemma, in Cantor.epsilon0.MSE0]
ltM_lt [lemma, in Cantor.epsilon0.MSE0]
ltM_appR [lemma, in Cantor.epsilon0.MSE0]
ltM_app [lemma, in Cantor.epsilon0.MSE0]
ltM_cons [lemma, in Cantor.epsilon0.MSE0]
ltM_inv3 [lemma, in Cantor.epsilon0.MSE0]
ltM_inv2 [lemma, in Cantor.epsilon0.MSE0]
ltM_inv [lemma, in Cantor.epsilon0.MSE0]
ltM_trans_2 [lemma, in Cantor.epsilon0.MSE0]
ltM_trans_1 [lemma, in Cantor.epsilon0.MSE0]
ltM_trans [lemma, in Cantor.epsilon0.MSE0]
ltM_equiv_ltMR [lemma, in Cantor.epsilon0.MSE0]
ltM_equiv_ltM [lemma, in Cantor.epsilon0.MSE0]
lt_succ_le [lemma, in Cantor.epsilon0.EPSILON0]
lt_succ_le_2 [lemma, in Cantor.epsilon0.EPSILON0]
lt_succ_le_R [lemma, in Cantor.epsilon0.EPSILON0]
lt_phi0_phi0 [lemma, in Cantor.epsilon0.EPSILON0]
lt_succ_succ [lemma, in Cantor.epsilon0.EPSILON0]
lt_succ [lemma, in Cantor.epsilon0.EPSILON0]
lt_intro [lemma, in Cantor.epsilon0.EPSILON0]
lt_a_phi0_a [lemma, in Cantor.epsilon0.EPSILON0]
lt_inc_rpo_0 [lemma, in Cantor.epsilon0.EPSILON0]
lt_subterm2 [lemma, in Cantor.epsilon0.EPSILON0]
lt_subterm1 [lemma, in Cantor.epsilon0.EPSILON0]
lt_le_dec [definition, in Cantor.epsilon0.EPSILON0]
lt_inv_le [lemma, in Cantor.epsilon0.EPSILON0]
lt_not_le [lemma, in Cantor.epsilon0.EPSILON0]
lt_le_trans [lemma, in Cantor.epsilon0.EPSILON0]
lt_not_wf [lemma, in Cantor.epsilon0.EPSILON0]
lt_not_well_founded.f [variable, in Cantor.epsilon0.EPSILON0]
lt_not_well_founded [section, in Cantor.epsilon0.EPSILON0]
lt_not_gt [lemma, in Cantor.epsilon0.EPSILON0]
lt_trans [lemma, in Cantor.epsilon0.EPSILON0]
lt_inv_b [lemma, in Cantor.epsilon0.EPSILON0]
lt_inv_nb [lemma, in Cantor.epsilon0.EPSILON0]
lt_irr [lemma, in Cantor.epsilon0.EPSILON0]
lt_inv [lemma, in Cantor.epsilon0.EPSILON0]
lt_epsilon0 [inductive, in Cantor.gamma0.Gamma0_prelude]
lt_7 [constructor, in Cantor.gamma0.Gamma0_prelude]
lt_6 [constructor, in Cantor.gamma0.Gamma0_prelude]
lt_5 [constructor, in Cantor.gamma0.Gamma0_prelude]
lt_4 [constructor, in Cantor.gamma0.Gamma0_prelude]
lt_3 [constructor, in Cantor.gamma0.Gamma0_prelude]
lt_2 [constructor, in Cantor.gamma0.Gamma0_prelude]
lt_1 [constructor, in Cantor.gamma0.Gamma0_prelude]
lt_not_gt [lemma, in Cantor.gamma0.Gamma0]
lt_epsilon0_succ [lemma, in Cantor.gamma0.Gamma0]
lt_epsilon0_trans [lemma, in Cantor.gamma0.Gamma0]
lt_T1_injection [definition, in Cantor.gamma0.Gamma0]
lt_epsilon0_okR [lemma, in Cantor.gamma0.Gamma0]
lt_epsilon0_ok [lemma, in Cantor.gamma0.Gamma0]
lt_a_phi_ab [lemma, in Cantor.gamma0.Gamma0]
lt_inc_rpo_0 [lemma, in Cantor.gamma0.Gamma0]
lt_rpo_cons_cons [lemma, in Cantor.gamma0.Gamma0]
lt_incl_rpo.H [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.nf2 [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.nf1 [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.Hrec [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.Hsize [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.n2 [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.n1 [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.c2 [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.b2 [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.a2 [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.c1 [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.b1 [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.a1 [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo.s [variable, in Cantor.gamma0.Gamma0]
lt_incl_rpo [section, in Cantor.gamma0.Gamma0]
lt_subterm1 [lemma, in Cantor.gamma0.Gamma0]
lt_succ_le [lemma, in Cantor.gamma0.Gamma0]
lt_succ [lemma, in Cantor.gamma0.Gamma0]
lt_compatR [lemma, in Cantor.gamma0.Gamma0]
lt_compat [lemma, in Cantor.gamma0.Gamma0]
lt_omega_is_finite [lemma, in Cantor.gamma0.Gamma0]
lt_omega_inv [lemma, in Cantor.gamma0.Gamma0]
lt_cons_omega_inv [lemma, in Cantor.gamma0.Gamma0]
lt_one_inv [lemma, in Cantor.gamma0.Gamma0]
lt_tail [lemma, in Cantor.gamma0.Gamma0]
lt_tail0 [lemma, in Cantor.gamma0.Gamma0]
lt_alpha_cons [lemma, in Cantor.gamma0.Gamma0]
lt_alpha_psi [lemma, in Cantor.gamma0.Gamma0]
lt_beta_cons [lemma, in Cantor.gamma0.Gamma0]
lt_beta_psi [lemma, in Cantor.gamma0.Gamma0]
lt_le_trans [lemma, in Cantor.gamma0.Gamma0]
lt_ge_dec [definition, in Cantor.gamma0.Gamma0]
lt_than_psi [lemma, in Cantor.gamma0.Gamma0]
lt_irr [lemma, in Cantor.gamma0.Gamma0]
lt_lt_Sn [lemma, in Cantor.prelude.More_nat]
lt_ltM2 [lemma, in Cantor.epsilon0.MSE0]
lt_ltM [lemma, in Cantor.epsilon0.MSE0]
lub [definition, in Cantor.gamma0.Gamma0]
lub_mono [lemma, in Cantor.gamma0.Gamma0]
lub_unicity [lemma, in Cantor.gamma0.Gamma0]
L1 [lemma, in Cantor.misc.G4]
L2 [lemma, in Cantor.misc.G4]
L3 [lemma, in Cantor.misc.G4]
L4 [lemma, in Cantor.misc.G4]
L5 [lemma, in Cantor.misc.G4]
M
Make [module, in Cantor.prelude.dickson]Make [module, in Cantor.prelude.list_set]
Make [module, in Cantor.rpo.term]
Make [module, in Cantor.prelude.list_permut]
Make [module, in Cantor.rpo.rpo]
Make.acc_build [lemma, in Cantor.rpo.rpo]
Make.acc_lex_drop_proof [lemma, in Cantor.rpo.rpo]
Make.ac_syntactic [lemma, in Cantor.prelude.list_permut]
Make.ac_syntactic_aux [lemma, in Cantor.prelude.list_permut]
Make.add [definition, in Cantor.prelude.list_set]
Make.add_comm [lemma, in Cantor.prelude.list_set]
Make.add_without_red [definition, in Cantor.prelude.list_set]
Make.add_12 [lemma, in Cantor.prelude.list_set]
Make.add_2 [lemma, in Cantor.prelude.list_set]
Make.add_1 [lemma, in Cantor.prelude.list_set]
Make.add_prf [lemma, in Cantor.prelude.list_set]
Make.apply_subst [definition, in Cantor.rpo.term]
Make.build_list_of_SN_terms [definition, in Cantor.rpo.rpo]
Make.cardinal [definition, in Cantor.prelude.list_set]
Make.cardinal_eq_set [lemma, in Cantor.prelude.list_set]
Make.cardinal_union [lemma, in Cantor.prelude.list_set]
Make.cardinal_union_inter_12 [lemma, in Cantor.prelude.list_set]
Make.cardinal_union_2 [lemma, in Cantor.prelude.list_set]
Make.cardinal_union_1 [lemma, in Cantor.prelude.list_set]
Make.cardinal_subset [lemma, in Cantor.prelude.list_set]
Make.cons_permut_in [lemma, in Cantor.prelude.list_permut]
Make.context_multiset_extension_step_app2 [lemma, in Cantor.prelude.dickson]
Make.context_trans_clos_multiset_extension_step_app1 [lemma, in Cantor.prelude.dickson]
Make.context_multiset_extension_step_app1 [lemma, in Cantor.prelude.dickson]
Make.context_list_permut_app2 [lemma, in Cantor.prelude.list_permut]
Make.context_list_permut_app1 [lemma, in Cantor.prelude.list_permut]
Make.context_list_permut_cons [lemma, in Cantor.prelude.list_permut]
Make.DecVar [module, in Cantor.rpo.term]
Make.DecVar.A [definition, in Cantor.rpo.term]
Make.DecVar.eq_A_dec [lemma, in Cantor.rpo.term]
Make.dickson [lemma, in Cantor.prelude.dickson]
Make.dickson_aux3 [lemma, in Cantor.prelude.dickson]
Make.dickson_aux2 [lemma, in Cantor.prelude.dickson]
Make.dickson_aux1 [lemma, in Cantor.prelude.dickson]
Make.direct_subterm [definition, in Cantor.rpo.term]
Make.DoubleRecursion [section, in Cantor.rpo.term]
Make.DoubleRecursion.Pl2 [variable, in Cantor.rpo.term]
Make.DoubleRecursion.P2 [variable, in Cantor.rpo.term]
Make.DS [module, in Cantor.prelude.dickson]
Make.DS [module, in Cantor.prelude.list_set]
Make.DS [module, in Cantor.prelude.list_permut]
Make.elt [definition, in Cantor.prelude.list_set]
Make.elt [definition, in Cantor.prelude.list_permut]
Make.empty [definition, in Cantor.prelude.list_set]
Make.empty_subst_is_id_list [lemma, in Cantor.rpo.term]
Make.empty_subst_is_id [lemma, in Cantor.rpo.term]
Make.Eq [constructor, in Cantor.rpo.rpo]
Make.eq_set_list_permut_support [lemma, in Cantor.prelude.list_set]
Make.eq_set_trans [lemma, in Cantor.prelude.list_set]
Make.eq_set_sym [lemma, in Cantor.prelude.list_set]
Make.eq_set_refl [lemma, in Cantor.prelude.list_set]
Make.eq_set_dec [lemma, in Cantor.prelude.list_set]
Make.eq_set [definition, in Cantor.prelude.list_set]
Make.eq_elt_dec [definition, in Cantor.prelude.list_set]
Make.eq_term_dec [lemma, in Cantor.rpo.term]
Make.eq_elt_dec [definition, in Cantor.prelude.list_permut]
Make.F [module, in Cantor.rpo.term]
Make.filter [definition, in Cantor.prelude.list_set]
Make.filter_union [lemma, in Cantor.prelude.list_set]
Make.filter_2 [lemma, in Cantor.prelude.list_set]
Make.filter_2_list [lemma, in Cantor.prelude.list_set]
Make.filter_1 [lemma, in Cantor.prelude.list_set]
Make.filter_1_list [lemma, in Cantor.prelude.list_set]
Make.filter_aux [definition, in Cantor.prelude.list_set]
Make.included_remove_red [lemma, in Cantor.prelude.list_set]
Make.included_filter_aux [lemma, in Cantor.prelude.list_set]
Make.inter [definition, in Cantor.prelude.list_set]
Make.inter_12 [lemma, in Cantor.prelude.list_set]
Make.inter_12_aux [lemma, in Cantor.prelude.list_set]
Make.inter_2 [lemma, in Cantor.prelude.list_set]
Make.inter_2_aux [lemma, in Cantor.prelude.list_set]
Make.inter_1 [lemma, in Cantor.prelude.list_set]
Make.inter_1_aux [lemma, in Cantor.prelude.list_set]
Make.in_permut_in [lemma, in Cantor.prelude.list_permut]
Make.in_mult_S [lemma, in Cantor.prelude.list_permut]
Make.in_sn_sn [lemma, in Cantor.rpo.rpo]
Make.is_a_set [projection, in Cantor.prelude.list_set]
Make.is_a_pos_exists_subtem [lemma, in Cantor.rpo.term]
Make.is_a_pos [definition, in Cantor.rpo.term]
Make.lex1 [lemma, in Cantor.rpo.rpo]
Make.lex1_bis [lemma, in Cantor.rpo.rpo]
Make.lex2 [lemma, in Cantor.rpo.rpo]
Make.lex3 [lemma, in Cantor.rpo.rpo]
Make.list_permut_acc [lemma, in Cantor.prelude.dickson]
Make.list_permut_multiset_extension_step_2 [lemma, in Cantor.prelude.dickson]
Make.list_permut_multiset_extension_step_1 [lemma, in Cantor.prelude.dickson]
Make.list_permut_dec [lemma, in Cantor.prelude.list_permut]
Make.list_permut_length_2 [lemma, in Cantor.prelude.list_permut]
Make.list_permut_length_1 [lemma, in Cantor.prelude.list_permut]
Make.list_permut_map [lemma, in Cantor.prelude.list_permut]
Make.list_permut_size [lemma, in Cantor.prelude.list_permut]
Make.list_permut_length [lemma, in Cantor.prelude.list_permut]
Make.list_permut_remove_hd [lemma, in Cantor.prelude.list_permut]
Make.list_permut_app_app [lemma, in Cantor.prelude.list_permut]
Make.list_permut_add_cons_inside [lemma, in Cantor.prelude.list_permut]
Make.list_permut_add_inside [lemma, in Cantor.prelude.list_permut]
Make.list_permut_nil [lemma, in Cantor.prelude.list_permut]
Make.list_permut_trans [lemma, in Cantor.prelude.list_permut]
Make.list_permut_sym [lemma, in Cantor.prelude.list_permut]
Make.list_permut_refl [lemma, in Cantor.prelude.list_permut]
Make.list_permut [definition, in Cantor.prelude.list_permut]
Make.list_to_multiset [definition, in Cantor.prelude.list_permut]
Make.list_permut_map_acc [lemma, in Cantor.rpo.rpo]
Make.List_mul_rest_step [constructor, in Cantor.rpo.rpo]
Make.List_mul_rest [constructor, in Cantor.rpo.rpo]
Make.List_eq_rest [constructor, in Cantor.rpo.rpo]
Make.List_gt_rest [constructor, in Cantor.rpo.rpo]
Make.List_mul [constructor, in Cantor.rpo.rpo]
Make.List_eq [constructor, in Cantor.rpo.rpo]
Make.List_gt [constructor, in Cantor.rpo.rpo]
Make.LP [module, in Cantor.prelude.dickson]
Make.LP [module, in Cantor.prelude.list_set]
Make.LP [module, in Cantor.rpo.rpo]
Make.Lt [constructor, in Cantor.rpo.rpo]
Make.make_set [definition, in Cantor.prelude.list_set]
Make.map_subst [definition, in Cantor.rpo.term]
Make.mem [definition, in Cantor.prelude.list_set]
Make.mem_dec [lemma, in Cantor.prelude.list_set]
Make.mk_set [constructor, in Cantor.prelude.list_set]
Make.mk_sn [constructor, in Cantor.rpo.rpo]
Make.multiplicity_app [lemma, in Cantor.prelude.list_permut]
Make.multiset_closure [lemma, in Cantor.prelude.dickson]
Make.multiset_extension_step [inductive, in Cantor.prelude.dickson]
Make.out_mult_O [lemma, in Cantor.prelude.list_permut]
Make.o_size3_trans [lemma, in Cantor.rpo.rpo]
Make.o_size3 [definition, in Cantor.rpo.rpo]
Make.o_size2 [definition, in Cantor.rpo.rpo]
Make.o_size [definition, in Cantor.rpo.rpo]
Make.P [module, in Cantor.rpo.rpo]
Make.projection_list_of_SN_terms [lemma, in Cantor.rpo.rpo]
Make.Recursion [section, in Cantor.rpo.term]
Make.Recursion.P [variable, in Cantor.rpo.term]
Make.Recursion.Pl [variable, in Cantor.rpo.term]
Make.remove_not_common [definition, in Cantor.prelude.list_set]
Make.remove_red_included [lemma, in Cantor.prelude.list_set]
Make.remove_red [definition, in Cantor.prelude.list_set]
Make.remove_context_list_permut_app2 [lemma, in Cantor.prelude.list_permut]
Make.remove_context_list_permut_cons [lemma, in Cantor.prelude.list_permut]
Make.replace_at_pos_list_replace_at_pos_in_subterm [lemma, in Cantor.rpo.term]
Make.replace_at_pos_is_replace_at_pos2 [lemma, in Cantor.rpo.term]
Make.replace_at_pos_is_replace_at_pos1 [lemma, in Cantor.rpo.term]
Make.replace_at_pos_unfold [lemma, in Cantor.rpo.term]
Make.replace_at_pos_list [definition, in Cantor.rpo.term]
Make.replace_at_pos [definition, in Cantor.rpo.term]
Make.rmv_case [constructor, in Cantor.prelude.dickson]
Make.rpo [inductive, in Cantor.rpo.rpo]
Make.rpo_add_context [lemma, in Cantor.rpo.rpo]
Make.rpo_subst [lemma, in Cantor.rpo.rpo]
Make.rpo_term [definition, in Cantor.rpo.rpo]
Make.rpo_mul_trans_clos [lemma, in Cantor.rpo.rpo]
Make.rpo_mul_rest_step [inductive, in Cantor.rpo.rpo]
Make.rpo_mul_rest [inductive, in Cantor.rpo.rpo]
Make.rpo_lex_rest_same_length [lemma, in Cantor.rpo.rpo]
Make.rpo_lex_rest [inductive, in Cantor.rpo.rpo]
Make.rpo_rest [definition, in Cantor.rpo.rpo]
Make.rpo_trans [lemma, in Cantor.rpo.rpo]
Make.rpo_closure [lemma, in Cantor.rpo.rpo]
Make.rpo_subterm [lemma, in Cantor.rpo.rpo]
Make.rpo_lex_same_length [lemma, in Cantor.rpo.rpo]
Make.rpo_mul [inductive, in Cantor.rpo.rpo]
Make.rpo_lex [inductive, in Cantor.rpo.rpo]
Make.rpo_eq [inductive, in Cantor.rpo.rpo]
Make.singleton [definition, in Cantor.prelude.list_set]
Make.size [definition, in Cantor.rpo.term]
Make.size_subterm_at_pos [lemma, in Cantor.rpo.term]
Make.size_direct_subterm [lemma, in Cantor.rpo.term]
Make.size_ge_one [lemma, in Cantor.rpo.term]
Make.size_unfold [lemma, in Cantor.rpo.term]
Make.size2 [definition, in Cantor.rpo.rpo]
Make.size3 [definition, in Cantor.rpo.rpo]
Make.sn [projection, in Cantor.rpo.rpo]
Make.SN_term [record, in Cantor.rpo.rpo]
Make.subset [definition, in Cantor.prelude.list_set]
Make.subset_cardinal_not_eq_not_eq_set [lemma, in Cantor.prelude.list_set]
Make.subset_subset_union [lemma, in Cantor.prelude.list_set]
Make.subset_compat [lemma, in Cantor.prelude.list_set]
Make.subset_compat_2 [lemma, in Cantor.prelude.list_set]
Make.subset_compat_1 [lemma, in Cantor.prelude.list_set]
Make.subset_filter [lemma, in Cantor.prelude.list_set]
Make.subset_inter_2 [lemma, in Cantor.prelude.list_set]
Make.subset_inter_1 [lemma, in Cantor.prelude.list_set]
Make.subset_union_2 [lemma, in Cantor.prelude.list_set]
Make.subset_union_1 [lemma, in Cantor.prelude.list_set]
Make.subset_dec [lemma, in Cantor.prelude.list_set]
Make.substitution [definition, in Cantor.rpo.term]
Make.subst_comp_is_subst_comp [lemma, in Cantor.rpo.term]
Make.subst_comp_is_subst_comp_aux2 [lemma, in Cantor.rpo.term]
Make.subst_comp_is_subst_comp_aux1 [lemma, in Cantor.rpo.term]
Make.subst_comp [definition, in Cantor.rpo.term]
Make.Subterm [constructor, in Cantor.rpo.rpo]
Make.subterm_at_pos_apply_subst_apply_subst_subterm_at_pos [lemma, in Cantor.rpo.term]
Make.subterm_at_pos [definition, in Cantor.rpo.term]
Make.support [projection, in Cantor.prelude.list_set]
Make.symbol [definition, in Cantor.rpo.term]
Make.t [record, in Cantor.prelude.list_set]
Make.T [module, in Cantor.rpo.rpo]
Make.Term [constructor, in Cantor.rpo.term]
Make.term [inductive, in Cantor.rpo.term]
Make.Term_eq_dec.eq_A_dec [definition, in Cantor.rpo.term]
Make.Term_eq_dec.A [definition, in Cantor.rpo.term]
Make.Term_eq_dec [module, in Cantor.rpo.term]
Make.term_rec8 [definition, in Cantor.rpo.term]
Make.term_rec7 [definition, in Cantor.rpo.term]
Make.term_rec4 [definition, in Cantor.rpo.term]
Make.term_rec3 [definition, in Cantor.rpo.term]
Make.term_rec2 [definition, in Cantor.rpo.term]
Make.Top_eq_mul [constructor, in Cantor.rpo.rpo]
Make.Top_eq_lex [constructor, in Cantor.rpo.rpo]
Make.Top_gt [constructor, in Cantor.rpo.rpo]
Make.tt [projection, in Cantor.rpo.rpo]
Make.two_cases [lemma, in Cantor.prelude.dickson]
Make.two_cases_rpo [lemma, in Cantor.rpo.rpo]
Make.union [definition, in Cantor.prelude.list_set]
Make.union_compat_eq_set [lemma, in Cantor.prelude.list_set]
Make.union_compat_subset_2 [lemma, in Cantor.prelude.list_set]
Make.union_compat_subset_1 [lemma, in Cantor.prelude.list_set]
Make.union_assoc [lemma, in Cantor.prelude.list_set]
Make.union_comm [lemma, in Cantor.prelude.list_set]
Make.union_empty_2 [lemma, in Cantor.prelude.list_set]
Make.union_empty_1 [lemma, in Cantor.prelude.list_set]
Make.union_12 [lemma, in Cantor.prelude.list_set]
Make.union_12_aux [lemma, in Cantor.prelude.list_set]
Make.union_2 [lemma, in Cantor.prelude.list_set]
Make.union_2_aux [lemma, in Cantor.prelude.list_set]
Make.union_1 [lemma, in Cantor.prelude.list_set]
Make.union_1_aux [lemma, in Cantor.prelude.list_set]
Make.Var [constructor, in Cantor.rpo.term]
Make.variable [definition, in Cantor.rpo.term]
Make.VSet [module, in Cantor.rpo.term]
Make.well_formed_apply_subst [lemma, in Cantor.rpo.term]
Make.well_formed_subst [definition, in Cantor.rpo.term]
Make.well_formed_list [definition, in Cantor.rpo.term]
Make.well_formed_fold [lemma, in Cantor.rpo.term]
Make.well_formed_unfold [lemma, in Cantor.rpo.term]
Make.well_formed [definition, in Cantor.rpo.term]
Make.wf_rpo [lemma, in Cantor.rpo.rpo]
Make.wf_rpo_term [lemma, in Cantor.rpo.rpo]
Make.wf_on_mul_rest [lemma, in Cantor.rpo.rpo]
Make.wf_on_lex_rest [lemma, in Cantor.rpo.rpo]
Make.wf_on_rest [lemma, in Cantor.rpo.rpo]
Make.wf_size3 [lemma, in Cantor.rpo.rpo]
Make.wf_size2 [lemma, in Cantor.rpo.rpo]
Make.wf_size [lemma, in Cantor.rpo.rpo]
Make.without_red_permut [lemma, in Cantor.prelude.list_set]
Make.without_red_remove_not_common [lemma, in Cantor.prelude.list_set]
Make.without_red_remove_not_common_aux [lemma, in Cantor.prelude.list_set]
Make.without_red_add_without_red [lemma, in Cantor.prelude.list_set]
Make.without_red_singleton [lemma, in Cantor.prelude.list_set]
Make.without_red_nil [lemma, in Cantor.prelude.list_set]
Make.without_red_add [lemma, in Cantor.prelude.list_set]
Make.without_red_remove [lemma, in Cantor.prelude.list_set]
Make.without_red_remove_red [lemma, in Cantor.prelude.list_set]
Make.without_red_filter_aux [lemma, in Cantor.prelude.list_set]
Make.without_red [definition, in Cantor.prelude.list_set]
Make.X [module, in Cantor.rpo.term]
map_without_repetition [definition, in Cantor.prelude.more_list]
map_app [lemma, in Cantor.prelude.more_list]
map_map [lemma, in Cantor.prelude.more_list]
map12_without_repetition [definition, in Cantor.prelude.more_list]
max [definition, in Cantor.epsilon0.EPSILON0]
max_assoc [lemma, in Cantor.epsilon0.EPSILON0]
max_nf [lemma, in Cantor.epsilon0.EPSILON0]
max_dec [lemma, in Cantor.epsilon0.EPSILON0]
max_comm [lemma, in Cantor.epsilon0.EPSILON0]
max_le_1 [lemma, in Cantor.epsilon0.EPSILON0]
max_le_regL [lemma, in Cantor.prelude.More_nat]
max_le_regR [lemma, in Cantor.prelude.More_nat]
max' [definition, in Cantor.epsilon0.EPSILON0]
minus [definition, in Cantor.epsilon0.EPSILON0]
minus_le [lemma, in Cantor.epsilon0.EPSILON0]
minus_a_a [lemma, in Cantor.epsilon0.EPSILON0]
minus_lt [lemma, in Cantor.epsilon0.EPSILON0]
ml_1 [lemma, in Cantor.gamma0.Gamma0]
ml_psi [lemma, in Cantor.gamma0.Gamma0]
more_list [library]
More_nat [library]
moser_lepper [definition, in Cantor.gamma0.Gamma0]
MSE0 [library]
mult [definition, in Cantor.epsilon0.EPSILON0]
multiplicity [definition, in Cantor.epsilon0.MSE0]
multiplicity_of_app [lemma, in Cantor.epsilon0.MSE0]
multiplicity_rw2 [lemma, in Cantor.epsilon0.MSE0]
multiplicity_rw1 [lemma, in Cantor.epsilon0.MSE0]
mult_a_1 [lemma, in Cantor.epsilon0.EPSILON0]
mult_1_a [lemma, in Cantor.epsilon0.EPSILON0]
mult_a_0 [lemma, in Cantor.epsilon0.EPSILON0]
mult_0_a [lemma, in Cantor.epsilon0.EPSILON0]
mult_compat [lemma, in Cantor.epsilon0.EPSILON0]
mult_fin_omega [lemma, in Cantor.epsilon0.EPSILON0]
N
nat_2_term_mono [lemma, in Cantor.epsilon0.EPSILON0]nat_lt_cons [lemma, in Cantor.epsilon0.EPSILON0]
nat_2_term [definition, in Cantor.epsilon0.EPSILON0]
nat_2_term_mono [lemma, in Cantor.gamma0.Gamma0]
nat_lt_psi [lemma, in Cantor.gamma0.Gamma0]
nat_lt_cons [lemma, in Cantor.gamma0.Gamma0]
nat_2_term [definition, in Cantor.gamma0.Gamma0]
nbterms [definition, in Cantor.gamma0.Gamma0_length]
nb_occ_app [lemma, in Cantor.prelude.more_list]
nb_occ [definition, in Cantor.prelude.more_list]
next [definition, in Cantor.misc.G4]
nexts [definition, in Cantor.misc.G4]
nexts_ok_R [lemma, in Cantor.misc.G4]
nexts_ok [lemma, in Cantor.misc.G4]
nexts_plus [lemma, in Cantor.misc.G4]
next_unicity [lemma, in Cantor.misc.G4]
nf [inductive, in Cantor.epsilon0.EPSILON0]
nf [inductive, in Cantor.gamma0.Gamma0_prelude]
nfs [inductive, in Cantor.epsilon0.MSE0]
nfs_to_nf [lemma, in Cantor.epsilon0.MSE0]
nfs_cons [constructor, in Cantor.epsilon0.MSE0]
nfs_nil [constructor, in Cantor.epsilon0.MSE0]
nf_Wf [lemma, in Cantor.epsilon0.EPSILON0]
nf_rect [definition, in Cantor.epsilon0.EPSILON0]
nf_tower [lemma, in Cantor.epsilon0.EPSILON0]
nf_phi0 [lemma, in Cantor.epsilon0.EPSILON0]
nf_omega [lemma, in Cantor.epsilon0.EPSILON0]
nf_of_finite [lemma, in Cantor.epsilon0.EPSILON0]
nf_coeff_irrelevance [lemma, in Cantor.epsilon0.EPSILON0]
nf_intro [lemma, in Cantor.epsilon0.EPSILON0]
nf_tail_lt_nf [lemma, in Cantor.epsilon0.EPSILON0]
nf_inv2 [lemma, in Cantor.epsilon0.EPSILON0]
nf_inv1 [lemma, in Cantor.epsilon0.EPSILON0]
nf_intro [lemma, in Cantor.gamma0.Gamma0]
nf_nat_irrelevance [lemma, in Cantor.gamma0.Gamma0]
nf_Wf [lemma, in Cantor.gamma0.Gamma0]
nf_c2 [lemma, in Cantor.gamma0.Gamma0]
nf_c1 [lemma, in Cantor.gamma0.Gamma0]
nf_b2 [lemma, in Cantor.gamma0.Gamma0]
nf_b1 [lemma, in Cantor.gamma0.Gamma0]
nf_a2 [lemma, in Cantor.gamma0.Gamma0]
nf_a1 [lemma, in Cantor.gamma0.Gamma0]
nf_subterm [lemma, in Cantor.gamma0.Gamma0]
nf_finite_inv [lemma, in Cantor.gamma0.Gamma0]
nf_epsilon [lemma, in Cantor.gamma0.Gamma0]
nf_epsilon0 [lemma, in Cantor.gamma0.Gamma0]
nf_omega [lemma, in Cantor.gamma0.Gamma0]
nf_inv_tail [lemma, in Cantor.gamma0.Gamma0]
nf_c [lemma, in Cantor.gamma0.Gamma0]
nf_b [lemma, in Cantor.gamma0.Gamma0]
nf_a [lemma, in Cantor.gamma0.Gamma0]
nf_unicity [lemma, in Cantor.epsilon0.MSE0]
nf_to_nfs [lemma, in Cantor.epsilon0.MSE0]
nf_multiplicity_big [lemma, in Cantor.epsilon0.MSE0]
nf_multiplicity_tail [lemma, in Cantor.epsilon0.MSE0]
nf_multiplicity_head [lemma, in Cantor.epsilon0.MSE0]
nf_nfs [lemma, in Cantor.epsilon0.MSE0]
nf2 [inductive, in Cantor.epsilon0.EPSILON0]
nf2_phi0R [lemma, in Cantor.epsilon0.EPSILON0]
nf2_phi0 [lemma, in Cantor.epsilon0.EPSILON0]
nf2_intro [lemma, in Cantor.epsilon0.EPSILON0]
nf2_c [constructor, in Cantor.epsilon0.EPSILON0]
nf2_z [constructor, in Cantor.epsilon0.EPSILON0]
node [constructor, in Cantor.epsilon0.Hydra]
none_nb_occ_O [lemma, in Cantor.prelude.more_list]
not_lt_zero [lemma, in Cantor.epsilon0.EPSILON0]
not_lt_zero [lemma, in Cantor.gamma0.Gamma0]
not_decreasing [lemma, in Cantor.prelude.not_decreasing]
not_decreasing_aux [lemma, in Cantor.prelude.not_decreasing]
not_acc [lemma, in Cantor.prelude.not_decreasing]
not_decreasing [library]
Now [constructor, in Cantor.epsilon0.Hydra]
no_critical [lemma, in Cantor.gamma0.Gamma0]
nth_item [definition, in Cantor.misc.G4]
nth_error_ok_in [lemma, in Cantor.prelude.more_list]
nth_error_map [lemma, in Cantor.prelude.more_list]
O
occurrence [definition, in Cantor.epsilon0.Hydra]omega [definition, in Cantor.epsilon0.EPSILON0]
omega [definition, in Cantor.gamma0.Gamma0_prelude]
omega_term_ambiguity [lemma, in Cantor.epsilon0.EPSILON0]
omega_exp_rw [lemma, in Cantor.epsilon0.EPSILON0]
omega_minus_one [lemma, in Cantor.epsilon0.EPSILON0]
omega_tower [definition, in Cantor.epsilon0.EPSILON0]
omega_term [definition, in Cantor.epsilon0.EPSILON0]
omega_lt_epsilon [lemma, in Cantor.gamma0.Gamma0]
omega_lt_epsilon0 [lemma, in Cantor.gamma0.Gamma0]
one [definition, in Cantor.gamma0.Gamma0_prelude]
on_length [section, in Cantor.gamma0.Gamma0_length]
ordinal_finite [lemma, in Cantor.epsilon0.EPSILON0]
ordinal_finite [lemma, in Cantor.gamma0.Gamma0]
o_length [definition, in Cantor.prelude.more_list]
P
PartialFix [library]partial_fix.FixPoint.F_ext [variable, in Cantor.prelude.PartialFix]
partial_fix.FixPoint.F [variable, in Cantor.prelude.PartialFix]
partial_fix.FixPoint.P [variable, in Cantor.prelude.PartialFix]
partial_fix.FixPoint [section, in Cantor.prelude.PartialFix]
partial_fun_induction [definition, in Cantor.prelude.PartialFix]
partial_fix.Acc_iterP.F [variable, in Cantor.prelude.PartialFix]
partial_fix.Acc_iterP.P [variable, in Cantor.prelude.PartialFix]
partial_fix.Acc_iterP [section, in Cantor.prelude.PartialFix]
partial_fix.D_Acc [variable, in Cantor.prelude.PartialFix]
partial_fix.gt_D [variable, in Cantor.prelude.PartialFix]
partial_fix.lt_D [variable, in Cantor.prelude.PartialFix]
partial_fix.lt [variable, in Cantor.prelude.PartialFix]
partial_fix.D [variable, in Cantor.prelude.PartialFix]
partial_fix.T [variable, in Cantor.prelude.PartialFix]
partial_fix [section, in Cantor.prelude.PartialFix]
Permut [module, in Cantor.prelude.list_permut]
Permut.DS [module, in Cantor.prelude.list_permut]
Permut.elt [definition, in Cantor.prelude.list_permut]
Permut.eq_elt_dec [definition, in Cantor.prelude.list_permut]
Permut.list_permut [definition, in Cantor.prelude.list_permut]
Permut.list_to_multiset [definition, in Cantor.prelude.list_permut]
PFix [definition, in Cantor.prelude.PartialFix]
PFix_eq [lemma, in Cantor.prelude.PartialFix]
PFix_F_inv [lemma, in Cantor.prelude.PartialFix]
PFix_F_eq [lemma, in Cantor.prelude.PartialFix]
phi [definition, in Cantor.gamma0.Gamma0]
phi_mono_RR [lemma, in Cantor.gamma0.Gamma0]
phi_psi [lemma, in Cantor.gamma0.Gamma0]
phi_to_psi_6 [lemma, in Cantor.gamma0.Gamma0]
phi_to_psi_5 [lemma, in Cantor.gamma0.Gamma0]
phi_to_psi_4 [lemma, in Cantor.gamma0.Gamma0]
phi_to_psi_3 [lemma, in Cantor.gamma0.Gamma0]
phi_to_psi_2 [lemma, in Cantor.gamma0.Gamma0]
phi_to_psi_1 [lemma, in Cantor.gamma0.Gamma0]
phi_to_psi.alpha [variable, in Cantor.gamma0.Gamma0]
phi_to_psi [section, in Cantor.gamma0.Gamma0]
phi_inj_r [lemma, in Cantor.gamma0.Gamma0]
phi_mono_weak_r [lemma, in Cantor.gamma0.Gamma0]
phi_mono_r [lemma, in Cantor.gamma0.Gamma0]
phi_of_psi_plus_finite [lemma, in Cantor.gamma0.Gamma0]
phi_principalR [lemma, in Cantor.gamma0.Gamma0]
phi_spec1 [lemma, in Cantor.gamma0.Gamma0]
phi_le_ge [lemma, in Cantor.gamma0.Gamma0]
phi_le [lemma, in Cantor.gamma0.Gamma0]
phi_fix [lemma, in Cantor.gamma0.Gamma0]
phi_of_any_cons [lemma, in Cantor.gamma0.Gamma0]
phi_nf [lemma, in Cantor.gamma0.Gamma0]
phi_cases [lemma, in Cantor.gamma0.Gamma0]
phi_cases' [lemma, in Cantor.gamma0.Gamma0]
phi_cases_aux [lemma, in Cantor.gamma0.Gamma0]
phi_of_psi_succ [lemma, in Cantor.gamma0.Gamma0]
phi_alpha_zero [lemma, in Cantor.gamma0.Gamma0]
phi_principal [lemma, in Cantor.gamma0.Gamma0]
phi_to_psi [lemma, in Cantor.gamma0.Gamma0]
phi_of_psi [lemma, in Cantor.gamma0.Gamma0]
phi0 [definition, in Cantor.epsilon0.EPSILON0]
phi0_plus_mult [lemma, in Cantor.epsilon0.EPSILON0]
phi0_log [lemma, in Cantor.epsilon0.EPSILON0]
phi0_ltR [lemma, in Cantor.epsilon0.EPSILON0]
phi0_lt [lemma, in Cantor.epsilon0.EPSILON0]
plus [definition, in Cantor.epsilon0.EPSILON0]
plus [definition, in Cantor.gamma0.Gamma0]
plus_compat [lemma, in Cantor.epsilon0.EPSILON0]
plus_is_zero [lemma, in Cantor.epsilon0.EPSILON0]
plus_to_cons [lemma, in Cantor.epsilon0.EPSILON0]
plus_nf [lemma, in Cantor.epsilon0.EPSILON0]
plus_nf0 [lemma, in Cantor.epsilon0.EPSILON0]
plus_cons_cons_rw3 [lemma, in Cantor.epsilon0.EPSILON0]
plus_cons_cons_rw2 [lemma, in Cantor.epsilon0.EPSILON0]
plus_cons_cons_rw1 [lemma, in Cantor.epsilon0.EPSILON0]
plus_not_comm [lemma, in Cantor.epsilon0.EPSILON0]
plus_fin_omega [lemma, in Cantor.epsilon0.EPSILON0]
plus_a_zero [lemma, in Cantor.epsilon0.EPSILON0]
plus_zero [lemma, in Cantor.epsilon0.EPSILON0]
plus_mono_l_weak [lemma, in Cantor.gamma0.Gamma0]
plus_mono_r [lemma, in Cantor.gamma0.Gamma0]
plus_nf [lemma, in Cantor.gamma0.Gamma0]
plus_alpha_0 [lemma, in Cantor.gamma0.Gamma0]
power [definition, in Cantor.misc.G4]
power [definition, in Cantor.prelude.More_nat]
power_of_1 [lemma, in Cantor.prelude.More_nat]
Precedence [module, in Cantor.rpo.rpo]
Precedence.A [axiom, in Cantor.rpo.rpo]
Precedence.Lex [constructor, in Cantor.rpo.rpo]
Precedence.Mul [constructor, in Cantor.rpo.rpo]
Precedence.prec [axiom, in Cantor.rpo.rpo]
Precedence.prec_transitive [axiom, in Cantor.rpo.rpo]
Precedence.prec_antisym [axiom, in Cantor.rpo.rpo]
Precedence.prec_dec [axiom, in Cantor.rpo.rpo]
Precedence.status [axiom, in Cantor.rpo.rpo]
Precedence.status_type [inductive, in Cantor.rpo.rpo]
pred [definition, in Cantor.epsilon0.EPSILON0]
pred [definition, in Cantor.gamma0.Gamma0_prelude]
Pred [definition, in Cantor.epsilon0.Goodstein]
predecessor [section, in Cantor.epsilon0.Goodstein]
predecessor.c [variable, in Cantor.epsilon0.Goodstein]
predecessor.coeff_ok [variable, in Cantor.epsilon0.Goodstein]
predecessor.N [variable, in Cantor.epsilon0.Goodstein]
predecessor.nf_c [variable, in Cantor.epsilon0.Goodstein]
predecessor.N0 [variable, in Cantor.epsilon0.Goodstein]
predecessor.recurr [variable, in Cantor.epsilon0.Goodstein]
PredF [definition, in Cantor.epsilon0.Goodstein]
pred_of_succ [lemma, in Cantor.gamma0.Gamma0]
pred_of_limit [lemma, in Cantor.gamma0.Gamma0]
pred_of_cons' [lemma, in Cantor.gamma0.Gamma0]
pred_of_cons [lemma, in Cantor.gamma0.Gamma0]
Pred_omega_anb [definition, in Cantor.epsilon0.Goodstein]
Pred_omega_an [definition, in Cantor.epsilon0.Goodstein]
Pred_omega_a [definition, in Cantor.epsilon0.Goodstein]
pred_n_zero [definition, in Cantor.epsilon0.Goodstein]
pred_spec [definition, in Cantor.epsilon0.Goodstein]
pred_of_power [lemma, in Cantor.prelude.More_nat]
prop_map12_without_repetition [lemma, in Cantor.prelude.more_list]
prop_map_without_repetition [lemma, in Cantor.prelude.more_list]
psi [definition, in Cantor.gamma0.Gamma0_prelude]
psi_eq [lemma, in Cantor.gamma0.Gamma0_prelude]
psi_term [definition, in Cantor.gamma0.Gamma0_prelude]
psi_principal [lemma, in Cantor.gamma0.Gamma0]
psi_lt_epsilon0 [lemma, in Cantor.gamma0.Gamma0]
psi_relevance [lemma, in Cantor.gamma0.Gamma0]
psi_le_cons [lemma, in Cantor.gamma0.Gamma0]
P_well_founded_induction_type [definition, in Cantor.prelude.AccP]
Q
quad [constructor, in Cantor.misc.G4]R
reachable [definition, in Cantor.misc.G4]reachable_Rgstar [lemma, in Cantor.misc.G4]
reduce_assoc_list [lemma, in Cantor.prelude.more_list]
remove [definition, in Cantor.prelude.more_list]
remove_list [definition, in Cantor.prelude.more_list]
replicate [definition, in Cantor.epsilon0.Hydra]
restrict [definition, in Cantor.prelude.AccP]
restricted_recursion.R [variable, in Cantor.prelude.AccP]
restricted_recursion.P [variable, in Cantor.prelude.AccP]
restricted_recursion.A [variable, in Cantor.prelude.AccP]
restricted_recursion [section, in Cantor.prelude.AccP]
Rg [inductive, in Cantor.misc.G4]
Rg [inductive, in Cantor.epsilon0.Goodstein]
Rgstar [definition, in Cantor.misc.G4]
Rg_i [constructor, in Cantor.epsilon0.Goodstein]
Rg0 [constructor, in Cantor.misc.G4]
Rg1 [constructor, in Cantor.misc.G4]
Rg2 [constructor, in Cantor.misc.G4]
Rh [inductive, in Cantor.epsilon0.Hydra]
Rh_decrease [lemma, in Cantor.epsilon0.Hydra]
Rh_head [lemma, in Cantor.epsilon0.Hydra]
Rn [inductive, in Cantor.epsilon0.Hydra]
Rnl_rest [constructor, in Cantor.epsilon0.Hydra]
Rn_decrease [lemma, in Cantor.epsilon0.Hydra]
Rn_head [lemma, in Cantor.epsilon0.Hydra]
Rn_rect2 [definition, in Cantor.epsilon0.Hydra]
Rn_plus [constructor, in Cantor.epsilon0.Hydra]
Rn_here [constructor, in Cantor.epsilon0.Hydra]
RPO [module, in Cantor.rpo.rpo]
rpo [library]
rpo_trans [lemma, in Cantor.epsilon0.EPSILON0]
rpo_7_1 [lemma, in Cantor.gamma0.Gamma0]
rpo_6_4 [lemma, in Cantor.gamma0.Gamma0]
rpo_6_1 [lemma, in Cantor.gamma0.Gamma0]
rpo_5_4 [lemma, in Cantor.gamma0.Gamma0]
rpo_5_1 [lemma, in Cantor.gamma0.Gamma0]
rpo_5_3 [lemma, in Cantor.gamma0.Gamma0]
rpo_5_2 [lemma, in Cantor.gamma0.Gamma0]
rpo_4_4 [lemma, in Cantor.gamma0.Gamma0]
rpo_4_1 [lemma, in Cantor.gamma0.Gamma0]
rpo_4_3 [lemma, in Cantor.gamma0.Gamma0]
rpo_4_2 [lemma, in Cantor.gamma0.Gamma0]
rpo_3_4 [lemma, in Cantor.gamma0.Gamma0]
rpo_3_1 [lemma, in Cantor.gamma0.Gamma0]
rpo_3_3 [lemma, in Cantor.gamma0.Gamma0]
rpo_3_2 [lemma, in Cantor.gamma0.Gamma0]
rpo_2_4 [lemma, in Cantor.gamma0.Gamma0]
rpo_2_1 [lemma, in Cantor.gamma0.Gamma0]
rpo_2_3 [lemma, in Cantor.gamma0.Gamma0]
rpo_2_2 [lemma, in Cantor.gamma0.Gamma0]
rpo_trans [lemma, in Cantor.gamma0.Gamma0]
RPO.Eq [constructor, in Cantor.rpo.rpo]
RPO.List_mul [constructor, in Cantor.rpo.rpo]
RPO.List_eq [constructor, in Cantor.rpo.rpo]
RPO.List_gt [constructor, in Cantor.rpo.rpo]
RPO.LP [module, in Cantor.rpo.rpo]
RPO.Lt [constructor, in Cantor.rpo.rpo]
RPO.P [module, in Cantor.rpo.rpo]
RPO.rpo [inductive, in Cantor.rpo.rpo]
RPO.rpo_add_context [axiom, in Cantor.rpo.rpo]
RPO.rpo_subst [axiom, in Cantor.rpo.rpo]
RPO.rpo_trans [axiom, in Cantor.rpo.rpo]
RPO.rpo_closure [axiom, in Cantor.rpo.rpo]
RPO.rpo_mul [inductive, in Cantor.rpo.rpo]
RPO.rpo_lex [inductive, in Cantor.rpo.rpo]
RPO.rpo_eq [inductive, in Cantor.rpo.rpo]
RPO.Subterm [constructor, in Cantor.rpo.rpo]
RPO.T [module, in Cantor.rpo.rpo]
RPO.Top_eq_mul [constructor, in Cantor.rpo.rpo]
RPO.Top_eq_lex [constructor, in Cantor.rpo.rpo]
RPO.Top_gt [constructor, in Cantor.rpo.rpo]
RPO.wf_rpo [axiom, in Cantor.rpo.rpo]
R_inc_rpo [lemma, in Cantor.epsilon0.EPSILON0]
R_pred_Sn [lemma, in Cantor.gamma0.Gamma0]
R_predD_0 [lemma, in Cantor.gamma0.Gamma0]
R_inc_rpo [lemma, in Cantor.gamma0.Gamma0]
R1 [lemma, in Cantor.epsilon0.EPSILON0]
R1 [inductive, in Cantor.epsilon0.Hydra]
R1 [lemma, in Cantor.gamma0.Gamma0]
R1_decrease [lemma, in Cantor.epsilon0.Hydra]
R1_head [lemma, in Cantor.epsilon0.Hydra]
R1_node [constructor, in Cantor.epsilon0.Hydra]
R1_single [constructor, in Cantor.epsilon0.Hydra]
R2 [lemma, in Cantor.epsilon0.EPSILON0]
R2 [lemma, in Cantor.gamma0.Gamma0]
R3 [lemma, in Cantor.epsilon0.EPSILON0]
R3 [lemma, in Cantor.gamma0.Gamma0]
R4 [lemma, in Cantor.epsilon0.EPSILON0]
R4 [lemma, in Cantor.gamma0.Gamma0]
R5 [lemma, in Cantor.gamma0.Gamma0]
S
S [module, in Cantor.prelude.decidable_set]S [module, in Cantor.prelude.list_set]
Sequences [section, in Cantor.prelude.not_decreasing]
Sequences.A [variable, in Cantor.prelude.not_decreasing]
Sequences.R [variable, in Cantor.prelude.not_decreasing]
Sequences.seq_intro.is_in_seq [variable, in Cantor.prelude.not_decreasing]
Sequences.seq_intro.seq [variable, in Cantor.prelude.not_decreasing]
Sequences.seq_intro [section, in Cantor.prelude.not_decreasing]
Sequences.W [variable, in Cantor.prelude.not_decreasing]
SF27 [lemma, in Cantor.misc.G4]
SF3 [lemma, in Cantor.misc.G4]
Sh [inductive, in Cantor.epsilon0.Hydra]
Sh_head [lemma, in Cantor.epsilon0.Hydra]
Sh_3 [constructor, in Cantor.epsilon0.Hydra]
Sh_2 [constructor, in Cantor.epsilon0.Hydra]
Sh_1 [constructor, in Cantor.epsilon0.Hydra]
Signature [module, in Cantor.rpo.term]
Signature.AC [constructor, in Cantor.rpo.term]
Signature.arity [axiom, in Cantor.rpo.term]
Signature.arity_type [inductive, in Cantor.rpo.term]
Signature.C [constructor, in Cantor.rpo.term]
Signature.eq_symbol_dec [axiom, in Cantor.rpo.term]
Signature.Free [constructor, in Cantor.rpo.term]
Signature.symb [axiom, in Cantor.rpo.term]
single [constructor, in Cantor.epsilon0.Hydra]
single_nf [constructor, in Cantor.epsilon0.EPSILON0]
single_nf [constructor, in Cantor.gamma0.Gamma0_prelude]
Sn [inductive, in Cantor.epsilon0.Hydra]
Sn_rect2 [definition, in Cantor.epsilon0.Hydra]
Sn_first [constructor, in Cantor.epsilon0.Hydra]
Sn_single [constructor, in Cantor.epsilon0.Hydra]
some_nb_occ_Sn [lemma, in Cantor.prelude.more_list]
sort [definition, in Cantor.epsilon0.MSE0]
sort_nf [lemma, in Cantor.epsilon0.MSE0]
sort_equiv [lemma, in Cantor.epsilon0.MSE0]
sort_aux_nf [lemma, in Cantor.epsilon0.MSE0]
sort_aux_equiv [lemma, in Cantor.epsilon0.MSE0]
sort_aux [definition, in Cantor.epsilon0.MSE0]
split_list_app_cons [lemma, in Cantor.prelude.more_list]
split_list [definition, in Cantor.prelude.more_list]
subterm [inductive, in Cantor.gamma0.Gamma0]
subterm_lt [lemma, in Cantor.gamma0.Gamma0]
subterm_trans [constructor, in Cantor.gamma0.Gamma0]
subterm_c [constructor, in Cantor.gamma0.Gamma0]
subterm_b [constructor, in Cantor.gamma0.Gamma0]
subterm_a [constructor, in Cantor.gamma0.Gamma0]
succ [definition, in Cantor.epsilon0.EPSILON0]
succ [definition, in Cantor.gamma0.Gamma0_prelude]
succ_compat [lemma, in Cantor.epsilon0.EPSILON0]
succ_is_plus_one [lemma, in Cantor.epsilon0.EPSILON0]
succ_nf [lemma, in Cantor.epsilon0.EPSILON0]
succ_nf2 [lemma, in Cantor.epsilon0.EPSILON0]
succ_finite [constructor, in Cantor.gamma0.Gamma0_prelude]
succ_limit_dec [lemma, in Cantor.gamma0.Gamma0]
succ_nf [lemma, in Cantor.gamma0.Gamma0]
succ_as_plus [lemma, in Cantor.gamma0.Gamma0]
succ_of_cons [lemma, in Cantor.gamma0.Gamma0]
succ_lt_le [lemma, in Cantor.gamma0.Gamma0]
S.A [axiom, in Cantor.prelude.decidable_set]
S.cardinal [definition, in Cantor.prelude.list_set]
S.cardinal_subset [axiom, in Cantor.prelude.list_set]
S.DS [module, in Cantor.prelude.list_set]
S.elt [definition, in Cantor.prelude.list_set]
S.eq_A_dec [axiom, in Cantor.prelude.decidable_set]
S.eq_elt_dec [definition, in Cantor.prelude.list_set]
S.is_a_set [projection, in Cantor.prelude.list_set]
S.mk_set [constructor, in Cantor.prelude.list_set]
S.subset [definition, in Cantor.prelude.list_set]
S.support [projection, in Cantor.prelude.list_set]
S.t [record, in Cantor.prelude.list_set]
S.without_red [definition, in Cantor.prelude.list_set]
S1 [inductive, in Cantor.epsilon0.Hydra]
S1_decrease [lemma, in Cantor.epsilon0.Hydra]
S1_head [lemma, in Cantor.epsilon0.Hydra]
S1_rest [constructor, in Cantor.epsilon0.Hydra]
S1_last [constructor, in Cantor.epsilon0.Hydra]
S1_first [constructor, in Cantor.epsilon0.Hydra]
S2 [inductive, in Cantor.epsilon0.Hydra]
S2_decrease [lemma, in Cantor.epsilon0.Hydra]
S2_head [lemma, in Cantor.epsilon0.Hydra]
S2_rest [constructor, in Cantor.epsilon0.Hydra]
S2_first [constructor, in Cantor.epsilon0.Hydra]
S2_single [constructor, in Cantor.epsilon0.Hydra]
T
tail [definition, in Cantor.gamma0.Gamma0_prelude]tail_lt_cons [lemma, in Cantor.epsilon0.EPSILON0]
tail_lt [constructor, in Cantor.epsilon0.EPSILON0]
Term [module, in Cantor.rpo.term]
term [library]
Term.apply_subst [definition, in Cantor.rpo.term]
Term.direct_subterm [definition, in Cantor.rpo.term]
Term.DoubleRecursion [section, in Cantor.rpo.term]
Term.DoubleRecursion.Pl2 [variable, in Cantor.rpo.term]
Term.DoubleRecursion.P2 [variable, in Cantor.rpo.term]
Term.empty_subst_is_id_list [axiom, in Cantor.rpo.term]
Term.empty_subst_is_id [axiom, in Cantor.rpo.term]
Term.eq_term_dec [axiom, in Cantor.rpo.term]
Term.F [module, in Cantor.rpo.term]
Term.is_a_pos_exists_subtem [axiom, in Cantor.rpo.term]
Term.is_a_pos [definition, in Cantor.rpo.term]
Term.map_subst [definition, in Cantor.rpo.term]
Term.Recursion [section, in Cantor.rpo.term]
Term.Recursion.P [variable, in Cantor.rpo.term]
Term.Recursion.Pl [variable, in Cantor.rpo.term]
Term.replace_at_pos_list_replace_at_pos_in_subterm [axiom, in Cantor.rpo.term]
Term.replace_at_pos_is_replace_at_pos2 [axiom, in Cantor.rpo.term]
Term.replace_at_pos_is_replace_at_pos1 [axiom, in Cantor.rpo.term]
Term.replace_at_pos_unfold [axiom, in Cantor.rpo.term]
Term.replace_at_pos_list [definition, in Cantor.rpo.term]
Term.replace_at_pos [definition, in Cantor.rpo.term]
Term.size [definition, in Cantor.rpo.term]
Term.size_subterm_at_pos [axiom, in Cantor.rpo.term]
Term.size_direct_subterm [axiom, in Cantor.rpo.term]
Term.size_ge_one [axiom, in Cantor.rpo.term]
Term.size_unfold [axiom, in Cantor.rpo.term]
Term.substitution [definition, in Cantor.rpo.term]
Term.subst_comp_is_subst_comp [axiom, in Cantor.rpo.term]
Term.subst_comp_is_subst_comp_aux1 [axiom, in Cantor.rpo.term]
Term.subst_comp [definition, in Cantor.rpo.term]
Term.subterm_at_pos_apply_subst_apply_subst_subterm_at_pos [axiom, in Cantor.rpo.term]
Term.subterm_at_pos [definition, in Cantor.rpo.term]
Term.symbol [definition, in Cantor.rpo.term]
Term.Term [constructor, in Cantor.rpo.term]
Term.term [inductive, in Cantor.rpo.term]
Term.Term_eq_dec [module, in Cantor.rpo.term]
Term.term_rec8 [axiom, in Cantor.rpo.term]
Term.term_rec7 [axiom, in Cantor.rpo.term]
Term.term_rec4 [axiom, in Cantor.rpo.term]
Term.term_rec3 [axiom, in Cantor.rpo.term]
Term.term_rec2 [axiom, in Cantor.rpo.term]
Term.Var [constructor, in Cantor.rpo.term]
Term.variable [definition, in Cantor.rpo.term]
Term.well_formed_apply_subst [axiom, in Cantor.rpo.term]
Term.well_formed_subst [definition, in Cantor.rpo.term]
Term.well_formed_list [definition, in Cantor.rpo.term]
Term.well_formed_fold [axiom, in Cantor.rpo.term]
Term.well_formed_unfold [axiom, in Cantor.rpo.term]
Term.well_formed [definition, in Cantor.rpo.term]
Term.X [module, in Cantor.rpo.term]
th_14_6 [lemma, in Cantor.gamma0.Gamma0]
th_14_5 [lemma, in Cantor.gamma0.Gamma0]
Tools [library]
transfinite_induction_Q [definition, in Cantor.epsilon0.EPSILON0]
transfinite_induction [definition, in Cantor.epsilon0.EPSILON0]
transfinite_induction_Q [definition, in Cantor.gamma0.Gamma0]
transfinite_induction [definition, in Cantor.gamma0.Gamma0]
transitivity [lemma, in Cantor.gamma0.Gamma0]
transitivity0 [lemma, in Cantor.gamma0.Gamma0]
trans_clos_is_trans [lemma, in Cantor.prelude.closure]
trans_clos [inductive, in Cantor.prelude.closure]
trans_aux [lemma, in Cantor.gamma0.Gamma0]
trans_proof.induc [variable, in Cantor.gamma0.Gamma0]
trans_proof.H23 [variable, in Cantor.gamma0.Gamma0]
trans_proof.H12 [variable, in Cantor.gamma0.Gamma0]
trans_proof.n3 [variable, in Cantor.gamma0.Gamma0]
trans_proof.n2 [variable, in Cantor.gamma0.Gamma0]
trans_proof.n1 [variable, in Cantor.gamma0.Gamma0]
trans_proof.c3 [variable, in Cantor.gamma0.Gamma0]
trans_proof.b3 [variable, in Cantor.gamma0.Gamma0]
trans_proof.a3 [variable, in Cantor.gamma0.Gamma0]
trans_proof.c2 [variable, in Cantor.gamma0.Gamma0]
trans_proof.b2 [variable, in Cantor.gamma0.Gamma0]
trans_proof.a2 [variable, in Cantor.gamma0.Gamma0]
trans_proof.c1 [variable, in Cantor.gamma0.Gamma0]
trans_proof.b1 [variable, in Cantor.gamma0.Gamma0]
trans_proof.a1 [variable, in Cantor.gamma0.Gamma0]
trans_proof [section, in Cantor.gamma0.Gamma0]
trichotomy [lemma, in Cantor.epsilon0.EPSILON0]
trichotomy_inf [definition, in Cantor.epsilon0.EPSILON0]
trichotomy_inf [definition, in Cantor.gamma0.Gamma0]
tricho_aux [lemma, in Cantor.gamma0.Gamma0]
tricho_lt_7 [lemma, in Cantor.gamma0.Gamma0]
tricho_lt_5 [lemma, in Cantor.gamma0.Gamma0]
tricho_lt_4' [lemma, in Cantor.gamma0.Gamma0]
tricho_lt_4 [lemma, in Cantor.gamma0.Gamma0]
tricho_lt_3 [lemma, in Cantor.gamma0.Gamma0]
tricho_lt_2' [lemma, in Cantor.gamma0.Gamma0]
tricho_lt_2 [lemma, in Cantor.gamma0.Gamma0]
t_trans [constructor, in Cantor.prelude.closure]
t_step [constructor, in Cantor.prelude.closure]
T1 [inductive, in Cantor.epsilon0.EPSILON0]
T1_size3 [lemma, in Cantor.epsilon0.EPSILON0]
T1_size2 [lemma, in Cantor.epsilon0.EPSILON0]
T1_size1 [lemma, in Cantor.epsilon0.EPSILON0]
T1_size [definition, in Cantor.epsilon0.EPSILON0]
T1_2_term [definition, in Cantor.epsilon0.EPSILON0]
T1_eq_dec [definition, in Cantor.epsilon0.EPSILON0]
T1_inj [definition, in Cantor.gamma0.Gamma0_prelude]
T1_injection_lt [lemma, in Cantor.gamma0.Gamma0]
T1_injection [lemma, in Cantor.gamma0.Gamma0]
T2 [inductive, in Cantor.gamma0.Gamma0_prelude]
T2_size_psi [lemma, in Cantor.gamma0.Gamma0]
T2_size4 [lemma, in Cantor.gamma0.Gamma0]
T2_size3 [lemma, in Cantor.gamma0.Gamma0]
T2_size2 [lemma, in Cantor.gamma0.Gamma0]
T2_size1 [lemma, in Cantor.gamma0.Gamma0]
T2_size [definition, in Cantor.gamma0.Gamma0]
T2_2_term [definition, in Cantor.gamma0.Gamma0]
V
val [definition, in Cantor.epsilon0.Goodstein]val_positive [lemma, in Cantor.epsilon0.Goodstein]
Variables [module, in Cantor.rpo.term]
Variables.eq_variable_dec [axiom, in Cantor.rpo.term]
Variables.var [axiom, in Cantor.rpo.term]
Vars [module, in Cantor.epsilon0.EPSILON0]
Vars [module, in Cantor.gamma0.Gamma0]
Vars.empty_set [inductive, in Cantor.epsilon0.EPSILON0]
Vars.empty_set [inductive, in Cantor.gamma0.Gamma0]
Vars.eq_variable_dec [lemma, in Cantor.epsilon0.EPSILON0]
Vars.eq_variable_dec [lemma, in Cantor.gamma0.Gamma0]
Vars.var [definition, in Cantor.epsilon0.EPSILON0]
Vars.var [definition, in Cantor.gamma0.Gamma0]
W
well_founded_P [definition, in Cantor.prelude.AccP]well_founded.R [variable, in Cantor.epsilon0.EPSILON0]
well_founded [section, in Cantor.epsilon0.EPSILON0]
well_founded_rpo [lemma, in Cantor.epsilon0.EPSILON0]
well_founded.R [variable, in Cantor.gamma0.Gamma0]
well_founded [section, in Cantor.gamma0.Gamma0]
well_founded_rpo [lemma, in Cantor.gamma0.Gamma0]
well_founded_length [lemma, in Cantor.prelude.more_list]
wf_trans [lemma, in Cantor.prelude.closure]
wf_lex [lemma, in Cantor.rpo.rpo]
Winner [lemma, in Cantor.epsilon0.Hydra]
Z
zero [constructor, in Cantor.epsilon0.EPSILON0]zero [constructor, in Cantor.gamma0.Gamma0_prelude]
zero_le [lemma, in Cantor.epsilon0.EPSILON0]
zero_nf [constructor, in Cantor.epsilon0.EPSILON0]
zero_lt [constructor, in Cantor.epsilon0.EPSILON0]
zero_lt_e0 [constructor, in Cantor.gamma0.Gamma0_prelude]
zero_nf [constructor, in Cantor.gamma0.Gamma0_prelude]
zero_finite [constructor, in Cantor.gamma0.Gamma0_prelude]
zero_not_lim [lemma, in Cantor.gamma0.Gamma0]
zero_lt_succ [lemma, in Cantor.gamma0.Gamma0]
Zero_correct [constructor, in Cantor.epsilon0.Goodstein]
other
_ ^ _ (cantor_scope) [notation, in Cantor.epsilon0.EPSILON0]_ * _ (cantor_scope) [notation, in Cantor.epsilon0.EPSILON0]
_ - _ (cantor_scope) [notation, in Cantor.epsilon0.EPSILON0]
_ + _ (cantor_scope) [notation, in Cantor.epsilon0.EPSILON0]
_ <= _ (cantor_scope) [notation, in Cantor.epsilon0.EPSILON0]
_ < _ (cantor_scope) [notation, in Cantor.epsilon0.EPSILON0]
F _ (cantor_scope) [notation, in Cantor.epsilon0.EPSILON0]
_ -G->* _ (cantor_scope) [notation, in Cantor.epsilon0.Goodstein]
_ -G-> _ (cantor_scope) [notation, in Cantor.epsilon0.Goodstein]
_ :: _ (cantor_scope) [notation, in Cantor.epsilon0.MSE0]
_ <= _ (g0_scope) [notation, in Cantor.gamma0.Gamma0_prelude]
_ < _ (g0_scope) [notation, in Cantor.gamma0.Gamma0_prelude]
F _ (g0_scope) [notation, in Cantor.gamma0.Gamma0_prelude]
[ _ , _ ] (g0_scope) [notation, in Cantor.gamma0.Gamma0_prelude]
_ + _ (g0_scope) [notation, in Cantor.gamma0.Gamma0]
_ ^ _ (nat_scope) [notation, in Cantor.misc.G4]
_ ^ _ (nat_scope) [notation, in Cantor.prelude.More_nat]
Notation Index
other
_ ^ _ (cantor_scope) [in Cantor.epsilon0.EPSILON0]_ * _ (cantor_scope) [in Cantor.epsilon0.EPSILON0]
_ - _ (cantor_scope) [in Cantor.epsilon0.EPSILON0]
_ + _ (cantor_scope) [in Cantor.epsilon0.EPSILON0]
_ <= _ (cantor_scope) [in Cantor.epsilon0.EPSILON0]
_ < _ (cantor_scope) [in Cantor.epsilon0.EPSILON0]
F _ (cantor_scope) [in Cantor.epsilon0.EPSILON0]
_ -G->* _ (cantor_scope) [in Cantor.epsilon0.Goodstein]
_ -G-> _ (cantor_scope) [in Cantor.epsilon0.Goodstein]
_ :: _ (cantor_scope) [in Cantor.epsilon0.MSE0]
_ <= _ (g0_scope) [in Cantor.gamma0.Gamma0_prelude]
_ < _ (g0_scope) [in Cantor.gamma0.Gamma0_prelude]
F _ (g0_scope) [in Cantor.gamma0.Gamma0_prelude]
[ _ , _ ] (g0_scope) [in Cantor.gamma0.Gamma0_prelude]
_ + _ (g0_scope) [in Cantor.gamma0.Gamma0]
_ ^ _ (nat_scope) [in Cantor.misc.G4]
_ ^ _ (nat_scope) [in Cantor.prelude.More_nat]
Module Index
E
Eps0_rpo [in Cantor.epsilon0.EPSILON0]Eps0_alg [in Cantor.epsilon0.EPSILON0]
Eps0_prec [in Cantor.epsilon0.EPSILON0]
Eps0_sig [in Cantor.epsilon0.EPSILON0]
G
Gamma0_rpo [in Cantor.gamma0.Gamma0]Gamma0_alg [in Cantor.gamma0.Gamma0]
Gamma0_prec [in Cantor.gamma0.Gamma0]
Gamma0_sig [in Cantor.gamma0.Gamma0]
M
Make [in Cantor.prelude.dickson]Make [in Cantor.prelude.list_set]
Make [in Cantor.rpo.term]
Make [in Cantor.prelude.list_permut]
Make [in Cantor.rpo.rpo]
Make.DecVar [in Cantor.rpo.term]
Make.DS [in Cantor.prelude.dickson]
Make.DS [in Cantor.prelude.list_set]
Make.DS [in Cantor.prelude.list_permut]
Make.F [in Cantor.rpo.term]
Make.LP [in Cantor.prelude.dickson]
Make.LP [in Cantor.prelude.list_set]
Make.LP [in Cantor.rpo.rpo]
Make.P [in Cantor.rpo.rpo]
Make.T [in Cantor.rpo.rpo]
Make.Term_eq_dec [in Cantor.rpo.term]
Make.VSet [in Cantor.rpo.term]
Make.X [in Cantor.rpo.term]
P
Permut [in Cantor.prelude.list_permut]Permut.DS [in Cantor.prelude.list_permut]
Precedence [in Cantor.rpo.rpo]
R
RPO [in Cantor.rpo.rpo]RPO.LP [in Cantor.rpo.rpo]
RPO.P [in Cantor.rpo.rpo]
RPO.T [in Cantor.rpo.rpo]
S
S [in Cantor.prelude.decidable_set]S [in Cantor.prelude.list_set]
Signature [in Cantor.rpo.term]
S.DS [in Cantor.prelude.list_set]
T
Term [in Cantor.rpo.term]Term.F [in Cantor.rpo.term]
Term.Term_eq_dec [in Cantor.rpo.term]
Term.X [in Cantor.rpo.term]
V
Variables [in Cantor.rpo.term]Vars [in Cantor.epsilon0.EPSILON0]
Vars [in Cantor.gamma0.Gamma0]
Variable Index
G
game.str [in Cantor.epsilon0.Hydra]game.str_hy [in Cantor.epsilon0.Hydra]
game.str_ok [in Cantor.epsilon0.Hydra]
L
lt_not_well_founded.f [in Cantor.epsilon0.EPSILON0]lt_incl_rpo.H [in Cantor.gamma0.Gamma0]
lt_incl_rpo.nf2 [in Cantor.gamma0.Gamma0]
lt_incl_rpo.nf1 [in Cantor.gamma0.Gamma0]
lt_incl_rpo.Hrec [in Cantor.gamma0.Gamma0]
lt_incl_rpo.Hsize [in Cantor.gamma0.Gamma0]
lt_incl_rpo.n2 [in Cantor.gamma0.Gamma0]
lt_incl_rpo.n1 [in Cantor.gamma0.Gamma0]
lt_incl_rpo.c2 [in Cantor.gamma0.Gamma0]
lt_incl_rpo.b2 [in Cantor.gamma0.Gamma0]
lt_incl_rpo.a2 [in Cantor.gamma0.Gamma0]
lt_incl_rpo.c1 [in Cantor.gamma0.Gamma0]
lt_incl_rpo.b1 [in Cantor.gamma0.Gamma0]
lt_incl_rpo.a1 [in Cantor.gamma0.Gamma0]
lt_incl_rpo.s [in Cantor.gamma0.Gamma0]
M
Make.DoubleRecursion.Pl2 [in Cantor.rpo.term]Make.DoubleRecursion.P2 [in Cantor.rpo.term]
Make.Recursion.P [in Cantor.rpo.term]
Make.Recursion.Pl [in Cantor.rpo.term]
P
partial_fix.FixPoint.F_ext [in Cantor.prelude.PartialFix]partial_fix.FixPoint.F [in Cantor.prelude.PartialFix]
partial_fix.FixPoint.P [in Cantor.prelude.PartialFix]
partial_fix.Acc_iterP.F [in Cantor.prelude.PartialFix]
partial_fix.Acc_iterP.P [in Cantor.prelude.PartialFix]
partial_fix.D_Acc [in Cantor.prelude.PartialFix]
partial_fix.gt_D [in Cantor.prelude.PartialFix]
partial_fix.lt_D [in Cantor.prelude.PartialFix]
partial_fix.lt [in Cantor.prelude.PartialFix]
partial_fix.D [in Cantor.prelude.PartialFix]
partial_fix.T [in Cantor.prelude.PartialFix]
phi_to_psi.alpha [in Cantor.gamma0.Gamma0]
predecessor.c [in Cantor.epsilon0.Goodstein]
predecessor.coeff_ok [in Cantor.epsilon0.Goodstein]
predecessor.N [in Cantor.epsilon0.Goodstein]
predecessor.nf_c [in Cantor.epsilon0.Goodstein]
predecessor.N0 [in Cantor.epsilon0.Goodstein]
predecessor.recurr [in Cantor.epsilon0.Goodstein]
R
restricted_recursion.R [in Cantor.prelude.AccP]restricted_recursion.P [in Cantor.prelude.AccP]
restricted_recursion.A [in Cantor.prelude.AccP]
S
Sequences.A [in Cantor.prelude.not_decreasing]Sequences.R [in Cantor.prelude.not_decreasing]
Sequences.seq_intro.is_in_seq [in Cantor.prelude.not_decreasing]
Sequences.seq_intro.seq [in Cantor.prelude.not_decreasing]
Sequences.W [in Cantor.prelude.not_decreasing]
T
Term.DoubleRecursion.Pl2 [in Cantor.rpo.term]Term.DoubleRecursion.P2 [in Cantor.rpo.term]
Term.Recursion.P [in Cantor.rpo.term]
Term.Recursion.Pl [in Cantor.rpo.term]
trans_proof.induc [in Cantor.gamma0.Gamma0]
trans_proof.H23 [in Cantor.gamma0.Gamma0]
trans_proof.H12 [in Cantor.gamma0.Gamma0]
trans_proof.n3 [in Cantor.gamma0.Gamma0]
trans_proof.n2 [in Cantor.gamma0.Gamma0]
trans_proof.n1 [in Cantor.gamma0.Gamma0]
trans_proof.c3 [in Cantor.gamma0.Gamma0]
trans_proof.b3 [in Cantor.gamma0.Gamma0]
trans_proof.a3 [in Cantor.gamma0.Gamma0]
trans_proof.c2 [in Cantor.gamma0.Gamma0]
trans_proof.b2 [in Cantor.gamma0.Gamma0]
trans_proof.a2 [in Cantor.gamma0.Gamma0]
trans_proof.c1 [in Cantor.gamma0.Gamma0]
trans_proof.b1 [in Cantor.gamma0.Gamma0]
trans_proof.a1 [in Cantor.gamma0.Gamma0]
W
well_founded.R [in Cantor.epsilon0.EPSILON0]well_founded.R [in Cantor.gamma0.Gamma0]
Library Index
A
AccPC
closureD
decidable_setdickson
E
EPSILON0G
Gamma0Gamma0_length
Gamma0_prelude
Goodstein
G4
H
HydraL
list_permutlist_set
M
more_listMore_nat
MSE0
N
not_decreasingP
PartialFixR
rpoT
termTools
Lemma Index
A
accElim3 [in Cantor.prelude.AccP]AccElim3 [in Cantor.prelude.AccP]
acc_trans [in Cantor.prelude.closure]
acc_imp [in Cantor.prelude.not_decreasing]
app_equiv_assoc [in Cantor.epsilon0.MSE0]
app_equiv_comm [in Cantor.epsilon0.MSE0]
ap_plusR [in Cantor.epsilon0.EPSILON0]
ap_plus [in Cantor.epsilon0.EPSILON0]
ap_phi0R [in Cantor.epsilon0.EPSILON0]
ap_phi0 [in Cantor.epsilon0.EPSILON0]
B
big_number_eq [in Cantor.misc.G4]C
Cantor_normal_form [in Cantor.epsilon0.EPSILON0]compare_reflectR [in Cantor.epsilon0.EPSILON0]
compare_rw3 [in Cantor.epsilon0.EPSILON0]
compare_rw2 [in Cantor.epsilon0.EPSILON0]
compare_rw1 [in Cantor.epsilon0.EPSILON0]
compare_reflect [in Cantor.epsilon0.EPSILON0]
compare_ok_1 [in Cantor.epsilon0.EPSILON0]
compare_rw_gt [in Cantor.gamma0.Gamma0]
compare_rw_eq [in Cantor.gamma0.Gamma0]
compare_rw_lt [in Cantor.gamma0.Gamma0]
compare_gt_rw [in Cantor.gamma0.Gamma0]
compare_eq_rw [in Cantor.gamma0.Gamma0]
compare_lt_rw [in Cantor.gamma0.Gamma0]
compare_reflect [in Cantor.gamma0.Gamma0]
cons_unicity [in Cantor.epsilon0.EPSILON0]
cons_ambiguity [in Cantor.epsilon0.EPSILON0]
cons_lt_epsilon0 [in Cantor.gamma0.Gamma0]
cons_rw [in Cantor.gamma0.Gamma0]
correct_succ [in Cantor.epsilon0.Goodstein]
E
epsilon_fxp [in Cantor.gamma0.Gamma0]epsilon0_as_lub [in Cantor.gamma0.Gamma0]
Eps0_prec.prec_transitive [in Cantor.epsilon0.EPSILON0]
Eps0_prec.prec_antisym [in Cantor.epsilon0.EPSILON0]
Eps0_prec.prec_dec [in Cantor.epsilon0.EPSILON0]
Eps0_sig.eq_symbol_dec [in Cantor.epsilon0.EPSILON0]
equiv_cong2 [in Cantor.epsilon0.MSE0]
equiv_cong1 [in Cantor.epsilon0.MSE0]
equiv_perm [in Cantor.epsilon0.MSE0]
equiv_tail [in Cantor.epsilon0.MSE0]
equiv_cons [in Cantor.epsilon0.MSE0]
equiv_trans [in Cantor.epsilon0.MSE0]
equiv_sym [in Cantor.epsilon0.MSE0]
equiv_refl [in Cantor.epsilon0.MSE0]
Euc1 [in Cantor.prelude.More_nat]
Euc2 [in Cantor.prelude.More_nat]
exists_map12_without_repetition [in Cantor.prelude.more_list]
exists_map_without_repetition [in Cantor.prelude.more_list]
exp_fin_omega [in Cantor.epsilon0.EPSILON0]
exp_compat [in Cantor.epsilon0.EPSILON0]
exp_F_compat [in Cantor.epsilon0.EPSILON0]
F
Final [in Cantor.misc.G4]final_no_future [in Cantor.misc.G4]
find_not_mem [in Cantor.prelude.more_list]
finite_ltR [in Cantor.epsilon0.EPSILON0]
finite_lt [in Cantor.epsilon0.EPSILON0]
finite_is_finite [in Cantor.gamma0.Gamma0]
finite_lt_omega [in Cantor.gamma0.Gamma0]
f_decreases [in Cantor.epsilon0.EPSILON0]
f_not_in_normal_form [in Cantor.epsilon0.EPSILON0]
f_Sn [in Cantor.misc.G4]
F_not_lim [in Cantor.gamma0.Gamma0]
F1 [in Cantor.misc.G4]
F2 [in Cantor.misc.G4]
F27 [in Cantor.misc.G4]
F28 [in Cantor.misc.G4]
F3 [in Cantor.misc.G4]
F4 [in Cantor.misc.G4]
G
Gamma0_prec.prec_transitive [in Cantor.gamma0.Gamma0]Gamma0_prec.prec_antisym [in Cantor.gamma0.Gamma0]
Gamma0_prec.prec_dec [in Cantor.gamma0.Gamma0]
Gamma0_sig.eq_symbol_dec [in Cantor.gamma0.Gamma0]
get_predecessor [in Cantor.prelude.More_nat]
Goodstein_thm [in Cantor.epsilon0.Goodstein]
Goodstein_decrease [in Cantor.epsilon0.Goodstein]
goodstein_next_ord_correct [in Cantor.epsilon0.Goodstein]
goodstein_next_ord_nf [in Cantor.epsilon0.Goodstein]
goodstein_next_ord_lt [in Cantor.epsilon0.Goodstein]
gpred_lt [in Cantor.epsilon0.Goodstein]
G4_length [in Cantor.misc.G4]
H
head_lt_cons [in Cantor.epsilon0.EPSILON0]head_at_l_S_cons [in Cantor.epsilon0.Hydra]
head_at_l_O_cons [in Cantor.epsilon0.Hydra]
head_at_l_S_nil [in Cantor.epsilon0.Hydra]
head_at_l_zero_nil [in Cantor.epsilon0.Hydra]
head_at_l_nil [in Cantor.epsilon0.Hydra]
head_at_S_cons [in Cantor.epsilon0.Hydra]
head_at_O_cons [in Cantor.epsilon0.Hydra]
head_at_S_nil [in Cantor.epsilon0.Hydra]
head_at_zero_nil [in Cantor.epsilon0.Hydra]
head_at_nil [in Cantor.epsilon0.Hydra]
Hydra_answers [in Cantor.epsilon0.Hydra]
Hydra_answers_nil [in Cantor.epsilon0.Hydra]
h2ol_nfs [in Cantor.epsilon0.Hydra]
h2o_nf [in Cantor.epsilon0.Hydra]
I
inj_monoR [in Cantor.gamma0.Gamma0]inj_mono [in Cantor.gamma0.Gamma0]
inv_trans [in Cantor.prelude.closure]
in_remove [in Cantor.prelude.more_list]
in_map_in [in Cantor.prelude.more_list]
in_in_map [in Cantor.prelude.more_list]
is_limit_ab [in Cantor.gamma0.Gamma0]
is_limit_intro [in Cantor.gamma0.Gamma0]
is_limit_cons_inv [in Cantor.gamma0.Gamma0]
is_limit_not_succ [in Cantor.gamma0.Gamma0]
is_succ_not_lim [in Cantor.gamma0.Gamma0]
is_finite_finite [in Cantor.gamma0.Gamma0]
L
Legend [in Cantor.epsilon0.Hydra]length_abnc [in Cantor.gamma0.Gamma0_length]
length_ab [in Cantor.gamma0.Gamma0_length]
length_psi [in Cantor.gamma0.Gamma0_length]
length_n [in Cantor.gamma0.Gamma0_length]
length_c [in Cantor.gamma0.Gamma0_length]
length_b [in Cantor.gamma0.Gamma0_length]
length_a [in Cantor.gamma0.Gamma0_length]
length_map [in Cantor.prelude.more_list]
lex_trans [in Cantor.rpo.rpo]
le_succ_succ [in Cantor.epsilon0.EPSILON0]
le_phi0_phi0 [in Cantor.epsilon0.EPSILON0]
le_tail [in Cantor.epsilon0.EPSILON0]
le_zero_inv [in Cantor.epsilon0.EPSILON0]
le_inv [in Cantor.epsilon0.EPSILON0]
le_lt_trans [in Cantor.epsilon0.EPSILON0]
le_trans [in Cantor.epsilon0.EPSILON0]
le_plus_l [in Cantor.gamma0.Gamma0]
le_plus_r [in Cantor.gamma0.Gamma0]
le_b_phi_ab [in Cantor.gamma0.Gamma0]
le_one_cons [in Cantor.gamma0.Gamma0]
le_cons_tail [in Cantor.gamma0.Gamma0]
le_trans [in Cantor.gamma0.Gamma0]
le_lt_trans [in Cantor.gamma0.Gamma0]
le_inv_nc [in Cantor.gamma0.Gamma0]
le_psi_term_le [in Cantor.gamma0.Gamma0]
le_zero_alpha [in Cantor.gamma0.Gamma0]
limit_plus_F_ok [in Cantor.gamma0.Gamma0]
limit_plus_F_inv0 [in Cantor.gamma0.Gamma0]
limit_plus_F_lim [in Cantor.gamma0.Gamma0]
limit_plus_F_plus [in Cantor.gamma0.Gamma0]
list_size_size_eq [in Cantor.prelude.more_list]
list_size_fold [in Cantor.prelude.more_list]
list_size_app [in Cantor.prelude.more_list]
list_size_tl_compat [in Cantor.prelude.more_list]
list_app_length [in Cantor.prelude.more_list]
log_nf [in Cantor.epsilon0.EPSILON0]
ltM_head [in Cantor.epsilon0.MSE0]
ltM_tail [in Cantor.epsilon0.MSE0]
ltM_lt [in Cantor.epsilon0.MSE0]
ltM_appR [in Cantor.epsilon0.MSE0]
ltM_app [in Cantor.epsilon0.MSE0]
ltM_cons [in Cantor.epsilon0.MSE0]
ltM_inv3 [in Cantor.epsilon0.MSE0]
ltM_inv2 [in Cantor.epsilon0.MSE0]
ltM_inv [in Cantor.epsilon0.MSE0]
ltM_trans_2 [in Cantor.epsilon0.MSE0]
ltM_trans_1 [in Cantor.epsilon0.MSE0]
ltM_trans [in Cantor.epsilon0.MSE0]
ltM_equiv_ltMR [in Cantor.epsilon0.MSE0]
ltM_equiv_ltM [in Cantor.epsilon0.MSE0]
lt_succ_le [in Cantor.epsilon0.EPSILON0]
lt_succ_le_2 [in Cantor.epsilon0.EPSILON0]
lt_succ_le_R [in Cantor.epsilon0.EPSILON0]
lt_phi0_phi0 [in Cantor.epsilon0.EPSILON0]
lt_succ_succ [in Cantor.epsilon0.EPSILON0]
lt_succ [in Cantor.epsilon0.EPSILON0]
lt_intro [in Cantor.epsilon0.EPSILON0]
lt_a_phi0_a [in Cantor.epsilon0.EPSILON0]
lt_inc_rpo_0 [in Cantor.epsilon0.EPSILON0]
lt_subterm2 [in Cantor.epsilon0.EPSILON0]
lt_subterm1 [in Cantor.epsilon0.EPSILON0]
lt_inv_le [in Cantor.epsilon0.EPSILON0]
lt_not_le [in Cantor.epsilon0.EPSILON0]
lt_le_trans [in Cantor.epsilon0.EPSILON0]
lt_not_wf [in Cantor.epsilon0.EPSILON0]
lt_not_gt [in Cantor.epsilon0.EPSILON0]
lt_trans [in Cantor.epsilon0.EPSILON0]
lt_inv_b [in Cantor.epsilon0.EPSILON0]
lt_inv_nb [in Cantor.epsilon0.EPSILON0]
lt_irr [in Cantor.epsilon0.EPSILON0]
lt_inv [in Cantor.epsilon0.EPSILON0]
lt_not_gt [in Cantor.gamma0.Gamma0]
lt_epsilon0_succ [in Cantor.gamma0.Gamma0]
lt_epsilon0_trans [in Cantor.gamma0.Gamma0]
lt_epsilon0_okR [in Cantor.gamma0.Gamma0]
lt_epsilon0_ok [in Cantor.gamma0.Gamma0]
lt_a_phi_ab [in Cantor.gamma0.Gamma0]
lt_inc_rpo_0 [in Cantor.gamma0.Gamma0]
lt_rpo_cons_cons [in Cantor.gamma0.Gamma0]
lt_subterm1 [in Cantor.gamma0.Gamma0]
lt_succ_le [in Cantor.gamma0.Gamma0]
lt_succ [in Cantor.gamma0.Gamma0]
lt_compatR [in Cantor.gamma0.Gamma0]
lt_compat [in Cantor.gamma0.Gamma0]
lt_omega_is_finite [in Cantor.gamma0.Gamma0]
lt_omega_inv [in Cantor.gamma0.Gamma0]
lt_cons_omega_inv [in Cantor.gamma0.Gamma0]
lt_one_inv [in Cantor.gamma0.Gamma0]
lt_tail [in Cantor.gamma0.Gamma0]
lt_tail0 [in Cantor.gamma0.Gamma0]
lt_alpha_cons [in Cantor.gamma0.Gamma0]
lt_alpha_psi [in Cantor.gamma0.Gamma0]
lt_beta_cons [in Cantor.gamma0.Gamma0]
lt_beta_psi [in Cantor.gamma0.Gamma0]
lt_le_trans [in Cantor.gamma0.Gamma0]
lt_than_psi [in Cantor.gamma0.Gamma0]
lt_irr [in Cantor.gamma0.Gamma0]
lt_lt_Sn [in Cantor.prelude.More_nat]
lt_ltM2 [in Cantor.epsilon0.MSE0]
lt_ltM [in Cantor.epsilon0.MSE0]
lub_mono [in Cantor.gamma0.Gamma0]
lub_unicity [in Cantor.gamma0.Gamma0]
L1 [in Cantor.misc.G4]
L2 [in Cantor.misc.G4]
L3 [in Cantor.misc.G4]
L4 [in Cantor.misc.G4]
L5 [in Cantor.misc.G4]
M
Make.acc_build [in Cantor.rpo.rpo]Make.acc_lex_drop_proof [in Cantor.rpo.rpo]
Make.ac_syntactic [in Cantor.prelude.list_permut]
Make.ac_syntactic_aux [in Cantor.prelude.list_permut]
Make.add_comm [in Cantor.prelude.list_set]
Make.add_12 [in Cantor.prelude.list_set]
Make.add_2 [in Cantor.prelude.list_set]
Make.add_1 [in Cantor.prelude.list_set]
Make.add_prf [in Cantor.prelude.list_set]
Make.cardinal_eq_set [in Cantor.prelude.list_set]
Make.cardinal_union [in Cantor.prelude.list_set]
Make.cardinal_union_inter_12 [in Cantor.prelude.list_set]
Make.cardinal_union_2 [in Cantor.prelude.list_set]
Make.cardinal_union_1 [in Cantor.prelude.list_set]
Make.cardinal_subset [in Cantor.prelude.list_set]
Make.cons_permut_in [in Cantor.prelude.list_permut]
Make.context_multiset_extension_step_app2 [in Cantor.prelude.dickson]
Make.context_trans_clos_multiset_extension_step_app1 [in Cantor.prelude.dickson]
Make.context_multiset_extension_step_app1 [in Cantor.prelude.dickson]
Make.context_list_permut_app2 [in Cantor.prelude.list_permut]
Make.context_list_permut_app1 [in Cantor.prelude.list_permut]
Make.context_list_permut_cons [in Cantor.prelude.list_permut]
Make.DecVar.eq_A_dec [in Cantor.rpo.term]
Make.dickson [in Cantor.prelude.dickson]
Make.dickson_aux3 [in Cantor.prelude.dickson]
Make.dickson_aux2 [in Cantor.prelude.dickson]
Make.dickson_aux1 [in Cantor.prelude.dickson]
Make.empty_subst_is_id_list [in Cantor.rpo.term]
Make.empty_subst_is_id [in Cantor.rpo.term]
Make.eq_set_list_permut_support [in Cantor.prelude.list_set]
Make.eq_set_trans [in Cantor.prelude.list_set]
Make.eq_set_sym [in Cantor.prelude.list_set]
Make.eq_set_refl [in Cantor.prelude.list_set]
Make.eq_set_dec [in Cantor.prelude.list_set]
Make.eq_term_dec [in Cantor.rpo.term]
Make.filter_union [in Cantor.prelude.list_set]
Make.filter_2 [in Cantor.prelude.list_set]
Make.filter_2_list [in Cantor.prelude.list_set]
Make.filter_1 [in Cantor.prelude.list_set]
Make.filter_1_list [in Cantor.prelude.list_set]
Make.included_remove_red [in Cantor.prelude.list_set]
Make.included_filter_aux [in Cantor.prelude.list_set]
Make.inter_12 [in Cantor.prelude.list_set]
Make.inter_12_aux [in Cantor.prelude.list_set]
Make.inter_2 [in Cantor.prelude.list_set]
Make.inter_2_aux [in Cantor.prelude.list_set]
Make.inter_1 [in Cantor.prelude.list_set]
Make.inter_1_aux [in Cantor.prelude.list_set]
Make.in_permut_in [in Cantor.prelude.list_permut]
Make.in_mult_S [in Cantor.prelude.list_permut]
Make.in_sn_sn [in Cantor.rpo.rpo]
Make.is_a_pos_exists_subtem [in Cantor.rpo.term]
Make.lex1 [in Cantor.rpo.rpo]
Make.lex1_bis [in Cantor.rpo.rpo]
Make.lex2 [in Cantor.rpo.rpo]
Make.lex3 [in Cantor.rpo.rpo]
Make.list_permut_acc [in Cantor.prelude.dickson]
Make.list_permut_multiset_extension_step_2 [in Cantor.prelude.dickson]
Make.list_permut_multiset_extension_step_1 [in Cantor.prelude.dickson]
Make.list_permut_dec [in Cantor.prelude.list_permut]
Make.list_permut_length_2 [in Cantor.prelude.list_permut]
Make.list_permut_length_1 [in Cantor.prelude.list_permut]
Make.list_permut_map [in Cantor.prelude.list_permut]
Make.list_permut_size [in Cantor.prelude.list_permut]
Make.list_permut_length [in Cantor.prelude.list_permut]
Make.list_permut_remove_hd [in Cantor.prelude.list_permut]
Make.list_permut_app_app [in Cantor.prelude.list_permut]
Make.list_permut_add_cons_inside [in Cantor.prelude.list_permut]
Make.list_permut_add_inside [in Cantor.prelude.list_permut]
Make.list_permut_nil [in Cantor.prelude.list_permut]
Make.list_permut_trans [in Cantor.prelude.list_permut]
Make.list_permut_sym [in Cantor.prelude.list_permut]
Make.list_permut_refl [in Cantor.prelude.list_permut]
Make.list_permut_map_acc [in Cantor.rpo.rpo]
Make.mem_dec [in Cantor.prelude.list_set]
Make.multiplicity_app [in Cantor.prelude.list_permut]
Make.multiset_closure [in Cantor.prelude.dickson]
Make.out_mult_O [in Cantor.prelude.list_permut]
Make.o_size3_trans [in Cantor.rpo.rpo]
Make.projection_list_of_SN_terms [in Cantor.rpo.rpo]
Make.remove_red_included [in Cantor.prelude.list_set]
Make.remove_context_list_permut_app2 [in Cantor.prelude.list_permut]
Make.remove_context_list_permut_cons [in Cantor.prelude.list_permut]
Make.replace_at_pos_list_replace_at_pos_in_subterm [in Cantor.rpo.term]
Make.replace_at_pos_is_replace_at_pos2 [in Cantor.rpo.term]
Make.replace_at_pos_is_replace_at_pos1 [in Cantor.rpo.term]
Make.replace_at_pos_unfold [in Cantor.rpo.term]
Make.rpo_add_context [in Cantor.rpo.rpo]
Make.rpo_subst [in Cantor.rpo.rpo]
Make.rpo_mul_trans_clos [in Cantor.rpo.rpo]
Make.rpo_lex_rest_same_length [in Cantor.rpo.rpo]
Make.rpo_trans [in Cantor.rpo.rpo]
Make.rpo_closure [in Cantor.rpo.rpo]
Make.rpo_subterm [in Cantor.rpo.rpo]
Make.rpo_lex_same_length [in Cantor.rpo.rpo]
Make.size_subterm_at_pos [in Cantor.rpo.term]
Make.size_direct_subterm [in Cantor.rpo.term]
Make.size_ge_one [in Cantor.rpo.term]
Make.size_unfold [in Cantor.rpo.term]
Make.subset_cardinal_not_eq_not_eq_set [in Cantor.prelude.list_set]
Make.subset_subset_union [in Cantor.prelude.list_set]
Make.subset_compat [in Cantor.prelude.list_set]
Make.subset_compat_2 [in Cantor.prelude.list_set]
Make.subset_compat_1 [in Cantor.prelude.list_set]
Make.subset_filter [in Cantor.prelude.list_set]
Make.subset_inter_2 [in Cantor.prelude.list_set]
Make.subset_inter_1 [in Cantor.prelude.list_set]
Make.subset_union_2 [in Cantor.prelude.list_set]
Make.subset_union_1 [in Cantor.prelude.list_set]
Make.subset_dec [in Cantor.prelude.list_set]
Make.subst_comp_is_subst_comp [in Cantor.rpo.term]
Make.subst_comp_is_subst_comp_aux2 [in Cantor.rpo.term]
Make.subst_comp_is_subst_comp_aux1 [in Cantor.rpo.term]
Make.subterm_at_pos_apply_subst_apply_subst_subterm_at_pos [in Cantor.rpo.term]
Make.two_cases [in Cantor.prelude.dickson]
Make.two_cases_rpo [in Cantor.rpo.rpo]
Make.union_compat_eq_set [in Cantor.prelude.list_set]
Make.union_compat_subset_2 [in Cantor.prelude.list_set]
Make.union_compat_subset_1 [in Cantor.prelude.list_set]
Make.union_assoc [in Cantor.prelude.list_set]
Make.union_comm [in Cantor.prelude.list_set]
Make.union_empty_2 [in Cantor.prelude.list_set]
Make.union_empty_1 [in Cantor.prelude.list_set]
Make.union_12 [in Cantor.prelude.list_set]
Make.union_12_aux [in Cantor.prelude.list_set]
Make.union_2 [in Cantor.prelude.list_set]
Make.union_2_aux [in Cantor.prelude.list_set]
Make.union_1 [in Cantor.prelude.list_set]
Make.union_1_aux [in Cantor.prelude.list_set]
Make.well_formed_apply_subst [in Cantor.rpo.term]
Make.well_formed_fold [in Cantor.rpo.term]
Make.well_formed_unfold [in Cantor.rpo.term]
Make.wf_rpo [in Cantor.rpo.rpo]
Make.wf_rpo_term [in Cantor.rpo.rpo]
Make.wf_on_mul_rest [in Cantor.rpo.rpo]
Make.wf_on_lex_rest [in Cantor.rpo.rpo]
Make.wf_on_rest [in Cantor.rpo.rpo]
Make.wf_size3 [in Cantor.rpo.rpo]
Make.wf_size2 [in Cantor.rpo.rpo]
Make.wf_size [in Cantor.rpo.rpo]
Make.without_red_permut [in Cantor.prelude.list_set]
Make.without_red_remove_not_common [in Cantor.prelude.list_set]
Make.without_red_remove_not_common_aux [in Cantor.prelude.list_set]
Make.without_red_add_without_red [in Cantor.prelude.list_set]
Make.without_red_singleton [in Cantor.prelude.list_set]
Make.without_red_nil [in Cantor.prelude.list_set]
Make.without_red_add [in Cantor.prelude.list_set]
Make.without_red_remove [in Cantor.prelude.list_set]
Make.without_red_remove_red [in Cantor.prelude.list_set]
Make.without_red_filter_aux [in Cantor.prelude.list_set]
map_app [in Cantor.prelude.more_list]
map_map [in Cantor.prelude.more_list]
max_assoc [in Cantor.epsilon0.EPSILON0]
max_nf [in Cantor.epsilon0.EPSILON0]
max_dec [in Cantor.epsilon0.EPSILON0]
max_comm [in Cantor.epsilon0.EPSILON0]
max_le_1 [in Cantor.epsilon0.EPSILON0]
max_le_regL [in Cantor.prelude.More_nat]
max_le_regR [in Cantor.prelude.More_nat]
minus_le [in Cantor.epsilon0.EPSILON0]
minus_a_a [in Cantor.epsilon0.EPSILON0]
minus_lt [in Cantor.epsilon0.EPSILON0]
ml_1 [in Cantor.gamma0.Gamma0]
ml_psi [in Cantor.gamma0.Gamma0]
multiplicity_of_app [in Cantor.epsilon0.MSE0]
multiplicity_rw2 [in Cantor.epsilon0.MSE0]
multiplicity_rw1 [in Cantor.epsilon0.MSE0]
mult_a_1 [in Cantor.epsilon0.EPSILON0]
mult_1_a [in Cantor.epsilon0.EPSILON0]
mult_a_0 [in Cantor.epsilon0.EPSILON0]
mult_0_a [in Cantor.epsilon0.EPSILON0]
mult_compat [in Cantor.epsilon0.EPSILON0]
mult_fin_omega [in Cantor.epsilon0.EPSILON0]
N
nat_2_term_mono [in Cantor.epsilon0.EPSILON0]nat_lt_cons [in Cantor.epsilon0.EPSILON0]
nat_2_term_mono [in Cantor.gamma0.Gamma0]
nat_lt_psi [in Cantor.gamma0.Gamma0]
nat_lt_cons [in Cantor.gamma0.Gamma0]
nb_occ_app [in Cantor.prelude.more_list]
nexts_ok_R [in Cantor.misc.G4]
nexts_ok [in Cantor.misc.G4]
nexts_plus [in Cantor.misc.G4]
next_unicity [in Cantor.misc.G4]
nfs_to_nf [in Cantor.epsilon0.MSE0]
nf_Wf [in Cantor.epsilon0.EPSILON0]
nf_tower [in Cantor.epsilon0.EPSILON0]
nf_phi0 [in Cantor.epsilon0.EPSILON0]
nf_omega [in Cantor.epsilon0.EPSILON0]
nf_of_finite [in Cantor.epsilon0.EPSILON0]
nf_coeff_irrelevance [in Cantor.epsilon0.EPSILON0]
nf_intro [in Cantor.epsilon0.EPSILON0]
nf_tail_lt_nf [in Cantor.epsilon0.EPSILON0]
nf_inv2 [in Cantor.epsilon0.EPSILON0]
nf_inv1 [in Cantor.epsilon0.EPSILON0]
nf_intro [in Cantor.gamma0.Gamma0]
nf_nat_irrelevance [in Cantor.gamma0.Gamma0]
nf_Wf [in Cantor.gamma0.Gamma0]
nf_c2 [in Cantor.gamma0.Gamma0]
nf_c1 [in Cantor.gamma0.Gamma0]
nf_b2 [in Cantor.gamma0.Gamma0]
nf_b1 [in Cantor.gamma0.Gamma0]
nf_a2 [in Cantor.gamma0.Gamma0]
nf_a1 [in Cantor.gamma0.Gamma0]
nf_subterm [in Cantor.gamma0.Gamma0]
nf_finite_inv [in Cantor.gamma0.Gamma0]
nf_epsilon [in Cantor.gamma0.Gamma0]
nf_epsilon0 [in Cantor.gamma0.Gamma0]
nf_omega [in Cantor.gamma0.Gamma0]
nf_inv_tail [in Cantor.gamma0.Gamma0]
nf_c [in Cantor.gamma0.Gamma0]
nf_b [in Cantor.gamma0.Gamma0]
nf_a [in Cantor.gamma0.Gamma0]
nf_unicity [in Cantor.epsilon0.MSE0]
nf_to_nfs [in Cantor.epsilon0.MSE0]
nf_multiplicity_big [in Cantor.epsilon0.MSE0]
nf_multiplicity_tail [in Cantor.epsilon0.MSE0]
nf_multiplicity_head [in Cantor.epsilon0.MSE0]
nf_nfs [in Cantor.epsilon0.MSE0]
nf2_phi0R [in Cantor.epsilon0.EPSILON0]
nf2_phi0 [in Cantor.epsilon0.EPSILON0]
nf2_intro [in Cantor.epsilon0.EPSILON0]
none_nb_occ_O [in Cantor.prelude.more_list]
not_lt_zero [in Cantor.epsilon0.EPSILON0]
not_lt_zero [in Cantor.gamma0.Gamma0]
not_decreasing [in Cantor.prelude.not_decreasing]
not_decreasing_aux [in Cantor.prelude.not_decreasing]
not_acc [in Cantor.prelude.not_decreasing]
no_critical [in Cantor.gamma0.Gamma0]
nth_error_ok_in [in Cantor.prelude.more_list]
nth_error_map [in Cantor.prelude.more_list]
O
omega_term_ambiguity [in Cantor.epsilon0.EPSILON0]omega_exp_rw [in Cantor.epsilon0.EPSILON0]
omega_minus_one [in Cantor.epsilon0.EPSILON0]
omega_lt_epsilon [in Cantor.gamma0.Gamma0]
omega_lt_epsilon0 [in Cantor.gamma0.Gamma0]
ordinal_finite [in Cantor.epsilon0.EPSILON0]
ordinal_finite [in Cantor.gamma0.Gamma0]
P
PFix_eq [in Cantor.prelude.PartialFix]PFix_F_inv [in Cantor.prelude.PartialFix]
PFix_F_eq [in Cantor.prelude.PartialFix]
phi_mono_RR [in Cantor.gamma0.Gamma0]
phi_psi [in Cantor.gamma0.Gamma0]
phi_to_psi_6 [in Cantor.gamma0.Gamma0]
phi_to_psi_5 [in Cantor.gamma0.Gamma0]
phi_to_psi_4 [in Cantor.gamma0.Gamma0]
phi_to_psi_3 [in Cantor.gamma0.Gamma0]
phi_to_psi_2 [in Cantor.gamma0.Gamma0]
phi_to_psi_1 [in Cantor.gamma0.Gamma0]
phi_inj_r [in Cantor.gamma0.Gamma0]
phi_mono_weak_r [in Cantor.gamma0.Gamma0]
phi_mono_r [in Cantor.gamma0.Gamma0]
phi_of_psi_plus_finite [in Cantor.gamma0.Gamma0]
phi_principalR [in Cantor.gamma0.Gamma0]
phi_spec1 [in Cantor.gamma0.Gamma0]
phi_le_ge [in Cantor.gamma0.Gamma0]
phi_le [in Cantor.gamma0.Gamma0]
phi_fix [in Cantor.gamma0.Gamma0]
phi_of_any_cons [in Cantor.gamma0.Gamma0]
phi_nf [in Cantor.gamma0.Gamma0]
phi_cases [in Cantor.gamma0.Gamma0]
phi_cases' [in Cantor.gamma0.Gamma0]
phi_cases_aux [in Cantor.gamma0.Gamma0]
phi_of_psi_succ [in Cantor.gamma0.Gamma0]
phi_alpha_zero [in Cantor.gamma0.Gamma0]
phi_principal [in Cantor.gamma0.Gamma0]
phi_to_psi [in Cantor.gamma0.Gamma0]
phi_of_psi [in Cantor.gamma0.Gamma0]
phi0_plus_mult [in Cantor.epsilon0.EPSILON0]
phi0_log [in Cantor.epsilon0.EPSILON0]
phi0_ltR [in Cantor.epsilon0.EPSILON0]
phi0_lt [in Cantor.epsilon0.EPSILON0]
plus_compat [in Cantor.epsilon0.EPSILON0]
plus_is_zero [in Cantor.epsilon0.EPSILON0]
plus_to_cons [in Cantor.epsilon0.EPSILON0]
plus_nf [in Cantor.epsilon0.EPSILON0]
plus_nf0 [in Cantor.epsilon0.EPSILON0]
plus_cons_cons_rw3 [in Cantor.epsilon0.EPSILON0]
plus_cons_cons_rw2 [in Cantor.epsilon0.EPSILON0]
plus_cons_cons_rw1 [in Cantor.epsilon0.EPSILON0]
plus_not_comm [in Cantor.epsilon0.EPSILON0]
plus_fin_omega [in Cantor.epsilon0.EPSILON0]
plus_a_zero [in Cantor.epsilon0.EPSILON0]
plus_zero [in Cantor.epsilon0.EPSILON0]
plus_mono_l_weak [in Cantor.gamma0.Gamma0]
plus_mono_r [in Cantor.gamma0.Gamma0]
plus_nf [in Cantor.gamma0.Gamma0]
plus_alpha_0 [in Cantor.gamma0.Gamma0]
power_of_1 [in Cantor.prelude.More_nat]
pred_of_succ [in Cantor.gamma0.Gamma0]
pred_of_limit [in Cantor.gamma0.Gamma0]
pred_of_cons' [in Cantor.gamma0.Gamma0]
pred_of_cons [in Cantor.gamma0.Gamma0]
pred_of_power [in Cantor.prelude.More_nat]
prop_map12_without_repetition [in Cantor.prelude.more_list]
prop_map_without_repetition [in Cantor.prelude.more_list]
psi_eq [in Cantor.gamma0.Gamma0_prelude]
psi_principal [in Cantor.gamma0.Gamma0]
psi_lt_epsilon0 [in Cantor.gamma0.Gamma0]
psi_relevance [in Cantor.gamma0.Gamma0]
psi_le_cons [in Cantor.gamma0.Gamma0]
R
reachable_Rgstar [in Cantor.misc.G4]reduce_assoc_list [in Cantor.prelude.more_list]
Rh_decrease [in Cantor.epsilon0.Hydra]
Rh_head [in Cantor.epsilon0.Hydra]
Rn_decrease [in Cantor.epsilon0.Hydra]
Rn_head [in Cantor.epsilon0.Hydra]
rpo_trans [in Cantor.epsilon0.EPSILON0]
rpo_7_1 [in Cantor.gamma0.Gamma0]
rpo_6_4 [in Cantor.gamma0.Gamma0]
rpo_6_1 [in Cantor.gamma0.Gamma0]
rpo_5_4 [in Cantor.gamma0.Gamma0]
rpo_5_1 [in Cantor.gamma0.Gamma0]
rpo_5_3 [in Cantor.gamma0.Gamma0]
rpo_5_2 [in Cantor.gamma0.Gamma0]
rpo_4_4 [in Cantor.gamma0.Gamma0]
rpo_4_1 [in Cantor.gamma0.Gamma0]
rpo_4_3 [in Cantor.gamma0.Gamma0]
rpo_4_2 [in Cantor.gamma0.Gamma0]
rpo_3_4 [in Cantor.gamma0.Gamma0]
rpo_3_1 [in Cantor.gamma0.Gamma0]
rpo_3_3 [in Cantor.gamma0.Gamma0]
rpo_3_2 [in Cantor.gamma0.Gamma0]
rpo_2_4 [in Cantor.gamma0.Gamma0]
rpo_2_1 [in Cantor.gamma0.Gamma0]
rpo_2_3 [in Cantor.gamma0.Gamma0]
rpo_2_2 [in Cantor.gamma0.Gamma0]
rpo_trans [in Cantor.gamma0.Gamma0]
R_inc_rpo [in Cantor.epsilon0.EPSILON0]
R_pred_Sn [in Cantor.gamma0.Gamma0]
R_predD_0 [in Cantor.gamma0.Gamma0]
R_inc_rpo [in Cantor.gamma0.Gamma0]
R1 [in Cantor.epsilon0.EPSILON0]
R1 [in Cantor.gamma0.Gamma0]
R1_decrease [in Cantor.epsilon0.Hydra]
R1_head [in Cantor.epsilon0.Hydra]
R2 [in Cantor.epsilon0.EPSILON0]
R2 [in Cantor.gamma0.Gamma0]
R3 [in Cantor.epsilon0.EPSILON0]
R3 [in Cantor.gamma0.Gamma0]
R4 [in Cantor.epsilon0.EPSILON0]
R4 [in Cantor.gamma0.Gamma0]
R5 [in Cantor.gamma0.Gamma0]
S
SF27 [in Cantor.misc.G4]SF3 [in Cantor.misc.G4]
Sh_head [in Cantor.epsilon0.Hydra]
some_nb_occ_Sn [in Cantor.prelude.more_list]
sort_nf [in Cantor.epsilon0.MSE0]
sort_equiv [in Cantor.epsilon0.MSE0]
sort_aux_nf [in Cantor.epsilon0.MSE0]
sort_aux_equiv [in Cantor.epsilon0.MSE0]
split_list_app_cons [in Cantor.prelude.more_list]
subterm_lt [in Cantor.gamma0.Gamma0]
succ_compat [in Cantor.epsilon0.EPSILON0]
succ_is_plus_one [in Cantor.epsilon0.EPSILON0]
succ_nf [in Cantor.epsilon0.EPSILON0]
succ_nf2 [in Cantor.epsilon0.EPSILON0]
succ_limit_dec [in Cantor.gamma0.Gamma0]
succ_nf [in Cantor.gamma0.Gamma0]
succ_as_plus [in Cantor.gamma0.Gamma0]
succ_of_cons [in Cantor.gamma0.Gamma0]
succ_lt_le [in Cantor.gamma0.Gamma0]
S1_decrease [in Cantor.epsilon0.Hydra]
S1_head [in Cantor.epsilon0.Hydra]
S2_decrease [in Cantor.epsilon0.Hydra]
S2_head [in Cantor.epsilon0.Hydra]
T
tail_lt_cons [in Cantor.epsilon0.EPSILON0]th_14_6 [in Cantor.gamma0.Gamma0]
th_14_5 [in Cantor.gamma0.Gamma0]
transitivity [in Cantor.gamma0.Gamma0]
transitivity0 [in Cantor.gamma0.Gamma0]
trans_clos_is_trans [in Cantor.prelude.closure]
trans_aux [in Cantor.gamma0.Gamma0]
trichotomy [in Cantor.epsilon0.EPSILON0]
tricho_aux [in Cantor.gamma0.Gamma0]
tricho_lt_7 [in Cantor.gamma0.Gamma0]
tricho_lt_5 [in Cantor.gamma0.Gamma0]
tricho_lt_4' [in Cantor.gamma0.Gamma0]
tricho_lt_4 [in Cantor.gamma0.Gamma0]
tricho_lt_3 [in Cantor.gamma0.Gamma0]
tricho_lt_2' [in Cantor.gamma0.Gamma0]
tricho_lt_2 [in Cantor.gamma0.Gamma0]
T1_size3 [in Cantor.epsilon0.EPSILON0]
T1_size2 [in Cantor.epsilon0.EPSILON0]
T1_size1 [in Cantor.epsilon0.EPSILON0]
T1_injection_lt [in Cantor.gamma0.Gamma0]
T1_injection [in Cantor.gamma0.Gamma0]
T2_size_psi [in Cantor.gamma0.Gamma0]
T2_size4 [in Cantor.gamma0.Gamma0]
T2_size3 [in Cantor.gamma0.Gamma0]
T2_size2 [in Cantor.gamma0.Gamma0]
T2_size1 [in Cantor.gamma0.Gamma0]
V
val_positive [in Cantor.epsilon0.Goodstein]Vars.eq_variable_dec [in Cantor.epsilon0.EPSILON0]
Vars.eq_variable_dec [in Cantor.gamma0.Gamma0]
W
well_founded_rpo [in Cantor.epsilon0.EPSILON0]well_founded_rpo [in Cantor.gamma0.Gamma0]
well_founded_length [in Cantor.prelude.more_list]
wf_trans [in Cantor.prelude.closure]
wf_lex [in Cantor.rpo.rpo]
Winner [in Cantor.epsilon0.Hydra]
Z
zero_le [in Cantor.epsilon0.EPSILON0]zero_not_lim [in Cantor.gamma0.Gamma0]
zero_lt_succ [in Cantor.gamma0.Gamma0]
Constructor Index
A
ap_intro [in Cantor.epsilon0.EPSILON0]ap_intro [in Cantor.gamma0.Gamma0_prelude]
C
coeff_lt [in Cantor.epsilon0.EPSILON0]cons [in Cantor.epsilon0.EPSILON0]
cons [in Cantor.gamma0.Gamma0_prelude]
cons_nf [in Cantor.epsilon0.EPSILON0]
cons_lt_e0 [in Cantor.gamma0.Gamma0_prelude]
cons_nf [in Cantor.gamma0.Gamma0_prelude]
cons_succ [in Cantor.gamma0.Gamma0]
Cons_correct [in Cantor.epsilon0.Goodstein]
D
depth1 [in Cantor.epsilon0.Hydra]depth2 [in Cantor.epsilon0.Hydra]
E
Eps0_prec.Mul [in Cantor.epsilon0.EPSILON0]Eps0_prec.Lex [in Cantor.epsilon0.EPSILON0]
Eps0_sig.Free [in Cantor.epsilon0.EPSILON0]
Eps0_sig.C [in Cantor.epsilon0.EPSILON0]
Eps0_sig.AC [in Cantor.epsilon0.EPSILON0]
Eps0_sig.ord_cons [in Cantor.epsilon0.EPSILON0]
Eps0_sig.ord_zero [in Cantor.epsilon0.EPSILON0]
Eps0_sig.nat_S [in Cantor.epsilon0.EPSILON0]
Eps0_sig.nat_0 [in Cantor.epsilon0.EPSILON0]
F
final_intro [in Cantor.misc.G4]finite_succ [in Cantor.gamma0.Gamma0]
G
Gamma0_prec.Mul [in Cantor.gamma0.Gamma0]Gamma0_prec.Lex [in Cantor.gamma0.Gamma0]
Gamma0_sig.Free [in Cantor.gamma0.Gamma0]
Gamma0_sig.C [in Cantor.gamma0.Gamma0]
Gamma0_sig.AC [in Cantor.gamma0.Gamma0]
Gamma0_sig.ord_cons [in Cantor.gamma0.Gamma0]
Gamma0_sig.ord_psi [in Cantor.gamma0.Gamma0]
Gamma0_sig.ord_zero [in Cantor.gamma0.Gamma0]
Gamma0_sig.nat_S [in Cantor.gamma0.Gamma0]
Gamma0_sig.nat_0 [in Cantor.gamma0.Gamma0]
H
hcons [in Cantor.epsilon0.Hydra]head [in Cantor.epsilon0.Hydra]
head_lt [in Cantor.epsilon0.EPSILON0]
I
is_limit_cons [in Cantor.gamma0.Gamma0]is_limit_0 [in Cantor.gamma0.Gamma0]
L
Later [in Cantor.epsilon0.Hydra]limit_plus_F_cons [in Cantor.gamma0.Gamma0]
limit_plus_F_0 [in Cantor.gamma0.Gamma0]
lt_7 [in Cantor.gamma0.Gamma0_prelude]
lt_6 [in Cantor.gamma0.Gamma0_prelude]
lt_5 [in Cantor.gamma0.Gamma0_prelude]
lt_4 [in Cantor.gamma0.Gamma0_prelude]
lt_3 [in Cantor.gamma0.Gamma0_prelude]
lt_2 [in Cantor.gamma0.Gamma0_prelude]
lt_1 [in Cantor.gamma0.Gamma0_prelude]
M
Make.Eq [in Cantor.rpo.rpo]Make.List_mul_rest_step [in Cantor.rpo.rpo]
Make.List_mul_rest [in Cantor.rpo.rpo]
Make.List_eq_rest [in Cantor.rpo.rpo]
Make.List_gt_rest [in Cantor.rpo.rpo]
Make.List_mul [in Cantor.rpo.rpo]
Make.List_eq [in Cantor.rpo.rpo]
Make.List_gt [in Cantor.rpo.rpo]
Make.Lt [in Cantor.rpo.rpo]
Make.mk_set [in Cantor.prelude.list_set]
Make.mk_sn [in Cantor.rpo.rpo]
Make.rmv_case [in Cantor.prelude.dickson]
Make.Subterm [in Cantor.rpo.rpo]
Make.Term [in Cantor.rpo.term]
Make.Top_eq_mul [in Cantor.rpo.rpo]
Make.Top_eq_lex [in Cantor.rpo.rpo]
Make.Top_gt [in Cantor.rpo.rpo]
Make.Var [in Cantor.rpo.term]
N
nfs_cons [in Cantor.epsilon0.MSE0]nfs_nil [in Cantor.epsilon0.MSE0]
nf2_c [in Cantor.epsilon0.EPSILON0]
nf2_z [in Cantor.epsilon0.EPSILON0]
node [in Cantor.epsilon0.Hydra]
Now [in Cantor.epsilon0.Hydra]
P
Precedence.Lex [in Cantor.rpo.rpo]Precedence.Mul [in Cantor.rpo.rpo]
Q
quad [in Cantor.misc.G4]R
Rg_i [in Cantor.epsilon0.Goodstein]Rg0 [in Cantor.misc.G4]
Rg1 [in Cantor.misc.G4]
Rg2 [in Cantor.misc.G4]
Rnl_rest [in Cantor.epsilon0.Hydra]
Rn_plus [in Cantor.epsilon0.Hydra]
Rn_here [in Cantor.epsilon0.Hydra]
RPO.Eq [in Cantor.rpo.rpo]
RPO.List_mul [in Cantor.rpo.rpo]
RPO.List_eq [in Cantor.rpo.rpo]
RPO.List_gt [in Cantor.rpo.rpo]
RPO.Lt [in Cantor.rpo.rpo]
RPO.Subterm [in Cantor.rpo.rpo]
RPO.Top_eq_mul [in Cantor.rpo.rpo]
RPO.Top_eq_lex [in Cantor.rpo.rpo]
RPO.Top_gt [in Cantor.rpo.rpo]
R1_node [in Cantor.epsilon0.Hydra]
R1_single [in Cantor.epsilon0.Hydra]
S
Sh_3 [in Cantor.epsilon0.Hydra]Sh_2 [in Cantor.epsilon0.Hydra]
Sh_1 [in Cantor.epsilon0.Hydra]
Signature.AC [in Cantor.rpo.term]
Signature.C [in Cantor.rpo.term]
Signature.Free [in Cantor.rpo.term]
single [in Cantor.epsilon0.Hydra]
single_nf [in Cantor.epsilon0.EPSILON0]
single_nf [in Cantor.gamma0.Gamma0_prelude]
Sn_first [in Cantor.epsilon0.Hydra]
Sn_single [in Cantor.epsilon0.Hydra]
subterm_trans [in Cantor.gamma0.Gamma0]
subterm_c [in Cantor.gamma0.Gamma0]
subterm_b [in Cantor.gamma0.Gamma0]
subterm_a [in Cantor.gamma0.Gamma0]
succ_finite [in Cantor.gamma0.Gamma0_prelude]
S.mk_set [in Cantor.prelude.list_set]
S1_rest [in Cantor.epsilon0.Hydra]
S1_last [in Cantor.epsilon0.Hydra]
S1_first [in Cantor.epsilon0.Hydra]
S2_rest [in Cantor.epsilon0.Hydra]
S2_first [in Cantor.epsilon0.Hydra]
S2_single [in Cantor.epsilon0.Hydra]
T
tail_lt [in Cantor.epsilon0.EPSILON0]Term.Term [in Cantor.rpo.term]
Term.Var [in Cantor.rpo.term]
t_trans [in Cantor.prelude.closure]
t_step [in Cantor.prelude.closure]
Z
zero [in Cantor.epsilon0.EPSILON0]zero [in Cantor.gamma0.Gamma0_prelude]
zero_nf [in Cantor.epsilon0.EPSILON0]
zero_lt [in Cantor.epsilon0.EPSILON0]
zero_lt_e0 [in Cantor.gamma0.Gamma0_prelude]
zero_nf [in Cantor.gamma0.Gamma0_prelude]
zero_finite [in Cantor.gamma0.Gamma0_prelude]
Zero_correct [in Cantor.epsilon0.Goodstein]
Axiom Index
P
Precedence.A [in Cantor.rpo.rpo]Precedence.prec [in Cantor.rpo.rpo]
Precedence.prec_transitive [in Cantor.rpo.rpo]
Precedence.prec_antisym [in Cantor.rpo.rpo]
Precedence.prec_dec [in Cantor.rpo.rpo]
Precedence.status [in Cantor.rpo.rpo]
R
RPO.rpo_add_context [in Cantor.rpo.rpo]RPO.rpo_subst [in Cantor.rpo.rpo]
RPO.rpo_trans [in Cantor.rpo.rpo]
RPO.rpo_closure [in Cantor.rpo.rpo]
RPO.wf_rpo [in Cantor.rpo.rpo]
S
Signature.arity [in Cantor.rpo.term]Signature.eq_symbol_dec [in Cantor.rpo.term]
Signature.symb [in Cantor.rpo.term]
S.A [in Cantor.prelude.decidable_set]
S.cardinal_subset [in Cantor.prelude.list_set]
S.eq_A_dec [in Cantor.prelude.decidable_set]
T
Term.empty_subst_is_id_list [in Cantor.rpo.term]Term.empty_subst_is_id [in Cantor.rpo.term]
Term.eq_term_dec [in Cantor.rpo.term]
Term.is_a_pos_exists_subtem [in Cantor.rpo.term]
Term.replace_at_pos_list_replace_at_pos_in_subterm [in Cantor.rpo.term]
Term.replace_at_pos_is_replace_at_pos2 [in Cantor.rpo.term]
Term.replace_at_pos_is_replace_at_pos1 [in Cantor.rpo.term]
Term.replace_at_pos_unfold [in Cantor.rpo.term]
Term.size_subterm_at_pos [in Cantor.rpo.term]
Term.size_direct_subterm [in Cantor.rpo.term]
Term.size_ge_one [in Cantor.rpo.term]
Term.size_unfold [in Cantor.rpo.term]
Term.subst_comp_is_subst_comp [in Cantor.rpo.term]
Term.subst_comp_is_subst_comp_aux1 [in Cantor.rpo.term]
Term.subterm_at_pos_apply_subst_apply_subst_subterm_at_pos [in Cantor.rpo.term]
Term.term_rec8 [in Cantor.rpo.term]
Term.term_rec7 [in Cantor.rpo.term]
Term.term_rec4 [in Cantor.rpo.term]
Term.term_rec3 [in Cantor.rpo.term]
Term.term_rec2 [in Cantor.rpo.term]
Term.well_formed_apply_subst [in Cantor.rpo.term]
Term.well_formed_fold [in Cantor.rpo.term]
Term.well_formed_unfold [in Cantor.rpo.term]
V
Variables.eq_variable_dec [in Cantor.rpo.term]Variables.var [in Cantor.rpo.term]
Inductive Index
A
ap [in Cantor.epsilon0.EPSILON0]ap [in Cantor.gamma0.Gamma0_prelude]
C
correct [in Cantor.epsilon0.Goodstein]E
Eps0_prec.status_type [in Cantor.epsilon0.EPSILON0]Eps0_sig.arity_type [in Cantor.epsilon0.EPSILON0]
Eps0_sig.symb0 [in Cantor.epsilon0.EPSILON0]
F
final [in Cantor.misc.G4]G
Gamma0_prec.status_type [in Cantor.gamma0.Gamma0]Gamma0_sig.arity_type [in Cantor.gamma0.Gamma0]
Gamma0_sig.symb0 [in Cantor.gamma0.Gamma0]
H
Hercules_wins [in Cantor.epsilon0.Hydra]Hydra [in Cantor.epsilon0.Hydra]
Hydrae [in Cantor.epsilon0.Hydra]
I
is_finite [in Cantor.gamma0.Gamma0_prelude]is_limit [in Cantor.gamma0.Gamma0]
is_successor [in Cantor.gamma0.Gamma0]
L
limit_plus_F [in Cantor.gamma0.Gamma0]lt [in Cantor.epsilon0.EPSILON0]
lt [in Cantor.gamma0.Gamma0_prelude]
lt_epsilon0 [in Cantor.gamma0.Gamma0_prelude]
M
Make.multiset_extension_step [in Cantor.prelude.dickson]Make.rpo [in Cantor.rpo.rpo]
Make.rpo_mul_rest_step [in Cantor.rpo.rpo]
Make.rpo_mul_rest [in Cantor.rpo.rpo]
Make.rpo_lex_rest [in Cantor.rpo.rpo]
Make.rpo_mul [in Cantor.rpo.rpo]
Make.rpo_lex [in Cantor.rpo.rpo]
Make.rpo_eq [in Cantor.rpo.rpo]
Make.term [in Cantor.rpo.term]
N
nf [in Cantor.epsilon0.EPSILON0]nf [in Cantor.gamma0.Gamma0_prelude]
nfs [in Cantor.epsilon0.MSE0]
nf2 [in Cantor.epsilon0.EPSILON0]
P
Precedence.status_type [in Cantor.rpo.rpo]R
Rg [in Cantor.misc.G4]Rg [in Cantor.epsilon0.Goodstein]
Rh [in Cantor.epsilon0.Hydra]
Rn [in Cantor.epsilon0.Hydra]
RPO.rpo [in Cantor.rpo.rpo]
RPO.rpo_mul [in Cantor.rpo.rpo]
RPO.rpo_lex [in Cantor.rpo.rpo]
RPO.rpo_eq [in Cantor.rpo.rpo]
R1 [in Cantor.epsilon0.Hydra]
S
Sh [in Cantor.epsilon0.Hydra]Signature.arity_type [in Cantor.rpo.term]
Sn [in Cantor.epsilon0.Hydra]
subterm [in Cantor.gamma0.Gamma0]
S1 [in Cantor.epsilon0.Hydra]
S2 [in Cantor.epsilon0.Hydra]
T
Term.term [in Cantor.rpo.term]trans_clos [in Cantor.prelude.closure]
T1 [in Cantor.epsilon0.EPSILON0]
T2 [in Cantor.gamma0.Gamma0_prelude]
V
Vars.empty_set [in Cantor.epsilon0.EPSILON0]Vars.empty_set [in Cantor.gamma0.Gamma0]
Projection Index
B
base [in Cantor.misc.G4]C
coeff0 [in Cantor.misc.G4]coeff1 [in Cantor.misc.G4]
coeff2 [in Cantor.misc.G4]
M
Make.is_a_set [in Cantor.prelude.list_set]Make.sn [in Cantor.rpo.rpo]
Make.support [in Cantor.prelude.list_set]
Make.tt [in Cantor.rpo.rpo]
S
S.is_a_set [in Cantor.prelude.list_set]S.support [in Cantor.prelude.list_set]
Section Index
G
game [in Cantor.epsilon0.Hydra]L
lemmas_on_length [in Cantor.gamma0.Gamma0]lt_not_well_founded [in Cantor.epsilon0.EPSILON0]
lt_incl_rpo [in Cantor.gamma0.Gamma0]
M
Make.DoubleRecursion [in Cantor.rpo.term]Make.Recursion [in Cantor.rpo.term]
O
on_length [in Cantor.gamma0.Gamma0_length]P
partial_fix.FixPoint [in Cantor.prelude.PartialFix]partial_fix.Acc_iterP [in Cantor.prelude.PartialFix]
partial_fix [in Cantor.prelude.PartialFix]
phi_to_psi [in Cantor.gamma0.Gamma0]
predecessor [in Cantor.epsilon0.Goodstein]
R
restricted_recursion [in Cantor.prelude.AccP]S
Sequences [in Cantor.prelude.not_decreasing]Sequences.seq_intro [in Cantor.prelude.not_decreasing]
T
Term.DoubleRecursion [in Cantor.rpo.term]Term.Recursion [in Cantor.rpo.term]
trans_proof [in Cantor.gamma0.Gamma0]
W
well_founded [in Cantor.epsilon0.EPSILON0]well_founded [in Cantor.gamma0.Gamma0]
Definition Index
A
Acc_iter_partial [in Cantor.prelude.PartialFix]app [in Cantor.epsilon0.MSE0]
C
compare [in Cantor.epsilon0.EPSILON0]compare [in Cantor.gamma0.Gamma0]
E
epsilon [in Cantor.gamma0.Gamma0_prelude]epsilon0 [in Cantor.gamma0.Gamma0_prelude]
Eps0_prec.status [in Cantor.epsilon0.EPSILON0]
Eps0_prec.prec [in Cantor.epsilon0.EPSILON0]
Eps0_prec.A [in Cantor.epsilon0.EPSILON0]
Eps0_sig.arity [in Cantor.epsilon0.EPSILON0]
Eps0_sig.symb [in Cantor.epsilon0.EPSILON0]
equiv [in Cantor.epsilon0.MSE0]
exp [in Cantor.epsilon0.EPSILON0]
exp_F [in Cantor.epsilon0.EPSILON0]
F
f [in Cantor.misc.G4]find [in Cantor.prelude.more_list]
finite [in Cantor.epsilon0.EPSILON0]
finite [in Cantor.gamma0.Gamma0_prelude]
fold_left2 [in Cantor.prelude.more_list]
f_Z [in Cantor.misc.G4]
G
Gamma0_prec.status [in Cantor.gamma0.Gamma0]Gamma0_prec.prec [in Cantor.gamma0.Gamma0]
Gamma0_prec.A [in Cantor.gamma0.Gamma0]
Gamma0_sig.arity [in Cantor.gamma0.Gamma0]
Gamma0_sig.symb [in Cantor.gamma0.Gamma0]
get_decomposition [in Cantor.epsilon0.EPSILON0]
goodstein_next_ord [in Cantor.epsilon0.Goodstein]
goodstein_next [in Cantor.epsilon0.Goodstein]
gpred [in Cantor.epsilon0.Goodstein]
H
head_at_l [in Cantor.epsilon0.Hydra]head_at [in Cantor.epsilon0.Hydra]
Hercules_ok [in Cantor.epsilon0.Hydra]
Hercules_strat [in Cantor.epsilon0.Hydra]
Hydrae_rect2 [in Cantor.epsilon0.Hydra]
Hydra_strat [in Cantor.epsilon0.Hydra]
Hydra_rect2 [in Cantor.epsilon0.Hydra]
h2o [in Cantor.epsilon0.Hydra]
h2ol [in Cantor.epsilon0.Hydra]
L
le [in Cantor.epsilon0.EPSILON0]le [in Cantor.gamma0.Gamma0_prelude]
length [in Cantor.gamma0.Gamma0_length]
length_aux [in Cantor.gamma0.Gamma0_length]
Lerne [in Cantor.epsilon0.Hydra]
lex [in Cantor.rpo.rpo]
list_rec3 [in Cantor.prelude.more_list]
list_rec2 [in Cantor.prelude.more_list]
list_size [in Cantor.prelude.more_list]
log [in Cantor.epsilon0.EPSILON0]
ltM [in Cantor.epsilon0.MSE0]
lt_le_dec [in Cantor.epsilon0.EPSILON0]
lt_T1_injection [in Cantor.gamma0.Gamma0]
lt_ge_dec [in Cantor.gamma0.Gamma0]
lub [in Cantor.gamma0.Gamma0]
M
Make.add [in Cantor.prelude.list_set]Make.add_without_red [in Cantor.prelude.list_set]
Make.apply_subst [in Cantor.rpo.term]
Make.build_list_of_SN_terms [in Cantor.rpo.rpo]
Make.cardinal [in Cantor.prelude.list_set]
Make.DecVar.A [in Cantor.rpo.term]
Make.direct_subterm [in Cantor.rpo.term]
Make.elt [in Cantor.prelude.list_set]
Make.elt [in Cantor.prelude.list_permut]
Make.empty [in Cantor.prelude.list_set]
Make.eq_set [in Cantor.prelude.list_set]
Make.eq_elt_dec [in Cantor.prelude.list_set]
Make.eq_elt_dec [in Cantor.prelude.list_permut]
Make.filter [in Cantor.prelude.list_set]
Make.filter_aux [in Cantor.prelude.list_set]
Make.inter [in Cantor.prelude.list_set]
Make.is_a_pos [in Cantor.rpo.term]
Make.list_permut [in Cantor.prelude.list_permut]
Make.list_to_multiset [in Cantor.prelude.list_permut]
Make.make_set [in Cantor.prelude.list_set]
Make.map_subst [in Cantor.rpo.term]
Make.mem [in Cantor.prelude.list_set]
Make.o_size3 [in Cantor.rpo.rpo]
Make.o_size2 [in Cantor.rpo.rpo]
Make.o_size [in Cantor.rpo.rpo]
Make.remove_not_common [in Cantor.prelude.list_set]
Make.remove_red [in Cantor.prelude.list_set]
Make.replace_at_pos_list [in Cantor.rpo.term]
Make.replace_at_pos [in Cantor.rpo.term]
Make.rpo_term [in Cantor.rpo.rpo]
Make.rpo_rest [in Cantor.rpo.rpo]
Make.singleton [in Cantor.prelude.list_set]
Make.size [in Cantor.rpo.term]
Make.size2 [in Cantor.rpo.rpo]
Make.size3 [in Cantor.rpo.rpo]
Make.subset [in Cantor.prelude.list_set]
Make.substitution [in Cantor.rpo.term]
Make.subst_comp [in Cantor.rpo.term]
Make.subterm_at_pos [in Cantor.rpo.term]
Make.symbol [in Cantor.rpo.term]
Make.Term_eq_dec.eq_A_dec [in Cantor.rpo.term]
Make.Term_eq_dec.A [in Cantor.rpo.term]
Make.term_rec8 [in Cantor.rpo.term]
Make.term_rec7 [in Cantor.rpo.term]
Make.term_rec4 [in Cantor.rpo.term]
Make.term_rec3 [in Cantor.rpo.term]
Make.term_rec2 [in Cantor.rpo.term]
Make.union [in Cantor.prelude.list_set]
Make.variable [in Cantor.rpo.term]
Make.well_formed_subst [in Cantor.rpo.term]
Make.well_formed_list [in Cantor.rpo.term]
Make.well_formed [in Cantor.rpo.term]
Make.without_red [in Cantor.prelude.list_set]
map_without_repetition [in Cantor.prelude.more_list]
map12_without_repetition [in Cantor.prelude.more_list]
max [in Cantor.epsilon0.EPSILON0]
max' [in Cantor.epsilon0.EPSILON0]
minus [in Cantor.epsilon0.EPSILON0]
moser_lepper [in Cantor.gamma0.Gamma0]
mult [in Cantor.epsilon0.EPSILON0]
multiplicity [in Cantor.epsilon0.MSE0]
N
nat_2_term [in Cantor.epsilon0.EPSILON0]nat_2_term [in Cantor.gamma0.Gamma0]
nbterms [in Cantor.gamma0.Gamma0_length]
nb_occ [in Cantor.prelude.more_list]
next [in Cantor.misc.G4]
nexts [in Cantor.misc.G4]
nf_rect [in Cantor.epsilon0.EPSILON0]
nth_item [in Cantor.misc.G4]
O
occurrence [in Cantor.epsilon0.Hydra]omega [in Cantor.epsilon0.EPSILON0]
omega [in Cantor.gamma0.Gamma0_prelude]
omega_tower [in Cantor.epsilon0.EPSILON0]
omega_term [in Cantor.epsilon0.EPSILON0]
one [in Cantor.gamma0.Gamma0_prelude]
o_length [in Cantor.prelude.more_list]
P
partial_fun_induction [in Cantor.prelude.PartialFix]Permut.elt [in Cantor.prelude.list_permut]
Permut.eq_elt_dec [in Cantor.prelude.list_permut]
Permut.list_permut [in Cantor.prelude.list_permut]
Permut.list_to_multiset [in Cantor.prelude.list_permut]
PFix [in Cantor.prelude.PartialFix]
phi [in Cantor.gamma0.Gamma0]
phi0 [in Cantor.epsilon0.EPSILON0]
plus [in Cantor.epsilon0.EPSILON0]
plus [in Cantor.gamma0.Gamma0]
power [in Cantor.misc.G4]
power [in Cantor.prelude.More_nat]
pred [in Cantor.epsilon0.EPSILON0]
pred [in Cantor.gamma0.Gamma0_prelude]
Pred [in Cantor.epsilon0.Goodstein]
PredF [in Cantor.epsilon0.Goodstein]
Pred_omega_anb [in Cantor.epsilon0.Goodstein]
Pred_omega_an [in Cantor.epsilon0.Goodstein]
Pred_omega_a [in Cantor.epsilon0.Goodstein]
pred_n_zero [in Cantor.epsilon0.Goodstein]
pred_spec [in Cantor.epsilon0.Goodstein]
psi [in Cantor.gamma0.Gamma0_prelude]
psi_term [in Cantor.gamma0.Gamma0_prelude]
P_well_founded_induction_type [in Cantor.prelude.AccP]
R
reachable [in Cantor.misc.G4]remove [in Cantor.prelude.more_list]
remove_list [in Cantor.prelude.more_list]
replicate [in Cantor.epsilon0.Hydra]
restrict [in Cantor.prelude.AccP]
Rgstar [in Cantor.misc.G4]
Rn_rect2 [in Cantor.epsilon0.Hydra]
S
Sn_rect2 [in Cantor.epsilon0.Hydra]sort [in Cantor.epsilon0.MSE0]
sort_aux [in Cantor.epsilon0.MSE0]
split_list [in Cantor.prelude.more_list]
succ [in Cantor.epsilon0.EPSILON0]
succ [in Cantor.gamma0.Gamma0_prelude]
S.cardinal [in Cantor.prelude.list_set]
S.elt [in Cantor.prelude.list_set]
S.eq_elt_dec [in Cantor.prelude.list_set]
S.subset [in Cantor.prelude.list_set]
S.without_red [in Cantor.prelude.list_set]
T
tail [in Cantor.gamma0.Gamma0_prelude]Term.apply_subst [in Cantor.rpo.term]
Term.direct_subterm [in Cantor.rpo.term]
Term.is_a_pos [in Cantor.rpo.term]
Term.map_subst [in Cantor.rpo.term]
Term.replace_at_pos_list [in Cantor.rpo.term]
Term.replace_at_pos [in Cantor.rpo.term]
Term.size [in Cantor.rpo.term]
Term.substitution [in Cantor.rpo.term]
Term.subst_comp [in Cantor.rpo.term]
Term.subterm_at_pos [in Cantor.rpo.term]
Term.symbol [in Cantor.rpo.term]
Term.variable [in Cantor.rpo.term]
Term.well_formed_subst [in Cantor.rpo.term]
Term.well_formed_list [in Cantor.rpo.term]
Term.well_formed [in Cantor.rpo.term]
transfinite_induction_Q [in Cantor.epsilon0.EPSILON0]
transfinite_induction [in Cantor.epsilon0.EPSILON0]
transfinite_induction_Q [in Cantor.gamma0.Gamma0]
transfinite_induction [in Cantor.gamma0.Gamma0]
trichotomy_inf [in Cantor.epsilon0.EPSILON0]
trichotomy_inf [in Cantor.gamma0.Gamma0]
T1_size [in Cantor.epsilon0.EPSILON0]
T1_2_term [in Cantor.epsilon0.EPSILON0]
T1_eq_dec [in Cantor.epsilon0.EPSILON0]
T1_inj [in Cantor.gamma0.Gamma0_prelude]
T2_size [in Cantor.gamma0.Gamma0]
T2_2_term [in Cantor.gamma0.Gamma0]
V
val [in Cantor.epsilon0.Goodstein]Vars.var [in Cantor.epsilon0.EPSILON0]
Vars.var [in Cantor.gamma0.Gamma0]
W
well_founded_P [in Cantor.prelude.AccP]Record Index
I
item [in Cantor.misc.G4]M
Make.SN_term [in Cantor.rpo.rpo]Make.t [in Cantor.prelude.list_set]
S
S.t [in Cantor.prelude.list_set]| 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 | (1232 entries) |
| Notation 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 | (17 entries) |
| Module 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 | (44 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 | (69 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 | (21 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 | (618 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 | (129 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 | (42 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 | (55 entries) |
| Projection 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 | (10 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 | (20 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 | (203 entries) |
| Record 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) |