| 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 | (1417 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 | (31 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 | (37 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 | (442 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 | (28 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 | (401 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |
| 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 | (21 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 | (18 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 | (3 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 | (58 entries) |
| Abbreviation 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 | (116 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 | (238 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 | (8 entries) |
Global Index
A
A [abbreviation, in chip.finn]access_to [definition, in chip.tarjan]
acyclic [definition, in chip.acyclic]
Acyclic [section, in chip.acyclic]
acyclic [library]
Acyclicity [section, in chip.acyclic]
Acyclicity.all_in_flatten [variable, in chip.acyclic]
Acyclicity.class_diconnected [variable, in chip.acyclic]
Acyclicity.g [variable, in chip.acyclic]
Acyclicity.sccs [variable, in chip.acyclic]
Acyclicity.uniq_flatten [variable, in chip.acyclic]
Acyclicity.V [variable, in chip.acyclic]
AcyclicRev [section, in chip.acyclic]
AcyclicRev.g [variable, in chip.acyclic]
AcyclicRev.g_acyclic [variable, in chip.acyclic]
AcyclicRev.V [variable, in chip.acyclic]
AcyclicSub [section, in chip.acyclic]
AcyclicSub.g [variable, in chip.acyclic]
AcyclicSub.g_acyclic [variable, in chip.acyclic]
AcyclicSub.P [variable, in chip.acyclic]
AcyclicSub.V [variable, in chip.acyclic]
acyclic_find_in_diconnect [lemma, in chip.topos]
acyclic_rev [lemma, in chip.acyclic]
acyclic_diconnect [lemma, in chip.acyclic]
acyclic_no_self_loop [lemma, in chip.acyclic]
Acyclic.g [variable, in chip.acyclic]
Acyclic.g_acyclic [variable, in chip.acyclic]
Acyclic.V [variable, in chip.acyclic]
add_stack_pre [lemma, in chip.tarjan]
add_stack_gwf [lemma, in chip.tarjan]
add_sccs_wf [lemma, in chip.tarjan]
add_blacks_ewf [lemma, in chip.tarjan]
add_stack_ewf [lemma, in chip.tarjan]
add_sccs [definition, in chip.tarjan]
add_blacks [definition, in chip.tarjan]
add_stack [definition, in chip.tarjan]
adjundup [definition, in chip.hierarchical]
all_in_flatten_tarjans [lemma, in chip.tarjan_acyclic]
all_in_cover_tarjan [lemma, in chip.tarjan_acyclic]
all_in_flatten_kosaraju [lemma, in chip.kosaraju_acyclic]
all_in_sccs [lemma, in chip.acyclic]
ascii_eqMixin [definition, in chip.string]
A_bot [abbreviation, in chip.finn]
A_top [abbreviation, in chip.finn]
B
before [definition, in chip.connect]before_can_toW [lemma, in chip.connect]
before_can_to [lemma, in chip.connect]
before_filter [lemma, in chip.connect]
before_filter_inv [lemma, in chip.connect]
blacks [projection, in chip.tarjan]
blacks_add_sccs [lemma, in chip.tarjan]
black_gsccs [definition, in chip.tarjan]
C
can_to_cat [lemma, in chip.connect]can_to_cons [lemma, in chip.connect]
can_to [definition, in chip.connect]
cert_check_impactedV'_check [lemma, in chip.check]
change [library]
Changed [section, in chip.change]
ChangedHierarchical [section, in chip.hierarchical_correct]
ChangedHierarchicalSub [section, in chip.hierarchical_sub_correct]
ChangedHierarchicalSubPt [section, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.A_bot [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.A_top [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.check [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.checkable [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.checkable_bot [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.checkable' [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.check_bot [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.check' [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f_bot_equal_g_bot [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f_top_equal_g_top [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f_top_partition [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f_top_bot [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f_bot [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f_top [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f'_bot [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f'_top [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.g_bot_top [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.g_bot [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.g_top [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.g'_bot [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.g'_top [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.p [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.p_partition [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.p_neq [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.P_bot [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.P_top [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.p' [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.p'_partition [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.p'_neq [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.R [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.U' [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.V_result_cert_uniq [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.V_result_certP [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.V_result_cert [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.V' [variable, in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSub.A_bot [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.A_top [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.check [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.checkable [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.checkable_bot [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.checkable' [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.check_bot [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.check' [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f_bot_equal_g_bot [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f_top_equal_g_top [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f_top_bot [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f_bot [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f_top [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f'_bot [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f'_top [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.g_bot_top [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.g_bot [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.g_top [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.g'_bot [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.g'_top [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.p [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.p_partition [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.p_neq [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.P_bot [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.P_top [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.p' [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.p'_partition [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.p'_neq [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.R [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.U' [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.V_result_cert_uniq [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.V_result_certP [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.V_result_cert [variable, in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.V' [variable, in chip.hierarchical_sub_correct]
ChangedHierarchical.A_bot [variable, in chip.hierarchical_correct]
ChangedHierarchical.A_top [variable, in chip.hierarchical_correct]
ChangedHierarchical.check [variable, in chip.hierarchical_correct]
ChangedHierarchical.checkable [variable, in chip.hierarchical_correct]
ChangedHierarchical.checkable_bot [variable, in chip.hierarchical_correct]
ChangedHierarchical.checkable' [variable, in chip.hierarchical_correct]
ChangedHierarchical.check_bot [variable, in chip.hierarchical_correct]
ChangedHierarchical.check' [variable, in chip.hierarchical_correct]
ChangedHierarchical.f_bot_equal_g_bot [variable, in chip.hierarchical_correct]
ChangedHierarchical.f_top_equal_g_top [variable, in chip.hierarchical_correct]
ChangedHierarchical.f_top_bot [variable, in chip.hierarchical_correct]
ChangedHierarchical.f_top_partition [variable, in chip.hierarchical_correct]
ChangedHierarchical.f_bot [variable, in chip.hierarchical_correct]
ChangedHierarchical.f_top [variable, in chip.hierarchical_correct]
ChangedHierarchical.f'_bot [variable, in chip.hierarchical_correct]
ChangedHierarchical.f'_top [variable, in chip.hierarchical_correct]
ChangedHierarchical.g_bot_top [variable, in chip.hierarchical_correct]
ChangedHierarchical.g_bot [variable, in chip.hierarchical_correct]
ChangedHierarchical.g_top [variable, in chip.hierarchical_correct]
ChangedHierarchical.g'_bot [variable, in chip.hierarchical_correct]
ChangedHierarchical.g'_top [variable, in chip.hierarchical_correct]
ChangedHierarchical.p [variable, in chip.hierarchical_correct]
ChangedHierarchical.p_partition [variable, in chip.hierarchical_correct]
ChangedHierarchical.p_neq [variable, in chip.hierarchical_correct]
ChangedHierarchical.P_bot [variable, in chip.hierarchical_correct]
ChangedHierarchical.P_top [variable, in chip.hierarchical_correct]
ChangedHierarchical.p' [variable, in chip.hierarchical_correct]
ChangedHierarchical.p'_partition [variable, in chip.hierarchical_correct]
ChangedHierarchical.p'_neq [variable, in chip.hierarchical_correct]
ChangedHierarchical.R [variable, in chip.hierarchical_correct]
ChangedHierarchical.U' [variable, in chip.hierarchical_correct]
ChangedHierarchical.V_result_cert_uniq [variable, in chip.hierarchical_correct]
ChangedHierarchical.V_result_certP [variable, in chip.hierarchical_correct]
ChangedHierarchical.V_result_cert [variable, in chip.hierarchical_correct]
ChangedHierarchical.V' [variable, in chip.hierarchical_correct]
Changed.A [variable, in chip.change]
Changed.check [variable, in chip.change]
Changed.checkable [variable, in chip.change]
Changed.checkable_V_V' [variable, in chip.change]
Changed.checkable' [variable, in chip.change]
Changed.check_V_V' [variable, in chip.change]
Changed.check' [variable, in chip.change]
Changed.f [variable, in chip.change]
Changed.f_equal_g [variable, in chip.change]
Changed.f' [variable, in chip.change]
Changed.g [variable, in chip.change]
Changed.g' [variable, in chip.change]
Changed.P [variable, in chip.change]
Changed.R [variable, in chip.change]
Changed.V_result_cert_uniq [variable, in chip.change]
Changed.V_result_certP [variable, in chip.change]
Changed.V_result_cert [variable, in chip.change]
Changed.V' [variable, in chip.change]
check [library]
checkable_impacted_fresh_sub_pt [definition, in chip.hierarchical_sub_pt]
checkable_impactedV'_sub_pt [definition, in chip.hierarchical_sub_pt]
checkable_pimpacted_fresh [definition, in chip.hierarchical]
checkable_pimpacted_V' [definition, in chip.hierarchical]
checkable_impacted_fresh_sub [definition, in chip.hierarchical_sub]
checkable_impactedV'_sub [definition, in chip.hierarchical_sub]
checkable_impacted_fresh [definition, in chip.check]
checkable_impactedV' [definition, in chip.check]
checkable_impacted [definition, in chip.check]
checkable_impactedV [definition, in chip.check]
Checked [section, in chip.check]
CheckedSeq [section, in chip.check_seq]
CheckedSeqHierarchical [section, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.A_bot [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.A_top [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.checkable'_bot [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.clos_bot_uniq [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.clos_top_uniq [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.clos_botP [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.clos_bot [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.clos_topP [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.clos_top [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.f_top_partition [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.f_top_bot_ps [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.f_bot [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.f_top [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.f'_bot [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.f'_top [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_bot_top_ps [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_bot_grev [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_bot [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_top_grev [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_top [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_bot_rev [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_top_rev [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.p [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.ps [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.ps_neq [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.ps_partition [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.ps' [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.ps'_neq [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.ps'_partition [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.p_uniq [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.p_ps_eq [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.P_bot [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.P_top [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.p' [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.p'_uniq [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.p'_ps'_eq [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.U' [variable, in chip.check_seq_hierarchical]
CheckedSeqHierarchical.V' [variable, in chip.check_seq_hierarchical]
CheckedSeq.A [variable, in chip.check_seq]
CheckedSeq.checkable' [variable, in chip.check_seq]
CheckedSeq.clos [variable, in chip.check_seq]
CheckedSeq.closP [variable, in chip.check_seq]
CheckedSeq.clos_uniq [variable, in chip.check_seq]
CheckedSeq.f [variable, in chip.check_seq]
CheckedSeq.f_equal_g [variable, in chip.check_seq]
CheckedSeq.f' [variable, in chip.check_seq]
CheckedSeq.g [variable, in chip.check_seq]
CheckedSeq.grev [variable, in chip.check_seq]
CheckedSeq.g_grev [variable, in chip.check_seq]
CheckedSeq.g' [variable, in chip.check_seq]
CheckedSeq.g'rev [variable, in chip.check_seq]
CheckedSeq.g'_g'rev [variable, in chip.check_seq]
CheckedSeq.g'_acyclic [variable, in chip.check_seq]
CheckedSeq.P [variable, in chip.check_seq]
CheckedSeq.ts [variable, in chip.check_seq]
CheckedSeq.ts_uniq [variable, in chip.check_seq]
CheckedSeq.ts_all [variable, in chip.check_seq]
CheckedSeq.ts_tsorted [variable, in chip.check_seq]
CheckedSeq.V' [variable, in chip.check_seq]
Checked.A [variable, in chip.check]
Checked.check [variable, in chip.check]
Checked.checkable [variable, in chip.check]
Checked.f [variable, in chip.check]
Checked.f' [variable, in chip.check]
Checked.g [variable, in chip.check]
Checked.P [variable, in chip.check]
Checked.R [variable, in chip.check]
Checked.V' [variable, in chip.check]
check_all_cert_V'_uniq_p [lemma, in chip.hierarchical_correct]
check_all_cert_sound_p [lemma, in chip.hierarchical_correct]
check_all_cert_complete_p [lemma, in chip.hierarchical_correct]
check_all_cert_V'_p [definition, in chip.hierarchical_correct]
check_all_cert_p [definition, in chip.hierarchical_correct]
check_impactedV'_sub_pt_cert [definition, in chip.hierarchical_sub_pt]
check_all_cert_sound_g2 [lemma, in chip.change]
check_all_cert_complete_g2 [lemma, in chip.change]
check_all_cert_V'_uniq_g2 [lemma, in chip.change]
check_all_cert_sound [lemma, in chip.change]
check_all_cert_complete [lemma, in chip.change]
check_all_cert_V'_uniq [lemma, in chip.change]
check_all_cert_V' [definition, in chip.change]
check_all_cert_cases [lemma, in chip.change]
check_all_cert [definition, in chip.change]
check_all_cert_V'_sub_uniq [lemma, in chip.hierarchical_sub_correct]
check_all_cert_sound_sub [lemma, in chip.hierarchical_sub_correct]
check_all_cert_complete_sub [lemma, in chip.hierarchical_sub_correct]
check_all_cert_V'_sub [definition, in chip.hierarchical_sub_correct]
check_all_cert_sub [definition, in chip.hierarchical_sub_correct]
check_pimpacted_V'_cert_uniq [lemma, in chip.hierarchical]
check_pimpacted_V'_certP [lemma, in chip.hierarchical]
check_pimpacted_V'_cert [definition, in chip.hierarchical]
check_all_cert_V'_sub_pt_uniq [lemma, in chip.hierarchical_sub_pt_correct]
check_all_cert_sound_sub_pt [lemma, in chip.hierarchical_sub_pt_correct]
check_all_cert_complete_sub_pt [lemma, in chip.hierarchical_sub_pt_correct]
check_all_cert_V'_sub_pt [definition, in chip.hierarchical_sub_pt_correct]
check_all_cert_sub_pt [definition, in chip.hierarchical_sub_pt_correct]
check_impactedV'_sub_cert [definition, in chip.hierarchical_sub]
check_impactedV'_cert_uniq [lemma, in chip.check]
check_impactedV'_certP [lemma, in chip.check]
check_impactedV'_cert_check [lemma, in chip.check]
check_impactedV'_cert [definition, in chip.check]
check_seq_hierarchical [library]
check_seq [library]
class_diconnected_tarjans [lemma, in chip.tarjan_acyclic]
class_diconnected_tarjan [lemma, in chip.tarjan_acyclic]
class_diconnected_kosaraju [lemma, in chip.kosaraju_acyclic]
class_acyclic [definition, in chip.acyclic]
close_dfs [library]
Closure [section, in chip.closure]
closure [library]
closureP [lemma, in chip.close_dfs]
closure_eqi [lemma, in chip.close_dfs]
closure_g [lemma, in chip.close_dfs]
closure_example [library]
Closure.g [variable, in chip.closure]
Closure.modified [variable, in chip.closure]
Closure.V [variable, in chip.closure]
ColorBlackStack [constructor, in chip.tarjan]
ColorGray [constructor, in chip.tarjan]
colorP [lemma, in chip.tarjan]
ColorSccs [constructor, in chip.tarjan]
ColorWhite [constructor, in chip.tarjan]
color_spec [inductive, in chip.tarjan]
connect [library]
connect_from [lemma, in chip.extra]
connect_to [lemma, in chip.extra]
connect_rev [lemma, in chip.extra]
connect_g_bot_rev_sub_g_bot_rev [lemma, in chip.check_seq_hierarchical]
connect_rel_sub [lemma, in chip.check_seq_hierarchical]
connect_f_f'_eq [lemma, in chip.change]
connect_gV'_rev [lemma, in chip.change]
connect_g'_imf [lemma, in chip.check_seq]
connect_imp [lemma, in chip.check_seq]
connect_to_rev [lemma, in chip.connect]
connect_to_C1_id [lemma, in chip.connect]
connect_to_C1l [lemma, in chip.connect]
connect_to_C1r [lemma, in chip.connect]
connect_to_forced [lemma, in chip.connect]
connect_toT [lemma, in chip.connect]
connect_to_sub [lemma, in chip.connect]
connect_toW [lemma, in chip.connect]
connect_to1 [lemma, in chip.connect]
connect_from_to [lemma, in chip.connect]
connect_to_from [lemma, in chip.connect]
connect_rev [lemma, in chip.connect]
connect_rev_v_u [lemma, in chip.hierarchical]
connect_checkable_impactedV' [lemma, in chip.check]
connect_impactedV'_eq [lemma, in chip.check]
connect_impactedV_eq [lemma, in chip.check]
connect1l [lemma, in chip.extra]
connect1r [lemma, in chip.extra]
cover_gsccs [definition, in chip.tarjan]
cover_tarjan [lemma, in chip.tarjan_acyclic]
cover_all_in [lemma, in chip.tarjan_acyclic]
cover0 [lemma, in chip.tarjan]
Cycles [section, in chip.acyclic]
Cycles.g [variable, in chip.acyclic]
Cycles.V [variable, in chip.acyclic]
cycle_path_diconnect [lemma, in chip.acyclic]
D
def_scc [definition, in chip.tarjan]DFS [module, in chip.dfs_set]
DFSearch [section, in chip.close_dfs]
DFSearch.T [variable, in chip.close_dfs]
dfs_uniq [lemma, in chip.close_dfs]
dfs_mems [lemma, in chip.close_dfs]
dfs_mem' [lemma, in chip.close_dfs]
dfs_mem [lemma, in chip.close_dfs]
dfs_eq_in [lemma, in chip.close_dfs]
dfs_in_in [lemma, in chip.close_dfs]
dfs_subset [lemma, in chip.close_dfs]
dfs_in [lemma, in chip.close_dfs]
dfs_set [library]
dfs' [definition, in chip.tarjan]
dfs'_is_correct [lemma, in chip.tarjan]
dfs'_correct [definition, in chip.tarjan]
DFS.dfs_sdfs_in [lemma, in chip.dfs_set]
DFS.elements_in_mem [lemma, in chip.dfs_set]
DFS.elts_srclosure'_uniq [lemma, in chip.dfs_set]
DFS.elts_srclosure_uniq [lemma, in chip.dfs_set]
DFS.elts_srclosure'Pg [lemma, in chip.dfs_set]
DFS.elts_srclosure'P [lemma, in chip.dfs_set]
DFS.elts_srclosurePg [lemma, in chip.dfs_set]
DFS.elts_srclosureP [lemma, in chip.dfs_set]
DFS.elts_srclosure' [definition, in chip.dfs_set]
DFS.elts_srclosure [definition, in chip.dfs_set]
DFS.in_foldr_mem [lemma, in chip.dfs_set]
DFS.MSF [module, in chip.dfs_set]
DFS.rclosed_elts_srclosure' [lemma, in chip.dfs_set]
DFS.rclosed_elts_srclosure [lemma, in chip.dfs_set]
DFS.rclosure_srclosure [lemma, in chip.dfs_set]
DFS.rclosure'_srclosure' [lemma, in chip.dfs_set]
DFS.sdfs [definition, in chip.dfs_set]
DFS.srclosure [definition, in chip.dfs_set]
DFS.srclosure_srclosure' [lemma, in chip.dfs_set]
DFS.srclosure' [definition, in chip.dfs_set]
DFS.subset_sdfs [lemma, in chip.dfs_set]
dfs1 [definition, in chip.tarjan]
dfs1_is_correct [lemma, in chip.tarjan]
dfs1_correct [definition, in chip.tarjan]
diconnect [definition, in chip.connect]
diconnect_can_to [lemma, in chip.connect]
diconnect_to_predT [lemma, in chip.connect]
diconnect_to_sub [lemma, in chip.connect]
diconnect_trans [lemma, in chip.connect]
diconnect_sym [lemma, in chip.connect]
diconnect_neq_sccs [lemma, in chip.acyclic]
diconnect_path_cycle [lemma, in chip.acyclic]
diconnect0 [lemma, in chip.connect]
disjoints1 [lemma, in chip.extra]
disjoint1s [lemma, in chip.extra]
drop_subseq [lemma, in chip.extra]
drop_subseq [lemma, in chip.tarjan]
E
edge [abbreviation, in chip.tarjan]enums [definition, in chip.tarjan_acyclic]
enumsP [lemma, in chip.tarjan_acyclic]
enums_enums'_in [lemma, in chip.tarjan_acyclic]
enums' [definition, in chip.tarjan_acyclic]
enums'P [lemma, in chip.tarjan_acyclic]
enum_tarjan_non_empty [lemma, in chip.tarjan_acyclic]
env [record, in chip.tarjan]
Env [constructor, in chip.tarjan]
eq_tsorted [lemma, in chip.connect]
eq_can_to [lemma, in chip.connect]
eq_diconnect_to [lemma, in chip.connect]
eq_diconnect [lemma, in chip.connect]
eq_foodP [lemma, in chip.closure_example]
eq_food [definition, in chip.closure_example]
eq_stringP [lemma, in chip.string]
eq_string [definition, in chip.string]
eq_asciiP [lemma, in chip.string]
eq_ascii [definition, in chip.string]
exist_p'u_for_v [lemma, in chip.hierarchical]
exist_list_pu_for_seq_v [lemma, in chip.hierarchical]
exist_pu_for_v [lemma, in chip.hierarchical]
extra [library]
extract_impacted [library]
extract_impacted_rbt [library]
extra_path.V [variable, in chip.extra]
extra_path [section, in chip.extra]
extra_fintype [section, in chip.extra]
extra_seq [section, in chip.extra]
extra_div [section, in chip.extra]
extra_finset [section, in chip.tarjan]
extra_seq [section, in chip.tarjan]
extra_div [section, in chip.tarjan]
e0 [definition, in chip.tarjan]
F
Fin [section, in chip.connect]Finn [section, in chip.finn]
finn [library]
FinnHierarchical [section, in chip.finn]
FinnHierarchical.checkable'_bot [variable, in chip.finn]
FinnHierarchical.f_top_partition [variable, in chip.finn]
FinnHierarchical.f_top_bot_ps [variable, in chip.finn]
FinnHierarchical.f_bot [variable, in chip.finn]
FinnHierarchical.f_top [variable, in chip.finn]
FinnHierarchical.f'_bot [variable, in chip.finn]
FinnHierarchical.f'_top [variable, in chip.finn]
FinnHierarchical.g_bot_top_ps [variable, in chip.finn]
FinnHierarchical.g_bot_grev [variable, in chip.finn]
FinnHierarchical.g_bot [variable, in chip.finn]
FinnHierarchical.g_top_grev [variable, in chip.finn]
FinnHierarchical.g_top [variable, in chip.finn]
FinnHierarchical.H_mn_bot [variable, in chip.finn]
FinnHierarchical.H_mn_top [variable, in chip.finn]
FinnHierarchical.m'_bot [variable, in chip.finn]
FinnHierarchical.m'_top [variable, in chip.finn]
FinnHierarchical.n_bot [variable, in chip.finn]
FinnHierarchical.n_top [variable, in chip.finn]
FinnHierarchical.p [variable, in chip.finn]
FinnHierarchical.ps [variable, in chip.finn]
FinnHierarchical.ps_neq [variable, in chip.finn]
FinnHierarchical.ps_partition [variable, in chip.finn]
FinnHierarchical.ps' [variable, in chip.finn]
FinnHierarchical.ps'_neq [variable, in chip.finn]
FinnHierarchical.ps'_partition [variable, in chip.finn]
FinnHierarchical.p_uniq [variable, in chip.finn]
FinnHierarchical.p_ps_eq [variable, in chip.finn]
FinnHierarchical.p' [variable, in chip.finn]
FinnHierarchical.p'_uniq [variable, in chip.finn]
FinnHierarchical.p'_ps'_eq [variable, in chip.finn]
FinnHierarchical.successors_bot [variable, in chip.finn]
FinnHierarchical.successors_top [variable, in chip.finn]
finn_set [library]
Finn.checkable' [variable, in chip.finn]
Finn.f [variable, in chip.finn]
Finn.f_equal_g [variable, in chip.finn]
Finn.f' [variable, in chip.finn]
Finn.g [variable, in chip.finn]
Finn.g_grev [variable, in chip.finn]
Finn.g' [variable, in chip.finn]
Finn.g'_acyclic [variable, in chip.finn]
Finn.g'_g'rev [variable, in chip.finn]
Finn.H_mn [variable, in chip.finn]
Finn.m' [variable, in chip.finn]
Finn.n [variable, in chip.finn]
Finn.successors [variable, in chip.finn]
Finn.successors' [variable, in chip.finn]
FinOrdType [module, in chip.dfs_set]
FinOrdType.irr_ordT [axiom, in chip.dfs_set]
FinOrdType.ordT [axiom, in chip.dfs_set]
FinOrdType.total_ordT [axiom, in chip.dfs_set]
FinOrdType.trans_ordT [axiom, in chip.dfs_set]
FinOrdUsualOrderedType [module, in chip.dfs_set]
FinOrdUsualOrderedType.compare [definition, in chip.dfs_set]
FinOrdUsualOrderedType.compare_spec [definition, in chip.dfs_set]
FinOrdUsualOrderedType.eq [definition, in chip.dfs_set]
FinOrdUsualOrderedType.eq_dec [definition, in chip.dfs_set]
FinOrdUsualOrderedType.eq_equiv [definition, in chip.dfs_set]
FinOrdUsualOrderedType.lt [definition, in chip.dfs_set]
FinOrdUsualOrderedType.lt_compat [definition, in chip.dfs_set]
FinOrdUsualOrderedType.lt_strorder [definition, in chip.dfs_set]
FinOrdUsualOrderedType.OT [module, in chip.dfs_set]
FinOrdUsualOrderedType.OTUOT [module, in chip.dfs_set]
FinOrdUsualOrderedType.OT.T [definition, in chip.dfs_set]
FinOrdUsualOrderedType.t [definition, in chip.dfs_set]
FinType [module, in chip.dfs_set]
FinTypeOrd [section, in chip.ordtype]
FinTypeOrd.T [variable, in chip.ordtype]
FinType.T [axiom, in chip.dfs_set]
FinUsualOrderedType [module, in chip.dfs_set]
FinUsualOrderedType.compare [axiom, in chip.dfs_set]
FinUsualOrderedType.compare_spec [axiom, in chip.dfs_set]
FinUsualOrderedType.eq [definition, in chip.dfs_set]
FinUsualOrderedType.eq_dec [axiom, in chip.dfs_set]
FinUsualOrderedType.eq_equiv [definition, in chip.dfs_set]
FinUsualOrderedType.lt [axiom, in chip.dfs_set]
FinUsualOrderedType.lt_compat [axiom, in chip.dfs_set]
FinUsualOrderedType.lt_strorder [axiom, in chip.dfs_set]
FinUsualOrderedType.t [definition, in chip.dfs_set]
fin_ordMixin [definition, in chip.ordtype]
Fin.ConnectRelto [section, in chip.connect]
Fin.ConnectRelto.g [variable, in chip.connect]
_ =[ _ ]< _ [notation, in chip.connect]
_ =[ _ ]= _ [notation, in chip.connect]
_ =[]= _ [notation, in chip.connect]
_ -[]-> _ [notation, in chip.connect]
_ -[ _ ]-> _ [notation, in chip.connect]
C[ _ ]_( _ , _ ) [notation, in chip.connect]
TS[ _ ] [notation, in chip.connect]
TS[ _ , _ ] [notation, in chip.connect]
Fin.Diconnect [section, in chip.connect]
Fin.Diconnect.g [variable, in chip.connect]
_ -[]-> _ [notation, in chip.connect]
Fin.Relto [section, in chip.connect]
Fin.Relto.g [variable, in chip.connect]
_ =[ _ ]< _ [notation, in chip.connect]
_ =[ _ ]= _ [notation, in chip.connect]
_ =[]= _ [notation, in chip.connect]
_ -[]-> _ [notation, in chip.connect]
_ -[ _ ]-> _ [notation, in chip.connect]
C[ _ ]_( _ , _ ) [notation, in chip.connect]
Fin.Sub [section, in chip.connect]
Fin.Sub.g [variable, in chip.connect]
Fin.Sub.P [variable, in chip.connect]
Fin.V [variable, in chip.connect]
foldr_pdfs_subset [lemma, in chip.topos]
food [inductive, in chip.closure_example]
food_rev_impacted [definition, in chip.closure_example]
food_rel_rev [abbreviation, in chip.closure_example]
food_acyclic [definition, in chip.closure_example]
food_rel [definition, in chip.closure_example]
food_depends [definition, in chip.closure_example]
food_finMixin [definition, in chip.closure_example]
food_finite [lemma, in chip.closure_example]
food_enum [definition, in chip.closure_example]
food_countMixin [definition, in chip.closure_example]
food_choiceMixin [definition, in chip.closure_example]
food_pcancel [lemma, in chip.closure_example]
food_unpickle [definition, in chip.closure_example]
food_pickle [definition, in chip.closure_example]
food_eqMixin [definition, in chip.closure_example]
freshV' [definition, in chip.check]
freshV'P [lemma, in chip.check]
freshV'_sub_eq [lemma, in chip.hierarchical_sub_pt]
freshV'_sub [definition, in chip.hierarchical_sub_pt]
fun_of [projection, in chip.ordtype]
FUOT5 [module, in chip.dfs_set]
G
g [abbreviation, in chip.kosaraju_acyclic]garlic [constructor, in chip.closure_example]
gbiconnect [abbreviation, in chip.tarjan]
gbiconnect_equiv [lemma, in chip.tarjan]
gconnect [abbreviation, in chip.tarjan]
ginsubexP [lemma, in chip.change]
ginsubP [lemma, in chip.change]
ginsub_eq [lemma, in chip.change]
grays [definition, in chip.tarjan]
grays_add_sccs [lemma, in chip.tarjan]
grays_add_blacks [lemma, in chip.tarjan]
grays_add_stack [lemma, in chip.tarjan]
grays_sccsF [lemma, in chip.tarjan]
grays_stack [lemma, in chip.tarjan]
grays0 [lemma, in chip.tarjan]
grev [abbreviation, in chip.change]
grev [abbreviation, in chip.acyclic]
grevinsubexP [lemma, in chip.change]
gsccs [definition, in chip.tarjan]
gsccs_partition [lemma, in chip.tarjan]
gsub [abbreviation, in chip.connect]
gsub [abbreviation, in chip.acyclic]
gsub_connect [lemma, in chip.connect]
gsub_path [lemma, in chip.connect]
gsub_acyclic [lemma, in chip.acyclic]
gV' [abbreviation, in chip.change]
gV' [abbreviation, in chip.check_seq]
gV' [abbreviation, in chip.finn]
gV'rev [abbreviation, in chip.change]
g_bot_V'_rev [abbreviation, in chip.hierarchical_correct]
g_bot_V' [abbreviation, in chip.hierarchical_correct]
g_top_U'_rev [abbreviation, in chip.hierarchical_correct]
g_top_U' [abbreviation, in chip.hierarchical_correct]
g_bot_rev [abbreviation, in chip.hierarchical_correct]
g_top_rev [abbreviation, in chip.hierarchical_correct]
g_bot_sub [abbreviation, in chip.hierarchical_sub_pt]
g_bot_rev [abbreviation, in chip.hierarchical_sub_pt]
g_top_rev [abbreviation, in chip.hierarchical_sub_pt]
g_bot_rev_sub_eqq [lemma, in chip.check_seq_hierarchical]
g_bot_rev_sub [definition, in chip.check_seq_hierarchical]
g_bot_sub [abbreviation, in chip.hierarchical_sub_correct]
g_bot_V'_rev [abbreviation, in chip.hierarchical_sub_correct]
g_bot_V' [abbreviation, in chip.hierarchical_sub_correct]
g_top_U'_rev [abbreviation, in chip.hierarchical_sub_correct]
g_top_U' [abbreviation, in chip.hierarchical_sub_correct]
g_bot_rev [abbreviation, in chip.hierarchical_sub_correct]
g_top_rev [abbreviation, in chip.hierarchical_sub_correct]
g_bot_rev [abbreviation, in chip.hierarchical]
g_top_rev [abbreviation, in chip.hierarchical]
g_bot_sub [abbreviation, in chip.hierarchical_sub_pt_correct]
g_bot_V'_rev [abbreviation, in chip.hierarchical_sub_pt_correct]
g_bot_V' [abbreviation, in chip.hierarchical_sub_pt_correct]
g_top_U'_rev [abbreviation, in chip.hierarchical_sub_pt_correct]
g_top_U' [abbreviation, in chip.hierarchical_sub_pt_correct]
g_bot_rev [abbreviation, in chip.hierarchical_sub_pt_correct]
g_top_rev [abbreviation, in chip.hierarchical_sub_pt_correct]
g_bot_sub [abbreviation, in chip.hierarchical_sub]
g_bot_rev [abbreviation, in chip.hierarchical_sub]
g_top_rev [abbreviation, in chip.hierarchical_sub]
g'rev [abbreviation, in chip.change]
g'rev_imf [definition, in chip.check_seq]
g'_bot_rev [abbreviation, in chip.hierarchical_correct]
g'_top_rev [abbreviation, in chip.hierarchical_correct]
g'_imf [abbreviation, in chip.check_seq]
g'_bot_rev [abbreviation, in chip.hierarchical_sub_correct]
g'_top_rev [abbreviation, in chip.hierarchical_sub_correct]
g'_bot_rev [abbreviation, in chip.hierarchical_sub_pt_correct]
g'_top_rev [abbreviation, in chip.hierarchical_sub_pt_correct]
g1V' [abbreviation, in chip.change]
H
hierarchical [library]HierarchicalSub [section, in chip.hierarchical_sub]
HierarchicalSubPt [section, in chip.hierarchical_sub_pt]
HierarchicalSubPt.A_bot [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.A_top [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.check [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.checkable [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.f_top_partition [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.f_top_bot [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.f_bot [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.f_top [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.f'_bot [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.f'_top [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.g_bot_top [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.g_bot [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.g_top [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.p [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.p_partition [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.p_neq [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.P_bot [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.P_top [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.p' [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.p'_partition [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.R [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.U' [variable, in chip.hierarchical_sub_pt]
HierarchicalSubPt.V' [variable, in chip.hierarchical_sub_pt]
HierarchicalSub.A_bot [variable, in chip.hierarchical_sub]
HierarchicalSub.A_top [variable, in chip.hierarchical_sub]
HierarchicalSub.check [variable, in chip.hierarchical_sub]
HierarchicalSub.checkable [variable, in chip.hierarchical_sub]
HierarchicalSub.f_top_bot [variable, in chip.hierarchical_sub]
HierarchicalSub.f_bot [variable, in chip.hierarchical_sub]
HierarchicalSub.f_top [variable, in chip.hierarchical_sub]
HierarchicalSub.f'_bot [variable, in chip.hierarchical_sub]
HierarchicalSub.f'_top [variable, in chip.hierarchical_sub]
HierarchicalSub.g_bot_top [variable, in chip.hierarchical_sub]
HierarchicalSub.g_bot [variable, in chip.hierarchical_sub]
HierarchicalSub.g_top [variable, in chip.hierarchical_sub]
HierarchicalSub.p [variable, in chip.hierarchical_sub]
HierarchicalSub.p_partition [variable, in chip.hierarchical_sub]
HierarchicalSub.p_neq [variable, in chip.hierarchical_sub]
HierarchicalSub.P_bot [variable, in chip.hierarchical_sub]
HierarchicalSub.P_top [variable, in chip.hierarchical_sub]
HierarchicalSub.R [variable, in chip.hierarchical_sub]
HierarchicalSub.U' [variable, in chip.hierarchical_sub]
HierarchicalSub.V' [variable, in chip.hierarchical_sub]
hierarchical_sub_pt_correct [library]
hierarchical_sub [library]
hierarchical_sub_correct [library]
hierarchical_sub_pt [library]
hierarchical_correct [library]
Hierarchy [section, in chip.hierarchical]
Hierarchy.A_bot [variable, in chip.hierarchical]
Hierarchy.A_top [variable, in chip.hierarchical]
Hierarchy.check [variable, in chip.hierarchical]
Hierarchy.checkable [variable, in chip.hierarchical]
Hierarchy.f_top_bot [variable, in chip.hierarchical]
Hierarchy.f_top_partition [variable, in chip.hierarchical]
Hierarchy.f_bot [variable, in chip.hierarchical]
Hierarchy.f_top [variable, in chip.hierarchical]
Hierarchy.f'_bot [variable, in chip.hierarchical]
Hierarchy.f'_top [variable, in chip.hierarchical]
Hierarchy.g_bot_top [variable, in chip.hierarchical]
Hierarchy.g_bot [variable, in chip.hierarchical]
Hierarchy.g_top [variable, in chip.hierarchical]
Hierarchy.p [variable, in chip.hierarchical]
Hierarchy.p_partition [variable, in chip.hierarchical]
Hierarchy.p_neq [variable, in chip.hierarchical]
Hierarchy.P_bot [variable, in chip.hierarchical]
Hierarchy.P_top [variable, in chip.hierarchical]
Hierarchy.p' [variable, in chip.hierarchical]
Hierarchy.p'_partition [variable, in chip.hierarchical]
Hierarchy.p'_neq [variable, in chip.hierarchical]
Hierarchy.R [variable, in chip.hierarchical]
Hierarchy.U' [variable, in chip.hierarchical]
Hierarchy.V' [variable, in chip.hierarchical]
I
I [abbreviation, in chip.connect]I [abbreviation, in chip.acyclic]
impacted [definition, in chip.closure]
impactedP [lemma, in chip.closure]
impactedVP [lemma, in chip.check]
impactedVV' [definition, in chip.check]
impactedVV'_sub_eq [lemma, in chip.hierarchical_sub]
impactedVV'_sub [definition, in chip.hierarchical_sub]
impactedVV'_freshV' [lemma, in chip.check]
impactedV_in_pimpacted_V [lemma, in chip.hierarchical]
impactedV_impactedV_sub_eq [lemma, in chip.hierarchical_sub]
impactedV_sub_impactedV_eq [lemma, in chip.hierarchical_sub]
impactedV_sub [definition, in chip.hierarchical_sub]
impactedV' [definition, in chip.check]
impactedV'P [lemma, in chip.check]
impactedV'_sub_pt_eq [lemma, in chip.hierarchical_sub_pt]
impactedV'_sub_pt [definition, in chip.hierarchical_sub_pt]
impactedV'_sub_eq [lemma, in chip.hierarchical_sub]
impactedV'_sub [definition, in chip.hierarchical_sub]
impacted_U' [definition, in chip.hierarchical]
impacted_U [definition, in chip.hierarchical]
impacted_fresh_sub [definition, in chip.hierarchical_sub]
impacted_fresh [definition, in chip.check]
impacted_closure [lemma, in chip.check]
index_find [lemma, in chip.connect]
infty [abbreviation, in chip.tarjan]
insub_g_bot [abbreviation, in chip.hierarchical_correct]
insub_g_top [abbreviation, in chip.hierarchical_correct]
insub_g [definition, in chip.change]
insub_g_bot [abbreviation, in chip.hierarchical_sub_correct]
insub_g_top [abbreviation, in chip.hierarchical_sub_correct]
insub_g_bot [abbreviation, in chip.hierarchical_sub_pt_correct]
insub_g_top [abbreviation, in chip.hierarchical_sub_pt_correct]
InvRel [section, in chip.check]
InvRel.T [variable, in chip.check]
in_ts_g'rev_imf_checkable_val [lemma, in chip.check_seq]
in_ts_g'rev_checkable_imf [lemma, in chip.check_seq]
in_enums_disjoint [lemma, in chip.tarjan_acyclic]
in_uniq_enums [lemma, in chip.tarjan_acyclic]
in_flatten [lemma, in chip.acyclic]
in_succs_ts [lemma, in chip.finn]
irr [lemma, in chip.ordtype]
irr_tt [lemma, in chip.ordtype]
irr_ords [lemma, in chip.ordtype]
irr_ordf [lemma, in chip.ordtype]
irr_lex [lemma, in chip.ordtype]
irr_ltn_nat [lemma, in chip.ordtype]
is_subscc1 [lemma, in chip.tarjan]
is_subscc_in_scc [lemma, in chip.tarjan]
is_subscc [definition, in chip.tarjan]
K
kosaraju [definition, in chip.kosaraju]Kosaraju [section, in chip.kosaraju]
kosaraju [library]
KosarajuAcyclicity [section, in chip.kosaraju_acyclic]
KosarajuAcyclicity.successors [variable, in chip.kosaraju_acyclic]
KosarajuAcyclicity.V [variable, in chip.kosaraju_acyclic]
kosaraju_correct [lemma, in chip.kosaraju]
kosaraju_acyclicP [lemma, in chip.kosaraju_acyclic]
kosaraju_acyclic [definition, in chip.kosaraju_acyclic]
kosaraju_acyclic [library]
Kosaraju.Pdfs [section, in chip.kosaraju]
Kosaraju.Pdfs.successors [variable, in chip.kosaraju]
_ =[]= _ [notation, in chip.kosaraju]
_ =[ _ ]= _ [notation, in chip.kosaraju]
_ -[]-> _ [notation, in chip.kosaraju]
_ -[ _ ]-> _ [notation, in chip.kosaraju]
TS[ _ ] [notation, in chip.kosaraju]
TS[ _ , _ ] [notation, in chip.kosaraju]
Kosaraju.Program [section, in chip.kosaraju]
Kosaraju.Program.r [variable, in chip.kosaraju]
Kosaraju.Stack [section, in chip.kosaraju]
Kosaraju.Stack.r [variable, in chip.kosaraju]
_ =[]= _ [notation, in chip.kosaraju]
_ =[ _ ]= _ [notation, in chip.kosaraju]
_ -[]-> _ [notation, in chip.kosaraju]
_ -[ _ ]-> _ [notation, in chip.kosaraju]
TS[ _ ] [notation, in chip.kosaraju]
TS[ _ , _ ] [notation, in chip.kosaraju]
Kosaraju.T [variable, in chip.kosaraju]
L
last_drop [lemma, in chip.extra]last_take [lemma, in chip.extra]
Lemmas [section, in chip.ordtype]
Lemmas.T [variable, in chip.ordtype]
leq_index_nth [lemma, in chip.connect]
lex [definition, in chip.ordtype]
ltn_mod2r [lemma, in chip.extra]
ltn_div2r [lemma, in chip.extra]
ltn_mod2r [lemma, in chip.tarjan]
ltn_div2r [lemma, in chip.tarjan]
lt_m_bot_pred [definition, in chip.finn]
lt_m_top_pred [definition, in chip.finn]
lt_m_pred [definition, in chip.finn]
M
m [abbreviation, in chip.finn]mem_can_to [lemma, in chip.connect]
mem_scc [lemma, in chip.tarjan]
modifiedV [definition, in chip.check]
modifiedV_sub_modifiedV_eq [lemma, in chip.hierarchical_sub]
modifiedV_pmodified_sub_V [lemma, in chip.hierarchical_sub]
modifiedV_sub [definition, in chip.hierarchical_sub]
mono [record, in chip.ordtype]
Mono [constructor, in chip.ordtype]
Mono [section, in chip.ordtype]
Mono.A [variable, in chip.ordtype]
Mono.B [variable, in chip.ordtype]
m_bot [abbreviation, in chip.finn]
m_top [abbreviation, in chip.finn]
N
NatOrd [section, in chip.ordtype]nat_ordMixin [definition, in chip.ordtype]
neq_connect_in_pimpacted_V [lemma, in chip.hierarchical]
noblack_to_white [definition, in chip.tarjan]
non_impacted_rel [lemma, in chip.check_seq]
non_singleton_cycle [lemma, in chip.acyclic]
non_singleton_neq [lemma, in chip.acyclic]
not_impactedP [lemma, in chip.check]
not_modifiedP [lemma, in chip.check]
nsym [lemma, in chip.ordtype]
O
OFOT5 [module, in chip.dfs_set]OFT5 [module, in chip.dfs_set]
OFT5.n [definition, in chip.dfs_set]
OFT5.T [definition, in chip.dfs_set]
oleq [definition, in chip.ordtype]
Ordered [module, in chip.ordtype]
Ordered.base [projection, in chip.ordtype]
Ordered.class [definition, in chip.ordtype]
Ordered.Class [constructor, in chip.ordtype]
Ordered.ClassDef [section, in chip.ordtype]
Ordered.ClassDef.cT [variable, in chip.ordtype]
Ordered.ClassDef.T [variable, in chip.ordtype]
Ordered.class_of [record, in chip.ordtype]
Ordered.clone [definition, in chip.ordtype]
Ordered.eqType [definition, in chip.ordtype]
Ordered.Exports [module, in chip.ordtype]
Ordered.Exports.ord [definition, in chip.ordtype]
Ordered.Exports.OrdMixin [abbreviation, in chip.ordtype]
Ordered.Exports.OrdType [abbreviation, in chip.ordtype]
Ordered.Exports.ordType [abbreviation, in chip.ordtype]
[ ordType of _ ] (form_scope) [notation, in chip.ordtype]
[ ordType of _ for _ ] (form_scope) [notation, in chip.ordtype]
Ordered.mixin [projection, in chip.ordtype]
Ordered.Mixin [constructor, in chip.ordtype]
Ordered.mixin_of [record, in chip.ordtype]
Ordered.ordering [projection, in chip.ordtype]
Ordered.pack [definition, in chip.ordtype]
Ordered.Pack [constructor, in chip.ordtype]
Ordered.RawMixin [section, in chip.ordtype]
Ordered.sort [projection, in chip.ordtype]
Ordered.type [record, in chip.ordtype]
ordf [definition, in chip.ordtype]
OrdinalFinOrdType [module, in chip.dfs_set]
OrdinalFinOrdType.irr_ordT [definition, in chip.dfs_set]
OrdinalFinOrdType.ordT [definition, in chip.dfs_set]
OrdinalFinOrdType.total_ordT [definition, in chip.dfs_set]
OrdinalFinOrdType.trans_ordT [definition, in chip.dfs_set]
OrdinalFinType [module, in chip.dfs_set]
OrdinalFinType.n [axiom, in chip.dfs_set]
OrdinalFinType.T [definition, in chip.dfs_set]
OrdinalsCheckableImpacted [module, in chip.finn_set]
OrdinalsCheckableImpacted.A [abbreviation, in chip.finn_set]
OrdinalsCheckableImpacted.Finn [section, in chip.finn_set]
OrdinalsCheckableImpacted.Finn.checkable' [variable, in chip.finn_set]
OrdinalsCheckableImpacted.Finn.f [variable, in chip.finn_set]
OrdinalsCheckableImpacted.Finn.f_equal_g [variable, in chip.finn_set]
OrdinalsCheckableImpacted.Finn.f' [variable, in chip.finn_set]
OrdinalsCheckableImpacted.Finn.g [variable, in chip.finn_set]
OrdinalsCheckableImpacted.Finn.g_grev [variable, in chip.finn_set]
OrdinalsCheckableImpacted.Finn.g' [variable, in chip.finn_set]
OrdinalsCheckableImpacted.Finn.g'_acyclic [variable, in chip.finn_set]
OrdinalsCheckableImpacted.Finn.g'_g'rev [variable, in chip.finn_set]
OrdinalsCheckableImpacted.Finn.successors [variable, in chip.finn_set]
OrdinalsCheckableImpacted.Finn.successors' [variable, in chip.finn_set]
OrdinalsCheckableImpacted.gV' [abbreviation, in chip.finn_set]
OrdinalsCheckableImpacted.in_succs_ts [lemma, in chip.finn_set]
OrdinalsCheckableImpacted.lt_m_pred [definition, in chip.finn_set]
OrdinalsCheckableImpacted.succs_tseq_before [lemma, in chip.finn_set]
OrdinalsCheckableImpacted.succs_ts_in [lemma, in chip.finn_set]
OrdinalsCheckableImpacted.succs_ts_uniq [lemma, in chip.finn_set]
OrdinalsCheckableImpacted.succs_checkable_impacted_fresh_uniq [lemma, in chip.finn_set]
OrdinalsCheckableImpacted.succs_impacted_fresh_uniq [lemma, in chip.finn_set]
OrdinalsCheckableImpacted.succs_checkable_impacted_fresh_eq [lemma, in chip.finn_set]
OrdinalsCheckableImpacted.succs_impacted_fresh_eq [lemma, in chip.finn_set]
OrdinalsCheckableImpacted.succs_ts [definition, in chip.finn_set]
OrdinalsCheckableImpacted.succs_checkable_impacted_fresh [definition, in chip.finn_set]
OrdinalsCheckableImpacted.succs_impacted_fresh [definition, in chip.finn_set]
OrdinalsCheckableImpacted.succs_checkable_impacted [definition, in chip.finn_set]
OrdinalsCheckableImpacted.succs_closure_uniq [definition, in chip.finn_set]
OrdinalsCheckableImpacted.succs_closureP [definition, in chip.finn_set]
OrdinalsCheckableImpacted.succs_closure [definition, in chip.finn_set]
OrdinalsCheckableImpacted.V [abbreviation, in chip.finn_set]
OrdinalsCheckableImpacted.VDFS [module, in chip.finn_set]
OrdinalsCheckableImpacted.VFinOrdType [module, in chip.finn_set]
OrdinalsCheckableImpacted.VFinOrdType.irr_ordT [definition, in chip.finn_set]
OrdinalsCheckableImpacted.VFinOrdType.ordT [definition, in chip.finn_set]
OrdinalsCheckableImpacted.VFinOrdType.total_ordT [definition, in chip.finn_set]
OrdinalsCheckableImpacted.VFinOrdType.trans_ordT [definition, in chip.finn_set]
OrdinalsCheckableImpacted.VFinOrdUsualOrderedType [module, in chip.finn_set]
OrdinalsCheckableImpacted.VFinType [module, in chip.finn_set]
OrdinalsCheckableImpacted.VFinType.T [definition, in chip.finn_set]
OrdinalsCheckableImpacted.VRBSet [module, in chip.finn_set]
OrdinalsCheckableImpacted.V' [abbreviation, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted [module, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.A_bot [abbreviation, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.A_top [abbreviation, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical [section, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.checkable'_bot [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.f_top_partition [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.f_top_bot_ps [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.f_bot [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.f_top [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.f'_bot [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.f'_top [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.g_bot_top_ps [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.g_bot_grev [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.g_bot [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.g_top_grev [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.g_top [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.p [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.ps [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.ps_neq [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.ps_partition [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.ps' [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.ps'_neq [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.ps'_partition [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.p_uniq [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.p_ps_eq [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.p' [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.p'_uniq [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.p'_ps'_eq [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.successors_bot [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.successors_top [variable, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.m_bot [abbreviation, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.m_top [abbreviation, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.n_bot [abbreviation, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.n_top [abbreviation, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.P_bot [abbreviation, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.P_top [abbreviation, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_checkable_impacted_fresh_sub_pt_uniq [lemma, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_impacted_fresh_sub_pt_uniq [lemma, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_checkable_impacted_fresh_sub_uniq [lemma, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_impacted_fresh_sub_uniq [lemma, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_checkable_impacted_fresh_sub_pt_eq [lemma, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_impacted_fresh_sub_pt_eq [lemma, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_checkable_impacted_fresh_sub_eq [lemma, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_impacted_fresh_sub_eq [lemma, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_checkable_impacted_fresh_sub_pt [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_impacted_fresh_sub_pt [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_checkable_impacted_fresh_sub [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_impacted_fresh_sub [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_modified_sub [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.U [abbreviation, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UDFS [module, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinOrdType [module, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinOrdType.irr_ordT [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinOrdType.ordT [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinOrdType.total_ordT [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinOrdType.trans_ordT [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinOrdUsualOrderedType [module, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinType [module, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinType.T [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.USet [module, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.U' [abbreviation, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.V [abbreviation, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VDFS [module, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinOrdType [module, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinOrdType.irr_ordT [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinOrdType.ordT [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinOrdType.total_ordT [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinOrdType.trans_ordT [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinOrdUsualOrderedType [module, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinType [module, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinType.T [definition, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VSet [module, in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.V' [abbreviation, in chip.finn_set]
OrdinalsType [module, in chip.finn_set]
OrdinalsType.H_mn [axiom, in chip.finn_set]
OrdinalsType.m [abbreviation, in chip.finn_set]
OrdinalsType.m' [axiom, in chip.finn_set]
OrdinalsType.n [axiom, in chip.finn_set]
ordinal_ordMixin [definition, in chip.ordtype]
ords [definition, in chip.ordtype]
OrdType [module, in chip.dfs_set]
ordtype [library]
OrdTypeUsualOrderedType [module, in chip.dfs_set]
OrdTypeUsualOrderedType.compare [definition, in chip.dfs_set]
OrdTypeUsualOrderedType.compare_spec [lemma, in chip.dfs_set]
OrdTypeUsualOrderedType.eq [definition, in chip.dfs_set]
OrdTypeUsualOrderedType.eq_dec [definition, in chip.dfs_set]
OrdTypeUsualOrderedType.eq_equiv [definition, in chip.dfs_set]
OrdTypeUsualOrderedType.lt [definition, in chip.dfs_set]
OrdTypeUsualOrderedType.lt_compat [lemma, in chip.dfs_set]
OrdTypeUsualOrderedType.lt_strorder [lemma, in chip.dfs_set]
OrdTypeUsualOrderedType.t [definition, in chip.dfs_set]
OrdType.T [axiom, in chip.dfs_set]
Other [section, in chip.change]
Other [section, in chip.check]
Other.A [variable, in chip.change]
Other.A [variable, in chip.check]
Other.check [variable, in chip.change]
Other.check [variable, in chip.check]
Other.checkable [variable, in chip.change]
Other.checkable [variable, in chip.check]
Other.checkable_V_V' [variable, in chip.change]
Other.checkable' [variable, in chip.change]
Other.check_V_V' [variable, in chip.change]
Other.check' [variable, in chip.change]
Other.f [variable, in chip.change]
Other.f [variable, in chip.check]
Other.f_equal_g1 [variable, in chip.change]
Other.f' [variable, in chip.change]
Other.f' [variable, in chip.check]
Other.g' [variable, in chip.change]
Other.g1 [variable, in chip.change]
Other.g1 [variable, in chip.check]
Other.g1_g2_connect [variable, in chip.change]
Other.g1_g2_connect [variable, in chip.check]
Other.g2 [variable, in chip.change]
Other.g2 [variable, in chip.check]
Other.P [variable, in chip.change]
Other.P [variable, in chip.check]
Other.R [variable, in chip.change]
Other.R [variable, in chip.check]
Other.V_result_cert_uniq [variable, in chip.change]
Other.V_result_certP [variable, in chip.change]
Other.V_result_cert [variable, in chip.change]
Other.V' [variable, in chip.change]
Other.V' [variable, in chip.check]
otrans [lemma, in chip.ordtype]
P
path_from [lemma, in chip.extra]path_to [lemma, in chip.extra]
path_xset_xedge [lemma, in chip.tarjan]
path_last [lemma, in chip.ordtype]
pdfs [definition, in chip.kosaraju]
pdfs_subset [lemma, in chip.topos]
pdfs_uniq [lemma, in chip.topos]
pdfs_connect [lemma, in chip.kosaraju]
pdfs_correct [lemma, in chip.kosaraju]
pdfs_connect' [lemma, in chip.kosaraju]
pdfs_correct' [lemma, in chip.kosaraju]
pfreshV' [definition, in chip.hierarchical_sub_pt]
pfreshV'_in_freshV' [lemma, in chip.hierarchical_sub_pt]
pimf [definition, in chip.check_seq]
pimpacted_V'_impactedV' [lemma, in chip.hierarchical]
pimpacted_V'_impactedVV' [lemma, in chip.hierarchical]
pimpacted_V'_fresh [lemma, in chip.hierarchical]
pimpacted_V' [definition, in chip.hierarchical]
pimpacted_V [definition, in chip.hierarchical]
pimpacted_sub_V [definition, in chip.hierarchical_sub]
pmodified_sub_V [definition, in chip.hierarchical_sub]
post_dfs [definition, in chip.tarjan]
PreDfs [constructor, in chip.tarjan]
pre_dfs_subroots [lemma, in chip.tarjan]
pre_sccs [projection, in chip.tarjan]
pre_wf_graph [projection, in chip.tarjan]
pre_wf_env [projection, in chip.tarjan]
pre_access_to [projection, in chip.tarjan]
pre_dfs [record, in chip.tarjan]
ProdOrd [section, in chip.ordtype]
ProdOrd.K [variable, in chip.ordtype]
ProdOrd.T [variable, in chip.ordtype]
prod_ordMixin [definition, in chip.ordtype]
P_V_sub_V_seq_sub_eq [lemma, in chip.check_seq_hierarchical]
P_V_seq_sub [definition, in chip.check_seq_hierarchical]
P_V_sub [definition, in chip.hierarchical_sub]
R
rank [definition, in chip.tarjan]rankE [lemma, in chip.tarjan]
rank_of_reachable [definition, in chip.tarjan]
rank_le_head [lemma, in chip.tarjan]
rank_mem [lemma, in chip.tarjan]
rank_infty [lemma, in chip.tarjan]
rank_lt [lemma, in chip.tarjan]
rank_le [lemma, in chip.tarjan]
rank_small [lemma, in chip.tarjan]
rank_catr [lemma, in chip.tarjan]
rank_catl [lemma, in chip.tarjan]
rank_cons [lemma, in chip.tarjan]
RBDFS5 [module, in chip.dfs_set]
RBSet5 [module, in chip.dfs_set]
rclosed [definition, in chip.close_dfs]
rclosed_rclosure' [lemma, in chip.close_dfs]
rclosed_rclosure [lemma, in chip.close_dfs]
rclosed_connect [lemma, in chip.close_dfs]
rclosed_impacted [lemma, in chip.closure]
rclose_subset [lemma, in chip.close_dfs]
rclosure [definition, in chip.close_dfs]
rclosureP [lemma, in chip.close_dfs]
rclosurePg [lemma, in chip.close_dfs]
rclosures [definition, in chip.close_dfs]
rclosuresP [lemma, in chip.close_dfs]
rclosures_connect [lemma, in chip.close_dfs]
rclosures' [definition, in chip.close_dfs]
rclosures'P [lemma, in chip.close_dfs]
rclosures'_connect [lemma, in chip.close_dfs]
rclosure_uniq [lemma, in chip.close_dfs]
rclosure_rclosure'_i [lemma, in chip.close_dfs]
rclosure_in_rl [lemma, in chip.close_dfs]
rclosure_in_lr [lemma, in chip.close_dfs]
rclosure_exist [lemma, in chip.close_dfs]
rclosure' [definition, in chip.close_dfs]
rclosure'P [lemma, in chip.close_dfs]
rclosure'Pg [lemma, in chip.close_dfs]
rclosure'_uniq [lemma, in chip.close_dfs]
red_pepper [constructor, in chip.closure_example]
relfrom [definition, in chip.extra]
relto [definition, in chip.extra]
reltoI [lemma, in chip.connect]
rigatoni [constructor, in chip.closure_example]
rigatoni_arrabiata [constructor, in chip.closure_example]
rinv [definition, in chip.check]
rpdfs [definition, in chip.kosaraju]
S
sauce [constructor, in chip.closure_example]sccs [projection, in chip.tarjan]
sccs_add_sccs [lemma, in chip.tarjan]
sccs_stackF [lemma, in chip.tarjan]
sccs_acyclicP [lemma, in chip.acyclic]
sccs_acyclic [definition, in chip.acyclic]
scc_of [abbreviation, in chip.tarjan]
self_loop_cycle [lemma, in chip.acyclic]
SeqOrd [section, in chip.ordtype]
SeqOrd.T [variable, in chip.ordtype]
SeqSet [section, in chip.tarjan_acyclic]
SeqSet.all_in_cover [variable, in chip.tarjan_acyclic]
SeqSet.sc [variable, in chip.tarjan_acyclic]
SeqSet.trivIset_sc [variable, in chip.tarjan_acyclic]
SeqSet.V [variable, in chip.tarjan_acyclic]
seq_checkable_impacted_fresh_sub_pt_uniq [lemma, in chip.check_seq_hierarchical]
seq_checkable_impacted_fresh_sub_uniq [lemma, in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_pt_uniq [lemma, in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_uniq [lemma, in chip.check_seq_hierarchical]
seq_freshV'_uniq [lemma, in chip.check_seq_hierarchical]
seq_impactedVV'_sub_uniq [lemma, in chip.check_seq_hierarchical]
seq_impactedV_sub_uniq [lemma, in chip.check_seq_hierarchical]
seq_modifiedV_sub_uniq [lemma, in chip.check_seq_hierarchical]
seq_freshV'_sub_uniq [lemma, in chip.check_seq_hierarchical]
seq_pfreshV'_uniq [lemma, in chip.check_seq_hierarchical]
seq_freshU'_uniq [lemma, in chip.check_seq_hierarchical]
seq_pimpacted_V_uniq [lemma, in chip.check_seq_hierarchical]
seq_pmodified_V_uniq [lemma, in chip.check_seq_hierarchical]
seq_impactedU_uniq [lemma, in chip.check_seq_hierarchical]
seq_modifiedU_uniq [lemma, in chip.check_seq_hierarchical]
seq_checkable_impacted_fresh_sub_pt_correct [lemma, in chip.check_seq_hierarchical]
seq_checkable_impacted_fresh_sub_correct [lemma, in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_pt_correct [lemma, in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_correct [lemma, in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_pt_eq [lemma, in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_eq [lemma, in chip.check_seq_hierarchical]
seq_freshV'_sub_eq [lemma, in chip.check_seq_hierarchical]
seq_impactedVV'_sub_eq [lemma, in chip.check_seq_hierarchical]
seq_modifiedV_sub_eq [lemma, in chip.check_seq_hierarchical]
seq_pfreshV'_eq [lemma, in chip.check_seq_hierarchical]
seq_pimpacted_V_eq [lemma, in chip.check_seq_hierarchical]
seq_freshU'_eq [lemma, in chip.check_seq_hierarchical]
seq_impactedU_eq [lemma, in chip.check_seq_hierarchical]
seq_modifiedU_eq [lemma, in chip.check_seq_hierarchical]
seq_checkable_impacted_fresh_sub_pt [definition, in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_pt [definition, in chip.check_seq_hierarchical]
seq_checkable_impacted_fresh_sub [definition, in chip.check_seq_hierarchical]
seq_impacted_fresh_sub [definition, in chip.check_seq_hierarchical]
seq_freshV'_sub [definition, in chip.check_seq_hierarchical]
seq_freshV' [definition, in chip.check_seq_hierarchical]
seq_impactedVV'_sub [definition, in chip.check_seq_hierarchical]
seq_impactedV_sub [definition, in chip.check_seq_hierarchical]
seq_modifiedV_sub [definition, in chip.check_seq_hierarchical]
seq_pfreshV' [definition, in chip.check_seq_hierarchical]
seq_pimpacted_V [definition, in chip.check_seq_hierarchical]
seq_pmodified_V [definition, in chip.check_seq_hierarchical]
seq_freshU' [definition, in chip.check_seq_hierarchical]
seq_impactedU [definition, in chip.check_seq_hierarchical]
seq_modifiedU [definition, in chip.check_seq_hierarchical]
seq_checkable_impacted_fresh_uniq [lemma, in chip.check_seq]
seq_impacted_fresh_uniq [lemma, in chip.check_seq]
seq_modifiedV_uniq [lemma, in chip.check_seq]
seq_checkable_impacted_fresh_eq [lemma, in chip.check_seq]
seq_impacted_fresh_eq [lemma, in chip.check_seq]
seq_impactedV'_eq [lemma, in chip.check_seq]
seq_freshV'_eq [lemma, in chip.check_seq]
seq_modifiedV_eq [lemma, in chip.check_seq]
seq_checkable_impacted_fresh [definition, in chip.check_seq]
seq_impacted_fresh [definition, in chip.check_seq]
seq_checkable_impacted [definition, in chip.check_seq]
seq_freshV' [definition, in chip.check_seq]
seq_impactedV' [definition, in chip.check_seq]
seq_impactedV [definition, in chip.check_seq]
seq_modifiedV [definition, in chip.check_seq]
seq_last_mono [lemma, in chip.ordtype]
seq_last_in [lemma, in chip.ordtype]
seq_ordMixin [definition, in chip.ordtype]
seq_of_stringK [lemma, in chip.string]
seq_of_string [definition, in chip.string]
set_last_default [lemma, in chip.extra]
sorted_max_key_last [lemma, in chip.ordtype]
sorted_last_key_max [lemma, in chip.ordtype]
sorted_oleq [lemma, in chip.ordtype]
split_after [definition, in chip.tarjan]
stack [projection, in chip.tarjan]
stack_add_sccs [lemma, in chip.tarjan]
stack_add_stack [lemma, in chip.tarjan]
strictly_increasing [definition, in chip.ordtype]
string [library]
string_eqMixin [definition, in chip.string]
string_of_seq [definition, in chip.string]
subltn [definition, in chip.finn_set]
subset_cover [lemma, in chip.extra]
subset_rclose [lemma, in chip.close_dfs]
subset_closure [lemma, in chip.close_dfs]
subset_bigcup [lemma, in chip.tarjan]
sub_freshV' [lemma, in chip.check]
succs_checkable_impacted_fresh_sub_pt_uniq [lemma, in chip.finn]
succs_impacted_fresh_sub_pt_uniq [lemma, in chip.finn]
succs_checkable_impacted_fresh_sub_uniq [lemma, in chip.finn]
succs_impacted_fresh_sub_uniq [lemma, in chip.finn]
succs_checkable_impacted_fresh_sub_pt_eq [lemma, in chip.finn]
succs_impacted_fresh_sub_pt_eq [lemma, in chip.finn]
succs_checkable_impacted_fresh_sub_eq [lemma, in chip.finn]
succs_impacted_fresh_sub_eq [lemma, in chip.finn]
succs_checkable_impacted_fresh_sub_pt [definition, in chip.finn]
succs_impacted_fresh_sub_pt [definition, in chip.finn]
succs_checkable_impacted_fresh_sub [definition, in chip.finn]
succs_impacted_fresh_sub [definition, in chip.finn]
succs_modified_sub [definition, in chip.finn]
succs_tseq_before [lemma, in chip.finn]
succs_ts_in [lemma, in chip.finn]
succs_ts_uniq [lemma, in chip.finn]
succs_checkable_impacted_fresh_uniq [lemma, in chip.finn]
succs_impacted_fresh_uniq [lemma, in chip.finn]
succs_checkable_impacted_fresh_eq [lemma, in chip.finn]
succs_impacted_fresh_eq [lemma, in chip.finn]
succs_ts [definition, in chip.finn]
succs_checkable_impacted_fresh [definition, in chip.finn]
succs_impacted_fresh [definition, in chip.finn]
succs_checkable_impacted [definition, in chip.finn]
succs_modified [definition, in chip.finn]
succs_closure_uniq [definition, in chip.finn]
succs_closureP [definition, in chip.finn]
succs_closure [definition, in chip.finn]
T
take_subseq [lemma, in chip.extra]tarjan [definition, in chip.tarjan]
tarjan [section, in chip.tarjan]
tarjan [library]
TarjanAcyclic [section, in chip.tarjan_acyclic]
TarjanAcyclic.g [variable, in chip.tarjan_acyclic]
TarjanAcyclic.V [variable, in chip.tarjan_acyclic]
tarjans [definition, in chip.tarjan_acyclic]
TarjanSeq [section, in chip.tarjan_acyclic]
TarjanSeq.successors [variable, in chip.tarjan_acyclic]
TarjanSeq.V [variable, in chip.tarjan_acyclic]
tarjansP [lemma, in chip.tarjan_acyclic]
tarjans_acyclicP [lemma, in chip.tarjan_acyclic]
tarjans_acyclic [definition, in chip.tarjan_acyclic]
tarjans' [definition, in chip.tarjan_acyclic]
tarjan_correct [lemma, in chip.tarjan]
tarjan_rec_is_correct [lemma, in chip.tarjan]
tarjan_rec_terminates [lemma, in chip.tarjan]
tarjan_rec [definition, in chip.tarjan]
tarjan_acyclic [library]
tarjan.N [variable, in chip.tarjan]
tarjan.successors [variable, in chip.tarjan]
tarjan.V [variable, in chip.tarjan]
tomato_puree [constructor, in chip.closure_example]
topos [library]
ToposAcyclic [section, in chip.topos]
ToposAcyclic.g [variable, in chip.topos]
ToposAcyclic.g_acyclic [variable, in chip.topos]
ToposAcyclic.ts [variable, in chip.topos]
ToposAcyclic.ts_all [variable, in chip.topos]
ToposAcyclic.ts_tsorted [variable, in chip.topos]
ToposAcyclic.V [variable, in chip.topos]
ToposTseq [section, in chip.topos]
ToposTseqRel [section, in chip.topos]
ToposTseqRel.g [variable, in chip.topos]
ToposTseqRel.g_acyclic [variable, in chip.topos]
ToposTseqRel.V [variable, in chip.topos]
ToposTseq.g_acyclic [variable, in chip.topos]
ToposTseq.successors [variable, in chip.topos]
ToposTseq.V [variable, in chip.topos]
total [lemma, in chip.ordtype]
Totality [section, in chip.ordtype]
Totality.K [variable, in chip.ordtype]
totalP [lemma, in chip.ordtype]
total_tt [lemma, in chip.ordtype]
total_ords [lemma, in chip.ordtype]
total_ordf [lemma, in chip.ordtype]
total_lex [lemma, in chip.ordtype]
total_ltn_nat [lemma, in chip.ordtype]
total_spec_gt [constructor, in chip.ordtype]
total_spec_eq [constructor, in chip.ordtype]
total_spec_lt [constructor, in chip.ordtype]
total_spec [inductive, in chip.ordtype]
trans [lemma, in chip.ordtype]
trans_tt [lemma, in chip.ordtype]
trans_ords [lemma, in chip.ordtype]
trans_ordf [lemma, in chip.ordtype]
trans_lex [lemma, in chip.ordtype]
trans_ltn_nat [lemma, in chip.ordtype]
trivIset_gsccs [lemma, in chip.tarjan]
trivIset_tarjan [lemma, in chip.tarjan_acyclic]
tseq [definition, in chip.kosaraju]
tseq_rgraph_connect_before [lemma, in chip.topos]
tseq_connect_before [lemma, in chip.topos]
tseq_uniq [lemma, in chip.topos]
tseq_all [lemma, in chip.topos]
tseq_sorted [lemma, in chip.topos]
tseq_correct [lemma, in chip.kosaraju]
tseq_correct' [lemma, in chip.kosaraju]
tsorted [definition, in chip.connect]
tsortedE [lemma, in chip.connect]
tsorted_cons_r [lemma, in chip.connect]
tsorted_setU1_l [lemma, in chip.connect]
tsorted_cat [lemma, in chip.connect]
tsorted_diconnect [lemma, in chip.connect]
tsorted_inv [lemma, in chip.connect]
tsorted_nil [lemma, in chip.connect]
ts_connect_before [lemma, in chip.topos]
ts_nth [lemma, in chip.topos]
ts_g'rev_imf_checkable_val_before [lemma, in chip.check_seq]
ts_g'rev_imf_checkable_val_in [lemma, in chip.check_seq]
ts_g'rev_imf_checkable_val_uniq [lemma, in chip.check_seq]
ts_g'rev_imf_checkable_val [definition, in chip.check_seq]
ts_g'rev_imf_checkable_before [lemma, in chip.check_seq]
ts_g'rev_imf_checkable [definition, in chip.check_seq]
ts_g'rev_imf_before [lemma, in chip.check_seq]
ts_g'rev_imf_uniq [lemma, in chip.check_seq]
ts_g'rev_imf_all [lemma, in chip.check_seq]
ts_g'rev_imf [definition, in chip.check_seq]
ts_g'rev_checkable_imf_before [lemma, in chip.check_seq]
ts_g'rev_checkable_imf_in [lemma, in chip.check_seq]
ts_g'rev_checkable_imf_uniq [lemma, in chip.check_seq]
ts_g'rev_checkable_imf [definition, in chip.check_seq]
ts_rev_before [lemma, in chip.check_seq]
ts_g'rev [definition, in chip.check_seq]
U
U [abbreviation, in chip.hierarchical_correct]U [abbreviation, in chip.hierarchical_sub_pt]
U [abbreviation, in chip.check_seq_hierarchical]
U [abbreviation, in chip.hierarchical_sub_correct]
U [abbreviation, in chip.hierarchical]
U [abbreviation, in chip.hierarchical_sub_pt_correct]
U [abbreviation, in chip.hierarchical_sub]
U [abbreviation, in chip.finn]
uniq_prod_eq [lemma, in chip.extra]
uniq_catRL [lemma, in chip.extra]
uniq_catLR [lemma, in chip.extra]
uniq_catRL [lemma, in chip.tarjan]
uniq_catLR [lemma, in chip.tarjan]
uniq_flatten_tarjans [lemma, in chip.tarjan_acyclic]
uniq_in_tarjans [lemma, in chip.tarjan_acyclic]
uniq_flatten [lemma, in chip.tarjan_acyclic]
uniq_enums [lemma, in chip.tarjan_acyclic]
uniq_flatten_kosaraju [lemma, in chip.kosaraju_acyclic]
unitOrd [section, in chip.ordtype]
unitOrd.ordtt [variable, in chip.ordtype]
unitOrd.unit_ordMixin [variable, in chip.ordtype]
U' [abbreviation, in chip.finn]
V
V [abbreviation, in chip.hierarchical_correct]V [abbreviation, in chip.hierarchical_sub_pt]
V [abbreviation, in chip.check_seq_hierarchical]
V [abbreviation, in chip.change]
V [abbreviation, in chip.change]
V [abbreviation, in chip.check_seq]
V [abbreviation, in chip.hierarchical_sub_correct]
V [abbreviation, in chip.hierarchical]
V [abbreviation, in chip.hierarchical_sub_pt_correct]
V [abbreviation, in chip.hierarchical_sub]
V [abbreviation, in chip.check]
V [abbreviation, in chip.check]
V [abbreviation, in chip.finn]
V [abbreviation, in chip.finn]
V_sub [abbreviation, in chip.hierarchical_sub_pt]
V_result_filter_cert_checkable' [lemma, in chip.change]
V_result_cert_sound [lemma, in chip.change]
V_result_cert_complete [lemma, in chip.change]
V_sub [abbreviation, in chip.hierarchical_sub_correct]
V_sub [abbreviation, in chip.hierarchical_sub_pt_correct]
V_sub [abbreviation, in chip.hierarchical_sub]
V' [abbreviation, in chip.finn]
V' [abbreviation, in chip.finn]
V'_result_filter_cert_p [definition, in chip.hierarchical_correct]
V'_result_filter_cert [definition, in chip.change]
V'_imf [abbreviation, in chip.check_seq]
V'_result_filter_cert_sub [definition, in chip.hierarchical_sub_correct]
V'_result_filter_cert_sub_pt [definition, in chip.hierarchical_sub_pt_correct]
W
WfEnv [constructor, in chip.tarjan]WfGraph [constructor, in chip.tarjan]
wf_noblack_towhite [projection, in chip.tarjan]
wf_stack_to_grays [projection, in chip.tarjan]
wf_grays_to_stack [projection, in chip.tarjan]
wf_graph [record, in chip.tarjan]
wf_stack_uniq [projection, in chip.tarjan]
wf_sccs [projection, in chip.tarjan]
wf_stack [projection, in chip.tarjan]
wf_env [record, in chip.tarjan]
whites [definition, in chip.tarjan]
whites_add_sccs [lemma, in chip.tarjan]
whites_add_blacks [lemma, in chip.tarjan]
whites_add_stack [lemma, in chip.tarjan]
whites_graysF [lemma, in chip.tarjan]
whites_stackF [lemma, in chip.tarjan]
whites_blacksF [lemma, in chip.tarjan]
X
xedges [definition, in chip.tarjan]other
_ ^-1 [notation, in chip.check][ fin_ordMixin of _ ] [notation, in chip.ordtype]
Notation Index
F
_ =[ _ ]< _ [in chip.connect]_ =[ _ ]= _ [in chip.connect]
_ =[]= _ [in chip.connect]
_ -[]-> _ [in chip.connect]
_ -[ _ ]-> _ [in chip.connect]
C[ _ ]_( _ , _ ) [in chip.connect]
TS[ _ ] [in chip.connect]
TS[ _ , _ ] [in chip.connect]
_ -[]-> _ [in chip.connect]
_ =[ _ ]< _ [in chip.connect]
_ =[ _ ]= _ [in chip.connect]
_ =[]= _ [in chip.connect]
_ -[]-> _ [in chip.connect]
_ -[ _ ]-> _ [in chip.connect]
C[ _ ]_( _ , _ ) [in chip.connect]
K
_ =[]= _ [in chip.kosaraju]_ =[ _ ]= _ [in chip.kosaraju]
_ -[]-> _ [in chip.kosaraju]
_ -[ _ ]-> _ [in chip.kosaraju]
TS[ _ ] [in chip.kosaraju]
TS[ _ , _ ] [in chip.kosaraju]
_ =[]= _ [in chip.kosaraju]
_ =[ _ ]= _ [in chip.kosaraju]
_ -[]-> _ [in chip.kosaraju]
_ -[ _ ]-> _ [in chip.kosaraju]
TS[ _ ] [in chip.kosaraju]
TS[ _ , _ ] [in chip.kosaraju]
O
[ ordType of _ ] (form_scope) [in chip.ordtype][ ordType of _ for _ ] (form_scope) [in chip.ordtype]
other
_ ^-1 [in chip.check][ fin_ordMixin of _ ] [in chip.ordtype]
Module Index
D
DFS [in chip.dfs_set]DFS.MSF [in chip.dfs_set]
F
FinOrdType [in chip.dfs_set]FinOrdUsualOrderedType [in chip.dfs_set]
FinOrdUsualOrderedType.OT [in chip.dfs_set]
FinOrdUsualOrderedType.OTUOT [in chip.dfs_set]
FinType [in chip.dfs_set]
FinUsualOrderedType [in chip.dfs_set]
FUOT5 [in chip.dfs_set]
O
OFOT5 [in chip.dfs_set]OFT5 [in chip.dfs_set]
Ordered [in chip.ordtype]
Ordered.Exports [in chip.ordtype]
OrdinalFinOrdType [in chip.dfs_set]
OrdinalFinType [in chip.dfs_set]
OrdinalsCheckableImpacted [in chip.finn_set]
OrdinalsCheckableImpacted.VDFS [in chip.finn_set]
OrdinalsCheckableImpacted.VFinOrdType [in chip.finn_set]
OrdinalsCheckableImpacted.VFinOrdUsualOrderedType [in chip.finn_set]
OrdinalsCheckableImpacted.VFinType [in chip.finn_set]
OrdinalsCheckableImpacted.VRBSet [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UDFS [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinOrdType [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinOrdUsualOrderedType [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinType [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.USet [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VDFS [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinOrdType [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinOrdUsualOrderedType [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinType [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VSet [in chip.finn_set]
OrdinalsType [in chip.finn_set]
OrdType [in chip.dfs_set]
OrdTypeUsualOrderedType [in chip.dfs_set]
R
RBDFS5 [in chip.dfs_set]RBSet5 [in chip.dfs_set]
Variable Index
A
Acyclicity.all_in_flatten [in chip.acyclic]Acyclicity.class_diconnected [in chip.acyclic]
Acyclicity.g [in chip.acyclic]
Acyclicity.sccs [in chip.acyclic]
Acyclicity.uniq_flatten [in chip.acyclic]
Acyclicity.V [in chip.acyclic]
AcyclicRev.g [in chip.acyclic]
AcyclicRev.g_acyclic [in chip.acyclic]
AcyclicRev.V [in chip.acyclic]
AcyclicSub.g [in chip.acyclic]
AcyclicSub.g_acyclic [in chip.acyclic]
AcyclicSub.P [in chip.acyclic]
AcyclicSub.V [in chip.acyclic]
Acyclic.g [in chip.acyclic]
Acyclic.g_acyclic [in chip.acyclic]
Acyclic.V [in chip.acyclic]
C
ChangedHierarchicalSubPt.A_bot [in chip.hierarchical_sub_pt_correct]ChangedHierarchicalSubPt.A_top [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.check [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.checkable [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.checkable_bot [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.checkable' [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.check_bot [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.check' [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f_bot_equal_g_bot [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f_top_equal_g_top [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f_top_partition [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f_top_bot [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f_bot [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f_top [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f'_bot [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.f'_top [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.g_bot_top [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.g_bot [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.g_top [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.g'_bot [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.g'_top [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.p [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.p_partition [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.p_neq [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.P_bot [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.P_top [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.p' [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.p'_partition [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.p'_neq [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.R [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.U' [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.V_result_cert_uniq [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.V_result_certP [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.V_result_cert [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSubPt.V' [in chip.hierarchical_sub_pt_correct]
ChangedHierarchicalSub.A_bot [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.A_top [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.check [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.checkable [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.checkable_bot [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.checkable' [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.check_bot [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.check' [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f_bot_equal_g_bot [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f_top_equal_g_top [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f_top_bot [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f_bot [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f_top [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f'_bot [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.f'_top [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.g_bot_top [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.g_bot [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.g_top [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.g'_bot [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.g'_top [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.p [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.p_partition [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.p_neq [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.P_bot [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.P_top [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.p' [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.p'_partition [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.p'_neq [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.R [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.U' [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.V_result_cert_uniq [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.V_result_certP [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.V_result_cert [in chip.hierarchical_sub_correct]
ChangedHierarchicalSub.V' [in chip.hierarchical_sub_correct]
ChangedHierarchical.A_bot [in chip.hierarchical_correct]
ChangedHierarchical.A_top [in chip.hierarchical_correct]
ChangedHierarchical.check [in chip.hierarchical_correct]
ChangedHierarchical.checkable [in chip.hierarchical_correct]
ChangedHierarchical.checkable_bot [in chip.hierarchical_correct]
ChangedHierarchical.checkable' [in chip.hierarchical_correct]
ChangedHierarchical.check_bot [in chip.hierarchical_correct]
ChangedHierarchical.check' [in chip.hierarchical_correct]
ChangedHierarchical.f_bot_equal_g_bot [in chip.hierarchical_correct]
ChangedHierarchical.f_top_equal_g_top [in chip.hierarchical_correct]
ChangedHierarchical.f_top_bot [in chip.hierarchical_correct]
ChangedHierarchical.f_top_partition [in chip.hierarchical_correct]
ChangedHierarchical.f_bot [in chip.hierarchical_correct]
ChangedHierarchical.f_top [in chip.hierarchical_correct]
ChangedHierarchical.f'_bot [in chip.hierarchical_correct]
ChangedHierarchical.f'_top [in chip.hierarchical_correct]
ChangedHierarchical.g_bot_top [in chip.hierarchical_correct]
ChangedHierarchical.g_bot [in chip.hierarchical_correct]
ChangedHierarchical.g_top [in chip.hierarchical_correct]
ChangedHierarchical.g'_bot [in chip.hierarchical_correct]
ChangedHierarchical.g'_top [in chip.hierarchical_correct]
ChangedHierarchical.p [in chip.hierarchical_correct]
ChangedHierarchical.p_partition [in chip.hierarchical_correct]
ChangedHierarchical.p_neq [in chip.hierarchical_correct]
ChangedHierarchical.P_bot [in chip.hierarchical_correct]
ChangedHierarchical.P_top [in chip.hierarchical_correct]
ChangedHierarchical.p' [in chip.hierarchical_correct]
ChangedHierarchical.p'_partition [in chip.hierarchical_correct]
ChangedHierarchical.p'_neq [in chip.hierarchical_correct]
ChangedHierarchical.R [in chip.hierarchical_correct]
ChangedHierarchical.U' [in chip.hierarchical_correct]
ChangedHierarchical.V_result_cert_uniq [in chip.hierarchical_correct]
ChangedHierarchical.V_result_certP [in chip.hierarchical_correct]
ChangedHierarchical.V_result_cert [in chip.hierarchical_correct]
ChangedHierarchical.V' [in chip.hierarchical_correct]
Changed.A [in chip.change]
Changed.check [in chip.change]
Changed.checkable [in chip.change]
Changed.checkable_V_V' [in chip.change]
Changed.checkable' [in chip.change]
Changed.check_V_V' [in chip.change]
Changed.check' [in chip.change]
Changed.f [in chip.change]
Changed.f_equal_g [in chip.change]
Changed.f' [in chip.change]
Changed.g [in chip.change]
Changed.g' [in chip.change]
Changed.P [in chip.change]
Changed.R [in chip.change]
Changed.V_result_cert_uniq [in chip.change]
Changed.V_result_certP [in chip.change]
Changed.V_result_cert [in chip.change]
Changed.V' [in chip.change]
CheckedSeqHierarchical.A_bot [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.A_top [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.checkable'_bot [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.clos_bot_uniq [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.clos_top_uniq [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.clos_botP [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.clos_bot [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.clos_topP [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.clos_top [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.f_top_partition [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.f_top_bot_ps [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.f_bot [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.f_top [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.f'_bot [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.f'_top [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_bot_top_ps [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_bot_grev [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_bot [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_top_grev [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_top [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_bot_rev [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.g_top_rev [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.p [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.ps [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.ps_neq [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.ps_partition [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.ps' [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.ps'_neq [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.ps'_partition [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.p_uniq [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.p_ps_eq [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.P_bot [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.P_top [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.p' [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.p'_uniq [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.p'_ps'_eq [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.U' [in chip.check_seq_hierarchical]
CheckedSeqHierarchical.V' [in chip.check_seq_hierarchical]
CheckedSeq.A [in chip.check_seq]
CheckedSeq.checkable' [in chip.check_seq]
CheckedSeq.clos [in chip.check_seq]
CheckedSeq.closP [in chip.check_seq]
CheckedSeq.clos_uniq [in chip.check_seq]
CheckedSeq.f [in chip.check_seq]
CheckedSeq.f_equal_g [in chip.check_seq]
CheckedSeq.f' [in chip.check_seq]
CheckedSeq.g [in chip.check_seq]
CheckedSeq.grev [in chip.check_seq]
CheckedSeq.g_grev [in chip.check_seq]
CheckedSeq.g' [in chip.check_seq]
CheckedSeq.g'rev [in chip.check_seq]
CheckedSeq.g'_g'rev [in chip.check_seq]
CheckedSeq.g'_acyclic [in chip.check_seq]
CheckedSeq.P [in chip.check_seq]
CheckedSeq.ts [in chip.check_seq]
CheckedSeq.ts_uniq [in chip.check_seq]
CheckedSeq.ts_all [in chip.check_seq]
CheckedSeq.ts_tsorted [in chip.check_seq]
CheckedSeq.V' [in chip.check_seq]
Checked.A [in chip.check]
Checked.check [in chip.check]
Checked.checkable [in chip.check]
Checked.f [in chip.check]
Checked.f' [in chip.check]
Checked.g [in chip.check]
Checked.P [in chip.check]
Checked.R [in chip.check]
Checked.V' [in chip.check]
Closure.g [in chip.closure]
Closure.modified [in chip.closure]
Closure.V [in chip.closure]
Cycles.g [in chip.acyclic]
Cycles.V [in chip.acyclic]
D
DFSearch.T [in chip.close_dfs]E
extra_path.V [in chip.extra]F
FinnHierarchical.checkable'_bot [in chip.finn]FinnHierarchical.f_top_partition [in chip.finn]
FinnHierarchical.f_top_bot_ps [in chip.finn]
FinnHierarchical.f_bot [in chip.finn]
FinnHierarchical.f_top [in chip.finn]
FinnHierarchical.f'_bot [in chip.finn]
FinnHierarchical.f'_top [in chip.finn]
FinnHierarchical.g_bot_top_ps [in chip.finn]
FinnHierarchical.g_bot_grev [in chip.finn]
FinnHierarchical.g_bot [in chip.finn]
FinnHierarchical.g_top_grev [in chip.finn]
FinnHierarchical.g_top [in chip.finn]
FinnHierarchical.H_mn_bot [in chip.finn]
FinnHierarchical.H_mn_top [in chip.finn]
FinnHierarchical.m'_bot [in chip.finn]
FinnHierarchical.m'_top [in chip.finn]
FinnHierarchical.n_bot [in chip.finn]
FinnHierarchical.n_top [in chip.finn]
FinnHierarchical.p [in chip.finn]
FinnHierarchical.ps [in chip.finn]
FinnHierarchical.ps_neq [in chip.finn]
FinnHierarchical.ps_partition [in chip.finn]
FinnHierarchical.ps' [in chip.finn]
FinnHierarchical.ps'_neq [in chip.finn]
FinnHierarchical.ps'_partition [in chip.finn]
FinnHierarchical.p_uniq [in chip.finn]
FinnHierarchical.p_ps_eq [in chip.finn]
FinnHierarchical.p' [in chip.finn]
FinnHierarchical.p'_uniq [in chip.finn]
FinnHierarchical.p'_ps'_eq [in chip.finn]
FinnHierarchical.successors_bot [in chip.finn]
FinnHierarchical.successors_top [in chip.finn]
Finn.checkable' [in chip.finn]
Finn.f [in chip.finn]
Finn.f_equal_g [in chip.finn]
Finn.f' [in chip.finn]
Finn.g [in chip.finn]
Finn.g_grev [in chip.finn]
Finn.g' [in chip.finn]
Finn.g'_acyclic [in chip.finn]
Finn.g'_g'rev [in chip.finn]
Finn.H_mn [in chip.finn]
Finn.m' [in chip.finn]
Finn.n [in chip.finn]
Finn.successors [in chip.finn]
Finn.successors' [in chip.finn]
FinTypeOrd.T [in chip.ordtype]
Fin.ConnectRelto.g [in chip.connect]
Fin.Diconnect.g [in chip.connect]
Fin.Relto.g [in chip.connect]
Fin.Sub.g [in chip.connect]
Fin.Sub.P [in chip.connect]
Fin.V [in chip.connect]
H
HierarchicalSubPt.A_bot [in chip.hierarchical_sub_pt]HierarchicalSubPt.A_top [in chip.hierarchical_sub_pt]
HierarchicalSubPt.check [in chip.hierarchical_sub_pt]
HierarchicalSubPt.checkable [in chip.hierarchical_sub_pt]
HierarchicalSubPt.f_top_partition [in chip.hierarchical_sub_pt]
HierarchicalSubPt.f_top_bot [in chip.hierarchical_sub_pt]
HierarchicalSubPt.f_bot [in chip.hierarchical_sub_pt]
HierarchicalSubPt.f_top [in chip.hierarchical_sub_pt]
HierarchicalSubPt.f'_bot [in chip.hierarchical_sub_pt]
HierarchicalSubPt.f'_top [in chip.hierarchical_sub_pt]
HierarchicalSubPt.g_bot_top [in chip.hierarchical_sub_pt]
HierarchicalSubPt.g_bot [in chip.hierarchical_sub_pt]
HierarchicalSubPt.g_top [in chip.hierarchical_sub_pt]
HierarchicalSubPt.p [in chip.hierarchical_sub_pt]
HierarchicalSubPt.p_partition [in chip.hierarchical_sub_pt]
HierarchicalSubPt.p_neq [in chip.hierarchical_sub_pt]
HierarchicalSubPt.P_bot [in chip.hierarchical_sub_pt]
HierarchicalSubPt.P_top [in chip.hierarchical_sub_pt]
HierarchicalSubPt.p' [in chip.hierarchical_sub_pt]
HierarchicalSubPt.p'_partition [in chip.hierarchical_sub_pt]
HierarchicalSubPt.R [in chip.hierarchical_sub_pt]
HierarchicalSubPt.U' [in chip.hierarchical_sub_pt]
HierarchicalSubPt.V' [in chip.hierarchical_sub_pt]
HierarchicalSub.A_bot [in chip.hierarchical_sub]
HierarchicalSub.A_top [in chip.hierarchical_sub]
HierarchicalSub.check [in chip.hierarchical_sub]
HierarchicalSub.checkable [in chip.hierarchical_sub]
HierarchicalSub.f_top_bot [in chip.hierarchical_sub]
HierarchicalSub.f_bot [in chip.hierarchical_sub]
HierarchicalSub.f_top [in chip.hierarchical_sub]
HierarchicalSub.f'_bot [in chip.hierarchical_sub]
HierarchicalSub.f'_top [in chip.hierarchical_sub]
HierarchicalSub.g_bot_top [in chip.hierarchical_sub]
HierarchicalSub.g_bot [in chip.hierarchical_sub]
HierarchicalSub.g_top [in chip.hierarchical_sub]
HierarchicalSub.p [in chip.hierarchical_sub]
HierarchicalSub.p_partition [in chip.hierarchical_sub]
HierarchicalSub.p_neq [in chip.hierarchical_sub]
HierarchicalSub.P_bot [in chip.hierarchical_sub]
HierarchicalSub.P_top [in chip.hierarchical_sub]
HierarchicalSub.R [in chip.hierarchical_sub]
HierarchicalSub.U' [in chip.hierarchical_sub]
HierarchicalSub.V' [in chip.hierarchical_sub]
Hierarchy.A_bot [in chip.hierarchical]
Hierarchy.A_top [in chip.hierarchical]
Hierarchy.check [in chip.hierarchical]
Hierarchy.checkable [in chip.hierarchical]
Hierarchy.f_top_bot [in chip.hierarchical]
Hierarchy.f_top_partition [in chip.hierarchical]
Hierarchy.f_bot [in chip.hierarchical]
Hierarchy.f_top [in chip.hierarchical]
Hierarchy.f'_bot [in chip.hierarchical]
Hierarchy.f'_top [in chip.hierarchical]
Hierarchy.g_bot_top [in chip.hierarchical]
Hierarchy.g_bot [in chip.hierarchical]
Hierarchy.g_top [in chip.hierarchical]
Hierarchy.p [in chip.hierarchical]
Hierarchy.p_partition [in chip.hierarchical]
Hierarchy.p_neq [in chip.hierarchical]
Hierarchy.P_bot [in chip.hierarchical]
Hierarchy.P_top [in chip.hierarchical]
Hierarchy.p' [in chip.hierarchical]
Hierarchy.p'_partition [in chip.hierarchical]
Hierarchy.p'_neq [in chip.hierarchical]
Hierarchy.R [in chip.hierarchical]
Hierarchy.U' [in chip.hierarchical]
Hierarchy.V' [in chip.hierarchical]
I
InvRel.T [in chip.check]K
KosarajuAcyclicity.successors [in chip.kosaraju_acyclic]KosarajuAcyclicity.V [in chip.kosaraju_acyclic]
Kosaraju.Pdfs.successors [in chip.kosaraju]
Kosaraju.Program.r [in chip.kosaraju]
Kosaraju.Stack.r [in chip.kosaraju]
Kosaraju.T [in chip.kosaraju]
L
Lemmas.T [in chip.ordtype]M
Mono.A [in chip.ordtype]Mono.B [in chip.ordtype]
O
Ordered.ClassDef.cT [in chip.ordtype]Ordered.ClassDef.T [in chip.ordtype]
OrdinalsCheckableImpacted.Finn.checkable' [in chip.finn_set]
OrdinalsCheckableImpacted.Finn.f [in chip.finn_set]
OrdinalsCheckableImpacted.Finn.f_equal_g [in chip.finn_set]
OrdinalsCheckableImpacted.Finn.f' [in chip.finn_set]
OrdinalsCheckableImpacted.Finn.g [in chip.finn_set]
OrdinalsCheckableImpacted.Finn.g_grev [in chip.finn_set]
OrdinalsCheckableImpacted.Finn.g' [in chip.finn_set]
OrdinalsCheckableImpacted.Finn.g'_acyclic [in chip.finn_set]
OrdinalsCheckableImpacted.Finn.g'_g'rev [in chip.finn_set]
OrdinalsCheckableImpacted.Finn.successors [in chip.finn_set]
OrdinalsCheckableImpacted.Finn.successors' [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.checkable'_bot [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.f_top_partition [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.f_top_bot_ps [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.f_bot [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.f_top [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.f'_bot [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.f'_top [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.g_bot_top_ps [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.g_bot_grev [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.g_bot [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.g_top_grev [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.g_top [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.p [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.ps [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.ps_neq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.ps_partition [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.ps' [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.ps'_neq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.ps'_partition [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.p_uniq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.p_ps_eq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.p' [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.p'_uniq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.p'_ps'_eq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.successors_bot [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical.successors_top [in chip.finn_set]
Other.A [in chip.change]
Other.A [in chip.check]
Other.check [in chip.change]
Other.check [in chip.check]
Other.checkable [in chip.change]
Other.checkable [in chip.check]
Other.checkable_V_V' [in chip.change]
Other.checkable' [in chip.change]
Other.check_V_V' [in chip.change]
Other.check' [in chip.change]
Other.f [in chip.change]
Other.f [in chip.check]
Other.f_equal_g1 [in chip.change]
Other.f' [in chip.change]
Other.f' [in chip.check]
Other.g' [in chip.change]
Other.g1 [in chip.change]
Other.g1 [in chip.check]
Other.g1_g2_connect [in chip.change]
Other.g1_g2_connect [in chip.check]
Other.g2 [in chip.change]
Other.g2 [in chip.check]
Other.P [in chip.change]
Other.P [in chip.check]
Other.R [in chip.change]
Other.R [in chip.check]
Other.V_result_cert_uniq [in chip.change]
Other.V_result_certP [in chip.change]
Other.V_result_cert [in chip.change]
Other.V' [in chip.change]
Other.V' [in chip.check]
P
ProdOrd.K [in chip.ordtype]ProdOrd.T [in chip.ordtype]
S
SeqOrd.T [in chip.ordtype]SeqSet.all_in_cover [in chip.tarjan_acyclic]
SeqSet.sc [in chip.tarjan_acyclic]
SeqSet.trivIset_sc [in chip.tarjan_acyclic]
SeqSet.V [in chip.tarjan_acyclic]
T
TarjanAcyclic.g [in chip.tarjan_acyclic]TarjanAcyclic.V [in chip.tarjan_acyclic]
TarjanSeq.successors [in chip.tarjan_acyclic]
TarjanSeq.V [in chip.tarjan_acyclic]
tarjan.N [in chip.tarjan]
tarjan.successors [in chip.tarjan]
tarjan.V [in chip.tarjan]
ToposAcyclic.g [in chip.topos]
ToposAcyclic.g_acyclic [in chip.topos]
ToposAcyclic.ts [in chip.topos]
ToposAcyclic.ts_all [in chip.topos]
ToposAcyclic.ts_tsorted [in chip.topos]
ToposAcyclic.V [in chip.topos]
ToposTseqRel.g [in chip.topos]
ToposTseqRel.g_acyclic [in chip.topos]
ToposTseqRel.V [in chip.topos]
ToposTseq.g_acyclic [in chip.topos]
ToposTseq.successors [in chip.topos]
ToposTseq.V [in chip.topos]
Totality.K [in chip.ordtype]
U
unitOrd.ordtt [in chip.ordtype]unitOrd.unit_ordMixin [in chip.ordtype]
Library Index
A
acyclicC
changecheck
check_seq_hierarchical
check_seq
close_dfs
closure
closure_example
connect
D
dfs_setE
extraextract_impacted
extract_impacted_rbt
F
finnfinn_set
H
hierarchicalhierarchical_sub_pt_correct
hierarchical_sub
hierarchical_sub_correct
hierarchical_sub_pt
hierarchical_correct
K
kosarajukosaraju_acyclic
O
ordtypeS
stringT
tarjantarjan_acyclic
topos
Lemma Index
A
acyclic_find_in_diconnect [in chip.topos]acyclic_rev [in chip.acyclic]
acyclic_diconnect [in chip.acyclic]
acyclic_no_self_loop [in chip.acyclic]
add_stack_pre [in chip.tarjan]
add_stack_gwf [in chip.tarjan]
add_sccs_wf [in chip.tarjan]
add_blacks_ewf [in chip.tarjan]
add_stack_ewf [in chip.tarjan]
all_in_flatten_tarjans [in chip.tarjan_acyclic]
all_in_cover_tarjan [in chip.tarjan_acyclic]
all_in_flatten_kosaraju [in chip.kosaraju_acyclic]
all_in_sccs [in chip.acyclic]
B
before_can_toW [in chip.connect]before_can_to [in chip.connect]
before_filter [in chip.connect]
before_filter_inv [in chip.connect]
blacks_add_sccs [in chip.tarjan]
C
can_to_cat [in chip.connect]can_to_cons [in chip.connect]
cert_check_impactedV'_check [in chip.check]
check_all_cert_V'_uniq_p [in chip.hierarchical_correct]
check_all_cert_sound_p [in chip.hierarchical_correct]
check_all_cert_complete_p [in chip.hierarchical_correct]
check_all_cert_sound_g2 [in chip.change]
check_all_cert_complete_g2 [in chip.change]
check_all_cert_V'_uniq_g2 [in chip.change]
check_all_cert_sound [in chip.change]
check_all_cert_complete [in chip.change]
check_all_cert_V'_uniq [in chip.change]
check_all_cert_cases [in chip.change]
check_all_cert_V'_sub_uniq [in chip.hierarchical_sub_correct]
check_all_cert_sound_sub [in chip.hierarchical_sub_correct]
check_all_cert_complete_sub [in chip.hierarchical_sub_correct]
check_pimpacted_V'_cert_uniq [in chip.hierarchical]
check_pimpacted_V'_certP [in chip.hierarchical]
check_all_cert_V'_sub_pt_uniq [in chip.hierarchical_sub_pt_correct]
check_all_cert_sound_sub_pt [in chip.hierarchical_sub_pt_correct]
check_all_cert_complete_sub_pt [in chip.hierarchical_sub_pt_correct]
check_impactedV'_cert_uniq [in chip.check]
check_impactedV'_certP [in chip.check]
check_impactedV'_cert_check [in chip.check]
class_diconnected_tarjans [in chip.tarjan_acyclic]
class_diconnected_tarjan [in chip.tarjan_acyclic]
class_diconnected_kosaraju [in chip.kosaraju_acyclic]
closureP [in chip.close_dfs]
closure_eqi [in chip.close_dfs]
closure_g [in chip.close_dfs]
colorP [in chip.tarjan]
connect_from [in chip.extra]
connect_to [in chip.extra]
connect_rev [in chip.extra]
connect_g_bot_rev_sub_g_bot_rev [in chip.check_seq_hierarchical]
connect_rel_sub [in chip.check_seq_hierarchical]
connect_f_f'_eq [in chip.change]
connect_gV'_rev [in chip.change]
connect_g'_imf [in chip.check_seq]
connect_imp [in chip.check_seq]
connect_to_rev [in chip.connect]
connect_to_C1_id [in chip.connect]
connect_to_C1l [in chip.connect]
connect_to_C1r [in chip.connect]
connect_to_forced [in chip.connect]
connect_toT [in chip.connect]
connect_to_sub [in chip.connect]
connect_toW [in chip.connect]
connect_to1 [in chip.connect]
connect_from_to [in chip.connect]
connect_to_from [in chip.connect]
connect_rev [in chip.connect]
connect_rev_v_u [in chip.hierarchical]
connect_checkable_impactedV' [in chip.check]
connect_impactedV'_eq [in chip.check]
connect_impactedV_eq [in chip.check]
connect1l [in chip.extra]
connect1r [in chip.extra]
cover_tarjan [in chip.tarjan_acyclic]
cover_all_in [in chip.tarjan_acyclic]
cover0 [in chip.tarjan]
cycle_path_diconnect [in chip.acyclic]
D
dfs_uniq [in chip.close_dfs]dfs_mems [in chip.close_dfs]
dfs_mem' [in chip.close_dfs]
dfs_mem [in chip.close_dfs]
dfs_eq_in [in chip.close_dfs]
dfs_in_in [in chip.close_dfs]
dfs_subset [in chip.close_dfs]
dfs_in [in chip.close_dfs]
dfs'_is_correct [in chip.tarjan]
DFS.dfs_sdfs_in [in chip.dfs_set]
DFS.elements_in_mem [in chip.dfs_set]
DFS.elts_srclosure'_uniq [in chip.dfs_set]
DFS.elts_srclosure_uniq [in chip.dfs_set]
DFS.elts_srclosure'Pg [in chip.dfs_set]
DFS.elts_srclosure'P [in chip.dfs_set]
DFS.elts_srclosurePg [in chip.dfs_set]
DFS.elts_srclosureP [in chip.dfs_set]
DFS.in_foldr_mem [in chip.dfs_set]
DFS.rclosed_elts_srclosure' [in chip.dfs_set]
DFS.rclosed_elts_srclosure [in chip.dfs_set]
DFS.rclosure_srclosure [in chip.dfs_set]
DFS.rclosure'_srclosure' [in chip.dfs_set]
DFS.srclosure_srclosure' [in chip.dfs_set]
DFS.subset_sdfs [in chip.dfs_set]
dfs1_is_correct [in chip.tarjan]
diconnect_can_to [in chip.connect]
diconnect_to_predT [in chip.connect]
diconnect_to_sub [in chip.connect]
diconnect_trans [in chip.connect]
diconnect_sym [in chip.connect]
diconnect_neq_sccs [in chip.acyclic]
diconnect_path_cycle [in chip.acyclic]
diconnect0 [in chip.connect]
disjoints1 [in chip.extra]
disjoint1s [in chip.extra]
drop_subseq [in chip.extra]
drop_subseq [in chip.tarjan]
E
enumsP [in chip.tarjan_acyclic]enums_enums'_in [in chip.tarjan_acyclic]
enums'P [in chip.tarjan_acyclic]
enum_tarjan_non_empty [in chip.tarjan_acyclic]
eq_tsorted [in chip.connect]
eq_can_to [in chip.connect]
eq_diconnect_to [in chip.connect]
eq_diconnect [in chip.connect]
eq_foodP [in chip.closure_example]
eq_stringP [in chip.string]
eq_asciiP [in chip.string]
exist_p'u_for_v [in chip.hierarchical]
exist_list_pu_for_seq_v [in chip.hierarchical]
exist_pu_for_v [in chip.hierarchical]
F
foldr_pdfs_subset [in chip.topos]food_finite [in chip.closure_example]
food_pcancel [in chip.closure_example]
freshV'P [in chip.check]
freshV'_sub_eq [in chip.hierarchical_sub_pt]
G
gbiconnect_equiv [in chip.tarjan]ginsubexP [in chip.change]
ginsubP [in chip.change]
ginsub_eq [in chip.change]
grays_add_sccs [in chip.tarjan]
grays_add_blacks [in chip.tarjan]
grays_add_stack [in chip.tarjan]
grays_sccsF [in chip.tarjan]
grays_stack [in chip.tarjan]
grays0 [in chip.tarjan]
grevinsubexP [in chip.change]
gsccs_partition [in chip.tarjan]
gsub_connect [in chip.connect]
gsub_path [in chip.connect]
gsub_acyclic [in chip.acyclic]
g_bot_rev_sub_eqq [in chip.check_seq_hierarchical]
I
impactedP [in chip.closure]impactedVP [in chip.check]
impactedVV'_sub_eq [in chip.hierarchical_sub]
impactedVV'_freshV' [in chip.check]
impactedV_in_pimpacted_V [in chip.hierarchical]
impactedV_impactedV_sub_eq [in chip.hierarchical_sub]
impactedV_sub_impactedV_eq [in chip.hierarchical_sub]
impactedV'P [in chip.check]
impactedV'_sub_pt_eq [in chip.hierarchical_sub_pt]
impactedV'_sub_eq [in chip.hierarchical_sub]
impacted_closure [in chip.check]
index_find [in chip.connect]
in_ts_g'rev_imf_checkable_val [in chip.check_seq]
in_ts_g'rev_checkable_imf [in chip.check_seq]
in_enums_disjoint [in chip.tarjan_acyclic]
in_uniq_enums [in chip.tarjan_acyclic]
in_flatten [in chip.acyclic]
in_succs_ts [in chip.finn]
irr [in chip.ordtype]
irr_tt [in chip.ordtype]
irr_ords [in chip.ordtype]
irr_ordf [in chip.ordtype]
irr_lex [in chip.ordtype]
irr_ltn_nat [in chip.ordtype]
is_subscc1 [in chip.tarjan]
is_subscc_in_scc [in chip.tarjan]
K
kosaraju_correct [in chip.kosaraju]kosaraju_acyclicP [in chip.kosaraju_acyclic]
L
last_drop [in chip.extra]last_take [in chip.extra]
leq_index_nth [in chip.connect]
ltn_mod2r [in chip.extra]
ltn_div2r [in chip.extra]
ltn_mod2r [in chip.tarjan]
ltn_div2r [in chip.tarjan]
M
mem_can_to [in chip.connect]mem_scc [in chip.tarjan]
modifiedV_sub_modifiedV_eq [in chip.hierarchical_sub]
modifiedV_pmodified_sub_V [in chip.hierarchical_sub]
N
neq_connect_in_pimpacted_V [in chip.hierarchical]non_impacted_rel [in chip.check_seq]
non_singleton_cycle [in chip.acyclic]
non_singleton_neq [in chip.acyclic]
not_impactedP [in chip.check]
not_modifiedP [in chip.check]
nsym [in chip.ordtype]
O
OrdinalsCheckableImpacted.in_succs_ts [in chip.finn_set]OrdinalsCheckableImpacted.succs_tseq_before [in chip.finn_set]
OrdinalsCheckableImpacted.succs_ts_in [in chip.finn_set]
OrdinalsCheckableImpacted.succs_ts_uniq [in chip.finn_set]
OrdinalsCheckableImpacted.succs_checkable_impacted_fresh_uniq [in chip.finn_set]
OrdinalsCheckableImpacted.succs_impacted_fresh_uniq [in chip.finn_set]
OrdinalsCheckableImpacted.succs_checkable_impacted_fresh_eq [in chip.finn_set]
OrdinalsCheckableImpacted.succs_impacted_fresh_eq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_checkable_impacted_fresh_sub_pt_uniq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_impacted_fresh_sub_pt_uniq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_checkable_impacted_fresh_sub_uniq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_impacted_fresh_sub_uniq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_checkable_impacted_fresh_sub_pt_eq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_impacted_fresh_sub_pt_eq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_checkable_impacted_fresh_sub_eq [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_impacted_fresh_sub_eq [in chip.finn_set]
OrdTypeUsualOrderedType.compare_spec [in chip.dfs_set]
OrdTypeUsualOrderedType.lt_compat [in chip.dfs_set]
OrdTypeUsualOrderedType.lt_strorder [in chip.dfs_set]
otrans [in chip.ordtype]
P
path_from [in chip.extra]path_to [in chip.extra]
path_xset_xedge [in chip.tarjan]
path_last [in chip.ordtype]
pdfs_subset [in chip.topos]
pdfs_uniq [in chip.topos]
pdfs_connect [in chip.kosaraju]
pdfs_correct [in chip.kosaraju]
pdfs_connect' [in chip.kosaraju]
pdfs_correct' [in chip.kosaraju]
pfreshV'_in_freshV' [in chip.hierarchical_sub_pt]
pimpacted_V'_impactedV' [in chip.hierarchical]
pimpacted_V'_impactedVV' [in chip.hierarchical]
pimpacted_V'_fresh [in chip.hierarchical]
pre_dfs_subroots [in chip.tarjan]
P_V_sub_V_seq_sub_eq [in chip.check_seq_hierarchical]
R
rankE [in chip.tarjan]rank_le_head [in chip.tarjan]
rank_mem [in chip.tarjan]
rank_infty [in chip.tarjan]
rank_lt [in chip.tarjan]
rank_le [in chip.tarjan]
rank_small [in chip.tarjan]
rank_catr [in chip.tarjan]
rank_catl [in chip.tarjan]
rank_cons [in chip.tarjan]
rclosed_rclosure' [in chip.close_dfs]
rclosed_rclosure [in chip.close_dfs]
rclosed_connect [in chip.close_dfs]
rclosed_impacted [in chip.closure]
rclose_subset [in chip.close_dfs]
rclosureP [in chip.close_dfs]
rclosurePg [in chip.close_dfs]
rclosuresP [in chip.close_dfs]
rclosures_connect [in chip.close_dfs]
rclosures'P [in chip.close_dfs]
rclosures'_connect [in chip.close_dfs]
rclosure_uniq [in chip.close_dfs]
rclosure_rclosure'_i [in chip.close_dfs]
rclosure_in_rl [in chip.close_dfs]
rclosure_in_lr [in chip.close_dfs]
rclosure_exist [in chip.close_dfs]
rclosure'P [in chip.close_dfs]
rclosure'Pg [in chip.close_dfs]
rclosure'_uniq [in chip.close_dfs]
reltoI [in chip.connect]
S
sccs_add_sccs [in chip.tarjan]sccs_stackF [in chip.tarjan]
sccs_acyclicP [in chip.acyclic]
self_loop_cycle [in chip.acyclic]
seq_checkable_impacted_fresh_sub_pt_uniq [in chip.check_seq_hierarchical]
seq_checkable_impacted_fresh_sub_uniq [in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_pt_uniq [in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_uniq [in chip.check_seq_hierarchical]
seq_freshV'_uniq [in chip.check_seq_hierarchical]
seq_impactedVV'_sub_uniq [in chip.check_seq_hierarchical]
seq_impactedV_sub_uniq [in chip.check_seq_hierarchical]
seq_modifiedV_sub_uniq [in chip.check_seq_hierarchical]
seq_freshV'_sub_uniq [in chip.check_seq_hierarchical]
seq_pfreshV'_uniq [in chip.check_seq_hierarchical]
seq_freshU'_uniq [in chip.check_seq_hierarchical]
seq_pimpacted_V_uniq [in chip.check_seq_hierarchical]
seq_pmodified_V_uniq [in chip.check_seq_hierarchical]
seq_impactedU_uniq [in chip.check_seq_hierarchical]
seq_modifiedU_uniq [in chip.check_seq_hierarchical]
seq_checkable_impacted_fresh_sub_pt_correct [in chip.check_seq_hierarchical]
seq_checkable_impacted_fresh_sub_correct [in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_pt_correct [in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_correct [in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_pt_eq [in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_eq [in chip.check_seq_hierarchical]
seq_freshV'_sub_eq [in chip.check_seq_hierarchical]
seq_impactedVV'_sub_eq [in chip.check_seq_hierarchical]
seq_modifiedV_sub_eq [in chip.check_seq_hierarchical]
seq_pfreshV'_eq [in chip.check_seq_hierarchical]
seq_pimpacted_V_eq [in chip.check_seq_hierarchical]
seq_freshU'_eq [in chip.check_seq_hierarchical]
seq_impactedU_eq [in chip.check_seq_hierarchical]
seq_modifiedU_eq [in chip.check_seq_hierarchical]
seq_checkable_impacted_fresh_uniq [in chip.check_seq]
seq_impacted_fresh_uniq [in chip.check_seq]
seq_modifiedV_uniq [in chip.check_seq]
seq_checkable_impacted_fresh_eq [in chip.check_seq]
seq_impacted_fresh_eq [in chip.check_seq]
seq_impactedV'_eq [in chip.check_seq]
seq_freshV'_eq [in chip.check_seq]
seq_modifiedV_eq [in chip.check_seq]
seq_last_mono [in chip.ordtype]
seq_last_in [in chip.ordtype]
seq_of_stringK [in chip.string]
set_last_default [in chip.extra]
sorted_max_key_last [in chip.ordtype]
sorted_last_key_max [in chip.ordtype]
sorted_oleq [in chip.ordtype]
stack_add_sccs [in chip.tarjan]
stack_add_stack [in chip.tarjan]
subset_cover [in chip.extra]
subset_rclose [in chip.close_dfs]
subset_closure [in chip.close_dfs]
subset_bigcup [in chip.tarjan]
sub_freshV' [in chip.check]
succs_checkable_impacted_fresh_sub_pt_uniq [in chip.finn]
succs_impacted_fresh_sub_pt_uniq [in chip.finn]
succs_checkable_impacted_fresh_sub_uniq [in chip.finn]
succs_impacted_fresh_sub_uniq [in chip.finn]
succs_checkable_impacted_fresh_sub_pt_eq [in chip.finn]
succs_impacted_fresh_sub_pt_eq [in chip.finn]
succs_checkable_impacted_fresh_sub_eq [in chip.finn]
succs_impacted_fresh_sub_eq [in chip.finn]
succs_tseq_before [in chip.finn]
succs_ts_in [in chip.finn]
succs_ts_uniq [in chip.finn]
succs_checkable_impacted_fresh_uniq [in chip.finn]
succs_impacted_fresh_uniq [in chip.finn]
succs_checkable_impacted_fresh_eq [in chip.finn]
succs_impacted_fresh_eq [in chip.finn]
T
take_subseq [in chip.extra]tarjansP [in chip.tarjan_acyclic]
tarjans_acyclicP [in chip.tarjan_acyclic]
tarjan_correct [in chip.tarjan]
tarjan_rec_is_correct [in chip.tarjan]
tarjan_rec_terminates [in chip.tarjan]
total [in chip.ordtype]
totalP [in chip.ordtype]
total_tt [in chip.ordtype]
total_ords [in chip.ordtype]
total_ordf [in chip.ordtype]
total_lex [in chip.ordtype]
total_ltn_nat [in chip.ordtype]
trans [in chip.ordtype]
trans_tt [in chip.ordtype]
trans_ords [in chip.ordtype]
trans_ordf [in chip.ordtype]
trans_lex [in chip.ordtype]
trans_ltn_nat [in chip.ordtype]
trivIset_gsccs [in chip.tarjan]
trivIset_tarjan [in chip.tarjan_acyclic]
tseq_rgraph_connect_before [in chip.topos]
tseq_connect_before [in chip.topos]
tseq_uniq [in chip.topos]
tseq_all [in chip.topos]
tseq_sorted [in chip.topos]
tseq_correct [in chip.kosaraju]
tseq_correct' [in chip.kosaraju]
tsortedE [in chip.connect]
tsorted_cons_r [in chip.connect]
tsorted_setU1_l [in chip.connect]
tsorted_cat [in chip.connect]
tsorted_diconnect [in chip.connect]
tsorted_inv [in chip.connect]
tsorted_nil [in chip.connect]
ts_connect_before [in chip.topos]
ts_nth [in chip.topos]
ts_g'rev_imf_checkable_val_before [in chip.check_seq]
ts_g'rev_imf_checkable_val_in [in chip.check_seq]
ts_g'rev_imf_checkable_val_uniq [in chip.check_seq]
ts_g'rev_imf_checkable_before [in chip.check_seq]
ts_g'rev_imf_before [in chip.check_seq]
ts_g'rev_imf_uniq [in chip.check_seq]
ts_g'rev_imf_all [in chip.check_seq]
ts_g'rev_checkable_imf_before [in chip.check_seq]
ts_g'rev_checkable_imf_in [in chip.check_seq]
ts_g'rev_checkable_imf_uniq [in chip.check_seq]
ts_rev_before [in chip.check_seq]
U
uniq_prod_eq [in chip.extra]uniq_catRL [in chip.extra]
uniq_catLR [in chip.extra]
uniq_catRL [in chip.tarjan]
uniq_catLR [in chip.tarjan]
uniq_flatten_tarjans [in chip.tarjan_acyclic]
uniq_in_tarjans [in chip.tarjan_acyclic]
uniq_flatten [in chip.tarjan_acyclic]
uniq_enums [in chip.tarjan_acyclic]
uniq_flatten_kosaraju [in chip.kosaraju_acyclic]
V
V_result_filter_cert_checkable' [in chip.change]V_result_cert_sound [in chip.change]
V_result_cert_complete [in chip.change]
W
whites_add_sccs [in chip.tarjan]whites_add_blacks [in chip.tarjan]
whites_add_stack [in chip.tarjan]
whites_graysF [in chip.tarjan]
whites_stackF [in chip.tarjan]
whites_blacksF [in chip.tarjan]
Axiom Index
F
FinOrdType.irr_ordT [in chip.dfs_set]FinOrdType.ordT [in chip.dfs_set]
FinOrdType.total_ordT [in chip.dfs_set]
FinOrdType.trans_ordT [in chip.dfs_set]
FinType.T [in chip.dfs_set]
FinUsualOrderedType.compare [in chip.dfs_set]
FinUsualOrderedType.compare_spec [in chip.dfs_set]
FinUsualOrderedType.eq_dec [in chip.dfs_set]
FinUsualOrderedType.lt [in chip.dfs_set]
FinUsualOrderedType.lt_compat [in chip.dfs_set]
FinUsualOrderedType.lt_strorder [in chip.dfs_set]
O
OrdinalFinType.n [in chip.dfs_set]OrdinalsType.H_mn [in chip.finn_set]
OrdinalsType.m' [in chip.finn_set]
OrdinalsType.n [in chip.finn_set]
OrdType.T [in chip.dfs_set]
Constructor Index
C
ColorBlackStack [in chip.tarjan]ColorGray [in chip.tarjan]
ColorSccs [in chip.tarjan]
ColorWhite [in chip.tarjan]
E
Env [in chip.tarjan]G
garlic [in chip.closure_example]M
Mono [in chip.ordtype]O
Ordered.Class [in chip.ordtype]Ordered.Mixin [in chip.ordtype]
Ordered.Pack [in chip.ordtype]
P
PreDfs [in chip.tarjan]R
red_pepper [in chip.closure_example]rigatoni [in chip.closure_example]
rigatoni_arrabiata [in chip.closure_example]
S
sauce [in chip.closure_example]T
tomato_puree [in chip.closure_example]total_spec_gt [in chip.ordtype]
total_spec_eq [in chip.ordtype]
total_spec_lt [in chip.ordtype]
W
WfEnv [in chip.tarjan]WfGraph [in chip.tarjan]
Projection Index
B
blacks [in chip.tarjan]F
fun_of [in chip.ordtype]O
Ordered.base [in chip.ordtype]Ordered.mixin [in chip.ordtype]
Ordered.ordering [in chip.ordtype]
Ordered.sort [in chip.ordtype]
P
pre_sccs [in chip.tarjan]pre_wf_graph [in chip.tarjan]
pre_wf_env [in chip.tarjan]
pre_access_to [in chip.tarjan]
S
sccs [in chip.tarjan]stack [in chip.tarjan]
W
wf_noblack_towhite [in chip.tarjan]wf_stack_to_grays [in chip.tarjan]
wf_grays_to_stack [in chip.tarjan]
wf_stack_uniq [in chip.tarjan]
wf_sccs [in chip.tarjan]
wf_stack [in chip.tarjan]
Inductive Index
C
color_spec [in chip.tarjan]F
food [in chip.closure_example]T
total_spec [in chip.ordtype]Section Index
A
Acyclic [in chip.acyclic]Acyclicity [in chip.acyclic]
AcyclicRev [in chip.acyclic]
AcyclicSub [in chip.acyclic]
C
Changed [in chip.change]ChangedHierarchical [in chip.hierarchical_correct]
ChangedHierarchicalSub [in chip.hierarchical_sub_correct]
ChangedHierarchicalSubPt [in chip.hierarchical_sub_pt_correct]
Checked [in chip.check]
CheckedSeq [in chip.check_seq]
CheckedSeqHierarchical [in chip.check_seq_hierarchical]
Closure [in chip.closure]
Cycles [in chip.acyclic]
D
DFSearch [in chip.close_dfs]E
extra_path [in chip.extra]extra_fintype [in chip.extra]
extra_seq [in chip.extra]
extra_div [in chip.extra]
extra_finset [in chip.tarjan]
extra_seq [in chip.tarjan]
extra_div [in chip.tarjan]
F
Fin [in chip.connect]Finn [in chip.finn]
FinnHierarchical [in chip.finn]
FinTypeOrd [in chip.ordtype]
Fin.ConnectRelto [in chip.connect]
Fin.Diconnect [in chip.connect]
Fin.Relto [in chip.connect]
Fin.Sub [in chip.connect]
H
HierarchicalSub [in chip.hierarchical_sub]HierarchicalSubPt [in chip.hierarchical_sub_pt]
Hierarchy [in chip.hierarchical]
I
InvRel [in chip.check]K
Kosaraju [in chip.kosaraju]KosarajuAcyclicity [in chip.kosaraju_acyclic]
Kosaraju.Pdfs [in chip.kosaraju]
Kosaraju.Program [in chip.kosaraju]
Kosaraju.Stack [in chip.kosaraju]
L
Lemmas [in chip.ordtype]M
Mono [in chip.ordtype]N
NatOrd [in chip.ordtype]O
Ordered.ClassDef [in chip.ordtype]Ordered.RawMixin [in chip.ordtype]
OrdinalsCheckableImpacted.Finn [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.FinnHierarchical [in chip.finn_set]
Other [in chip.change]
Other [in chip.check]
P
ProdOrd [in chip.ordtype]S
SeqOrd [in chip.ordtype]SeqSet [in chip.tarjan_acyclic]
T
tarjan [in chip.tarjan]TarjanAcyclic [in chip.tarjan_acyclic]
TarjanSeq [in chip.tarjan_acyclic]
ToposAcyclic [in chip.topos]
ToposTseq [in chip.topos]
ToposTseqRel [in chip.topos]
Totality [in chip.ordtype]
U
unitOrd [in chip.ordtype]Abbreviation Index
A
A [in chip.finn]A_bot [in chip.finn]
A_top [in chip.finn]
E
edge [in chip.tarjan]F
food_rel_rev [in chip.closure_example]G
g [in chip.kosaraju_acyclic]gbiconnect [in chip.tarjan]
gconnect [in chip.tarjan]
grev [in chip.change]
grev [in chip.acyclic]
gsub [in chip.connect]
gsub [in chip.acyclic]
gV' [in chip.change]
gV' [in chip.check_seq]
gV' [in chip.finn]
gV'rev [in chip.change]
g_bot_V'_rev [in chip.hierarchical_correct]
g_bot_V' [in chip.hierarchical_correct]
g_top_U'_rev [in chip.hierarchical_correct]
g_top_U' [in chip.hierarchical_correct]
g_bot_rev [in chip.hierarchical_correct]
g_top_rev [in chip.hierarchical_correct]
g_bot_sub [in chip.hierarchical_sub_pt]
g_bot_rev [in chip.hierarchical_sub_pt]
g_top_rev [in chip.hierarchical_sub_pt]
g_bot_sub [in chip.hierarchical_sub_correct]
g_bot_V'_rev [in chip.hierarchical_sub_correct]
g_bot_V' [in chip.hierarchical_sub_correct]
g_top_U'_rev [in chip.hierarchical_sub_correct]
g_top_U' [in chip.hierarchical_sub_correct]
g_bot_rev [in chip.hierarchical_sub_correct]
g_top_rev [in chip.hierarchical_sub_correct]
g_bot_rev [in chip.hierarchical]
g_top_rev [in chip.hierarchical]
g_bot_sub [in chip.hierarchical_sub_pt_correct]
g_bot_V'_rev [in chip.hierarchical_sub_pt_correct]
g_bot_V' [in chip.hierarchical_sub_pt_correct]
g_top_U'_rev [in chip.hierarchical_sub_pt_correct]
g_top_U' [in chip.hierarchical_sub_pt_correct]
g_bot_rev [in chip.hierarchical_sub_pt_correct]
g_top_rev [in chip.hierarchical_sub_pt_correct]
g_bot_sub [in chip.hierarchical_sub]
g_bot_rev [in chip.hierarchical_sub]
g_top_rev [in chip.hierarchical_sub]
g'rev [in chip.change]
g'_bot_rev [in chip.hierarchical_correct]
g'_top_rev [in chip.hierarchical_correct]
g'_imf [in chip.check_seq]
g'_bot_rev [in chip.hierarchical_sub_correct]
g'_top_rev [in chip.hierarchical_sub_correct]
g'_bot_rev [in chip.hierarchical_sub_pt_correct]
g'_top_rev [in chip.hierarchical_sub_pt_correct]
g1V' [in chip.change]
I
I [in chip.connect]I [in chip.acyclic]
infty [in chip.tarjan]
insub_g_bot [in chip.hierarchical_correct]
insub_g_top [in chip.hierarchical_correct]
insub_g_bot [in chip.hierarchical_sub_correct]
insub_g_top [in chip.hierarchical_sub_correct]
insub_g_bot [in chip.hierarchical_sub_pt_correct]
insub_g_top [in chip.hierarchical_sub_pt_correct]
M
m [in chip.finn]m_bot [in chip.finn]
m_top [in chip.finn]
O
Ordered.Exports.OrdMixin [in chip.ordtype]Ordered.Exports.OrdType [in chip.ordtype]
Ordered.Exports.ordType [in chip.ordtype]
OrdinalsCheckableImpacted.A [in chip.finn_set]
OrdinalsCheckableImpacted.gV' [in chip.finn_set]
OrdinalsCheckableImpacted.V [in chip.finn_set]
OrdinalsCheckableImpacted.V' [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.A_bot [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.A_top [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.m_bot [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.m_top [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.n_bot [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.n_top [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.P_bot [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.P_top [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.U [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.U' [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.V [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.V' [in chip.finn_set]
OrdinalsType.m [in chip.finn_set]
S
scc_of [in chip.tarjan]U
U [in chip.hierarchical_correct]U [in chip.hierarchical_sub_pt]
U [in chip.check_seq_hierarchical]
U [in chip.hierarchical_sub_correct]
U [in chip.hierarchical]
U [in chip.hierarchical_sub_pt_correct]
U [in chip.hierarchical_sub]
U [in chip.finn]
U' [in chip.finn]
V
V [in chip.hierarchical_correct]V [in chip.hierarchical_sub_pt]
V [in chip.check_seq_hierarchical]
V [in chip.change]
V [in chip.change]
V [in chip.check_seq]
V [in chip.hierarchical_sub_correct]
V [in chip.hierarchical]
V [in chip.hierarchical_sub_pt_correct]
V [in chip.hierarchical_sub]
V [in chip.check]
V [in chip.check]
V [in chip.finn]
V [in chip.finn]
V_sub [in chip.hierarchical_sub_pt]
V_sub [in chip.hierarchical_sub_correct]
V_sub [in chip.hierarchical_sub_pt_correct]
V_sub [in chip.hierarchical_sub]
V' [in chip.finn]
V' [in chip.finn]
V'_imf [in chip.check_seq]
Definition Index
A
access_to [in chip.tarjan]acyclic [in chip.acyclic]
add_sccs [in chip.tarjan]
add_blacks [in chip.tarjan]
add_stack [in chip.tarjan]
adjundup [in chip.hierarchical]
ascii_eqMixin [in chip.string]
B
before [in chip.connect]black_gsccs [in chip.tarjan]
C
can_to [in chip.connect]checkable_impacted_fresh_sub_pt [in chip.hierarchical_sub_pt]
checkable_impactedV'_sub_pt [in chip.hierarchical_sub_pt]
checkable_pimpacted_fresh [in chip.hierarchical]
checkable_pimpacted_V' [in chip.hierarchical]
checkable_impacted_fresh_sub [in chip.hierarchical_sub]
checkable_impactedV'_sub [in chip.hierarchical_sub]
checkable_impacted_fresh [in chip.check]
checkable_impactedV' [in chip.check]
checkable_impacted [in chip.check]
checkable_impactedV [in chip.check]
check_all_cert_V'_p [in chip.hierarchical_correct]
check_all_cert_p [in chip.hierarchical_correct]
check_impactedV'_sub_pt_cert [in chip.hierarchical_sub_pt]
check_all_cert_V' [in chip.change]
check_all_cert [in chip.change]
check_all_cert_V'_sub [in chip.hierarchical_sub_correct]
check_all_cert_sub [in chip.hierarchical_sub_correct]
check_pimpacted_V'_cert [in chip.hierarchical]
check_all_cert_V'_sub_pt [in chip.hierarchical_sub_pt_correct]
check_all_cert_sub_pt [in chip.hierarchical_sub_pt_correct]
check_impactedV'_sub_cert [in chip.hierarchical_sub]
check_impactedV'_cert [in chip.check]
class_acyclic [in chip.acyclic]
cover_gsccs [in chip.tarjan]
D
def_scc [in chip.tarjan]dfs' [in chip.tarjan]
dfs'_correct [in chip.tarjan]
DFS.elts_srclosure' [in chip.dfs_set]
DFS.elts_srclosure [in chip.dfs_set]
DFS.sdfs [in chip.dfs_set]
DFS.srclosure [in chip.dfs_set]
DFS.srclosure' [in chip.dfs_set]
dfs1 [in chip.tarjan]
dfs1_correct [in chip.tarjan]
diconnect [in chip.connect]
E
enums [in chip.tarjan_acyclic]enums' [in chip.tarjan_acyclic]
eq_food [in chip.closure_example]
eq_string [in chip.string]
eq_ascii [in chip.string]
e0 [in chip.tarjan]
F
FinOrdUsualOrderedType.compare [in chip.dfs_set]FinOrdUsualOrderedType.compare_spec [in chip.dfs_set]
FinOrdUsualOrderedType.eq [in chip.dfs_set]
FinOrdUsualOrderedType.eq_dec [in chip.dfs_set]
FinOrdUsualOrderedType.eq_equiv [in chip.dfs_set]
FinOrdUsualOrderedType.lt [in chip.dfs_set]
FinOrdUsualOrderedType.lt_compat [in chip.dfs_set]
FinOrdUsualOrderedType.lt_strorder [in chip.dfs_set]
FinOrdUsualOrderedType.OT.T [in chip.dfs_set]
FinOrdUsualOrderedType.t [in chip.dfs_set]
FinUsualOrderedType.eq [in chip.dfs_set]
FinUsualOrderedType.eq_equiv [in chip.dfs_set]
FinUsualOrderedType.t [in chip.dfs_set]
fin_ordMixin [in chip.ordtype]
food_rev_impacted [in chip.closure_example]
food_acyclic [in chip.closure_example]
food_rel [in chip.closure_example]
food_depends [in chip.closure_example]
food_finMixin [in chip.closure_example]
food_enum [in chip.closure_example]
food_countMixin [in chip.closure_example]
food_choiceMixin [in chip.closure_example]
food_unpickle [in chip.closure_example]
food_pickle [in chip.closure_example]
food_eqMixin [in chip.closure_example]
freshV' [in chip.check]
freshV'_sub [in chip.hierarchical_sub_pt]
G
grays [in chip.tarjan]gsccs [in chip.tarjan]
g_bot_rev_sub [in chip.check_seq_hierarchical]
g'rev_imf [in chip.check_seq]
I
impacted [in chip.closure]impactedVV' [in chip.check]
impactedVV'_sub [in chip.hierarchical_sub]
impactedV_sub [in chip.hierarchical_sub]
impactedV' [in chip.check]
impactedV'_sub_pt [in chip.hierarchical_sub_pt]
impactedV'_sub [in chip.hierarchical_sub]
impacted_U' [in chip.hierarchical]
impacted_U [in chip.hierarchical]
impacted_fresh_sub [in chip.hierarchical_sub]
impacted_fresh [in chip.check]
insub_g [in chip.change]
is_subscc [in chip.tarjan]
K
kosaraju [in chip.kosaraju]kosaraju_acyclic [in chip.kosaraju_acyclic]
L
lex [in chip.ordtype]lt_m_bot_pred [in chip.finn]
lt_m_top_pred [in chip.finn]
lt_m_pred [in chip.finn]
M
modifiedV [in chip.check]modifiedV_sub [in chip.hierarchical_sub]
N
nat_ordMixin [in chip.ordtype]noblack_to_white [in chip.tarjan]
O
OFT5.n [in chip.dfs_set]OFT5.T [in chip.dfs_set]
oleq [in chip.ordtype]
Ordered.class [in chip.ordtype]
Ordered.clone [in chip.ordtype]
Ordered.eqType [in chip.ordtype]
Ordered.Exports.ord [in chip.ordtype]
Ordered.pack [in chip.ordtype]
ordf [in chip.ordtype]
OrdinalFinOrdType.irr_ordT [in chip.dfs_set]
OrdinalFinOrdType.ordT [in chip.dfs_set]
OrdinalFinOrdType.total_ordT [in chip.dfs_set]
OrdinalFinOrdType.trans_ordT [in chip.dfs_set]
OrdinalFinType.T [in chip.dfs_set]
OrdinalsCheckableImpacted.lt_m_pred [in chip.finn_set]
OrdinalsCheckableImpacted.succs_ts [in chip.finn_set]
OrdinalsCheckableImpacted.succs_checkable_impacted_fresh [in chip.finn_set]
OrdinalsCheckableImpacted.succs_impacted_fresh [in chip.finn_set]
OrdinalsCheckableImpacted.succs_checkable_impacted [in chip.finn_set]
OrdinalsCheckableImpacted.succs_closure_uniq [in chip.finn_set]
OrdinalsCheckableImpacted.succs_closureP [in chip.finn_set]
OrdinalsCheckableImpacted.succs_closure [in chip.finn_set]
OrdinalsCheckableImpacted.VFinOrdType.irr_ordT [in chip.finn_set]
OrdinalsCheckableImpacted.VFinOrdType.ordT [in chip.finn_set]
OrdinalsCheckableImpacted.VFinOrdType.total_ordT [in chip.finn_set]
OrdinalsCheckableImpacted.VFinOrdType.trans_ordT [in chip.finn_set]
OrdinalsCheckableImpacted.VFinType.T [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_checkable_impacted_fresh_sub_pt [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_impacted_fresh_sub_pt [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_checkable_impacted_fresh_sub [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_impacted_fresh_sub [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.succs_modified_sub [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinOrdType.irr_ordT [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinOrdType.ordT [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinOrdType.total_ordT [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinOrdType.trans_ordT [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.UFinType.T [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinOrdType.irr_ordT [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinOrdType.ordT [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinOrdType.total_ordT [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinOrdType.trans_ordT [in chip.finn_set]
OrdinalsHierarchicalCheckableImpacted.VFinType.T [in chip.finn_set]
ordinal_ordMixin [in chip.ordtype]
ords [in chip.ordtype]
OrdTypeUsualOrderedType.compare [in chip.dfs_set]
OrdTypeUsualOrderedType.eq [in chip.dfs_set]
OrdTypeUsualOrderedType.eq_dec [in chip.dfs_set]
OrdTypeUsualOrderedType.eq_equiv [in chip.dfs_set]
OrdTypeUsualOrderedType.lt [in chip.dfs_set]
OrdTypeUsualOrderedType.t [in chip.dfs_set]
P
pdfs [in chip.kosaraju]pfreshV' [in chip.hierarchical_sub_pt]
pimf [in chip.check_seq]
pimpacted_V' [in chip.hierarchical]
pimpacted_V [in chip.hierarchical]
pimpacted_sub_V [in chip.hierarchical_sub]
pmodified_sub_V [in chip.hierarchical_sub]
post_dfs [in chip.tarjan]
prod_ordMixin [in chip.ordtype]
P_V_seq_sub [in chip.check_seq_hierarchical]
P_V_sub [in chip.hierarchical_sub]
R
rank [in chip.tarjan]rank_of_reachable [in chip.tarjan]
rclosed [in chip.close_dfs]
rclosure [in chip.close_dfs]
rclosures [in chip.close_dfs]
rclosures' [in chip.close_dfs]
rclosure' [in chip.close_dfs]
relfrom [in chip.extra]
relto [in chip.extra]
rinv [in chip.check]
rpdfs [in chip.kosaraju]
S
sccs_acyclic [in chip.acyclic]seq_checkable_impacted_fresh_sub_pt [in chip.check_seq_hierarchical]
seq_impacted_fresh_sub_pt [in chip.check_seq_hierarchical]
seq_checkable_impacted_fresh_sub [in chip.check_seq_hierarchical]
seq_impacted_fresh_sub [in chip.check_seq_hierarchical]
seq_freshV'_sub [in chip.check_seq_hierarchical]
seq_freshV' [in chip.check_seq_hierarchical]
seq_impactedVV'_sub [in chip.check_seq_hierarchical]
seq_impactedV_sub [in chip.check_seq_hierarchical]
seq_modifiedV_sub [in chip.check_seq_hierarchical]
seq_pfreshV' [in chip.check_seq_hierarchical]
seq_pimpacted_V [in chip.check_seq_hierarchical]
seq_pmodified_V [in chip.check_seq_hierarchical]
seq_freshU' [in chip.check_seq_hierarchical]
seq_impactedU [in chip.check_seq_hierarchical]
seq_modifiedU [in chip.check_seq_hierarchical]
seq_checkable_impacted_fresh [in chip.check_seq]
seq_impacted_fresh [in chip.check_seq]
seq_checkable_impacted [in chip.check_seq]
seq_freshV' [in chip.check_seq]
seq_impactedV' [in chip.check_seq]
seq_impactedV [in chip.check_seq]
seq_modifiedV [in chip.check_seq]
seq_ordMixin [in chip.ordtype]
seq_of_string [in chip.string]
split_after [in chip.tarjan]
strictly_increasing [in chip.ordtype]
string_eqMixin [in chip.string]
string_of_seq [in chip.string]
subltn [in chip.finn_set]
succs_checkable_impacted_fresh_sub_pt [in chip.finn]
succs_impacted_fresh_sub_pt [in chip.finn]
succs_checkable_impacted_fresh_sub [in chip.finn]
succs_impacted_fresh_sub [in chip.finn]
succs_modified_sub [in chip.finn]
succs_ts [in chip.finn]
succs_checkable_impacted_fresh [in chip.finn]
succs_impacted_fresh [in chip.finn]
succs_checkable_impacted [in chip.finn]
succs_modified [in chip.finn]
succs_closure_uniq [in chip.finn]
succs_closureP [in chip.finn]
succs_closure [in chip.finn]
T
tarjan [in chip.tarjan]tarjans [in chip.tarjan_acyclic]
tarjans_acyclic [in chip.tarjan_acyclic]
tarjans' [in chip.tarjan_acyclic]
tarjan_rec [in chip.tarjan]
tseq [in chip.kosaraju]
tsorted [in chip.connect]
ts_g'rev_imf_checkable_val [in chip.check_seq]
ts_g'rev_imf_checkable [in chip.check_seq]
ts_g'rev_imf [in chip.check_seq]
ts_g'rev_checkable_imf [in chip.check_seq]
ts_g'rev [in chip.check_seq]
V
V'_result_filter_cert_p [in chip.hierarchical_correct]V'_result_filter_cert [in chip.change]
V'_result_filter_cert_sub [in chip.hierarchical_sub_correct]
V'_result_filter_cert_sub_pt [in chip.hierarchical_sub_pt_correct]
W
whites [in chip.tarjan]X
xedges [in chip.tarjan]Record Index
E
env [in chip.tarjan]M
mono [in chip.ordtype]O
Ordered.class_of [in chip.ordtype]Ordered.mixin_of [in chip.ordtype]
Ordered.type [in chip.ordtype]
P
pre_dfs [in chip.tarjan]W
wf_graph [in chip.tarjan]wf_env [in chip.tarjan]
| 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 | (1417 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 | (31 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 | (37 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 | (442 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 | (28 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 | (401 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |
| 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 | (21 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 | (18 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 | (3 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 | (58 entries) |
| Abbreviation 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 | (116 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 | (238 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 | (8 entries) |