| 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 | (550 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 | (7 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 | (2 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 | (25 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 | (19 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 | (299 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 | (89 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 | (4 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 | (21 entries) |
| Instance 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 | (34 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 | (14 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 | (36 entries) |
Global Index
A
and_dec [instance, in Base]app_equi_proper [instance, in Base]
app_incl_proper [instance, in Base]
AutoIndTac [library]
B
Base [library]bool_eq_dec [instance, in Base]
bound [inductive, in FreeVariables]
BoundChoice [constructor, in FreeVariables]
BoundEps [constructor, in FreeVariables]
BoundFix [constructor, in FreeVariables]
BoundSeq [constructor, in FreeVariables]
boundT [inductive, in Traces]
BoundTP [constructor, in Traces]
BoundTT [constructor, in Traces]
BoundTV [constructor, in Traces]
boundT_terminal_compose [lemma, in Traces]
boundT_butLast_preserve [lemma, in Traces]
boundT_ren_lift [lemma, in Traces]
boundT_step [lemma, in Traces]
boundT_ren_shift_reconstruct [lemma, in Traces]
boundT_ren_shift_preserve [lemma, in Traces]
boundT_zero [lemma, in Traces]
boundT_concat_decompose_right [lemma, in Traces]
boundT_concat_decompose_left [lemma, in Traces]
boundT_concat_compose [lemma, in Traces]
BoundVar1 [constructor, in FreeVariables]
BoundVar2 [constructor, in FreeVariables]
bound_boundT [lemma, in FreeVariables]
bound_subst_preserve [lemma, in FreeVariables]
bound_subst [lemma, in FreeVariables]
bound_shift [lemma, in FreeVariables]
bound_lift [lemma, in FreeVariables]
bound_ren_preserve [lemma, in FreeVariables]
bound_ren [lemma, in FreeVariables]
bound_trans [lemma, in FreeVariables]
bound_shift_interval [lemma, in FreeVariables]
bound_step [lemma, in FreeVariables]
bound_zero [lemma, in FreeVariables]
bound_reg [lemma, in Regularity]
bound_lin [lemma, in Linearity]
butLast [definition, in Traces]
butLast_total_preserve [lemma, in Traces]
butLast_partial_preserve [lemma, in Traces]
butLast_concat_distribute [lemma, in Traces]
butLast_P_distribute [lemma, in Traces]
butLast_V_distribute [lemma, in Traces]
C
card [definition, in Base]Cardinality [section, in Base]
Cardinality.X [variable, in Base]
card_equi_proper [instance, in Base]
card_or [lemma, in Base]
card_lt [lemma, in Base]
card_equi [lemma, in Base]
card_ex [lemma, in Base]
card_0 [lemma, in Base]
card_cons_rem [lemma, in Base]
card_eq [lemma, in Base]
card_le [lemma, in Base]
card_not_in_rem [lemma, in Base]
card_in_rem [lemma, in Base]
cfa [definition, in IMP]
cfa_correspondence [lemma, in IMP]
cfp [inductive, in CFP]
CFP [library]
CFPChoice [constructor, in CFP]
CFPEps [constructor, in CFP]
CFPFix [constructor, in CFP]
CFPSeq [constructor, in CFP]
CFPVar [constructor, in CFP]
cfp_dec [instance, in CFP]
cfp_eq_dec [lemma, in CFP]
Choice_eqTC_proper [instance, in Congruence]
Choice_idem [lemma, in Equivalences]
Choice_assoc [lemma, in Equivalences]
Choice_Null_iden_left [lemma, in Equivalences]
Choice_commute [lemma, in Equivalences]
Choice_Null_iden_right [lemma, in Equivalences]
cmd [inductive, in IMP]
CmdAct [constructor, in IMP]
CmdIf [constructor, in IMP]
CmdSeq [constructor, in IMP]
CmdSkip [constructor, in IMP]
CmdWhile [constructor, in IMP]
composed [inductive, in Traces]
ComposedV [constructor, in Traces]
comp_charact [axiom, in IMP]
concat [definition, in Traces]
concat_composed_compose [lemma, in Traces]
concat_total_decompose [lemma, in Traces]
concat_partial_compose [lemma, in Traces]
concat_P_partial_right [lemma, in Traces]
concat_total_compose [lemma, in Traces]
concat_partial_preserve_right [lemma, in Traces]
concat_partial_absorb_right [lemma, in Traces]
concat_P_iden_right [lemma, in Traces]
concat_T_iden_left [lemma, in Traces]
concat_T_iden_right [lemma, in Traces]
concat_assoc [lemma, in Traces]
Congruence [library]
congruent_Choice [lemma, in Congruence]
congruent_Seq [lemma, in Congruence]
congruent_Fix [lemma, in Congruence]
congruent_Fix_help [lemma, in Congruence]
cons_equi_proper [instance, in Base]
cons_incl_proper [instance, in Base]
D
dec [definition, in Base]decision [definition, in Base]
decomp [definition, in Regularizer]
decomposed_Star_lift [lemma, in DistributeFix]
decomposed_Star [lemma, in DistributeFix]
decomposed_Fix_distribute_lift [lemma, in DistributeFix]
decomposed_unfold_distribute_lift [lemma, in DistributeFix]
decomposed_unfold_distribute [lemma, in DistributeFix]
decomposed_unfold [lemma, in DistributeFix]
decomposed_subst [lemma, in DistributeFix]
decompose_correct [lemma, in Regularizer]
decompose_Fix_distribute [lemma, in DistributeFix]
decomp_correct [lemma, in Regularizer]
decomp_total [lemma, in Regularizer]
dec_prop_iff [lemma, in Base]
dec_DM_impl [lemma, in Base]
dec_DM_and [lemma, in Base]
dec_DN [lemma, in Base]
DirectLinearizer [library]
disjoint [definition, in Base]
disjoint_app [lemma, in Base]
disjoint_cons [lemma, in Base]
disjoint_nil' [lemma, in Base]
disjoint_nil [lemma, in Base]
disjoint_incl [lemma, in Base]
disjoint_symm [lemma, in Base]
disjoint_forall [lemma, in Base]
DistributeFix [library]
DM_exists [lemma, in Base]
DM_or [lemma, in Base]
Dupfree [section, in Base]
dupfree [inductive, in Base]
dupfreeC [constructor, in Base]
dupfreeN [constructor, in Base]
dupfree_inv [definition, in Base]
dupfree_in_power [lemma, in Base]
dupfree_power [lemma, in Base]
dupfree_undup [lemma, in Base]
dupfree_card [lemma, in Base]
dupfree_dec [lemma, in Base]
dupfree_filter [lemma, in Base]
dupfree_map [lemma, in Base]
dupfree_app [lemma, in Base]
dupfree_cons [lemma, in Base]
Dupfree.X [variable, in Base]
E
eqSem [definition, in IMP]eqTC [definition, in TraceSemantics]
eqTC_Equivalence [instance, in TraceSemantics]
Equi [section, in Base]
equi [definition, in Base]
Equivalences [library]
equi_rotate [lemma, in Base]
equi_shift [lemma, in Base]
equi_swap [lemma, in Base]
equi_dup [lemma, in Base]
equi_push [lemma, in Base]
equi_Equivalence [instance, in Base]
Equi.X [variable, in Base]
extens [lemma, in CFP]
F
False_dec [instance, in Base]FCI [module, in Base]
FCI.C [definition, in Base]
FCI.closure [lemma, in Base]
FCI.F [definition, in Base]
FCI.FCI [section, in Base]
FCI.FCI.step [variable, in Base]
FCI.FCI.V [variable, in Base]
FCI.FCI.X [variable, in Base]
FCI.fp [lemma, in Base]
FCI.incl [lemma, in Base]
FCI.ind [lemma, in Base]
FCI.it_incl [lemma, in Base]
FCI.pick [lemma, in Base]
filter [definition, in Base]
FilterComm [section, in Base]
FilterComm.p [variable, in Base]
FilterComm.q [variable, in Base]
FilterComm.X [variable, in Base]
FilterLemmas [section, in Base]
FilterLemmas_pq.q [variable, in Base]
FilterLemmas_pq.p [variable, in Base]
FilterLemmas_pq.X [variable, in Base]
FilterLemmas_pq [section, in Base]
FilterLemmas.p [variable, in Base]
FilterLemmas.X [variable, in Base]
filter_comm [lemma, in Base]
filter_and [lemma, in Base]
filter_pq_eq [lemma, in Base]
filter_pq_mono [lemma, in Base]
filter_fst' [lemma, in Base]
filter_fst [lemma, in Base]
filter_app [lemma, in Base]
filter_id [lemma, in Base]
filter_mono [lemma, in Base]
filter_incl [lemma, in Base]
Fix_unfold_subsume [lemma, in Unfolding]
Fix_eqTC_proper [instance, in Congruence]
Fix_unfold [lemma, in Equivalences]
FP [definition, in Base]
FreeVariables [library]
I
Ids_term [instance, in CFP]id_shift [lemma, in CFP]
iff_dec [instance, in Base]
Imp [section, in IMP]
IMP [library]
impl_dec [instance, in Base]
Imp.comp [variable, in IMP]
Imp.exec [variable, in IMP]
Imp.state [variable, in IMP]
Imp.test [variable, in IMP]
_ =B _ [notation, in IMP]
inclp [definition, in Base]
Inclusion [section, in Base]
Inclusion.X [variable, in Base]
incl_equi_proper [instance, in Base]
incl_preorder [instance, in Base]
incl_app_left [lemma, in Base]
incl_lrcons [lemma, in Base]
incl_rcons [lemma, in Base]
incl_sing [lemma, in Base]
incl_lcons [lemma, in Base]
incl_shift [lemma, in Base]
incl_nil_eq [lemma, in Base]
incl_map [lemma, in Base]
incl_nil [lemma, in Base]
inj_test_action_inj [axiom, in IMP]
inj_test_action [axiom, in IMP]
inv_cfa_Eps [lemma, in IMP]
inv_cfa_Fix [lemma, in IMP]
inv_cfa_Choice [lemma, in IMP]
inv_cfa_Seq [lemma, in IMP]
inv_cfa_Var [lemma, in IMP]
inv_subst_Fix [lemma, in Substitutivity]
inv_subst_Choice [lemma, in Substitutivity]
inv_subst_Seq [lemma, in Substitutivity]
inv_subst_Var [lemma, in Substitutivity]
inv_subst_Eps [lemma, in Substitutivity]
inv_concat_V [lemma, in Traces]
inv_concat_T [lemma, in Traces]
inv_concat_P [lemma, in Traces]
in_rem_iff [lemma, in Base]
in_filter_iff [lemma, in Base]
in_equi_proper [instance, in Base]
in_incl_proper [instance, in Base]
in_cons_neq [lemma, in Base]
in_sing [lemma, in Base]
it [definition, in Base]
iterate [definition, in TraceSemantics]
Iteration [section, in Base]
Iteration.f [variable, in Base]
Iteration.X [variable, in Base]
it_fp [lemma, in Base]
it_ind [lemma, in Base]
L
lin [inductive, in Linearity]LinChoice [constructor, in Linearity]
Linearity [library]
linearize [definition, in DirectLinearizer]
linearize_correct_final [lemma, in DirectLinearizer]
linearize_correct [lemma, in DirectLinearizer]
linearize_correct2 [lemma, in DirectLinearizer]
linearize_correct1 [lemma, in DirectLinearizer]
linearize_lin [lemma, in DirectLinearizer]
linearize_tailrec [lemma, in DirectLinearizer]
LinEps [constructor, in Linearity]
LinFix [constructor, in Linearity]
lini [definition, in RegLinearizer]
lini_correct_final [lemma, in RegLinearizer]
lini_correct [lemma, in RegLinearizer]
lini_lin [lemma, in RegLinearizer]
LinSeq [constructor, in Linearity]
LinVar [constructor, in Linearity]
lin_ren_preserve [lemma, in Linearity]
lin_tailrec [lemma, in Linearity]
lin_step [lemma, in Linearity]
list_cc [lemma, in Base]
list_exists_not_incl [lemma, in Base]
list_exists_DM [lemma, in Base]
list_exists_dec [instance, in Base]
list_forall_dec [instance, in Base]
list_sigma_forall [lemma, in Base]
list_in_dec [instance, in Base]
list_eq_dec [instance, in Base]
list_cycle [lemma, in Base]
M
Membership [section, in Base]Membership.X [variable, in Base]
modus_ponens [lemma, in Util]
N
nat_le_dec [instance, in Base]nat_eq_dec [instance, in Base]
notBlock [definition, in IMP]
not_in_cons [lemma, in Base]
not_dec [instance, in Base]
not_partial_total [lemma, in Traces]
no_Null_annulate_right [lemma, in Equivalences]
Null [definition, in CFP]
Null_trace [lemma, in TraceSemantics]
O
or_dec [instance, in Base]P
P [constructor, in Traces]part [definition, in CFP]
partial [inductive, in Traces]
PartialP [constructor, in Traces]
PartialV [constructor, in Traces]
partial_dec [instance, in Traces]
partial_decision [lemma, in Traces]
power [definition, in Base]
PowerRep [section, in Base]
PowerRep.X [variable, in Base]
power_extensional [lemma, in Base]
power_nil [lemma, in Base]
power_incl [lemma, in Base]
prefix_closed [lemma, in TraceSemantics]
P_trivialtrace [lemma, in TraceSemantics]
R
reg [inductive, in Regularity]RegChoice [constructor, in Regularity]
RegEps [constructor, in Regularity]
regi [inductive, in Regularity]
RegiChoice [constructor, in Regularity]
RegiEps [constructor, in Regularity]
RegiNull [constructor, in Regularity]
RegiSeq [constructor, in Regularity]
RegiStar [constructor, in Regularity]
RegiVar [constructor, in Regularity]
regi_reg [lemma, in Regularity]
RegLinearizer [library]
RegNull [constructor, in Regularity]
RegSeq [constructor, in Regularity]
RegStar [constructor, in Regularity]
Regularity [library]
regularize [definition, in Regularizer]
Regularizer [library]
regularize_correct_final [lemma, in Regularizer]
regularize_correct [lemma, in Regularizer]
RegVar [constructor, in Regularity]
reg_regularize [lemma, in Regularizer]
reg_decomp [lemma, in Regularizer]
reg_correct [lemma, in Regularity]
reg_regi [lemma, in Regularity]
reg_shift [lemma, in Regularity]
reg_name_preserve [lemma, in Regularity]
reg_step [lemma, in Regularity]
reg_tailrec [lemma, in Regularity]
reg_bound [lemma, in Regularity]
rem [definition, in Base]
Removal [section, in Base]
Removal.X [variable, in Base]
rem_inclr [lemma, in Base]
rem_reorder [lemma, in Base]
rem_id [lemma, in Base]
rem_fst' [lemma, in Base]
rem_fst [lemma, in Base]
rem_comm [lemma, in Base]
rem_equi [lemma, in Base]
rem_app' [lemma, in Base]
rem_app [lemma, in Base]
rem_neq [lemma, in Base]
rem_in [lemma, in Base]
rem_cons' [lemma, in Base]
rem_cons [lemma, in Base]
rem_mono [lemma, in Base]
rem_incl [lemma, in Base]
rem_not_in [lemma, in Base]
Rename_term [instance, in CFP]
ren_trace_ren [lemma, in TraceSemantics]
ren_butLast_distribute [lemma, in Traces]
ren_composed_preserve [lemma, in Traces]
ren_total_origin [lemma, in Traces]
ren_partial_origin [lemma, in Traces]
ren_partial_preserve [lemma, in Traces]
ren_total_preserve [lemma, in Traces]
ren_trace_id_inc_shift [lemma, in Traces]
ren_concat_distribute [lemma, in Traces]
ren_trace [definition, in Traces]
rep [definition, in Base]
rep_dupfree [lemma, in Base]
rep_idempotent [lemma, in Base]
rep_injective [lemma, in Base]
rep_eq [lemma, in Base]
rep_eq' [lemma, in Base]
rep_mono [lemma, in Base]
rep_equi [lemma, in Base]
rep_in [lemma, in Base]
rep_incl [lemma, in Base]
rep_power [lemma, in Base]
run [inductive, in IMP]
RunT [constructor, in IMP]
RunV [constructor, in IMP]
run_concat2 [lemma, in IMP]
run_concat [lemma, in IMP]
S
sem [inductive, in IMP]SemCmdIfFalse [constructor, in IMP]
SemCmdIfTrue [constructor, in IMP]
SemCmdInput [constructor, in IMP]
SemCmdSeq [constructor, in IMP]
SemCmdSkip [constructor, in IMP]
SemCmdWhileFalse [constructor, in IMP]
SemCmdWhileTrue [constructor, in IMP]
sem_trace [lemma, in IMP]
Seq_eqTC_proper [instance, in Congruence]
Seq_Eps_iden_left [lemma, in Equivalences]
Seq_Eps_iden_right [lemma, in Equivalences]
Seq_Null_absorb_left [lemma, in Equivalences]
Seq_Choice_distribute2 [lemma, in Equivalences]
Seq_Choice_distribute1 [lemma, in Equivalences]
Seq_assoc [lemma, in Equivalences]
shift [definition, in CFP]
shift_id [lemma, in CFP]
simulatesI [definition, in CFP]
simulatesI_shift [lemma, in CFP]
simulate_shift [lemma, in CFP]
size_recursion [lemma, in Base]
Star [definition, in CFP]
substitutivity [lemma, in Substitutivity]
Substitutivity [library]
substitutivity1 [lemma, in Substitutivity]
substitutivity2 [lemma, in Substitutivity]
SubstLemmas_term [instance, in CFP]
substPos [definition, in CFP]
substPos_up [lemma, in CFP]
substPos_zero_extens [lemma, in CFP]
substPos_zero [lemma, in CFP]
substPos_gt [lemma, in CFP]
substPos_lt [lemma, in CFP]
substPos_eq [lemma, in CFP]
substT [inductive, in Substitutivity]
SubstTP [constructor, in Substitutivity]
SubstTT [constructor, in Substitutivity]
SubstTV [constructor, in Substitutivity]
substT_concat_decompose [lemma, in Substitutivity]
substT_concat_compose [lemma, in Substitutivity]
substT_total [lemma, in Substitutivity]
subst_Fix_distribute [lemma, in CFP]
Subst_term [instance, in CFP]
subst_Fix_unfold_subsume [lemma, in Unfolding]
subst_subsumption_transfer [lemma, in Substitutivity]
subst_tracesubsumption_preserve [lemma, in Substitutivity]
subst_trace_deconstruct [lemma, in Substitutivity]
subst_trace_construct [lemma, in Substitutivity]
T
T [constructor, in Traces]tailrec [inductive, in TailRecursion]
TailRecChoice [constructor, in TailRecursion]
TailRecEps [constructor, in TailRecursion]
TailRecFix [constructor, in TailRecursion]
TailRecSeq [constructor, in TailRecursion]
TailRecursion [library]
TailRecVar [constructor, in TailRecursion]
tailrec_cfa [lemma, in IMP]
tailrec_subst_trace_decompose [lemma, in DirectLinearizer]
tailrec_subst_trace_compose2 [lemma, in DirectLinearizer]
tailrec_subst_trace_compose1 [lemma, in DirectLinearizer]
tailrec_trace_butLast_boundT [lemma, in Traces]
tailrec_trace [definition, in Traces]
tailrec_trec [lemma, in TailRecursion]
tailrec_tailrec_trace [lemma, in TailRecursion]
tailrec_terminal [lemma, in TailRecursion]
tailrec_subst_preserve [lemma, in TailRecursion]
tailrec_lift [lemma, in TailRecursion]
tailrec_ren_preserve [lemma, in TailRecursion]
tailrec_bound_lift [lemma, in TailRecursion]
tailrec_step [lemma, in TailRecursion]
TC [inductive, in TraceSemantics]
TCChoiceRight [constructor, in TraceSemantics]
TCFix [constructor, in TraceSemantics]
TChoiceLeft [constructor, in TraceSemantics]
TCPartial [constructor, in TraceSemantics]
TCsubst [inductive, in Substitutivity]
TCsubstChoiceLeft [constructor, in Substitutivity]
TCsubstChoiceRight [constructor, in Substitutivity]
TCsubstFix [constructor, in Substitutivity]
TCsubstPartial [constructor, in Substitutivity]
TCsubstSeq [constructor, in Substitutivity]
TCsubstTotal [constructor, in Substitutivity]
TCsubstVar [constructor, in Substitutivity]
TCsubst_TC [lemma, in Substitutivity]
TCTotal [constructor, in TraceSemantics]
TCVarPartial [constructor, in TraceSemantics]
TCVarTotal [constructor, in TraceSemantics]
TC_TCsubst [lemma, in Substitutivity]
terminal [inductive, in Traces]
TerminalP [constructor, in Traces]
TerminalT [constructor, in Traces]
TerminalV [constructor, in Traces]
terminal_concat_decompose [lemma, in Traces]
terminal_concat_decompose_right [lemma, in Traces]
terminal_ren_shift_reconstruct [lemma, in Traces]
terminal_ren_shift_preserve [lemma, in Traces]
terminal_boundT_contradict [lemma, in Traces]
terminal_concat_P_compose [lemma, in Traces]
terminal_concat_compose [lemma, in Traces]
terminal_unique [lemma, in Traces]
terminal_composed [lemma, in Traces]
Test [module, in AutoIndTac]
test_charact [axiom, in IMP]
Test.all_zero [lemma, in AutoIndTac]
Test.all_zero_by_hand [lemma, in AutoIndTac]
Test.base [constructor, in AutoIndTac]
Test.decreasing [inductive, in AutoIndTac]
Test.step [constructor, in AutoIndTac]
total [inductive, in Traces]
TotalT [constructor, in Traces]
TotalV [constructor, in Traces]
trace [inductive, in Traces]
Traces [library]
TraceSemantics [library]
trace_partial_prefix2 [lemma, in TraceSemantics]
trace_partial_prefix [lemma, in TraceSemantics]
trace_partial_Seq_left [lemma, in TraceSemantics]
trace_concat_partial_left [lemma, in TraceSemantics]
trace_concat_P [lemma, in TraceSemantics]
trace_sem [lemma, in IMP]
trec [inductive, in TailRecursion]
TrecChoice [constructor, in TailRecursion]
TrecEps [constructor, in TailRecursion]
TrecFix [constructor, in TailRecursion]
TrecSeq [constructor, in TailRecursion]
TrecVar1 [constructor, in TailRecursion]
TrecVar2 [constructor, in TailRecursion]
trec_correct [lemma, in TailRecursion]
trec_tailrec [lemma, in TailRecursion]
trec_bound_ren [lemma, in TailRecursion]
trec_shift [lemma, in TailRecursion]
trec_ren_preserve [lemma, in TailRecursion]
trec_bound_lift [lemma, in TailRecursion]
True_dec [instance, in Base]
TSeq [constructor, in TraceSemantics]
U
undup [definition, in Base]Undup [section, in Base]
undup_idempotent [lemma, in Base]
undup_id [lemma, in Base]
undup_equi [lemma, in Base]
undup_incl [lemma, in Base]
undup_id_equi [lemma, in Base]
Undup.X [variable, in Base]
unfold [definition, in Unfolding]
Unfolding [library]
unfold_Fix_subsume [lemma, in Unfolding]
unfold_subst [lemma, in Unfolding]
unfold_step [lemma, in Unfolding]
up_change [lemma, in CFP]
Util [library]
V
V [constructor, in Traces]other
_ =T _ [notation, in TraceSemantics]_ === _ [notation, in Base]
_ <<= _ [notation, in Base]
_ el _ [notation, in Base]
eq_dec _ [notation, in Base]
| _ | [notation, in Base]
Notation Index
I
_ =B _ [in IMP]other
_ =T _ [in TraceSemantics]_ === _ [in Base]
_ <<= _ [in Base]
_ el _ [in Base]
eq_dec _ [in Base]
| _ | [in Base]
Module Index
F
FCI [in Base]T
Test [in AutoIndTac]Variable Index
C
Cardinality.X [in Base]D
Dupfree.X [in Base]E
Equi.X [in Base]F
FCI.FCI.step [in Base]FCI.FCI.V [in Base]
FCI.FCI.X [in Base]
FilterComm.p [in Base]
FilterComm.q [in Base]
FilterComm.X [in Base]
FilterLemmas_pq.q [in Base]
FilterLemmas_pq.p [in Base]
FilterLemmas_pq.X [in Base]
FilterLemmas.p [in Base]
FilterLemmas.X [in Base]
I
Imp.comp [in IMP]Imp.exec [in IMP]
Imp.state [in IMP]
Imp.test [in IMP]
Inclusion.X [in Base]
Iteration.f [in Base]
Iteration.X [in Base]
M
Membership.X [in Base]P
PowerRep.X [in Base]R
Removal.X [in Base]U
Undup.X [in Base]Library Index
A
AutoIndTacB
BaseC
CFPCongruence
D
DirectLinearizerDistributeFix
E
EquivalencesF
FreeVariablesI
IMPL
LinearityR
RegLinearizerRegularity
Regularizer
S
SubstitutivityT
TailRecursionTraces
TraceSemantics
U
UnfoldingUtil
Lemma Index
B
boundT_terminal_compose [in Traces]boundT_butLast_preserve [in Traces]
boundT_ren_lift [in Traces]
boundT_step [in Traces]
boundT_ren_shift_reconstruct [in Traces]
boundT_ren_shift_preserve [in Traces]
boundT_zero [in Traces]
boundT_concat_decompose_right [in Traces]
boundT_concat_decompose_left [in Traces]
boundT_concat_compose [in Traces]
bound_boundT [in FreeVariables]
bound_subst_preserve [in FreeVariables]
bound_subst [in FreeVariables]
bound_shift [in FreeVariables]
bound_lift [in FreeVariables]
bound_ren_preserve [in FreeVariables]
bound_ren [in FreeVariables]
bound_trans [in FreeVariables]
bound_shift_interval [in FreeVariables]
bound_step [in FreeVariables]
bound_zero [in FreeVariables]
bound_reg [in Regularity]
bound_lin [in Linearity]
butLast_total_preserve [in Traces]
butLast_partial_preserve [in Traces]
butLast_concat_distribute [in Traces]
butLast_P_distribute [in Traces]
butLast_V_distribute [in Traces]
C
card_or [in Base]card_lt [in Base]
card_equi [in Base]
card_ex [in Base]
card_0 [in Base]
card_cons_rem [in Base]
card_eq [in Base]
card_le [in Base]
card_not_in_rem [in Base]
card_in_rem [in Base]
cfa_correspondence [in IMP]
cfp_eq_dec [in CFP]
Choice_idem [in Equivalences]
Choice_assoc [in Equivalences]
Choice_Null_iden_left [in Equivalences]
Choice_commute [in Equivalences]
Choice_Null_iden_right [in Equivalences]
concat_composed_compose [in Traces]
concat_total_decompose [in Traces]
concat_partial_compose [in Traces]
concat_P_partial_right [in Traces]
concat_total_compose [in Traces]
concat_partial_preserve_right [in Traces]
concat_partial_absorb_right [in Traces]
concat_P_iden_right [in Traces]
concat_T_iden_left [in Traces]
concat_T_iden_right [in Traces]
concat_assoc [in Traces]
congruent_Choice [in Congruence]
congruent_Seq [in Congruence]
congruent_Fix [in Congruence]
congruent_Fix_help [in Congruence]
D
decomposed_Star_lift [in DistributeFix]decomposed_Star [in DistributeFix]
decomposed_Fix_distribute_lift [in DistributeFix]
decomposed_unfold_distribute_lift [in DistributeFix]
decomposed_unfold_distribute [in DistributeFix]
decomposed_unfold [in DistributeFix]
decomposed_subst [in DistributeFix]
decompose_correct [in Regularizer]
decompose_Fix_distribute [in DistributeFix]
decomp_correct [in Regularizer]
decomp_total [in Regularizer]
dec_prop_iff [in Base]
dec_DM_impl [in Base]
dec_DM_and [in Base]
dec_DN [in Base]
disjoint_app [in Base]
disjoint_cons [in Base]
disjoint_nil' [in Base]
disjoint_nil [in Base]
disjoint_incl [in Base]
disjoint_symm [in Base]
disjoint_forall [in Base]
DM_exists [in Base]
DM_or [in Base]
dupfree_in_power [in Base]
dupfree_power [in Base]
dupfree_undup [in Base]
dupfree_card [in Base]
dupfree_dec [in Base]
dupfree_filter [in Base]
dupfree_map [in Base]
dupfree_app [in Base]
dupfree_cons [in Base]
E
equi_rotate [in Base]equi_shift [in Base]
equi_swap [in Base]
equi_dup [in Base]
equi_push [in Base]
extens [in CFP]
F
FCI.closure [in Base]FCI.fp [in Base]
FCI.incl [in Base]
FCI.ind [in Base]
FCI.it_incl [in Base]
FCI.pick [in Base]
filter_comm [in Base]
filter_and [in Base]
filter_pq_eq [in Base]
filter_pq_mono [in Base]
filter_fst' [in Base]
filter_fst [in Base]
filter_app [in Base]
filter_id [in Base]
filter_mono [in Base]
filter_incl [in Base]
Fix_unfold_subsume [in Unfolding]
Fix_unfold [in Equivalences]
I
id_shift [in CFP]incl_app_left [in Base]
incl_lrcons [in Base]
incl_rcons [in Base]
incl_sing [in Base]
incl_lcons [in Base]
incl_shift [in Base]
incl_nil_eq [in Base]
incl_map [in Base]
incl_nil [in Base]
inv_cfa_Eps [in IMP]
inv_cfa_Fix [in IMP]
inv_cfa_Choice [in IMP]
inv_cfa_Seq [in IMP]
inv_cfa_Var [in IMP]
inv_subst_Fix [in Substitutivity]
inv_subst_Choice [in Substitutivity]
inv_subst_Seq [in Substitutivity]
inv_subst_Var [in Substitutivity]
inv_subst_Eps [in Substitutivity]
inv_concat_V [in Traces]
inv_concat_T [in Traces]
inv_concat_P [in Traces]
in_rem_iff [in Base]
in_filter_iff [in Base]
in_cons_neq [in Base]
in_sing [in Base]
it_fp [in Base]
it_ind [in Base]
L
linearize_correct_final [in DirectLinearizer]linearize_correct [in DirectLinearizer]
linearize_correct2 [in DirectLinearizer]
linearize_correct1 [in DirectLinearizer]
linearize_lin [in DirectLinearizer]
linearize_tailrec [in DirectLinearizer]
lini_correct_final [in RegLinearizer]
lini_correct [in RegLinearizer]
lini_lin [in RegLinearizer]
lin_ren_preserve [in Linearity]
lin_tailrec [in Linearity]
lin_step [in Linearity]
list_cc [in Base]
list_exists_not_incl [in Base]
list_exists_DM [in Base]
list_sigma_forall [in Base]
list_cycle [in Base]
M
modus_ponens [in Util]N
not_in_cons [in Base]not_partial_total [in Traces]
no_Null_annulate_right [in Equivalences]
Null_trace [in TraceSemantics]
P
partial_decision [in Traces]power_extensional [in Base]
power_nil [in Base]
power_incl [in Base]
prefix_closed [in TraceSemantics]
P_trivialtrace [in TraceSemantics]
R
regi_reg [in Regularity]regularize_correct_final [in Regularizer]
regularize_correct [in Regularizer]
reg_regularize [in Regularizer]
reg_decomp [in Regularizer]
reg_correct [in Regularity]
reg_regi [in Regularity]
reg_shift [in Regularity]
reg_name_preserve [in Regularity]
reg_step [in Regularity]
reg_tailrec [in Regularity]
reg_bound [in Regularity]
rem_inclr [in Base]
rem_reorder [in Base]
rem_id [in Base]
rem_fst' [in Base]
rem_fst [in Base]
rem_comm [in Base]
rem_equi [in Base]
rem_app' [in Base]
rem_app [in Base]
rem_neq [in Base]
rem_in [in Base]
rem_cons' [in Base]
rem_cons [in Base]
rem_mono [in Base]
rem_incl [in Base]
rem_not_in [in Base]
ren_trace_ren [in TraceSemantics]
ren_butLast_distribute [in Traces]
ren_composed_preserve [in Traces]
ren_total_origin [in Traces]
ren_partial_origin [in Traces]
ren_partial_preserve [in Traces]
ren_total_preserve [in Traces]
ren_trace_id_inc_shift [in Traces]
ren_concat_distribute [in Traces]
rep_dupfree [in Base]
rep_idempotent [in Base]
rep_injective [in Base]
rep_eq [in Base]
rep_eq' [in Base]
rep_mono [in Base]
rep_equi [in Base]
rep_in [in Base]
rep_incl [in Base]
rep_power [in Base]
run_concat2 [in IMP]
run_concat [in IMP]
S
sem_trace [in IMP]Seq_Eps_iden_left [in Equivalences]
Seq_Eps_iden_right [in Equivalences]
Seq_Null_absorb_left [in Equivalences]
Seq_Choice_distribute2 [in Equivalences]
Seq_Choice_distribute1 [in Equivalences]
Seq_assoc [in Equivalences]
shift_id [in CFP]
simulatesI_shift [in CFP]
simulate_shift [in CFP]
size_recursion [in Base]
substitutivity [in Substitutivity]
substitutivity1 [in Substitutivity]
substitutivity2 [in Substitutivity]
substPos_up [in CFP]
substPos_zero_extens [in CFP]
substPos_zero [in CFP]
substPos_gt [in CFP]
substPos_lt [in CFP]
substPos_eq [in CFP]
substT_concat_decompose [in Substitutivity]
substT_concat_compose [in Substitutivity]
substT_total [in Substitutivity]
subst_Fix_distribute [in CFP]
subst_Fix_unfold_subsume [in Unfolding]
subst_subsumption_transfer [in Substitutivity]
subst_tracesubsumption_preserve [in Substitutivity]
subst_trace_deconstruct [in Substitutivity]
subst_trace_construct [in Substitutivity]
T
tailrec_cfa [in IMP]tailrec_subst_trace_decompose [in DirectLinearizer]
tailrec_subst_trace_compose2 [in DirectLinearizer]
tailrec_subst_trace_compose1 [in DirectLinearizer]
tailrec_trace_butLast_boundT [in Traces]
tailrec_trec [in TailRecursion]
tailrec_tailrec_trace [in TailRecursion]
tailrec_terminal [in TailRecursion]
tailrec_subst_preserve [in TailRecursion]
tailrec_lift [in TailRecursion]
tailrec_ren_preserve [in TailRecursion]
tailrec_bound_lift [in TailRecursion]
tailrec_step [in TailRecursion]
TCsubst_TC [in Substitutivity]
TC_TCsubst [in Substitutivity]
terminal_concat_decompose [in Traces]
terminal_concat_decompose_right [in Traces]
terminal_ren_shift_reconstruct [in Traces]
terminal_ren_shift_preserve [in Traces]
terminal_boundT_contradict [in Traces]
terminal_concat_P_compose [in Traces]
terminal_concat_compose [in Traces]
terminal_unique [in Traces]
terminal_composed [in Traces]
Test.all_zero [in AutoIndTac]
Test.all_zero_by_hand [in AutoIndTac]
trace_partial_prefix2 [in TraceSemantics]
trace_partial_prefix [in TraceSemantics]
trace_partial_Seq_left [in TraceSemantics]
trace_concat_partial_left [in TraceSemantics]
trace_concat_P [in TraceSemantics]
trace_sem [in IMP]
trec_correct [in TailRecursion]
trec_tailrec [in TailRecursion]
trec_bound_ren [in TailRecursion]
trec_shift [in TailRecursion]
trec_ren_preserve [in TailRecursion]
trec_bound_lift [in TailRecursion]
U
undup_idempotent [in Base]undup_id [in Base]
undup_equi [in Base]
undup_incl [in Base]
undup_id_equi [in Base]
unfold_Fix_subsume [in Unfolding]
unfold_subst [in Unfolding]
unfold_step [in Unfolding]
up_change [in CFP]
Constructor Index
B
BoundChoice [in FreeVariables]BoundEps [in FreeVariables]
BoundFix [in FreeVariables]
BoundSeq [in FreeVariables]
BoundTP [in Traces]
BoundTT [in Traces]
BoundTV [in Traces]
BoundVar1 [in FreeVariables]
BoundVar2 [in FreeVariables]
C
CFPChoice [in CFP]CFPEps [in CFP]
CFPFix [in CFP]
CFPSeq [in CFP]
CFPVar [in CFP]
CmdAct [in IMP]
CmdIf [in IMP]
CmdSeq [in IMP]
CmdSkip [in IMP]
CmdWhile [in IMP]
ComposedV [in Traces]
D
dupfreeC [in Base]dupfreeN [in Base]
L
LinChoice [in Linearity]LinEps [in Linearity]
LinFix [in Linearity]
LinSeq [in Linearity]
LinVar [in Linearity]
P
P [in Traces]PartialP [in Traces]
PartialV [in Traces]
R
RegChoice [in Regularity]RegEps [in Regularity]
RegiChoice [in Regularity]
RegiEps [in Regularity]
RegiNull [in Regularity]
RegiSeq [in Regularity]
RegiStar [in Regularity]
RegiVar [in Regularity]
RegNull [in Regularity]
RegSeq [in Regularity]
RegStar [in Regularity]
RegVar [in Regularity]
RunT [in IMP]
RunV [in IMP]
S
SemCmdIfFalse [in IMP]SemCmdIfTrue [in IMP]
SemCmdInput [in IMP]
SemCmdSeq [in IMP]
SemCmdSkip [in IMP]
SemCmdWhileFalse [in IMP]
SemCmdWhileTrue [in IMP]
SubstTP [in Substitutivity]
SubstTT [in Substitutivity]
SubstTV [in Substitutivity]
T
T [in Traces]TailRecChoice [in TailRecursion]
TailRecEps [in TailRecursion]
TailRecFix [in TailRecursion]
TailRecSeq [in TailRecursion]
TailRecVar [in TailRecursion]
TCChoiceRight [in TraceSemantics]
TCFix [in TraceSemantics]
TChoiceLeft [in TraceSemantics]
TCPartial [in TraceSemantics]
TCsubstChoiceLeft [in Substitutivity]
TCsubstChoiceRight [in Substitutivity]
TCsubstFix [in Substitutivity]
TCsubstPartial [in Substitutivity]
TCsubstSeq [in Substitutivity]
TCsubstTotal [in Substitutivity]
TCsubstVar [in Substitutivity]
TCTotal [in TraceSemantics]
TCVarPartial [in TraceSemantics]
TCVarTotal [in TraceSemantics]
TerminalP [in Traces]
TerminalT [in Traces]
TerminalV [in Traces]
Test.base [in AutoIndTac]
Test.step [in AutoIndTac]
TotalT [in Traces]
TotalV [in Traces]
TrecChoice [in TailRecursion]
TrecEps [in TailRecursion]
TrecFix [in TailRecursion]
TrecSeq [in TailRecursion]
TrecVar1 [in TailRecursion]
TrecVar2 [in TailRecursion]
TSeq [in TraceSemantics]
V
V [in Traces]Axiom Index
C
comp_charact [in IMP]I
inj_test_action_inj [in IMP]inj_test_action [in IMP]
T
test_charact [in IMP]Inductive Index
B
bound [in FreeVariables]boundT [in Traces]
C
cfp [in CFP]cmd [in IMP]
composed [in Traces]
D
dupfree [in Base]L
lin [in Linearity]P
partial [in Traces]R
reg [in Regularity]regi [in Regularity]
run [in IMP]
S
sem [in IMP]substT [in Substitutivity]
T
tailrec [in TailRecursion]TC [in TraceSemantics]
TCsubst [in Substitutivity]
terminal [in Traces]
Test.decreasing [in AutoIndTac]
total [in Traces]
trace [in Traces]
trec [in TailRecursion]
Instance Index
A
and_dec [in Base]app_equi_proper [in Base]
app_incl_proper [in Base]
B
bool_eq_dec [in Base]C
card_equi_proper [in Base]cfp_dec [in CFP]
Choice_eqTC_proper [in Congruence]
cons_equi_proper [in Base]
cons_incl_proper [in Base]
E
eqTC_Equivalence [in TraceSemantics]equi_Equivalence [in Base]
F
False_dec [in Base]Fix_eqTC_proper [in Congruence]
I
Ids_term [in CFP]iff_dec [in Base]
impl_dec [in Base]
incl_equi_proper [in Base]
incl_preorder [in Base]
in_equi_proper [in Base]
in_incl_proper [in Base]
L
list_exists_dec [in Base]list_forall_dec [in Base]
list_in_dec [in Base]
list_eq_dec [in Base]
N
nat_le_dec [in Base]nat_eq_dec [in Base]
not_dec [in Base]
O
or_dec [in Base]P
partial_dec [in Traces]R
Rename_term [in CFP]S
Seq_eqTC_proper [in Congruence]SubstLemmas_term [in CFP]
Subst_term [in CFP]
T
True_dec [in Base]Section Index
C
Cardinality [in Base]D
Dupfree [in Base]E
Equi [in Base]F
FCI.FCI [in Base]FilterComm [in Base]
FilterLemmas [in Base]
FilterLemmas_pq [in Base]
I
Imp [in IMP]Inclusion [in Base]
Iteration [in Base]
M
Membership [in Base]P
PowerRep [in Base]R
Removal [in Base]U
Undup [in Base]Definition Index
B
butLast [in Traces]C
card [in Base]cfa [in IMP]
concat [in Traces]
D
dec [in Base]decision [in Base]
decomp [in Regularizer]
disjoint [in Base]
dupfree_inv [in Base]
E
eqSem [in IMP]eqTC [in TraceSemantics]
equi [in Base]
F
FCI.C [in Base]FCI.F [in Base]
filter [in Base]
FP [in Base]
I
inclp [in Base]it [in Base]
iterate [in TraceSemantics]
L
linearize [in DirectLinearizer]lini [in RegLinearizer]
N
notBlock [in IMP]Null [in CFP]
P
part [in CFP]power [in Base]
R
regularize [in Regularizer]rem [in Base]
ren_trace [in Traces]
rep [in Base]
S
shift [in CFP]simulatesI [in CFP]
Star [in CFP]
substPos [in CFP]
T
tailrec_trace [in Traces]U
undup [in Base]unfold [in Unfolding]
| 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 | (550 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 | (7 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 | (2 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 | (25 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 | (19 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 | (299 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 | (89 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 | (4 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 | (21 entries) |
| Instance 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 | (34 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 | (14 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 | (36 entries) |
This page has been generated by coqdoc