Per-module assurance inventory

Generated by tools/assurance_inventory.py from the F* source, the extracted OCaml, formal/fstar/build-ocaml.sh, .github/test-suites/*.yaml and the committed suite logs. No row on this page is hand-written. It exists to keep three different claims apart: implemented in F*, accepted by the verifier, and proved correct against a formalisation of the specification.

Tree: c618f71d2 · 224 modules from 236 .fst/.fsti files.

11W3C-refinement theorem

13internal-refinement theorem

29algorithm-correctness theorem

17specification / proof module

13local lemmas only

122merely Tot

0specification only (erased)

19unclassified (oracle unavailable)

Iron rule #10, proved rather than asserted

0active admissions

0--lax / --admit_smt_queries regions

81active assume val

The assume val count is not a defect count: under iron rule #3 each is either an acknowledged gap with an open issue or an allowed realisation (pure I/O, a host-engine call-out, or a vendored crypto primitive).

How a module earns each bucket

Shipping function — a name that appears as a top-level value binding in ocaml-output/<Module>.ml. Extraction, not naming, is the oracle. Extracted types do not count.
Declarative relation — a top-level definition F* erases (absent from the extracted .ml) whose return type is prop, Type0 or logical. That is formalised specification.
Pure formalisation module — in the build module list, yet extracts to no .ml at all: verified on every extract run, contributing zero executable code.
W3C-refinement theorem — names a shipping function and a declarative relation from a different pure formalisation module, so the specification is stated independently of both the code and the proof.
Internal-refinement theorem — names a shipping function and a declarative relation, but the relation lives beside the code it constrains: an invariant, not an independent formalisation.
Algorithm-correctness theorem — relates two or more shipping functions, with no declarative relation.
merely Tot — the module has shipping functions and no lemma anywhere in the corpus mentions them.

Name resolution is limited to the host module plus the modules it opens or aliases; an ambiguous identifier is dropped rather than counted. The classifier therefore fails downward — a module can be under-credited here, never over-credited.

Modules with a W3C-refinement theorem (11)

Module	Theorem	Proved in	Shipping function	Declarative relation	Unconditional
`OWL.Closure`	`theorem_sameAs_symmetry_licensed`	`OWL.RL.Refinement`	`owl_rule_sameAs_symmetry`	`eq_sym_derives`	no (has `requires`)
`OWL.Closure`	`theorem_sameAs_reflexivity_licensed`	`OWL.RL.Refinement`	`owl_rule_sameAs_reflexivity`	`eq_ref_derives`	no (has `requires`)
`OWL.Closure`	`theorem_symmetric_property_licensed`	`OWL.RL.Refinement`	`owl_rule_symmetric_property`	`prp_symp_derives`	no (has `requires`)
`OWL.Closure`	`theorem_equivalent_class_licensed`	`OWL.RL.Refinement`	`owl_rule_equivalent_class`	`scm_eqc1_derives`	no (has `requires`)
`OWL.Closure`	`theorem_equivalent_property_licensed`	`OWL.RL.Refinement`	`owl_rule_equivalent_property`	`scm_eqp1_derives`	no (has `requires`)
`OWL.Closure`	`theorem_inverse_of_licensed`	`OWL.RL.Refinement`	`owl_rule_inverse_of`	`prp_inv1_derives`, `prp_inv2_derives`	no (has `requires`)
`OWL.Closure`	`owl_rule_sameAs_transitivity_licensed`	`OWL.RL.Refinement`	`owl_rule_sameAs_transitivity`	`eq_trans_licensed`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`theorem_sameAs_transitivity_licensed`	`OWL.RL.Refinement`	`owl_rule_sameAs_transitivity`	`eq_trans_derives`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_transitive_property_licensed`	`OWL.RL.Refinement`	`owl_rule_transitive_property`	`ig_wf_sp`, `prp_trp_licensed`	no (has `requires`)
`OWL.Closure`	`theorem_transitive_property_licensed`	`OWL.RL.Refinement`	`owl_rule_transitive_property`	`ig_wf_sp`, `prp_trp_derives`	no (has `requires`)
`OWL.Closure`	`lemma_scm_eqc2_emission_licensed`	`OWL.RL.Refinement`	`find_objects_indexed`, `owl_equivalentClass`, `rdfs_subClassOf`, `term_is_iri`	`ig_wf_sp`, `scm_eqc2_derives`	no (has `requires`)
`OWL.Closure`	`owl_rule_scm_eqc2_licensed`	`OWL.RL.Refinement`	`owl_rule_scm_eqc2`	`ig_wf_sp`, `scm_eqc2_licensed`	no (has `requires`)
`OWL.Closure`	`theorem_scm_eqc2_licensed`	`OWL.RL.Refinement`	`owl_rule_scm_eqc2`	`ig_wf_sp`, `scm_eqc2_derives`	no (has `requires`)
`OWL.Closure`	`owl_rule_sameAs_replace_subject_licensed`	`OWL.RL.Refinement`	`owl_rule_sameAs_replace_subject`	`eq_rep_s_licensed`, `ig_wf_subj`	no (has `requires`)
`OWL.Closure`	`theorem_sameAs_replace_subject_licensed`	`OWL.RL.Refinement`	`owl_rule_sameAs_replace_subject`	`eq_rep_s_derives`, `ig_wf_subj`	no (has `requires`)
`OWL.Closure`	`owl_rule_sameAs_replace_object_licensed`	`OWL.RL.Refinement`	`owl_rule_sameAs_replace_object`	`eq_rep_o_licensed`, `ig_wf_obj`	no (has `requires`)
`OWL.Closure`	`theorem_sameAs_replace_object_licensed`	`OWL.RL.Refinement`	`owl_rule_sameAs_replace_object`	`eq_rep_o_derives`, `ig_wf_obj`	no (has `requires`)
`OWL.Closure`	`owl_rule_sameAs_replace_predicate_licensed`	`OWL.RL.Refinement`	`owl_rule_sameAs_replace_predicate`	`eq_rep_p_licensed`, `ig_wf_pred`	no (has `requires`)
`OWL.Closure`	`theorem_sameAs_replace_predicate_licensed`	`OWL.RL.Refinement`	`owl_rule_sameAs_replace_predicate`	`eq_rep_p_derives`, `ig_wf_pred`	no (has `requires`)
`OWL.Closure`	`lemma_scm_eqp2_emission_licensed`	`OWL.RL.Refinement`	`find_objects_indexed`, `owl_equivalentProperty`, `rdfs_subPropertyOf`, `term_is_iri`	`ig_wf_sp`, `scm_eqp2_derives`	no (has `requires`)
`OWL.Closure`	`owl_rule_scm_eqp2_licensed`	`OWL.RL.Refinement`	`owl_rule_scm_eqp2`	`ig_wf_sp`, `scm_eqp2_licensed`	no (has `requires`)
`OWL.Closure`	`theorem_scm_eqp2_licensed`	`OWL.RL.Refinement`	`owl_rule_scm_eqp2`	`ig_wf_sp`, `scm_eqp2_derives`	no (has `requires`)
`OWL.Closure`	`owl_rule_scm_dom2_licensed`	`OWL.RL.Refinement`	`owl_rule_scm_dom2`	`ig_wf_sp`, `scm_dom1_licensed`	no (has `requires`)
`OWL.Closure`	`theorem_scm_dom2_licensed`	`OWL.RL.Refinement`	`owl_rule_scm_dom2`	`ig_wf_sp`, `scm_dom1_derives`	no (has `requires`)
`OWL.Closure`	`owl_rule_scm_rng2_licensed`	`OWL.RL.Refinement`	`owl_rule_scm_rng2`	`ig_wf_sp`, `scm_rng1_licensed`	no (has `requires`)
`OWL.Closure`	`theorem_scm_rng2_licensed`	`OWL.RL.Refinement`	`owl_rule_scm_rng2`	`ig_wf_sp`, `scm_rng1_derives`	no (has `requires`)
`OWL.Closure`	`owl_rule_subprop_domain_range_licensed`	`OWL.RL.Refinement`	`owl_rule_subprop_domain_range`	`ig_wf_sp`, `subprop_domain_range_licensed`	no (has `requires`)
`OWL.Closure`	`theorem_subprop_domain_range_licensed`	`OWL.RL.Refinement`	`owl_rule_subprop_domain_range`	`ig_wf_sp`, `scm_dom2_derives`, `scm_rng2_derives`	no (has `requires`)
`OWL.Closure`	`lemma_decode_iri_list_licensed`	`OWL.RL.Refinement`	`decode_iri_list`	`ig_wf_sp`, `owl_list_denotes`	no (has `requires`)
`OWL.Closure`	`owl_rule_cls_oneof_licensed`	`OWL.RL.Refinement`	`owl_rule_cls_oneof`	`cls_oo_licensed`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`theorem_cls_oneof_licensed`	`OWL.RL.Refinement`	`owl_rule_cls_oneof`	`cls_oo_derives`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_cls_int1_licensed`	`OWL.RL.Refinement`	`owl_rule_cls_int1`	`cls_int2_licensed`, `ig_wf_po_spec`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`theorem_cls_int1_licensed`	`OWL.RL.Refinement`	`owl_rule_cls_int1`	`cls_int2_derives`, `ig_wf_po_spec`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_cls_uni_licensed`	`OWL.RL.Refinement`	`owl_rule_cls_uni`	`cls_uni_licensed`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`theorem_cls_uni_licensed`	`OWL.RL.Refinement`	`owl_rule_cls_uni`	`cls_disjoint_union_ext_derives`, `ig_wf_sp`, `scm_uni_derives`	no (has `requires`)
`OWL.Closure`	`lemma_all_keys_match_shares_approx`	`OWL.RL.Refinement`	`all_keys_match`	`ig_wf_sp`, `shares_key_values_approx`	no (has `requires`)
`OWL.Closure`	`owl_rule_prp_key_licensed`	`OWL.RL.Refinement`	`owl_rule_prp_key`	`ig_wf_sp`, `prp_key_licensed`	no (has `requires`)
`OWL.Closure`	`theorem_prp_key_licensed`	`OWL.RL.Refinement`	`owl_rule_prp_key`	`ig_wf_sp`, `prp_key_derives_approx`	no (has `requires`)
`OWL.Closure`	`lemma_prp_fp_derives_intro`	`OWL.RL.Refinement`	`owl_sameAs`	`fp_from_decl`, `prp_fp_derives`	no (has `requires`)
`OWL.Closure`	`owl_rule_functional_licensed`	`OWL.RL.Refinement`	`owl_rule_functional`	`ig_wf_sp`, `prp_fp_licensed`	no (has `requires`)
`OWL.Closure`	`theorem_functional_licensed`	`OWL.RL.Refinement`	`owl_rule_functional`	`ig_wf_sp`, `prp_fp_derives`	no (has `requires`)
`OWL.Closure`	`lemma_prp_ifp_derives_intro`	`OWL.RL.Refinement`	`owl_sameAs`	`ifp_from_decl`, `prp_ifp_derives`	no (has `requires`)
`OWL.Closure`	`owl_rule_inverse_functional_licensed`	`OWL.RL.Refinement`	`owl_rule_inverse_functional`	`graph_literal_match_exact`, `ig_wf_po`, `ig_wf_pred`, `prp_ifp_licensed`	no (has `requires`)
`OWL.Closure`	`theorem_inverse_functional_licensed`	`OWL.RL.Refinement`	`owl_rule_inverse_functional`	`graph_literal_match_exact`, `ig_wf_po`, `ig_wf_pred`, `prp_ifp_derives`	no (has `requires`)
`OWL.Closure`	`lemma_cls_hv1_row_intro`	`OWL.RL.Refinement`	`find_subjects_indexed`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_hv1_derives`, `ig_wf_po`	no (has `requires`)
`OWL.Closure`	`lemma_cls_hv1_members_fold`	`OWL.RL.Refinement`	`find_subjects_indexed`, `owl_cls_hv1_emit`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_hv1_licensed`, `ig_wf_po`	no (has `requires`)
`OWL.Closure`	`lemma_cls_hv1_mid_step`	`OWL.RL.Refinement`	`find_objects_indexed`, `owl_cls_hv1_mid`, `owl_hasValue_iri`, `owl_onProperty_iri`	`cls_hv1_licensed`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_cls_hv1_licensed`	`OWL.RL.Refinement`	`owl_rule_cls_hv1`	`cls_hv1_licensed`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`theorem_cls_hv1_licensed`	`OWL.RL.Refinement`	`owl_rule_cls_hv1`	`cls_hv1_derives`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_cls_hv2_licensed`	`OWL.RL.Refinement`	`owl_rule_cls_hv2`	`cls_hv2_licensed`, `ig_wf_po`, `ig_wf_pred`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`theorem_cls_hv2_licensed`	`OWL.RL.Refinement`	`owl_rule_cls_hv2`	`cls_hv2_derives_approx`, `ig_wf_po`, `ig_wf_pred`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`lemma_decode_chain_pair_licensed`	`OWL.RL.Refinement`	`decode_chain_pair`	`ig_wf_sp`, `owl_list_denotes`	no (has `requires`)
`OWL.Closure`	`lemma_prp_spo2_row_intro`	`OWL.RL.Refinement`	`find_objects_indexed`, `owl_propertyChainAxiom`	`ig_wf_sp`, `owl_list_denotes`, `prp_spo2_derives`	no (has `requires`)
`OWL.Closure`	`lemma_prp_spo2_mid_step`	`OWL.RL.Refinement`	`owl_chain2_mid`, `owl_propertyChainAxiom`	`ig_wf_sp`, `owl_list_denotes`, `prp_spo2_licensed`	no (has `requires`)
`OWL.Closure`	`owl_rule_property_chain_2_licensed`	`OWL.RL.Refinement`	`owl_rule_property_chain_2`	`ig_wf_sp`, `prp_spo2_licensed`	no (has `requires`)
`OWL.Closure`	`theorem_property_chain_2_licensed`	`OWL.RL.Refinement`	`owl_rule_property_chain_2`	`ig_wf_sp`, `prp_spo2_derives`	no (has `requires`)
`OWL.Closure`	`lemma_cls_avf_row_intro`	`OWL.RL.Refinement`	`find_objects_indexed`, `find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_avf_derives`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`lemma_cls_avf_member_step`	`OWL.RL.Refinement`	`find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_cls_avf1_member`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_avf_licensed`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`lemma_cls_avf_prop_step`	`OWL.RL.Refinement`	`find_objects_indexed`, `owl_allValuesFrom_iri`, `owl_cls_avf1_prop`, `owl_onProperty_iri`	`cls_avf_licensed`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_cls_avf1_licensed`	`OWL.RL.Refinement`	`owl_rule_cls_avf1`	`cls_avf_licensed`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`theorem_cls_avf1_licensed`	`OWL.RL.Refinement`	`owl_rule_cls_avf1`	`cls_avf_derives`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`theorem_cax_adc_cax_dw_detection_sound`	`OWL.RL.Refinement`	`owl_has_disjoint_class_clash`	`rdf_type_objects_resource`, `table6_clashes`	no (has `requires`)
`OWL.Closure`	`owl_rule_symmetric_property_sound`	`OWL.Semantics.Soundness`	`owl_rule_symmetric_property`	`cond_symmetric`, `holds_all`	no (has `requires`)
`OWL.Closure`	`lemma_sameas_pairs_hold`	`OWL.Semantics.Soundness`	`sameas_pairs`	`holds_all`, `sameas_pairs_hold`	no (has `requires`)
`OWL.Closure`	`owl_rule_sameAs_symmetry_sound`	`OWL.Semantics.Soundness`	`owl_rule_sameAs_symmetry`	`cond_sameas_identity`, `holds_all`	no (has `requires`)
`OWL.Closure`	`decode_iri_list_sound`	`OWL.Semantics.Soundness`	`decode_iri_list`	`holds_all`, `ig_wf_sp`, `seq_is`	no (has `requires`)
`OWL.Closure`	`owl_rule_cls_oneof_sound`	`OWL.Semantics.Soundness`	`owl_rule_cls_oneof`	`cond_oneof`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_equivalent_class_sound`	`OWL.Semantics.Soundness`	`owl_rule_equivalent_class`	`cond_equivalent_class`, `holds_all`	no (has `requires`)
`OWL.Closure`	`owl_rule_equivalent_property_sound`	`OWL.Semantics.Soundness`	`owl_rule_equivalent_property`	`cond_equivalent_property`, `holds_all`	no (has `requires`)
`OWL.Closure`	`owl_rule_sameAs_reflexivity_sound`	`OWL.Semantics.Soundness`	`owl_rule_sameAs_reflexivity`	`cond_sameas_reflexive`, `holds_all`	no (has `requires`)
`OWL.Closure`	`owl_rule_differentFrom_symmetry_sound`	`OWL.Semantics.Soundness`	`owl_rule_differentFrom_symmetry`	`cond_differentfrom_symmetric`, `holds_all`	no (has `requires`)
`OWL.Closure`	`owl_rule_disjoint_with_propagation_sound`	`OWL.Semantics.Soundness`	`owl_rule_disjoint_with_propagation`	`cond_complementof_disjoint`, `cond_disjointwith_symmetric`, `holds_all`	no (has `requires`)
`OWL.Closure`	`owl_rule_symmetric_metapredicates_sound`	`OWL.Semantics.Soundness`	`owl_rule_symmetric_metapredicates`	`cond_complementof_symmetric`, `cond_disjointwith_symmetric`, `cond_equivalentclass_symmetric`, `cond_equivalentproperty_symmetric`, `cond_inverseof_symmetric`, `cond_propertydisjointwith_symmetric`, `holds_all`	no (has `requires`)
`OWL.Closure`	`decode_chain_pair_sound`	`OWL.Semantics.Soundness`	`decode_chain_pair`	`holds_all`, `ig_wf_sp`, `seq_is`	no (has `requires`)
`OWL.Closure`	`owl_rule_chain_to_transitive_sound`	`OWL.Semantics.Soundness`	`owl_rule_chain_to_transitive`	`cond_chain2_transitive`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_scm_cls_restriction_sound`	`OWL.Semantics.Soundness`	`owl_rule_scm_cls_restriction`	`cond_restriction_subclass_of_class`, `holds_all`	no (has `requires`)
`OWL.Closure`	`owl_rule_scm_eqc2_sound`	`OWL.Semantics.Soundness`	`owl_rule_scm_eqc2`	`cond_mutual_subclass_equivalent`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_sameAs_replace_subject_sound`	`OWL.Semantics.Soundness`	`owl_rule_sameAs_replace_subject`	`cond_sameas_identity`, `holds_all`, `ig_wf_subj`	no (has `requires`)
`OWL.Closure`	`owl_rule_sameAs_replace_object_sound`	`OWL.Semantics.Soundness`	`owl_rule_sameAs_replace_object`	`cond_sameas_identity`, `holds_all`, `ig_wf_obj`	no (has `requires`)
`OWL.Closure`	`owl_rule_sameAs_replace_predicate_sound`	`OWL.Semantics.Soundness`	`owl_rule_sameAs_replace_predicate`	`cond_sameas_identity`, `holds_all`, `ig_wf_pred`	no (has `requires`)
`OWL.Closure`	`owl_rule_scm_eqp2_sound`	`OWL.Semantics.Soundness`	`owl_rule_scm_eqp2`	`cond_mutual_subproperty_equivalent`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_sameAs_transitivity_sound`	`OWL.Semantics.Soundness`	`owl_rule_sameAs_transitivity`	`cond_sameas_identity`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_transitive_property_sound`	`OWL.Semantics.Soundness`	`owl_rule_transitive_property`	`cond_transitive`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_functional_sound`	`OWL.Semantics.Soundness`	`owl_rule_functional`	`cond_functional`, `cond_sameas_identity`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_inverse_functional_sound`	`OWL.Semantics.Soundness`	`owl_rule_inverse_functional`	`cond_inverse_functional`, `cond_sameas_identity`, `graph_literal_match_exact`, `holds_all`, `ig_wf_po`, `ig_wf_pred`	no (has `requires`)
`OWL.Closure`	`owl_rule_inverse_of_sound`	`OWL.Semantics.Soundness`	`owl_rule_inverse_of`	`cond_inverse_of`, `holds_all`	no (has `requires`)
`OWL.Closure`	`owl_rule_prp_key_sound`	`OWL.Semantics.Soundness`	`owl_rule_prp_key`	`cond_haskey`, `cond_literal_term_eq_respecting`, `cond_sameas_identity`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_scm_dom2_sound`	`OWL.Semantics.Soundness`	`owl_rule_scm_dom2`	`cond_domain_subclass`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_scm_rng2_sound`	`OWL.Semantics.Soundness`	`owl_rule_scm_rng2`	`cond_range_subclass`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_subprop_domain_range_sound`	`OWL.Semantics.Soundness`	`owl_rule_subprop_domain_range`	`cond_domain_subprop`, `cond_range_subprop`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_cls_int1_sound`	`OWL.Semantics.Soundness`	`owl_rule_cls_int1`	`cond_intersection_of`, `holds_all`, `ig_wf_po_spec`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_cls_uni_sound`	`OWL.Semantics.Soundness`	`owl_rule_cls_uni`	`cond_union_of`, `holds_all`, `ig_wf_sp`, `no_disjoint_union`	no (has `requires`)
`OWL.Closure`	`lemma_cls_hv1_witness_holds`	`OWL.Semantics.Soundness`	`find_subjects_indexed`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_hasvalue`, `holds_all`, `ig_wf_po`, `triple_holds`	no (has `requires`)
`OWL.Closure`	`lemma_cls_hv1_members_fold_sound`	`OWL.Semantics.Soundness`	`find_subjects_indexed`, `owl_cls_hv1_emit`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_hasvalue`, `holds_all`, `ig_wf_po`	no (has `requires`)
`OWL.Closure`	`lemma_cls_hv1_mid_step_sound`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `owl_cls_hv1_mid`, `owl_hasValue_iri`, `owl_onProperty_iri`	`cond_hasvalue`, `holds_all`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_cls_hv1_sound`	`OWL.Semantics.Soundness`	`owl_rule_cls_hv1`	`cond_hasvalue`, `holds_all`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`lemma_cls_hv2_witness_holds`	`OWL.Semantics.Soundness`	`find_subjects_indexed`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_hasvalue`, `cond_literal_term_eq_respecting`, `holds_all`, `ig_wf_po`, `ig_wf_pred`, `triple_holds`	no (has `requires`)
`OWL.Closure`	`owl_rule_cls_hv2_sound`	`OWL.Semantics.Soundness`	`owl_rule_cls_hv2`	`cond_hasvalue`, `cond_literal_term_eq_respecting`, `holds_all`, `ig_wf_po`, `ig_wf_pred`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`lemma_cls_avf_witness_holds`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`, `term_to_subject`	`cond_allvaluesfrom`, `holds_all`, `ig_wf_po`, `ig_wf_sp`, `triple_holds`	no (has `requires`)
`OWL.Closure`	`lemma_cls_avf_member_fold_sound`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_cls_avf1_emit`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_allvaluesfrom`, `holds_all`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`lemma_cls_avf_prop_step_sound`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `owl_allValuesFrom_iri`, `owl_cls_avf1_prop`, `owl_onProperty_iri`	`cond_allvaluesfrom`, `holds_all`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_cls_avf1_sound`	`OWL.Semantics.Soundness`	`owl_rule_cls_avf1`	`cond_allvaluesfrom`, `holds_all`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`lemma_prp_spo2_witness_holds`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `owl_propertyChainAxiom`, `term_to_subject`	`cond_chain2_compose`, `holds_all`, `ig_wf_sp`, `seq_is`, `triple_holds`	no (has `requires`)
`OWL.Closure`	`lemma_prp_spo2_mid_step_sound`	`OWL.Semantics.Soundness`	`owl_chain2_mid`, `owl_propertyChainAxiom`, `term_to_subject`	`cond_chain2_compose`, `holds_all`, `ig_wf_sp`, `seq_is`	no (has `requires`)
`OWL.Closure`	`owl_rule_property_chain_2_sound`	`OWL.Semantics.Soundness`	`owl_rule_property_chain_2`	`cond_chain2_compose`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`OWL.Closure`	`owl_rule_symmetric_property_entailed`	`OWL.Semantics.Soundness`	`owl_rule_symmetric_property`	`pilot_entails`	yes
`OWL.Closure`	`owl_rule_sameAs_symmetry_entailed`	`OWL.Semantics.Soundness`	`build_indexed`, `owl_rule_sameAs_symmetry`	`pilot_entails`	yes
`OWL.Closure`	`owl_rule_cls_oneof_entailed`	`OWL.Semantics.Soundness`	`build_indexed`, `owl_rule_cls_oneof`	`ig_wf_sp`, `pilot_entails`	no (has `requires`)
`Parser.NTriples`	`entails_ntriples_boundary`	`RDF.Entailment.Simple.Boundary`	`parse_ntriples_strict`	`graph_exact`, `simple_entailment_spec`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_pre_dedup_clean`	`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure_step_pre_dedup`	`graph_clean`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_pre_dedup_no_dup_keys`	`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure_step_pre_dedup`	`graph_clean`, `no_dup_keys`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_step_clean`	`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure_step`	`graph_clean`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_closure_iter_clean`	`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure_iter`	`graph_clean`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_closure_extensive_aux`	`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure`	`is_subgraph`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure_extensive`	`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure`	`graph_clean`, `is_subgraph`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure_extensive_chain`	`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure`	`is_subgraph`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_step_sound`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step`	`holds_all`, `ig_wf_sp`, `rho_df_conditions`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_closure_sound_aux`	`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure`	`holds_all`, `rho_df_conditions`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_f1_bad_triple_derived`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `f1_bad_triple`, `f1_witness`, `i_rdfs_subPropertyOf`, `rdfs_rule_subPropertyOf`	`ig_wf_sp`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_frag_preservation_fails`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `f1_bad_triple`, `f1_witness`, `i_rdfs_subPropertyOf`, `rdfs_rule_subPropertyOf`	`ig_wf_sp`, `rho_df_frag_graph`, `rho_df_frag_triple`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_closed_row_domain`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rdfs2_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_closed_row_range`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rdfs3_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_closed_row_subPropertyOf`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rdfs7_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_closed_row_subClassOf_trans`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rdfs11_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_closed_row_subPropertyOf_trans`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rdfs5_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_closed_row_subClassOf`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rdfs9_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure_closed`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `graph_len`, `rho_df_closure`, `rho_df_closure_step`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rho_df_closed`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure_decides`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `graph_len`, `rho_df_closure`, `rho_df_closure_step`, `rho_df_closure_step_pre_dedup`	`graph_tt_free`, `ig_wf_sp`, `no_dup_keys`, `rho_df_entails`, `rho_df_frag_graph`, `simple_entailment_spec`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_decides_hyps_suffices`	`SPARQL11.EntailmentRegime.RDFS`	`rho_df_closure`	`graph_tt_free`, `rho_df_decides_hyps`, `rho_df_entails`, `simple_entailment_spec`	no (has `requires`)
`RDF.Entailment.Simple`	`simple_entails_rename_invariant`	`RDF.Entailment.Simple.Boundary`	`simple_entails`	`graph_exact`	no (has `requires`)
`RDF.Entailment.Simple`	`simple_entails_iff_model_theory`	`RDF.Entailment.Simple.ModelTheory`	`simple_entails`	`graph_exact`, `graph_tt_free`, `simple_entails_mt`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_match_subj_complete`	`RDF.Entailment.Simple.Refinement`	`match_subj`	`binding_compat`, `subj_inst`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_match_term_complete`	`RDF.Entailment.Simple.Refinement`	`match_term`	`binding_compat`, `bnd_total`, `leq_reflexive`, `term_inst`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_match_triple_complete`	`RDF.Entailment.Simple.Refinement`	`match_triple`	`binding_compat`, `bnd_total`, `leq_reflexive`, `triple_inst`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_try_alts_complete`	`RDF.Entailment.Simple.Refinement`	`try_alts`	`all_matched`, `binding_compat`, `bnd_total`, `leq_reflexive`, `triple_inst`	no (has `requires`)
`RDF.Entailment.Simple`	`simple_entails_complete`	`RDF.Entailment.Simple.Refinement`	`simple_entails`	`simple_entailment_spec`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_match_subj_sound`	`RDF.Entailment.Simple.Refinement`	`match_subj`	`binding_exact`, `binding_extends`, `subj_inst`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_match_term_sound`	`RDF.Entailment.Simple.Refinement`	`match_term`	`binding_exact`, `binding_extends`, `leq_exact_identity`, `term_exact`, `term_inst`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_match_triple_sound`	`RDF.Entailment.Simple.Refinement`	`match_triple`	`binding_exact`, `binding_extends`, `leq_exact_identity`, `triple_exact`, `triple_inst`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_try_match_sound`	`RDF.Entailment.Simple.Refinement`	`try_match`	`binding_exact`, `graph_exact`, `leq_exact_identity`, `search_witness`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_try_alts_sound`	`RDF.Entailment.Simple.Refinement`	`try_alts`	`binding_exact`, `graph_exact`, `is_subgraph`, `leq_exact_identity`, `search_witness`, `triple_exact`	no (has `requires`)
`RDF.Entailment.Simple`	`simple_entails_sound`	`RDF.Entailment.Simple.Refinement`	`simple_entails`	`graph_exact`, `simple_entailment_spec`	no (has `requires`)
`RDF.Entailment.Simple`	`entails_with_complete`	`RDF.Entailment.Simple.Refinement`	`entails_with`	`bnd_total`, `leq_reflexive`, `simple_entailment_spec`	no (has `requires`)
`RDF.Entailment.Simple`	`entails_with_sound`	`RDF.Entailment.Simple.Refinement`	`entails_with`	`graph_exact`, `leq_exact_identity`, `simple_entailment_spec`	no (has `requires`)
`RDF.Entailment.Simple`	`simple_entails_iff_spec`	`RDF.Entailment.Simple.Refinement`	`simple_entails`	`graph_exact`, `simple_entailment_spec`	no (has `requires`)
`RDF.Entailment.Simple`	`simple_entails_se1_regression`	`RDF.Entailment.Simple.Refinement`	`simple_entails`	`simple_entailment_spec`	no (has `requires`)
`RDF.Entailment.Simple`	`simple_entails_se1_positive_regression`	`RDF.Entailment.Simple.Refinement`	`simple_entails`	`simple_entailment_spec`	yes
`RDF.Entailment.Simple`	`lemma_try_match_ground_sound`	`RDF.Entailment.Simple.Refinement`	`try_match`	`graph_ground`, `is_subgraph`, `leq_always_identity`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_try_alts_ground_sound`	`RDF.Entailment.Simple.Refinement`	`try_alts`	`graph_ground`, `is_subgraph`, `leq_always_identity`	no (has `requires`)
`RDF.Entailment.Simple`	`simple_entails_sound_ground`	`RDF.Entailment.Simple.Refinement`	`simple_entails`	`graph_ground`, `simple_entailment_spec`	no (has `requires`)
`RDF.Graph`	`lemma_single_add_licensed`	`OWL.RL.Refinement`	`add_triple_unchecked`	`cls_disjoint_union_ext_derives`, `cls_uni_licensed`, `scm_uni_derives`	no (has `requires`)
`RDF.Graph`	`lemma_find_subjects_indexed_wf_subj`	`OWL.RL.Refinement`	`find_subjects_indexed`, `subject_to_term`	`ig_wf_po`	no (has `requires`)
`RDF.Graph`	`lemma_cls_hv1_row_intro`	`OWL.RL.Refinement`	`find_subjects_indexed`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_hv1_derives`, `ig_wf_po`	no (has `requires`)
`RDF.Graph`	`lemma_cls_hv1_members_fold`	`OWL.RL.Refinement`	`find_subjects_indexed`, `owl_cls_hv1_emit`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_hv1_licensed`, `ig_wf_po`	no (has `requires`)
`RDF.Graph`	`lemma_cls_avf_row_intro`	`OWL.RL.Refinement`	`find_objects_indexed`, `find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_avf_derives`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDF.Graph`	`lemma_cls_avf_member_step`	`OWL.RL.Refinement`	`find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_cls_avf1_member`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_avf_licensed`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDF.Graph`	`lemma_cls_hv1_witness_holds`	`OWL.Semantics.Soundness`	`find_subjects_indexed`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_hasvalue`, `holds_all`, `ig_wf_po`, `triple_holds`	no (has `requires`)
`RDF.Graph`	`lemma_cls_hv1_members_fold_sound`	`OWL.Semantics.Soundness`	`find_subjects_indexed`, `owl_cls_hv1_emit`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_hasvalue`, `holds_all`, `ig_wf_po`	no (has `requires`)
`RDF.Graph`	`lemma_cls_hv2_witness_holds`	`OWL.Semantics.Soundness`	`find_subjects_indexed`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_hasvalue`, `cond_literal_term_eq_respecting`, `holds_all`, `ig_wf_po`, `ig_wf_pred`, `triple_holds`	no (has `requires`)
`RDF.Graph`	`lemma_cls_avf_witness_holds`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`, `term_to_subject`	`cond_allvaluesfrom`, `holds_all`, `ig_wf_po`, `ig_wf_sp`, `triple_holds`	no (has `requires`)
`RDF.Graph`	`lemma_cls_avf_member_fold_sound`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_cls_avf1_emit`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_allvaluesfrom`, `holds_all`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDF.Graph`	`lemma_prp_spo2_witness_holds`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `owl_propertyChainAxiom`, `term_to_subject`	`cond_chain2_compose`, `holds_all`, `ig_wf_sp`, `seq_is`, `triple_holds`	no (has `requires`)
`RDF.Graph`	`lemma_prp_spo2_mid_step_sound`	`OWL.Semantics.Soundness`	`owl_chain2_mid`, `owl_propertyChainAxiom`, `term_to_subject`	`cond_chain2_compose`, `holds_all`, `ig_wf_sp`, `seq_is`	no (has `requires`)
`RDF.Graph`	`lemma_len_eq_saturated_sep_free`	`RDF.Entailment.RDFS.FixedPoint`	`graph_len`, `rdfs_closure_step`	`graph_obj_not_tt`, `graph_sep_free`, `step_saturated`	no (has `requires`)
`RDF.Graph`	`lemma_add_triples_if_new_holds`	`RDF.Entailment.RDFS.ModelTheory`	`add_triples_if_new`	`holds_all`	no (has `requires`)
`RDF.Graph`	`rs2_rows_complete_at_build_indexed`	`RDF.Entailment.RDFS.Refinement`	`build_indexed`, `is_typed_as`, `rdf_type`, `rdfs_Class`, `rdfs_Datatype`, `rdfs_Literal`, `rdfs_Resource`, `rdfs_rule_class_subclass_resource`, `rdfs_rule_datatype_subclass_literal`, `rdfs_rule_recognized_datatypes`, `rdfs_rule_resource_object`, `rdfs_rule_resource_subject`, `rdfs_subClassOf`, `recognized_datatypes`, `term_to_subject`	`ig_wf_sp`	no (has `requires`)
`RDF.Graph`	`rho_df_closure_closed`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `graph_len`, `rho_df_closure`, `rho_df_closure_step`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rho_df_closed`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Graph`	`rho_df_closure_decides`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `graph_len`, `rho_df_closure`, `rho_df_closure_step`, `rho_df_closure_step_pre_dedup`	`graph_tt_free`, `ig_wf_sp`, `no_dup_keys`, `rho_df_entails`, `rho_df_frag_graph`, `simple_entailment_spec`	no (has `requires`)
`RDF.Indexed`	`lemma_find_objects_indexed_sp_elim`	`OWL.RL.Refinement`	`find_objects_indexed`	`ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`lemma_scm_eqc2_emission_licensed`	`OWL.RL.Refinement`	`find_objects_indexed`, `owl_equivalentClass`, `rdfs_subClassOf`, `term_is_iri`	`ig_wf_sp`, `scm_eqc2_derives`	no (has `requires`)
`RDF.Indexed`	`lemma_scm_eqp2_emission_licensed`	`OWL.RL.Refinement`	`find_objects_indexed`, `owl_equivalentProperty`, `rdfs_subPropertyOf`, `term_is_iri`	`ig_wf_sp`, `scm_eqp2_derives`	no (has `requires`)
`RDF.Indexed`	`lemma_find_subjects_indexed_wf`	`OWL.RL.Refinement`	`find_subjects_indexed`	`graph_literal_match_exact`, `ig_wf_po`, `ig_wf_pred`	no (has `requires`)
`RDF.Indexed`	`lemma_find_subjects_indexed_wf_subj`	`OWL.RL.Refinement`	`find_subjects_indexed`, `subject_to_term`	`ig_wf_po`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_hv1_row_intro`	`OWL.RL.Refinement`	`find_subjects_indexed`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_hv1_derives`, `ig_wf_po`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_hv1_members_fold`	`OWL.RL.Refinement`	`find_subjects_indexed`, `owl_cls_hv1_emit`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_hv1_licensed`, `ig_wf_po`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_hv1_mid_step`	`OWL.RL.Refinement`	`find_objects_indexed`, `owl_cls_hv1_mid`, `owl_hasValue_iri`, `owl_onProperty_iri`	`cls_hv1_licensed`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`lemma_find_subjects_indexed_wf_approx`	`OWL.RL.Refinement`	`find_subjects_indexed`, `rdf_term_eq`	`ig_wf_po`, `ig_wf_pred`	no (has `requires`)
`RDF.Indexed`	`lemma_prp_spo2_row_intro`	`OWL.RL.Refinement`	`find_objects_indexed`, `owl_propertyChainAxiom`	`ig_wf_sp`, `owl_list_denotes`, `prp_spo2_derives`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_avf_row_intro`	`OWL.RL.Refinement`	`find_objects_indexed`, `find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_avf_derives`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_avf_member_step`	`OWL.RL.Refinement`	`find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_cls_avf1_member`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_avf_licensed`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_avf_prop_step`	`OWL.RL.Refinement`	`find_objects_indexed`, `owl_allValuesFrom_iri`, `owl_cls_avf1_prop`, `owl_onProperty_iri`	`cls_avf_licensed`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_hv1_witness_holds`	`OWL.Semantics.Soundness`	`find_subjects_indexed`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_hasvalue`, `holds_all`, `ig_wf_po`, `triple_holds`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_hv1_members_fold_sound`	`OWL.Semantics.Soundness`	`find_subjects_indexed`, `owl_cls_hv1_emit`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_hasvalue`, `holds_all`, `ig_wf_po`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_hv1_mid_step_sound`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `owl_cls_hv1_mid`, `owl_hasValue_iri`, `owl_onProperty_iri`	`cond_hasvalue`, `holds_all`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_hv2_witness_holds`	`OWL.Semantics.Soundness`	`find_subjects_indexed`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_hasvalue`, `cond_literal_term_eq_respecting`, `holds_all`, `ig_wf_po`, `ig_wf_pred`, `triple_holds`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_avf_witness_holds`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`, `term_to_subject`	`cond_allvaluesfrom`, `holds_all`, `ig_wf_po`, `ig_wf_sp`, `triple_holds`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_avf_member_fold_sound`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_cls_avf1_emit`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_allvaluesfrom`, `holds_all`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`lemma_cls_avf_prop_step_sound`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `owl_allValuesFrom_iri`, `owl_cls_avf1_prop`, `owl_onProperty_iri`	`cond_allvaluesfrom`, `holds_all`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`lemma_prp_spo2_witness_holds`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `owl_propertyChainAxiom`, `term_to_subject`	`cond_chain2_compose`, `holds_all`, `ig_wf_sp`, `seq_is`, `triple_holds`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_domain_entailed`	`OWL.Semantics.Soundness`	`build_indexed`, `rdfs_rule_domain`	`pilot_entails`	yes
`RDF.Indexed`	`rdfs_rule_range_entailed`	`OWL.Semantics.Soundness`	`build_indexed`, `rdfs_rule_range`	`pilot_entails`	yes
`RDF.Indexed`	`owl_rule_sameAs_symmetry_entailed`	`OWL.Semantics.Soundness`	`build_indexed`, `owl_rule_sameAs_symmetry`	`pilot_entails`	yes
`RDF.Indexed`	`owl_rule_cls_oneof_entailed`	`OWL.Semantics.Soundness`	`build_indexed`, `owl_rule_cls_oneof`	`ig_wf_sp`, `pilot_entails`	no (has `requires`)
`RDF.Indexed`	`lemma_closure_chain_wf_step`	`RDF.Entailment.RDFS.ChainWf`	`build_indexed`	`graph_sep_free`, `ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`lemma_rdfs_rule_subPropertyOf_clean`	`RDF.Entailment.RDFS.FixedPoint`	`build_indexed`, `rdfs_rule_subPropertyOf`	`graph_clean`	no (has `requires`)
`RDF.Indexed`	`lemma_rdfs_rule_domain_clean`	`RDF.Entailment.RDFS.FixedPoint`	`build_indexed`, `rdfs_rule_domain`	`graph_clean`	no (has `requires`)
`RDF.Indexed`	`lemma_rdfs_rule_range_clean`	`RDF.Entailment.RDFS.FixedPoint`	`build_indexed`, `rdfs_rule_range`	`graph_clean`	no (has `requires`)
`RDF.Indexed`	`lemma_rdfs_rule_subClassOf_clean`	`RDF.Entailment.RDFS.FixedPoint`	`build_indexed`, `rdfs_rule_subClassOf`	`graph_clean`	no (has `requires`)
`RDF.Indexed`	`lemma_rdfs_rule_subClassOf_trans_clean`	`RDF.Entailment.RDFS.FixedPoint`	`build_indexed`, `rdfs_rule_subClassOf_trans`	`graph_clean`	no (has `requires`)
`RDF.Indexed`	`lemma_rdfs_rule_subPropertyOf_trans_clean`	`RDF.Entailment.RDFS.FixedPoint`	`build_indexed`, `rdfs_rule_subPropertyOf_trans`	`graph_clean`	no (has `requires`)
`RDF.Indexed`	`rdfs_closure_step_sound`	`RDF.Entailment.RDFS.ModelTheory`	`build_indexed`, `rdfs_closure_step`	`holds_all`, `ig_wf_sp`, `rdfs_conditions`	no (has `requires`)
`RDF.Indexed`	`lemma_find_objects_elim`	`RDF.Entailment.RDFS.Refinement`	`find_objects_indexed`	`ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`rs2_rows_complete_at_build_indexed`	`RDF.Entailment.RDFS.Refinement`	`build_indexed`, `is_typed_as`, `rdf_type`, `rdfs_Class`, `rdfs_Datatype`, `rdfs_Literal`, `rdfs_Resource`, `rdfs_rule_class_subclass_resource`, `rdfs_rule_datatype_subclass_literal`, `rdfs_rule_recognized_datatypes`, `rdfs_rule_resource_object`, `rdfs_rule_resource_subject`, `rdfs_subClassOf`, `recognized_datatypes`, `term_to_subject`	`ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`lemma_rho_df_step_sound`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step`	`holds_all`, `ig_wf_sp`, `rho_df_conditions`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_domain_reaches2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`	`ig_wf_sp`, `is_subgraph`, `rdfs2_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_domain_reaches`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`	`ig_wf_sp`, `rdfs2_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_range_reaches2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_range`	`ig_wf_sp`, `is_subgraph`, `rdfs3_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_range_reaches`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_range`	`ig_wf_sp`, `rdfs3_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_subPropertyOf_reaches2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf`	`ig_wf_sp`, `is_subgraph`, `rdfs7_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_subPropertyOf_reaches`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf`	`ig_wf_sp`, `rdfs7_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_subClassOf_trans_reaches2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subClassOf_trans`	`ig_wf_sp`, `is_subgraph`, `rdfs11_derives`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_subClassOf_trans_reaches`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subClassOf_trans`	`ig_wf_sp`, `rdfs11_derives`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_subPropertyOf_trans_reaches2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf_trans`	`ig_wf_sp`, `is_subgraph`, `rdfs5_derives`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_subPropertyOf_trans_reaches`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf_trans`	`ig_wf_sp`, `rdfs5_derives`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_subClassOf_reaches_iri2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `i_rdf_type`, `i_rdfs_subClassOf`, `rdfs_rule_subClassOf`	`ig_wf_sp`, `is_subgraph`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`rdfs_rule_subClassOf_reaches_iri`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `i_rdf_type`, `i_rdfs_subClassOf`, `rdfs_rule_subClassOf`	`ig_wf_sp`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`lemma_f1_bad_triple_derived`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `f1_bad_triple`, `f1_witness`, `i_rdfs_subPropertyOf`, `rdfs_rule_subPropertyOf`	`ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`rho_df_frag_preservation_fails`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `f1_bad_triple`, `f1_witness`, `i_rdfs_subPropertyOf`, `rdfs_rule_subPropertyOf`	`ig_wf_sp`, `rho_df_frag_graph`, `rho_df_frag_triple`	no (has `requires`)
`RDF.Indexed`	`lemma_c_in_g1`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf`	`is_subgraph`	no (has `requires`)
`RDF.Indexed`	`lemma_c_in_g2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_subPropertyOf`	`is_subgraph`	no (has `requires`)
`RDF.Indexed`	`lemma_c_in_g3`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subPropertyOf`	`is_subgraph`	no (has `requires`)
`RDF.Indexed`	`lemma_c_in_g4`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subClassOf`, `rdfs_rule_subPropertyOf`	`is_subgraph`	no (has `requires`)
`RDF.Indexed`	`lemma_c_in_g5`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subClassOf`, `rdfs_rule_subClassOf_trans`, `rdfs_rule_subPropertyOf`	`is_subgraph`	no (has `requires`)
`RDF.Indexed`	`lemma_rho_df_closed_row_domain`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rdfs2_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`lemma_rho_df_closed_row_range`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rdfs3_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`lemma_rho_df_closed_row_subPropertyOf`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rdfs7_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`lemma_rho_df_closed_row_subClassOf_trans`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rdfs11_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`lemma_rho_df_closed_row_subPropertyOf_trans`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rdfs5_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`lemma_rho_df_closed_row_subClassOf`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rdfs9_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`rho_df_closure_closed`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `graph_len`, `rho_df_closure`, `rho_df_closure_step`, `rho_df_closure_step_pre_dedup`	`ig_wf_sp`, `no_dup_keys`, `rho_df_closed`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Indexed`	`rho_df_closure_decides`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `graph_len`, `rho_df_closure`, `rho_df_closure_step`, `rho_df_closure_step_pre_dedup`	`graph_tt_free`, `ig_wf_sp`, `no_dup_keys`, `rho_df_entails`, `rho_df_frag_graph`, `simple_entailment_spec`	no (has `requires`)
`RDF.Indexed`	`lemma_build_indexed_wf_sp`	`RDF.Indexed.KeyInjectivity`	`build_indexed`	`graph_sp_sep_free`, `ig_wf_sp`	no (has `requires`)
`RDF.Indexed`	`theorem_wf_sp_nonempty_instance`	`RDF.Indexed.KeyInjectivity`	`build_indexed`	`ig_wf_sp`	yes
`RDF.Indexed`	`lemma_build_indexed_wf_subj`	`RDF.Indexed.KeyInjectivity`	`build_indexed`	`ig_wf_subj`	yes
`RDF.Indexed`	`lemma_build_indexed_wf_obj`	`RDF.Indexed.KeyInjectivity`	`build_indexed`	`ig_wf_obj`	yes
`RDF.Indexed`	`lemma_build_indexed_wf_po`	`RDF.Indexed.KeyInjectivity`	`build_indexed`	`graph_po_sep_free`, `ig_wf_po`	no (has `requires`)
`RDF.Indexed`	`theorem_ig_wf_pred_witness`	`RDF.Semantics.HypothesisWitness`	`bucket_lookup`	`ig_wf_pred`	yes
`RDF.Indexed`	`theorem_ig_wf_sp_satisfiable_degenerately`	`RDF.Semantics.HypothesisWitness`	`bucket_lookup`, `sp_key`	`ig_wf_sp`	yes
`RDF.Indexed`	`lemma_ig_wf_sp_of_empty`	`RDF.Semantics.HypothesisWitness`	`build_indexed`	`ig_wf_sp`	yes
`RDF.Indexed`	`theorem_closure_chain_wf_n0_of_empty`	`RDF.Semantics.HypothesisWitness`	`build_indexed`	`ig_wf_sp`	yes
`RDF.List.Helpers`	`lemma_assoc_tr_congr`	`SPARQL11.Algebra.Refinement`	`assoc_tr`	`smap_eq`	no (has `requires`)
`RDF.Term`	`lemma_find_subjects_indexed_wf_approx`	`OWL.RL.Refinement`	`find_subjects_indexed`, `rdf_term_eq`	`ig_wf_po`, `ig_wf_pred`	no (has `requires`)
`RDF.Term`	`lemma_literal_eq_exact`	`RDF.Entailment.Simple.Refinement`	`literal_eq`	`lit_exact`	no (has `requires`)
`RDF.Term`	`lemma_rdf_term_eq_exact_identity`	`RDF.Entailment.Simple.Refinement`	`rdf_term_eq`	`term_exact`	no (has `requires`)
`RDF.Vocabulary.Axioms`	`lemma_selfloop_not_in_herbrand`	`RDF.Entailment.RDFS.Completeness`	`i_rdfs_subClassOf`	`herb_iext`	no (has `requires`)
`RDF.Vocabulary.Axioms`	`lemma_graph_clean_satisfiable`	`RDF.Entailment.RDFS.RhoDFClosure`	`i_rdf_type`, `i_rdfs_Class`, `i_rdfs_Resource`	`graph_clean`	yes
`RDF.Vocabulary.Axioms`	`rdfs_rule_subClassOf_reaches_iri2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `i_rdf_type`, `i_rdfs_subClassOf`, `rdfs_rule_subClassOf`	`ig_wf_sp`, `is_subgraph`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Vocabulary.Axioms`	`rdfs_rule_subClassOf_reaches_iri`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `i_rdf_type`, `i_rdfs_subClassOf`, `rdfs_rule_subClassOf`	`ig_wf_sp`, `rho_df_frag_graph`	no (has `requires`)
`RDF.Vocabulary.Axioms`	`lemma_f1_bad_triple_derived`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `f1_bad_triple`, `f1_witness`, `i_rdfs_subPropertyOf`, `rdfs_rule_subPropertyOf`	`ig_wf_sp`	no (has `requires`)
`RDF.Vocabulary.Axioms`	`rho_df_frag_preservation_fails`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `f1_bad_triple`, `f1_witness`, `i_rdfs_subPropertyOf`, `rdfs_rule_subPropertyOf`	`ig_wf_sp`, `rho_df_frag_graph`, `rho_df_frag_triple`	no (has `requires`)
`RDF.Vocabulary.Axioms`	`lemma_vocab_sep_free`	`RDF.Entailment.RDFS.SepFree`	`i_rdf_Property`, `i_rdf_type`, `i_rdfs_Class`, `i_rdfs_ContainerMembershipProperty`, `i_rdfs_Datatype`, `i_rdfs_Literal`, `i_rdfs_Resource`, `i_rdfs_domain`, `i_rdfs_member`, `i_rdfs_range`, `i_rdfs_subClassOf`, `i_rdfs_subPropertyOf`	`str_sep_free`	yes
`RDF.Vocabulary.Axioms`	`lemma_axiomatic_tables_sep_free`	`RDF.Entailment.RDFS.SepFree`	`container_membership_properties`, `rdf_axiomatic_triples`, `rdfs_axiomatic_triples`	`str_sep_free`, `triple_sep_free`	yes
`RDFS.Closure`	`lemma_scm_eqc2_emission_licensed`	`OWL.RL.Refinement`	`find_objects_indexed`, `owl_equivalentClass`, `rdfs_subClassOf`, `term_is_iri`	`ig_wf_sp`, `scm_eqc2_derives`	no (has `requires`)
`RDFS.Closure`	`lemma_scm_eqp2_emission_licensed`	`OWL.RL.Refinement`	`find_objects_indexed`, `owl_equivalentProperty`, `rdfs_subPropertyOf`, `term_is_iri`	`ig_wf_sp`, `scm_eqp2_derives`	no (has `requires`)
`RDFS.Closure`	`lemma_cls_hv1_row_intro`	`OWL.RL.Refinement`	`find_subjects_indexed`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_hv1_derives`, `ig_wf_po`	no (has `requires`)
`RDFS.Closure`	`lemma_cls_hv1_members_fold`	`OWL.RL.Refinement`	`find_subjects_indexed`, `owl_cls_hv1_emit`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_hv1_licensed`, `ig_wf_po`	no (has `requires`)
`RDFS.Closure`	`lemma_cls_avf_row_intro`	`OWL.RL.Refinement`	`find_objects_indexed`, `find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_avf_derives`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDFS.Closure`	`lemma_cls_avf_member_step`	`OWL.RL.Refinement`	`find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_cls_avf1_member`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cls_avf_licensed`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_domain_sound`	`OWL.Semantics.Soundness`	`rdfs_rule_domain`	`cond_domain`, `holds_all`, `ig_wf_pred`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_range_sound`	`OWL.Semantics.Soundness`	`rdfs_rule_range`	`cond_range`, `holds_all`, `ig_wf_pred`	no (has `requires`)
`RDFS.Closure`	`lemma_cls_hv1_witness_holds`	`OWL.Semantics.Soundness`	`find_subjects_indexed`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_hasvalue`, `holds_all`, `ig_wf_po`, `triple_holds`	no (has `requires`)
`RDFS.Closure`	`lemma_cls_hv1_members_fold_sound`	`OWL.Semantics.Soundness`	`find_subjects_indexed`, `owl_cls_hv1_emit`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_hasvalue`, `holds_all`, `ig_wf_po`	no (has `requires`)
`RDFS.Closure`	`lemma_cls_hv2_witness_holds`	`OWL.Semantics.Soundness`	`find_subjects_indexed`, `owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_hasvalue`, `cond_literal_term_eq_respecting`, `holds_all`, `ig_wf_po`, `ig_wf_pred`, `triple_holds`	no (has `requires`)
`RDFS.Closure`	`lemma_cls_avf_witness_holds`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`, `term_to_subject`	`cond_allvaluesfrom`, `holds_all`, `ig_wf_po`, `ig_wf_sp`, `triple_holds`	no (has `requires`)
`RDFS.Closure`	`lemma_cls_avf_member_fold_sound`	`OWL.Semantics.Soundness`	`find_objects_indexed`, `find_subjects_indexed`, `owl_allValuesFrom_iri`, `owl_cls_avf1_emit`, `owl_onProperty_iri`, `rdf_type`, `subject_to_term`	`cond_allvaluesfrom`, `holds_all`, `ig_wf_po`, `ig_wf_sp`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_domain_entailed`	`OWL.Semantics.Soundness`	`build_indexed`, `rdfs_rule_domain`	`pilot_entails`	yes
`RDFS.Closure`	`rdfs_rule_range_entailed`	`OWL.Semantics.Soundness`	`build_indexed`, `rdfs_rule_range`	`pilot_entails`	yes
`RDFS.Closure`	`rdfs_rule_subPropertyOf_preserves_sep`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_rule_subPropertyOf`	`graph_sep_free`, `ig_wf_pred`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_domain_preserves_sep`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_rule_domain`	`graph_sep_free`, `ig_wf_pred`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_range_preserves_sep`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_rule_range`	`graph_sep_free`, `ig_wf_pred`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subClassOf_preserves_sep`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_rule_subClassOf`	`graph_sep_free`, `ig_wf_sp`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_container_membership_preserves_sep`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_rule_container_membership`	`graph_sep_free`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subClassOf_trans_preserves_sep`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_rule_subClassOf_trans`	`graph_sep_free`, `ig_wf_sp`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subPropertyOf_trans_preserves_sep`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_rule_subPropertyOf_trans`	`graph_sep_free`, `ig_wf_sp`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_recognized_datatypes_preserves_sep`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_rule_recognized_datatypes`	`graph_sep_free`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_class_subclass_resource_preserves_sep`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_rule_class_subclass_resource`	`graph_sep_free`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_datatype_subclass_literal_preserves_sep`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_rule_datatype_subclass_literal`	`graph_sep_free`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_resource_subject_preserves_sep`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_rule_resource_subject`	`graph_sep_free`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_resource_object_preserves_sep`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_rule_resource_object`	`graph_sep_free`	no (has `requires`)
`RDFS.Closure`	`step_preserves_sep_free`	`RDF.Entailment.RDFS.ChainWf`	`rdfs_closure_step`	`graph_sep_free`	no (has `requires`)
`RDFS.Closure`	`step_domain`	`RDF.Entailment.RDFS.Completeness`	`rdf_type`, `rdfs_domain`	`herb_iext`, `rho_df_closed`	no (has `requires`)
`RDFS.Closure`	`step_range`	`RDF.Entailment.RDFS.Completeness`	`rdf_type`, `rdfs_range`	`herb_iext`, `rho_df_closed`, `rho_df_frag_graph`	no (has `requires`)
`RDFS.Closure`	`step_sub_property`	`RDF.Entailment.RDFS.Completeness`	`rdfs_subPropertyOf`	`herb_iext`, `rho_df_closed`, `rho_df_frag_graph`	no (has `requires`)
`RDFS.Closure`	`step_sub_property_trans`	`RDF.Entailment.RDFS.Completeness`	`rdfs_subPropertyOf`	`herb_iext`, `rho_df_closed`	no (has `requires`)
`RDFS.Closure`	`step_sub_class`	`RDF.Entailment.RDFS.Completeness`	`rdf_type`, `rdfs_subClassOf`	`herb_iext`, `rho_df_closed`	no (has `requires`)
`RDFS.Closure`	`step_sub_class_trans`	`RDF.Entailment.RDFS.Completeness`	`rdfs_subClassOf`	`herb_iext`, `rho_df_closed`	no (has `requires`)
`RDFS.Closure`	`rdfs_closure_rho_df_complete`	`RDF.Entailment.RDFS.Completeness`	`rdfs_closure`	`graph_tt_free`, `is_subgraph`, `rho_df_closed`, `rho_df_entails`, `rho_df_frag_graph`, `simple_entailment_spec`	no (has `requires`)
`RDFS.Closure`	`lemma_rdfs_rule_subPropertyOf_clean`	`RDF.Entailment.RDFS.FixedPoint`	`build_indexed`, `rdfs_rule_subPropertyOf`	`graph_clean`	no (has `requires`)
`RDFS.Closure`	`lemma_rdfs_rule_domain_clean`	`RDF.Entailment.RDFS.FixedPoint`	`build_indexed`, `rdfs_rule_domain`	`graph_clean`	no (has `requires`)
`RDFS.Closure`	`lemma_rdfs_rule_range_clean`	`RDF.Entailment.RDFS.FixedPoint`	`build_indexed`, `rdfs_rule_range`	`graph_clean`	no (has `requires`)
`RDFS.Closure`	`lemma_rdfs_rule_subClassOf_clean`	`RDF.Entailment.RDFS.FixedPoint`	`build_indexed`, `rdfs_rule_subClassOf`	`graph_clean`	no (has `requires`)
`RDFS.Closure`	`lemma_rdfs_rule_container_membership_clean`	`RDF.Entailment.RDFS.FixedPoint`	`rdfs_rule_container_membership`	`graph_clean`	no (has `requires`)
`RDFS.Closure`	`lemma_rdfs_rule_subClassOf_trans_clean`	`RDF.Entailment.RDFS.FixedPoint`	`build_indexed`, `rdfs_rule_subClassOf_trans`	`graph_clean`	no (has `requires`)
`RDFS.Closure`	`lemma_rdfs_rule_subPropertyOf_trans_clean`	`RDF.Entailment.RDFS.FixedPoint`	`build_indexed`, `rdfs_rule_subPropertyOf_trans`	`graph_clean`	no (has `requires`)
`RDFS.Closure`	`lemma_rdfs_rule_recognized_datatypes_clean`	`RDF.Entailment.RDFS.FixedPoint`	`rdfs_rule_recognized_datatypes`	`graph_clean`	no (has `requires`)
`RDFS.Closure`	`lemma_rdfs_rule_class_subclass_resource_clean`	`RDF.Entailment.RDFS.FixedPoint`	`rdfs_rule_class_subclass_resource`	`graph_clean`	no (has `requires`)
`RDFS.Closure`	`lemma_rdfs_rule_datatype_subclass_literal_clean`	`RDF.Entailment.RDFS.FixedPoint`	`rdfs_rule_datatype_subclass_literal`	`graph_clean`	no (has `requires`)
`RDFS.Closure`	`lemma_rdfs_rule_resource_subject_clean`	`RDF.Entailment.RDFS.FixedPoint`	`rdfs_rule_resource_subject`	`graph_clean`	no (has `requires`)
`RDFS.Closure`	`lemma_rdfs_rule_resource_object_clean`	`RDF.Entailment.RDFS.FixedPoint`	`rdfs_rule_resource_object`	`graph_clean`	no (has `requires`)
`RDFS.Closure`	`lemma_len_eq_saturated_sep_free`	`RDF.Entailment.RDFS.FixedPoint`	`graph_len`, `rdfs_closure_step`	`graph_obj_not_tt`, `graph_sep_free`, `step_saturated`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subPropertyOf_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_rule_subPropertyOf`	`cond_subPropertyOf`, `holds_all`, `ig_wf_pred`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_domain_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_rule_domain`	`cond_domain`, `holds_all`, `ig_wf_pred`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_range_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_rule_range`	`cond_range`, `holds_all`, `ig_wf_pred`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subClassOf_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_rule_subClassOf`	`cond_subClassOf`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subClassOf_trans_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_rule_subClassOf_trans`	`cond_subClassOf_trans`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subPropertyOf_trans_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_rule_subPropertyOf_trans`	`cond_subPropertyOf_trans`, `holds_all`, `ig_wf_sp`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_container_membership_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_rule_container_membership`	`cond_cmp_member`, `cond_rdfs_axioms`, `holds_all`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_recognized_datatypes_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_rule_recognized_datatypes`	`cond_datatypes_minimal`, `holds_all`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_resource_subject_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_rule_resource_subject`	`cond_resource`, `holds_all`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_resource_object_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_rule_resource_object`	`cond_resource`, `holds_all`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_class_subclass_resource_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_rule_class_subclass_resource`	`cond_class_subclass_resource`, `holds_all`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_datatype_subclass_literal_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_rule_datatype_subclass_literal`	`cond_datatype_subclass_literal`, `holds_all`	no (has `requires`)
`RDFS.Closure`	`rdfs_closure_step_sound`	`RDF.Entailment.RDFS.ModelTheory`	`build_indexed`, `rdfs_closure_step`	`holds_all`, `ig_wf_sp`, `rdfs_conditions`	no (has `requires`)
`RDFS.Closure`	`rdfs_closure_sound`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_closure`	`closure_chain_wf`, `holds_all`, `rdfs_conditions`	no (has `requires`)
`RDFS.Closure`	`rdfs_reflexivity_axioms_preserves`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_reflexivity_axioms`	`holds_all`, `rdfs_conditions`	no (has `requires`)
`RDFS.Closure`	`rdfs_closure_with_reflexivity_sound`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_closure_with_reflexivity`	`closure_chain_wf`, `holds_all`, `rdfs_conditions`	no (has `requires`)
`RDFS.Closure`	`reflexivity_needs_rdfs_Class`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_Class`, `rdfs_subClassOf`	`cond_subClassOf_refl`, `icext`	no (has `requires`)
`RDFS.Closure`	`rdf_property_axiom_closure_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdf_property_axiom_closure`	`rdfD2_derives`	yes
`RDFS.Closure`	`rdfs_rule_domain_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_domain`	`ig_wf_pred`, `licensed_by2`, `rdfs2_derives`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_range_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_range`	`ig_wf_pred`, `licensed_by2`, `rdfs3_derives`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subPropertyOf_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_subPropertyOf`	`ig_wf_pred`, `licensed_by2`, `rdfs7_derives`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subClassOf_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_subClassOf`	`ig_wf_sp`, `licensed_by2`, `rdfs9_derives2`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subClassOf_trans_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_subClassOf_trans`	`ig_wf_sp`, `licensed_by2`, `rdfs11_derives2`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subPropertyOf_trans_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_subPropertyOf_trans`	`ig_wf_sp`, `licensed_by2`, `rdfs5_derives2`	no (has `requires`)
`RDFS.Closure`	`lemma_rdf_member_iris`	`RDF.Entailment.RDFS.Refinement`	`rdf_1`, `rdf_2`, `rdf_3`, `rdf_4`, `rdf_5`	`is_rdf_member_iri`	yes
`RDFS.Closure`	`rdfs_rule_container_membership_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_container_membership`	`rdfs_axiomatic`, `rdfs_member_subproperty`	yes
`RDFS.Closure`	`rdfs_rule_recognized_datatypes_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_recognized_datatypes`	`rdfs1_derives`	yes
`RDFS.Closure`	`rdfs_rule_resource_subject_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_resource_subject`	`licensed_by`, `rdfs4a_derives`	yes
`RDFS.Closure`	`rdfs_rule_resource_object_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_resource_object`	`licensed_by`, `rdfs4b_derives`	yes
`RDFS.Closure`	`rdfs_rule_class_subclass_resource_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_class_subclass_resource`	`licensed_by`, `rdfs8_derives`	yes
`RDFS.Closure`	`rdfs_rule_datatype_subclass_literal_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_datatype_subclass_literal`	`licensed_by`, `rdfs13_derives`	yes
`RDFS.Closure`	`lemma_snapshot_carries_elim`	`RDF.Entailment.RDFS.Refinement`	`snapshot_carries`	`ig_wf_sp`	no (has `requires`)
`RDFS.Closure`	`lemma_emit_once`	`RDF.Entailment.RDFS.Refinement`	`emit_once`	`ig_wf_sp`, `snapshot_subset`	no (has `requires`)
`RDFS.Closure`	`lemma_emit_once_all`	`RDF.Entailment.RDFS.Refinement`	`emit_once`	`ig_wf_sp`, `snapshot_subset`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_recognized_datatypes_complete`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_recognized_datatypes`, `recognized_datatypes`	`ig_wf_sp`, `snapshot_subset`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_resource_subject_complete`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_resource_subject`	`ig_wf_sp`, `snapshot_subset`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_resource_object_complete`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_resource_object`	`ig_wf_sp`, `snapshot_subset`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_class_subclass_resource_complete`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_class_subclass_resource`	`ig_wf_sp`, `snapshot_subset`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_datatype_subclass_literal_complete`	`RDF.Entailment.RDFS.Refinement`	`rdfs_rule_datatype_subclass_literal`	`ig_wf_sp`, `snapshot_subset`	no (has `requires`)
`RDFS.Closure`	`rs2_rows_complete_at_build_indexed`	`RDF.Entailment.RDFS.Refinement`	`build_indexed`, `is_typed_as`, `rdf_type`, `rdfs_Class`, `rdfs_Datatype`, `rdfs_Literal`, `rdfs_Resource`, `rdfs_rule_class_subclass_resource`, `rdfs_rule_datatype_subclass_literal`, `rdfs_rule_recognized_datatypes`, `rdfs_rule_resource_object`, `rdfs_rule_resource_subject`, `rdfs_subClassOf`, `recognized_datatypes`, `term_to_subject`	`ig_wf_sp`	no (has `requires`)
`RDFS.Closure`	`lemma_class_refl_licensed`	`RDF.Entailment.RDFS.Refinement`	`is_class_type_object_rdfs`, `rdfs_subClassOf`	`harvest_source`, `rdfs_licensed`	no (has `requires`)
`RDFS.Closure`	`lemma_property_refl_licensed`	`RDF.Entailment.RDFS.Refinement`	`is_property_type_object_rdfs`, `rdfs_subPropertyOf`	`harvest_source`, `rdfs_licensed`	no (has `requires`)
`RDFS.Closure`	`rdfs_reflexivity_axioms_licensed`	`RDF.Entailment.RDFS.Refinement`	`rdfs_reflexivity_axioms`	`rdfs_licensed`	yes
`RDFS.Closure`	`owl_reflexivity_axioms_not_rdfs_sound`	`RDF.Entailment.RDFS.Refinement`	`owl_reflexivity_axioms`	`rdfs_licensed`	yes
`RDFS.Closure`	`lemma_emit_once_term_reaches`	`RDF.Entailment.RDFS.RhoDFClosure`	`emit_once_term`	`ig_wf_sp`, `rho_df_frag_graph`, `rho_df_object_ok`, `snapshot_subset`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_domain_reaches2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`	`ig_wf_sp`, `is_subgraph`, `rdfs2_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_domain_reaches`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`	`ig_wf_sp`, `rdfs2_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_range_reaches2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_range`	`ig_wf_sp`, `is_subgraph`, `rdfs3_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_range_reaches`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_range`	`ig_wf_sp`, `rdfs3_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subPropertyOf_reaches2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf`	`ig_wf_sp`, `is_subgraph`, `rdfs7_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subPropertyOf_reaches`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf`	`ig_wf_sp`, `rdfs7_derives`, `rho_df_frag_graph`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subClassOf_trans_reaches2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subClassOf_trans`	`ig_wf_sp`, `is_subgraph`, `rdfs11_derives`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subClassOf_trans_reaches`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subClassOf_trans`	`ig_wf_sp`, `rdfs11_derives`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subPropertyOf_trans_reaches2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf_trans`	`ig_wf_sp`, `is_subgraph`, `rdfs5_derives`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subPropertyOf_trans_reaches`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf_trans`	`ig_wf_sp`, `rdfs5_derives`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subClassOf_reaches_iri2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `i_rdf_type`, `i_rdfs_subClassOf`, `rdfs_rule_subClassOf`	`ig_wf_sp`, `is_subgraph`, `rho_df_frag_graph`	no (has `requires`)
`RDFS.Closure`	`rdfs_rule_subClassOf_reaches_iri`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `i_rdf_type`, `i_rdfs_subClassOf`, `rdfs_rule_subClassOf`	`ig_wf_sp`, `rho_df_frag_graph`	no (has `requires`)
`RDFS.Closure`	`lemma_f1_bad_triple_derived`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `f1_bad_triple`, `f1_witness`, `i_rdfs_subPropertyOf`, `rdfs_rule_subPropertyOf`	`ig_wf_sp`	no (has `requires`)
`RDFS.Closure`	`rho_df_frag_preservation_fails`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `f1_bad_triple`, `f1_witness`, `i_rdfs_subPropertyOf`, `rdfs_rule_subPropertyOf`	`ig_wf_sp`, `rho_df_frag_graph`, `rho_df_frag_triple`	no (has `requires`)
`RDFS.Closure`	`lemma_c_in_g1`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf`	`is_subgraph`	no (has `requires`)
`RDFS.Closure`	`lemma_c_in_g2`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_subPropertyOf`	`is_subgraph`	no (has `requires`)
`RDFS.Closure`	`lemma_c_in_g3`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subPropertyOf`	`is_subgraph`	no (has `requires`)
`RDFS.Closure`	`lemma_c_in_g4`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subClassOf`, `rdfs_rule_subPropertyOf`	`is_subgraph`	no (has `requires`)
`RDFS.Closure`	`lemma_c_in_g5`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subClassOf`, `rdfs_rule_subClassOf_trans`, `rdfs_rule_subPropertyOf`	`is_subgraph`	no (has `requires`)
`RDFS.Closure`	`lemma_axiomatic_tables_sep_free`	`RDF.Entailment.RDFS.SepFree`	`container_membership_properties`, `rdf_axiomatic_triples`, `rdfs_axiomatic_triples`	`str_sep_free`, `triple_sep_free`	yes
`SPARQL11.Algebra`	`theorem_tp_match_instantiates_ext`	`SPARQL11.Algebra.BGPRefinement`	`instantiate_tp`, `tp_match`	`binding_extends`, `ptrm_exact`, `smap_exact`, `term_exact`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_sound_fuel`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp_store_from_mu_fuel`, `graph_to_store`	`bgp_frag`, `bgp_subgraph_clause`, `binding_extends`, `graph_frag`, `smap_exact`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_bgp_sol_spec_from_subgraph_clause`	`SPARQL11.Algebra.BGPRefinement`	`instantiate_tp`	`bgp_sol_spec`, `bgp_subgraph_clause`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_store_sound_fuel`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp_store_from_mu_fuel`	`bgp_frag`, `bgp_subgraph_clause`, `binding_extends`, `graph_frag`, `smap_exact`, `store_search_sound`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_term_exact_subject`	`SPARQL11.Algebra.BGPRefinement`	`subject_to_term`	`term_exact`	yes
`SPARQL11.Algebra`	`lemma_bound_subject_mono`	`SPARQL11.Algebra.BGPRefinement`	`bound_subject_of_pattern`	`binding_extends`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_bound_predicate_mono`	`SPARQL11.Algebra.BGPRefinement`	`bound_predicate_of_pattern`	`binding_extends`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_bound_object_mono`	`SPARQL11.Algebra.BGPRefinement`	`bound_object_of_pattern`	`binding_extends`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_bound_object_exact`	`SPARQL11.Algebra.BGPRefinement`	`bound_object_of_pattern`	`ptrm_exact`, `smap_exact`, `term_exact`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_sm_bind_extends`	`SPARQL11.Algebra.BGPRefinement`	`sm_bind`	`binding_extends`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_sm_bind_under`	`SPARQL11.Algebra.BGPRefinement`	`sm_bind`	`binding_extends`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_try_bind_subject_complete`	`SPARQL11.Algebra.BGPRefinement`	`bound_subject_of_pattern`, `try_bind_subject`	`binding_extends`, `smap_exact`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_try_bind_term_complete`	`SPARQL11.Algebra.BGPRefinement`	`bound_object_of_pattern`, `try_bind_term`	`binding_extends`, `smap_exact`, `term_exact`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_tp_match_complete`	`SPARQL11.Algebra.BGPRefinement`	`instantiate_tp`, `tp_match`	`binding_extends`, `smap_exact`, `term_exact`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_bound_holds_of_instantiate`	`SPARQL11.Algebra.BGPRefinement`	`instantiate_tp`	`binding_extends`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_single_tp_complete_at`	`SPARQL11.Algebra.BGPRefinement`	`instantiate_tp`	`binding_extends`, `graph_frag`, `single_tp_goal`, `smap_exact`, `store_search_complete`, `tp_frag`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_store_complete`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp_store`	`bgp_frag`, `bgp_subgraph_clause`, `binding_extends`, `graph_frag`, `smap_exact`, `store_search_complete`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_complete`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp`	`bgp_frag`, `bgp_subgraph_clause`, `binding_extends`, `graph_frag`, `smap_exact`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_instantiate_tp_mono`	`SPARQL11.Algebra.BGPRefinement`	`instantiate_tp`	`binding_extends`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_instantiate_bgp_agree`	`SPARQL11.Algebra.BGPRefinement`	`instantiate_bgp`, `instantiate_tp`	`binding_extends`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_full_spec`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp`, `instantiate_tp`, `tp_vars`	`bgp_frag`, `bgp_sol_spec`, `graph_frag`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_sm_compatible_sound`	`SPARQL11.Algebra.Refinement`	`sm_compatible`	`compatible_spec`, `smap_exact`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_sm_compatible_complete`	`SPARQL11.Algebra.Refinement`	`sm_compatible`	`compatible_spec`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_sm_merge_is_merge`	`SPARQL11.Algebra.Refinement`	`sm_merge`	`is_merge`	yes
`SPARQL11.Algebra`	`theorem_domains_disjoint_sound`	`SPARQL11.Algebra.Refinement`	`domains_disjoint`	`dom_disjoint_spec`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_domains_disjoint_complete`	`SPARQL11.Algebra.Refinement`	`domains_disjoint`	`dom_disjoint_spec`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_union_card`	`SPARQL11.Algebra.Refinement`	`union`	`union_card_spec`	yes
`SPARQL11.Algebra`	`theorem_union_sound`	`SPARQL11.Algebra.Refinement`	`union`	`in_union_spec`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_sm_lookup_congr`	`SPARQL11.Algebra.Refinement`	`sm_lookup`	`smap_eq`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_fx_ctx_get_congr`	`SPARQL11.Algebra.Refinement`	`fx_ctx_get`	`smap_eq`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_expr_congr`	`SPARQL11.Algebra.Refinement`	`eval_expr_with_base`	`smap_eq`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_coalesce_congr`	`SPARQL11.Algebra.Refinement`	`eval_coalesce_with_base`	`smap_eq`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_geof_args_congr`	`SPARQL11.Algebra.Refinement`	`eval_geof_args_with_base`	`smap_eq`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_in_congr`	`SPARQL11.Algebra.Refinement`	`eval_in_with_base`	`smap_eq`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_concat_congr`	`SPARQL11.Algebra.Refinement`	`eval_concat_with_base`	`smap_eq`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_expr_opt_congr`	`SPARQL11.Algebra.Refinement`	`eval_expr_with_base`	`smap_eq`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_sr1_witness_now_card_conformant`	`SPARQL11.Algebra.Refinement`	`distinct_solutions`	`distinct_card_spec`	yes
`SPARQL11.Algebra`	`theorem_sm_equal_matches_smap_eq_on_witness`	`SPARQL11.Algebra.Refinement`	`sm_equal`	`smap_eq`	yes
`SPARQL11.Algebra`	`theorem_join_nested_loop_sound`	`SPARQL11.Algebra.Refinement`	`join_nested_loop`	`in_join_spec`, `seq_exact`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_join_nested_loop_complete`	`SPARQL11.Algebra.Refinement`	`join_nested_loop`	`compatible_spec`, `is_merge`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_project_is_proj`	`SPARQL11.Algebra.Refinement`	`project`	`is_proj`	yes
`SPARQL11.Algebra`	`theorem_project_solutions_sound`	`SPARQL11.Algebra.Refinement`	`project_solutions`	`in_project_spec`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_project_card`	`SPARQL11.Algebra.Refinement`	`project_solutions`	`project_card_spec`	yes
`SPARQL11.Algebra`	`lemma_not_compatible_of_engine`	`SPARQL11.Algebra.Refinement`	`sm_compatible`	`compatible_spec`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_minus_sound`	`SPARQL11.Algebra.Refinement`	`minus`	`in_minus_spec`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_minus_complete`	`SPARQL11.Algebra.Refinement`	`minus`	`compatible_spec`, `dom_disjoint_spec`, `smap_exact`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_left_join_empty_right`	`SPARQL11.Algebra.Refinement`	`eval_expr_ebv`, `left_join`	`in_leftjoin_spec`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_sm_bind_is_extend`	`SPARQL11.Algebra.Refinement`	`sm_bind`	`is_extend_at`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_sr3_distinct_card_spec_false`	`SPARQL11.Algebra.Refinement`	`distinct_solutions`	`distinct_card_spec`	yes

Modules with an internal-refinement theorem (23)

Module	Theorem	Proved in	Shipping functions	Declarative relation	Unconditional
`OWL.Closure`	`lemma_sameas_pairs_provenance`	`OWL.RL.Refinement`	`sameas_pairs`	`pairs_licensed`	yes
`OWL.Closure`	`owl_rule_sameAs_symmetry_licensed`	`OWL.RL.Refinement`	`owl_rule_sameAs_symmetry`	`eq_sym_licensed`	yes
`OWL.Closure`	`lemma_collect_nodes_provenance`	`OWL.RL.Refinement`	`collect_iri_or_bnode_terms`	`nodes_licensed`	yes
`OWL.Closure`	`owl_rule_sameAs_reflexivity_licensed`	`OWL.RL.Refinement`	`owl_rule_sameAs_reflexivity`	`eq_ref_licensed`	yes
`OWL.Closure`	`owl_rule_symmetric_property_licensed`	`OWL.RL.Refinement`	`owl_rule_symmetric_property`	`prp_symp_licensed`	yes
`OWL.Closure`	`owl_rule_equivalent_class_licensed`	`OWL.RL.Refinement`	`owl_rule_equivalent_class`	`scm_eqc1_licensed`	yes
`OWL.Closure`	`owl_rule_equivalent_property_licensed`	`OWL.RL.Refinement`	`owl_rule_equivalent_property`	`scm_eqp1_licensed`	yes
`OWL.Closure`	`owl_rule_inverse_of_licensed`	`OWL.RL.Refinement`	`owl_rule_inverse_of`	`inv_licensed`	yes
`OWL.Closure`	`lemma_no_disjoint_union_elim`	`OWL.RL.Refinement`	`owl_disjointUnionOf_iri`	`no_disjoint_union`	no (has `requires`)
`OWL.Closure`	`lemma_collect_haskey_axioms_licensed`	`OWL.RL.Refinement`	`collect_haskey_axioms`	`haskey_axioms_licensed`	yes
`OWL.Closure`	`lemma_members_of_class_licensed`	`OWL.RL.Refinement`	`members_of_class`	`class_members_licensed`	yes
`Parser.FastString`	`lemma_parse_nquads_acc_blank_step_shift`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`blank_line_wf`	no (has `requires`)
`Parser.FastString`	`lemma_parse_nquads_acc_skip_blanks`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`blank_chain_wf`	no (has `requires`)
`Parser.FastString`	`lemma_parse_nquads_acc_comment_step_shift`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`comment_line_wf`	no (has `requires`)
`Parser.FastString`	`lemma_parse_nquads_acc_quad_fail_step_shift`	`RDF.NQuads.Streaming`	`fs_byte_at`, `fs_byte_length`, `parse_nquad`, `parse_nquads_acc`	`quad_fail_line_wf`	no (has `requires`)
`Parser.FastString`	`lemma_parse_nquads_acc_quad_ok_step_shift`	`RDF.NQuads.Streaming`	`dataset_add_quad`, `fs_byte_length`, `parse_iri`, `parse_nquad`, `parse_nquads_acc`, `parse_object`, `parse_opt_graph_label`, `parse_subject`	`quad_ok_line_wf`	no (has `requires`)
`Parser.FastString`	`lemma_parse_nquads_acc_line_step_shift`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`lw_wf`	no (has `requires`)
`Parser.FastString`	`lemma_parse_nquads_acc_restart`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`chain_wf`	no (has `requires`)
`Parser.FastString`	`lemma_parse_nquads_acc_full_via_chain`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`chain_wf`	no (has `requires`)
`Parser.FastString`	`lemma_parse_nquads_acc_concat_line_general`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`chain_wf`	no (has `requires`)
`Parser.FastString`	`theorem_stream_eq_batch_single_chunk_general`	`RDF.NQuads.Streaming`	`fs_byte_length`	`chain_wf`	no (has `requires`)
`Parser.FastString`	`stream_fold_eq_batch`	`RDF.NQuads.Streaming`	`dataset_finalise`, `fs_byte_length`, `parse_nquads_acc`	`stream_fold_wf`	no (has `requires`)
`Parser.FastString`	`lw_wf_shift_left_blank`	`RDF.NQuads.Streaming`	`fs_byte_length`	`lw_wf`	no (has `requires`)
`Parser.FastString`	`lw_wf_shift_left_comment`	`RDF.NQuads.Streaming`	`fs_byte_length`	`lw_wf`	no (has `requires`)
`Parser.FastString`	`lw_wf_shift_left_quadfail`	`RDF.NQuads.Streaming`	`fs_byte_length`	`lw_wf`	no (has `requires`)
`Parser.FastString`	`lw_wf_shift_left_quadok`	`RDF.NQuads.Streaming`	`fs_byte_length`	`lw_wf`	no (has `requires`)
`Parser.FastString`	`lw_wf_shift_left`	`RDF.NQuads.Streaming`	`fs_byte_length`	`lw_wf`	no (has `requires`)
`Parser.FastString`	`lw_ds_step_shift`	`RDF.NQuads.Streaming`	`fs_byte_length`	`lw_wf`	no (has `requires`)
`Parser.FastString`	`chain_wf_shift_left`	`RDF.NQuads.Streaming`	`fs_byte_length`	`chain_wf`	no (has `requires`)
`Parser.FastString`	`chain_ds_fold_shift`	`RDF.NQuads.Streaming`	`fs_byte_length`	`chain_wf`	no (has `requires`)
`Parser.FastString`	`chain_append`	`RDF.NQuads.Streaming`	`fs_byte_length`	`chain_wf`	no (has `requires`)
`Parser.FastString`	`stream_consume_dataset_fold_eq_batch`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`stream_fold_wf`	no (has `requires`)
`Parser.FastString`	`stream_consume_dataset_eq_batch_raw`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`stream_fold_wf`	no (has `requires`)
`Parser.FastString`	`lemma_fold_nquads_acc_blank_step_shift`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`blank_line_wf`	no (has `requires`)
`Parser.FastString`	`lemma_fold_nquads_acc_comment_step_shift`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`comment_line_wf`	no (has `requires`)
`Parser.FastString`	`lemma_fold_nquads_acc_quad_fail_step_shift`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_at`, `fs_byte_length`, `parse_nquad`	`quad_fail_line_wf`	no (has `requires`)
`Parser.FastString`	`lemma_fold_nquads_acc_quad_ok_step_shift`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`, `parse_iri`, `parse_nquad`, `parse_object`, `parse_opt_graph_label`, `parse_subject`	`quad_ok_line_wf`	no (has `requires`)
`Parser.FastString`	`lemma_fold_nquads_acc_line_step_shift`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`lw_wf`	no (has `requires`)
`Parser.FastString`	`lemma_fold_nquads_acc_restart`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`chain_wf`	no (has `requires`)
`Parser.FastString`	`lemma_fold_nquads_acc_full_via_chain`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`chain_wf`	no (has `requires`)
`Parser.FastString`	`fold_nquads_acc_concat_line_general`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`chain_wf`	no (has `requires`)
`Parser.FastString`	`stream_consume_generic_fold_eq_batch`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`stream_fold_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_nquads_acc_blank_step_shift`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`blank_line_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_nquads_acc_skip_blanks`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`blank_chain_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_nquads_acc_comment_step_shift`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`comment_line_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_nquads_acc_quad_fail_step_shift`	`RDF.NQuads.Streaming`	`fs_byte_at`, `fs_byte_length`, `parse_nquad`, `parse_nquads_acc`	`quad_fail_line_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_nquads_acc_quad_ok_step_shift`	`RDF.NQuads.Streaming`	`dataset_add_quad`, `fs_byte_length`, `parse_iri`, `parse_nquad`, `parse_nquads_acc`, `parse_object`, `parse_opt_graph_label`, `parse_subject`	`quad_ok_line_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_nquads_acc_line_step_shift`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`lw_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_nquads_acc_restart`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`chain_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_nquads_acc_full_via_chain`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`chain_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_nquads_acc_concat_line_general`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`chain_wf`	no (has `requires`)
`Parser.NQuads`	`stream_fold_eq_batch`	`RDF.NQuads.Streaming`	`dataset_finalise`, `fs_byte_length`, `parse_nquads_acc`	`stream_fold_wf`	no (has `requires`)
`Parser.NQuads`	`stream_consume_dataset_fold_eq_batch`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`stream_fold_wf`	no (has `requires`)
`Parser.NQuads`	`stream_consume_dataset_eq_batch_raw`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	`stream_fold_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_fold_nquads_acc_blank_step_shift`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`blank_line_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_fold_nquads_acc_comment_step_shift`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`comment_line_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_fold_nquads_acc_quad_fail_step_shift`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_at`, `fs_byte_length`, `parse_nquad`	`quad_fail_line_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_fold_nquads_acc_quad_ok_step_shift`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`, `parse_iri`, `parse_nquad`, `parse_object`, `parse_opt_graph_label`, `parse_subject`	`quad_ok_line_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_fold_nquads_acc_line_step_shift`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`lw_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_fold_nquads_acc_restart`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`chain_wf`	no (has `requires`)
`Parser.NQuads`	`lemma_fold_nquads_acc_full_via_chain`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`chain_wf`	no (has `requires`)
`Parser.NQuads`	`fold_nquads_acc_concat_line_general`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`chain_wf`	no (has `requires`)
`Parser.NQuads`	`stream_consume_generic_fold_eq_batch`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	`stream_fold_wf`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_nquads_acc_quad_ok_step_shift`	`RDF.NQuads.Streaming`	`dataset_add_quad`, `fs_byte_length`, `parse_iri`, `parse_nquad`, `parse_nquads_acc`, `parse_object`, `parse_opt_graph_label`, `parse_subject`	`quad_ok_line_wf`	no (has `requires`)
`Parser.NTriples`	`lemma_fold_nquads_acc_quad_ok_step_shift`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`, `parse_iri`, `parse_nquad`, `parse_object`, `parse_opt_graph_label`, `parse_subject`	`quad_ok_line_wf`	no (has `requires`)
`RDF.Canonical`	`lemma_issue_fresh_label_shape`	`RDF.Canonical`	`issue_fresh`	`is_issuer_label`	yes
`RDF.Canonical`	`lemma_issue_identifier_fresh_label_shape`	`RDF.Canonical`	`issue_identifier`, `lookup_issued`	`is_issuer_label`	no (has `requires`)
`RDF.CottasStore`	`tables_of_handle_agree`	`RDF.CottasStore`	`tables_of_handle`	`token_tables_agree_with`	yes
`RDF.CottasStore`	`graph_bound_to_raw_token_agrees`	`RDF.CottasStore`	`graph_bound_to_raw_token_with`, `tables_of_handle`	`token_tables_agree_with`	no (has `requires`)
`RDF.CottasStore`	`build_qp_row_agrees`	`RDF.CottasStore`	`build_qp_row_with`, `tables_of_handle`	`token_tables_agree_with`	no (has `requires`)
`RDF.CottasStore.CompoundPresenceBitmap`	`rg_could_contain_pair_sound`	`RDF.CottasStore.CompoundPresenceBitmap`	`rg_could_contain_pair`	`compound_built_correctly`	no (has `requires`)
`RDF.CottasStore.PresenceBitmap`	`rg_contains_token_sound`	`RDF.CottasStore.PresenceBitmap`	`rg_contains_token`	`bitmap_built_correctly`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_step_extensive`	`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure_step`, `rho_df_closure_step_pre_dedup`	`no_dup_keys`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure_sound`	`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure`	`rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_f1_witness_frag`	`RDF.Entailment.RDFS.RhoDFClosure`	`f1_witness`, `i_rdfs_subPropertyOf`	`rho_df_frag_graph`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_f1_bad_triple_not_frag`	`RDF.Entailment.RDFS.RhoDFClosure`	`f1_bad_triple`	`rho_df_frag_triple`	yes
`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_len_eq_saturated`	`RDF.Entailment.RDFS.RhoDFClosure`	`graph_len`, `rho_df_closure_step`, `rho_df_closure_step_pre_dedup`	`no_dup_keys`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_pre_dedup_in_c`	`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure_step_pre_dedup`	`no_dup_keys`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_is_rho_df_object_ok_correct`	`RDF.Entailment.RDFS.RhoDFClosure`	`is_rho_df_object_ok`	`rho_df_object_ok`	yes
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_is_rho_df_frag_triple_correct`	`RDF.Entailment.RDFS.RhoDFClosure`	`is_rho_df_frag_triple`	`rho_df_frag_triple`	yes
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_is_rho_df_frag_correct`	`RDF.Entailment.RDFS.RhoDFClosure`	`is_rho_df_frag`	`rho_df_frag_graph`	yes
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_bgp_sound`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp`, `instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_bgp_complete_conditional`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp`, `instantiate_bgp`, `rho_df_closure`	`eval_bgp_complete_at`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_bgp_exact`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp`, `instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `eval_bgp_complete_at`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_ask_sound`	`SPARQL11.EntailmentRegime.RDFS`	`instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_ask_complete_conditional`	`SPARQL11.EntailmentRegime.RDFS`	`instantiate_bgp`, `rho_df_closure`	`eval_bgp_complete_at`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_bgp_sound_selective`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp_store`, `graph_to_store_for`, `instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_ask_pattern_sound`	`SPARQL11.EntailmentRegime.RDFS`	`instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_ask_query_sound`	`SPARQL11.EntailmentRegime.RDFS`	`eval_ask_query`, `instantiate_bgp`, `query`, `rho_df_closure`	`bgp_frag`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_bgp_complete_conditional_selective`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp_store`, `graph_to_store_for`, `instantiate_bgp`, `rho_df_closure`	`eval_bgp_store_complete_at`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_ask_query_complete_conditional`	`SPARQL11.EntailmentRegime.RDFS`	`eval_ask_query`, `instantiate_bgp`, `query`, `rho_df_closure`	`eval_bgp_store_complete_at`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_regime_answer_is_subgraph`	`SPARQL11.EntailmentRegime.RDFS`	`instantiate_bgp`, `rho_df_closure`	`rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_bgp_complete`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp`, `instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `bgp_instantiable`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_bgp_exact_answer`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp`, `instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `bgp_instantiable`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_ask_complete`	`SPARQL11.EntailmentRegime.RDFS`	`instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `bgp_instantiable`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_bgp_complete_selective`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp_store`, `graph_to_store_for`, `instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `bgp_instantiable`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`theorem_rdfs_regime_ask_query_complete`	`SPARQL11.EntailmentRegime.RDFS`	`eval_ask_query`, `instantiate_bgp`, `query`, `rho_df_closure`	`bgp_frag`, `bgp_instantiable`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_try_match_complete`	`RDF.Entailment.Simple.Refinement`	`try_match`	`all_matched`, `binding_compat`, `bnd_total`, `leq_reflexive`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_match_term_ground_sound`	`RDF.Entailment.Simple.Refinement`	`match_term`	`leq_always_identity`	no (has `requires`)
`RDF.Entailment.Simple`	`lemma_match_triple_ground_sound`	`RDF.Entailment.Simple.Refinement`	`match_triple`	`leq_always_identity`	no (has `requires`)
`RDF.Graph`	`lemma_dedup_sorted_decorated_extensive`	`RDF.Entailment.RDFS.FixedPoint`	`dedup_sorted_decorated_aux`, `triple_to_key`	`decoration_consistent`, `no_dup_keys_combined`	no (has `requires`)
`RDF.Graph`	`lemma_graph_dedup_sort_extensive`	`RDF.Entailment.RDFS.FixedPoint`	`graph_dedup_sort`	`no_dup_keys`	no (has `requires`)
`RDF.Graph`	`lemma_len_eq_saturated`	`RDF.Entailment.RDFS.FixedPoint`	`graph_len`, `rdfs_closure_step`	`no_dup_keys`, `step_saturated`	no (has `requires`)
`RDF.Graph`	`lemma_sortWith_sorted_pairs_dt`	`RDF.Entailment.RDFS.FixedPoint`	`cmp_decorated_triple`	`sorted_pairs_dt`	yes
`RDF.Graph`	`lemma_dedup_sorted_decorated_no_repeats`	`RDF.Entailment.RDFS.FixedPoint`	`dedup_sorted_decorated_aux`	`decoration_consistent`, `dedup_acc_inv`, `sorted_pairs_dt`	no (has `requires`)
`RDF.Graph`	`lemma_len_eq_saturated_gapB`	`RDF.Entailment.RDFS.FixedPoint`	`graph_len`, `rdfs_closure_step`	`no_dup_keys`, `step_saturated`	no (has `requires`)
`RDF.Graph`	`rho_df_len_eq_saturated`	`RDF.Entailment.RDFS.RhoDFClosure`	`graph_len`, `rho_df_closure_step`, `rho_df_closure_step_pre_dedup`	`no_dup_keys`	no (has `requires`)
`RDF.Graph`	`lemma_lit_key_lang_part_sep_free`	`RDF.Indexed.KeyInjectivity`	`lit_key_lang_part`	`str_sep_free`	no (has `requires`)
`RDF.Graph`	`lemma_literal_key_injective`	`RDF.Indexed.KeyInjectivity`	`term_to_key_total`	`literal_sep_free`	no (has `requires`)
`RDF.Graph`	`lemma_term_to_key_total_injective`	`RDF.Indexed.KeyInjectivity`	`term_to_key_total`	`term_sep_free`	no (has `requires`)
`RDF.Graph`	`lemma_triple_to_key_injective`	`RDF.Indexed.KeyInjectivity`	`triple_to_key`	`triple_full_sep_free`	no (has `requires`)
`RDF.Graph`	`lemma_graph_full_sep_free_no_dup_keys`	`RDF.Indexed.KeyInjectivity`	`triple_to_key`	`graph_full_sep_free`	no (has `requires`)
`RDF.Graph.Executable`	`stream_fold_eq_batch`	`RDF.NQuads.Streaming`	`dataset_finalise`, `fs_byte_length`, `parse_nquads_acc`	`stream_fold_wf`	no (has `requires`)
`RDF.Graph.Executable`	`theorem_stream_consume_dataset_eq_batch`	`RDF.NQuads.Streaming`	`dataset_finalise`	`stream_fold_wf`	no (has `requires`)
`RDF.Indexed`	`lemma_tree_ok_lookup`	`OWL.Semantics.MemLemmas`	`bucket_lookup`	`tree_ok`	no (has `requires`)
`RDF.Indexed`	`lemma_slt_tree_ok`	`OWL.Semantics.MemLemmas`	`sorted_list_to_tree_fuel`	`pairs_ok`, `tree_ok`	no (has `requires`)
`RDF.Indexed`	`lemma_group_ok`	`OWL.Semantics.MemLemmas`	`group_sorted_decorated_aux`	`dec_ok`, `pairs_ok`	no (has `requires`)
`RDF.Indexed`	`lemma_build_bucket_ok`	`OWL.Semantics.MemLemmas`	`build_bucket`	`tree_ok`	yes
`RDF.Indexed`	`lemma_sortWith_sorted_pairs`	`RDF.Indexed.Completeness`	`cmp_by_decorated_key`	`sorted_pairs`	yes
`RDF.Indexed`	`lemma_group_sorted`	`RDF.Indexed.Completeness`	`group_sorted_decorated_aux`	`group_sorted_inv`, `sorted_kv_desc`	no (has `requires`)
`RDF.Indexed`	`lemma_slt_lookup_complete`	`RDF.Indexed.Completeness`	`bucket_lookup`, `sorted_list_to_tree_fuel`	`sorted_kv`	no (has `requires`)
`RDF.Indexed`	`lemma_subject_key_sep_free`	`RDF.Indexed.KeyInjectivity`	`subject_to_key`	`str_sep_free`, `subj_label_sep_free`	no (has `requires`)
`RDF.Indexed`	`sp_key_injective_one_sided`	`RDF.Indexed.KeyInjectivity`	`sp_key`	`str_sep_free`, `subj_label_sep_free`	no (has `requires`)
`RDF.Indexed`	`po_key_injective_one_sided`	`RDF.Indexed.KeyInjectivity`	`po_key`	`str_sep_free`, `subj_label_sep_free`	no (has `requires`)
`RDF.Indexed`	`lemma_triple_term_prefix_sep_free`	`RDF.Indexed.KeyInjectivity`	`subject_to_key`	`str_sep_free`	no (has `requires`)
`RDF.Store.Columnar.DeltaMerge`	`lemma_state_agrees_init`	`RDF.Store.Columnar.DeltaMerge`	`delta_resolved_empty`	`state_agrees`	yes
`RDF.Store.Columnar.DeltaMerge`	`lemma_state_agrees_step`	`RDF.Store.Columnar.DeltaMerge`	`apply_entry_ref_step`, `apply_entry_to_delta`	`state_agrees`	no (has `requires`)
`RDF.Store.Columnar.DeltaMerge`	`lemma_apply_entries_state_agrees`	`RDF.Store.Columnar.DeltaMerge`	`apply_entries_ref`, `fold_entries_for_graph`	`state_agrees`	no (has `requires`)
`RDF.Store.Columnar.OffsetIndex`	`row_positions_for_count_sound`	`RDF.Store.Columnar.OffsetIndex`	`row_positions_for`	`offsets_built_correctly`	no (has `requires`)
`RDF.Store.Columnar.SubjectOffsetIndex`	`range_for_subject_count_sound`	`RDF.Store.Columnar.SubjectOffsetIndex`	`range_for_subject`, `subject_range_count`	`subject_offsets_built_correctly`	no (has `requires`)
`RDF.Term`	`lemma_rdf_term_eq_denot`	`OWL.Semantics`	`rdf_term_eq`	`cond_literal_term_eq_respecting`	no (has `requires`)
`RDF.Term`	`lemma_rdf_term_eq_sound`	`RDF.Entailment.RDFS.RhoDFClosure`	`rdf_term_eq`	`rho_df_object_ok`	no (has `requires`)
`RDF.Turtle.Serialize`	`lemma_ts_abbreviate_iri_pname_safe`	`RDF.Turtle.Serialize`	`ts_abbreviate_iri`	`compacts_to_pname_safe`	yes
`RDF.Vocabulary.Axioms`	`finite_rdf_axioms_sound`	`RDF.Entailment.RDF.Spec`	`rdf_axiomatic_triples`	`rdf_axiomatic`	no (has `requires`)
`RDF.Vocabulary.Axioms`	`lemma_f1_witness_frag`	`RDF.Entailment.RDFS.RhoDFClosure`	`f1_witness`, `i_rdfs_subPropertyOf`	`rho_df_frag_graph`	no (has `requires`)
`RDFS.Closure`	`lemma_step_extensive`	`RDF.Entailment.RDFS.FixedPoint`	`rdfs_closure_step`	`no_dup_keys`	no (has `requires`)
`RDFS.Closure`	`lemma_len_eq_saturated`	`RDF.Entailment.RDFS.FixedPoint`	`graph_len`, `rdfs_closure_step`	`no_dup_keys`, `step_saturated`	no (has `requires`)
`RDFS.Closure`	`lemma_len_eq_saturated_gapB`	`RDF.Entailment.RDFS.FixedPoint`	`graph_len`, `rdfs_closure_step`	`no_dup_keys`, `step_saturated`	no (has `requires`)
`RDFS.Closure`	`lemma_chain_shift`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_closure_step`	`closure_chain_wf`	no (has `requires`)
`RDFS.Closure`	`rdfs_closure_entails`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_closure`	`closure_chain_wf`, `rdfs_entails`	no (has `requires`)
`RDFS.Closure`	`rdf_property_axiom_closure_entails`	`RDF.Entailment.RDFS.ModelTheory`	`rdf_property_axiom_closure`	`rdf_entails`	yes
`RDFS.Closure`	`rdfs_closure_with_reflexivity_entails`	`RDF.Entailment.RDFS.ModelTheory`	`rdfs_closure_with_reflexivity`	`closure_chain_wf`, `rdfs_entails`	no (has `requires`)
`RDFS.Closure`	`collect_related_iris_source`	`RDF.Entailment.RDFS.Refinement`	`collect_related_iris`	`harvest_source`	yes
`RIF.Core.Eval`	`lemma_fixpoint_extends`	`RIF.Core.Eval`	`fixpoint`	`graph_subset`	yes
`RIF.Core.Eval`	`rif_fixpoint_extensive`	`RIF.Core.Refinement`	`fixpoint`	`graph_subset`	yes
`RIF.Core.Eval`	`rif_one_round_extensive`	`RIF.Core.Refinement`	`one_round`	`graph_subset`	yes
`RIF.Core.Eval`	`rif_fire_rule_extensive`	`RIF.Core.Refinement`	`fire_rule`	`graph_subset`	yes
`RIF.Core.Eval`	`fire_head_per_bindings_licensed`	`RIF.Core.Refinement`	`fire_head_per_bindings`	`rif_bindings_derive`	yes
`RIF.Core.Eval`	`fire_rule_licensed`	`RIF.Core.Refinement`	`fire_rule`	`rif_rule_derives`	yes
`RIF.Core.Eval`	`lemma_one_round_aux_licensed`	`RIF.Core.Refinement`	`one_round_aux`	`graph_subset`, `rif_derives`	no (has `requires`)
`RIF.Core.Eval`	`one_round_licensed`	`RIF.Core.Refinement`	`one_round`	`rif_derives`	yes
`RIF.Core.Eval`	`fixpoint_licensed`	`RIF.Core.Refinement`	`fixpoint`	`rif_derives`	yes
`RIF.Core.Tests`	`lemma_saturate_extends`	`RIF.Core.Tests`	`saturate_with_program`	`graph_subset`	yes
`SPARQL11.Algebra`	`lemma_pick_smaller_bucket_sound`	`SPARQL11.Algebra.BGPRefinement`	`pick_smaller_bucket`	`bucket_cand_sound`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_pick_smaller_bucket_complete`	`SPARQL11.Algebra.BGPRefinement`	`pick_smaller_bucket`	`bucket_cand_complete`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_ig_search_complete_selective`	`SPARQL11.Algebra.BGPRefinement`	`ig_search`	`bound_obj_exact`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_ig_search_complete`	`SPARQL11.Algebra.BGPRefinement`	`ig_search`	`bound_obj_exact`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_store_search_complete`	`SPARQL11.Algebra.BGPRefinement`	`graph_to_store`, `store_search`	`bound_obj_exact`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_store_search_complete_for`	`SPARQL11.Algebra.BGPRefinement`	`graph_to_store_for`, `group_graph_pattern`, `store_search`	`bound_obj_exact`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_subgraph`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp`	`bgp_frag`, `bgp_subgraph_clause`, `graph_frag`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_instantiate_bgp_subset`	`SPARQL11.Algebra.BGPRefinement`	`instantiate_bgp`	`bgp_subgraph_clause`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_instantiates_into_graph`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp`, `instantiate_bgp`	`bgp_frag`, `graph_frag`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_graph_to_store_sound`	`SPARQL11.Algebra.BGPRefinement`	`graph_to_store`	`store_search_sound`	yes
`SPARQL11.Algebra`	`lemma_graph_to_store_for_sound`	`SPARQL11.Algebra.BGPRefinement`	`graph_to_store_for`, `group_graph_pattern`	`store_search_sound`	yes
`SPARQL11.Algebra`	`lemma_eval_single_tp_sound_at`	`SPARQL11.Algebra.BGPRefinement`	`eval_single_tp_store_default`, `tp_match`	`store_search_sound`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_store_subgraph`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp_store`	`bgp_frag`, `bgp_subgraph_clause`, `graph_frag`, `store_search_sound`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_store_instantiates_into_graph`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp_store`, `instantiate_bgp`	`bgp_frag`, `graph_frag`, `store_search_sound`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_store_for_instantiates_into_graph`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp_store`, `graph_to_store_for`, `group_graph_pattern`, `instantiate_bgp`	`bgp_frag`, `graph_frag`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_graph_to_store_complete`	`SPARQL11.Algebra.BGPRefinement`	`graph_to_store`	`store_search_complete`	yes
`SPARQL11.Algebra`	`lemma_graph_to_store_for_complete`	`SPARQL11.Algebra.BGPRefinement`	`graph_to_store_for`, `group_graph_pattern`	`store_search_complete`	yes
`SPARQL11.Algebra`	`lemma_subgraph_clause_of_instantiated`	`SPARQL11.Algebra.BGPRefinement`	`instantiate_bgp`, `instantiate_tp`	`bgp_subgraph_clause`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_store_complete_answer`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp_store`, `instantiate_bgp`	`bgp_frag`, `bgp_subgraph_clause`, `graph_frag`, `store_search_complete`, `store_search_sound`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_store_complete_from_subset`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp_store`, `instantiate_bgp`, `instantiate_tp`	`bgp_frag`, `graph_frag`, `store_search_complete`, `store_search_sound`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_complete_from_subset`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp`, `instantiate_bgp`, `instantiate_tp`	`bgp_frag`, `graph_frag`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_store_for_complete_from_subset`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp_store`, `graph_to_store_for`, `group_graph_pattern`, `instantiate_bgp`, `instantiate_tp`	`bgp_frag`, `graph_frag`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_single_tp_store_domain`	`SPARQL11.Algebra.BGPRefinement`	`eval_single_tp_store`, `tp_vars`	`tp_frag`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_store_domain_fuel`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp_store_from_mu_fuel`	`bgp_dom_grow_clause`, `bgp_frag`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_domain`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp`, `sm_empty`	`bgp_dom_grow_clause`, `bgp_frag`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_eval_bgp_dom_clause`	`SPARQL11.Algebra.BGPRefinement`	`eval_bgp`	`bgp_dom_clause`, `bgp_frag`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_sm_compatible_sound`	`SPARQL11.Algebra.Refinement`	`sm_compatible`	`smap_exact`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_try_bind_term_instantiates`	`SPARQL11.Algebra.Refinement`	`bound_object_of_pattern`, `try_bind_term`	`binding_extends`, `ptrm_exact`, `smap_exact`, `term_exact`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_try_bind_subject_instantiates`	`SPARQL11.Algebra.Refinement`	`bound_subject_of_pattern`, `try_bind_subject`	`binding_extends`, `smap_exact`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_tp_match_instantiates`	`SPARQL11.Algebra.Refinement`	`instantiate_tp`, `tp_match`	`binding_extends`, `ptrm_exact`, `smap_exact`, `term_exact`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_sort_solutions_sorted`	`SPARQL11.Algebra.Refinement`	`compare_on_conditions`, `order_condition`, `sort_solutions`	`sorted_by`, `totality_on`, `transitivity_on`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_sparql_order_numeric_frag_totality`	`SPARQL11.Algebra.Refinement`	`sparql_order`	`er_num_plain`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_sparql_order_numeric_frag_trans`	`SPARQL11.Algebra.Refinement`	`sparql_order`	`er_num_plain`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_smap_ground_lookup`	`SPARQL11.EntailmentRegime.RDFS`	`sm_lookup`	`smap_ground`, `term_ground`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_bound_subject_ground`	`SPARQL11.EntailmentRegime.RDFS`	`bound_subject_of_pattern`	`smap_ground`, `subject_ground`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_bound_object_ground`	`SPARQL11.EntailmentRegime.RDFS`	`bound_object_of_pattern`	`smap_ground`, `term_ground`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_instantiate_tp_ground`	`SPARQL11.EntailmentRegime.RDFS`	`instantiate_tp`	`smap_ground`, `tp_ground_positions`, `triple_ground`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_instantiate_bgp_ground`	`SPARQL11.EntailmentRegime.RDFS`	`instantiate_bgp`	`bgp_ground_positions`, `smap_ground`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_bgp_sound`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp`, `instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_bgp_complete_conditional`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp`, `instantiate_bgp`, `rho_df_closure`	`eval_bgp_complete_at`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_bgp_exact`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp`, `instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `eval_bgp_complete_at`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_ask_sound`	`SPARQL11.EntailmentRegime.RDFS`	`instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_ask_complete_conditional`	`SPARQL11.EntailmentRegime.RDFS`	`instantiate_bgp`, `rho_df_closure`	`eval_bgp_complete_at`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_bgp_sound_selective`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp_store`, `graph_to_store_for`, `instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_ask_pattern_sound`	`SPARQL11.EntailmentRegime.RDFS`	`instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_ask_query_sound`	`SPARQL11.EntailmentRegime.RDFS`	`eval_ask_query`, `instantiate_bgp`, `query`, `rho_df_closure`	`bgp_frag`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_bgp_complete_conditional_selective`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp_store`, `graph_to_store_for`, `instantiate_bgp`, `rho_df_closure`	`eval_bgp_store_complete_at`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_ask_query_complete_conditional`	`SPARQL11.EntailmentRegime.RDFS`	`eval_ask_query`, `instantiate_bgp`, `query`, `rho_df_closure`	`eval_bgp_store_complete_at`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_regime_answer_is_subgraph`	`SPARQL11.EntailmentRegime.RDFS`	`instantiate_bgp`, `rho_df_closure`	`rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_bgp_complete`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp`, `instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `bgp_instantiable`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_bgp_exact_answer`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp`, `instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `bgp_instantiable`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_ask_complete`	`SPARQL11.EntailmentRegime.RDFS`	`instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `bgp_instantiable`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_bgp_complete_selective`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp_store`, `graph_to_store_for`, `instantiate_bgp`, `rho_df_closure`	`bgp_frag`, `bgp_instantiable`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_rdfs_regime_ask_query_complete`	`SPARQL11.EntailmentRegime.RDFS`	`eval_ask_query`, `instantiate_bgp`, `query`, `rho_df_closure`	`bgp_frag`, `bgp_instantiable`, `graph_frag`, `rho_df_decides_hyps`, `rho_df_entails`	no (has `requires`)

Modules with an algorithm-correctness theorem (45)

Module	Theorem	Proved in	Shipping functions named	Unconditional
`Dep.Reachability`	`no_root_reaches`	`Dep.Reachability`	`all_mem`, `is_closed`	no (has `requires`)
`HDT.Container`	`lemma_parse_control_info_rejects_bad_cookie`	`HDT.Container`	`byte_get`, `parse_control_info`	no (has `requires`)
`HDT.Container`	`lemma_bad_global_cookie_rejects_container`	`HDT.Container`	`byte_get`, `hdt_parse_inventory_hex`	no (has `requires`)
`OWL.Closure`	`lemma_vocab_symp_agree`	`OWL.RL.Refinement`	`owl_SymmetricProperty`, `rdf_type`	yes
`OWL.Closure`	`lemma_vocab_eqc_agree`	`OWL.RL.Refinement`	`owl_equivalentClass`, `rdfs_subClassOf`	yes
`OWL.Closure`	`lemma_vocab_eqp_agree`	`OWL.RL.Refinement`	`owl_equivalentProperty`, `rdfs_subPropertyOf`	yes
`OWL.Closure`	`lemma_vocab_trp_agree`	`OWL.RL.Refinement`	`owl_TransitiveProperty`, `rdf_type`	yes
`OWL.Closure`	`lemma_vocab_list_agree`	`OWL.RL.Refinement`	`rdf_first`, `rdf_nil_iri`, `rdf_rest`	yes
`OWL.Closure`	`lemma_vocab_cls_oo_agree`	`OWL.RL.Refinement`	`owl_oneOf_iri`, `rdf_type`	yes
`OWL.Closure`	`lemma_vocab_cls_int_agree`	`OWL.RL.Refinement`	`owl_intersectionOf_iri`, `rdf_type`	yes
`OWL.Closure`	`lemma_vocab_cls_uni_agree`	`OWL.RL.Refinement`	`owl_unionOf_iri`, `rdfs_subClassOf`	yes
`OWL.Closure`	`lemma_vocab_fp_agree`	`OWL.RL.Refinement`	`owl_FunctionalProperty`, `rdf_type`	yes
`OWL.Closure`	`lemma_vocab_ifp_agree`	`OWL.RL.Refinement`	`owl_InverseFunctionalProperty`, `rdf_type`	yes
`OWL.Closure`	`lemma_vocab_hv_agree`	`OWL.RL.Refinement`	`owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`	yes
`OWL.Closure`	`lemma_vocab_avf_agree`	`OWL.RL.Refinement`	`owl_allValuesFrom_iri`, `owl_onProperty_iri`, `rdf_type`	yes
`OWL.Closure`	`lemma_vocab_clash_agree`	`OWL.RL.Refinement`	`owl_disjointWith_iri`, `owl_propertyDisjointWith`, `rdf_type`	yes
`Parquet.Footer`	`lemma_parse_version_hex_literal`	`RDF.CottasStore.BaseWriter`	`cottas_format_version`, `parse_file_metadata_version_hex`	yes
`Parquet.Footer`	`lemma_version_field_roundtrip`	`RDF.CottasStore.BaseWriter`	`bytes_to_hex`, `cottas_format_version`, `parse_file_metadata_version_hex`, `version_field_bytes`	yes
`Parser.Combinators`	`lemma_ptake_while_acc_pos_shift_headroom`	`Parser.NTriples.Locality`	`fs_byte_length`, `ptake_while_acc`	no (has `requires`)
`Parser.Combinators`	`lemma_ptake_while_scan_shift_headroom`	`Parser.NTriples.Locality`	`fs_byte_length`, `ptake_while_scan`	no (has `requires`)
`Parser.Combinators`	`lemma_ptake_while1_pos_shift`	`Parser.NTriples.Locality`	`fs_byte_length`, `ptake_while1_pos`, `ptake_while_scan`	no (has `requires`)
`Parser.Combinators`	`lemma_parse_lang_tag_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_alpha`, `is_lang_char`, `parse_lang_tag`, `ptake_while_scan`	no (has `requires`)
`Parser.Combinators`	`lemma_parse_literal_lang_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_alpha`, `is_lang_char`, `parse_literal`, `parse_string_literal`, `ptake_while_scan`	no (has `requires`)
`Parser.FastString`	`fs_byte_at_concat`	`Parser.FastString.Axioms`	`fs_byte_at`, `fs_byte_length`	no (has `requires`)
`Parser.FastString`	`fs_byte_sub_concat_left`	`Parser.FastString.Axioms`	`fs_byte_length`, `fs_byte_sub`	no (has `requires`)
`Parser.FastString`	`fs_byte_sub_concat_right`	`Parser.FastString.Axioms`	`fs_byte_length`, `fs_byte_sub`	no (has `requires`)
`Parser.FastString`	`fs_cp_at_ascii`	`Parser.FastString.Axioms`	`fs_byte_at`, `fs_byte_length`, `fs_cp_at`	no (has `requires`)
`Parser.FastString`	`fs_byte_sub_self`	`Parser.FastString.Axioms`	`fs_byte_length`, `fs_byte_sub`	yes
`Parser.FastString`	`fs_ascii_singleton_facts`	`Parser.FastString.BaseCases`	`fs_byte_at`, `fs_byte_length`	no (has `requires`)
`Parser.FastString`	`lemma_byte_at_after_prefix`	`Parser.FastString.RoundTripLemmas`	`fs_byte_at`, `fs_byte_length`	no (has `requires`)
`Parser.FastString`	`fs_byte_sub_by_charcount`	`Parser.FastString.RoundTripLemmas`	`fs_byte_sub`, `slice_chars`, `take_chars`, `utf8_enc_char`	yes
`Parser.FastString`	`fs_byte_length_eq`	`Parser.FastString`	`fs_byte_length`, `utf8_bytes`	yes
`Parser.FastString`	`fs_byte_at_eq`	`Parser.FastString`	`fs_byte_at`, `nth_byte`, `utf8_bytes`	yes
`Parser.FastString`	`fs_byte_sub_eq`	`Parser.FastString`	`fs_byte_sub`, `slice_bytes`, `utf8_bytes`, `utf8_decode_all`	yes
`Parser.FastString`	`fs_find_byte_eq`	`Parser.FastString`	`find_byte`, `fs_find_byte`, `utf8_bytes`	yes
`Parser.FastString`	`fs_cp_at_eq`	`Parser.FastString`	`fs_cp_at`, `utf8_bytes`, `utf8_decode_at`	yes
`Parser.FastString`	`fs_cp_len_eq`	`Parser.FastString`	`fs_cp_len`, `utf8_bytes`, `utf8_decode_at`	yes
`Parser.FastString`	`fs_byte_index_eq`	`Parser.FastString`	`fs_byte_at`, `fs_byte_index`	yes
`Parser.FastString`	`lemma_byte_index_at_middle`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`	no (has `requires`)
`Parser.FastString`	`lemma_scan_iri_end_shift`	`Parser.NTriples.Locality`	`fs_byte_length`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_scan_iri_end_shift_from_start`	`Parser.NTriples.Locality`	`fs_byte_length`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_scan_iri_end_shift_headroom`	`Parser.NTriples.Locality`	`fs_byte_length`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_ptake_while_acc_pos_shift_headroom`	`Parser.NTriples.Locality`	`fs_byte_length`, `ptake_while_acc`	no (has `requires`)
`Parser.FastString`	`lemma_pws_shift`	`Parser.NTriples.Locality`	`fs_byte_length`, `pws`	no (has `requires`)
`Parser.FastString`	`lemma_parse_iri_raw_fastpath_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_parse_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_parse_subject_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri_raw`, `parse_subject`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_parse_object_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri_raw`, `parse_object`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_parse_iri_body_acc_shift`	`Parser.NTriples.Locality`	`fs_byte_length`, `parse_iri_body_acc`	no (has `requires`)
`Parser.FastString`	`lemma_scan_iri_end_success_bound`	`Parser.NTriples.Locality`	`fs_byte_length`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_parse_iri_body_acc_success_bound`	`Parser.NTriples.Locality`	`fs_byte_length`, `parse_iri_body_acc`	no (has `requires`)
`Parser.FastString`	`lemma_cp_at_at_middle`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `fs_cp_at`, `is_continuation`	no (has `requires`)
`Parser.FastString`	`lemma_byte_at_at_middle`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`	no (has `requires`)
`Parser.FastString`	`lemma_scan_bnode_body_cp_shift_headroom`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `is_continuation`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.FastString`	`lemma_scan_string_fast_shift_headroom`	`Parser.NTriples.Locality`	`fs_byte_length`, `scan_string_fast`	no (has `requires`)
`Parser.FastString`	`lemma_parse_string_body_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `is_continuation`, `parse_string_body`	no (has `requires`)
`Parser.FastString`	`lemma_scan_string_fast_shift_hasescapes`	`Parser.NTriples.Locality`	`fs_byte_length`, `scan_string_fast`	no (has `requires`)
`Parser.FastString`	`lemma_parse_string_literal_fastpath_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_string_literal`, `scan_string_fast`	no (has `requires`)
`Parser.FastString`	`lemma_parse_string_literal_escapepath_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `is_continuation`, `parse_string_body`, `parse_string_literal`, `scan_string_fast`	no (has `requires`)
`Parser.FastString`	`lemma_ptake_while_scan_shift_headroom`	`Parser.NTriples.Locality`	`fs_byte_length`, `ptake_while_scan`	no (has `requires`)
`Parser.FastString`	`lemma_ptake_while1_pos_shift`	`Parser.NTriples.Locality`	`fs_byte_length`, `ptake_while1_pos`, `ptake_while_scan`	no (has `requires`)
`Parser.FastString`	`lemma_parse_lang_tag_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_alpha`, `is_lang_char`, `parse_lang_tag`, `ptake_while_scan`	no (has `requires`)
`Parser.FastString`	`lemma_parse_datatype_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_datatype`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_parse_graph_label_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_graph_label`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_parse_opt_graph_label_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri_raw`, `parse_opt_graph_label`, `pws`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_parse_opt_graph_label_none_dot_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_opt_graph_label`, `pws`	no (has `requires`)
`Parser.FastString`	`lemma_skip_eol_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `skip_eol`	no (has `requires`)
`Parser.FastString`	`lemma_nt_skip_to_eol_shift`	`Parser.NTriples.Locality`	`fs_byte_length`, `nt_skip_to_eol`	no (has `requires`)
`Parser.FastString`	`lemma_nq_skip_line_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `nq_skip_line`	no (has `requires`)
`Parser.FastString`	`lemma_pws_noop`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_nt_ws`, `pws`	no (has `requires`)
`Parser.FastString`	`lemma_parse_nquad_iri_nograph_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri`, `parse_iri_raw`, `parse_nquad`, `parse_object`, `parse_subject`, `pws`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_parse_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_bnode`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.FastString`	`lemma_parse_subject_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_subject`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.FastString`	`lemma_parse_object_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_object`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.FastString`	`lemma_parse_literal_plain_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_literal`, `parse_string_literal`	no (has `requires`)
`Parser.FastString`	`lemma_parse_literal_lang_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_alpha`, `is_lang_char`, `parse_literal`, `parse_string_literal`, `ptake_while_scan`	no (has `requires`)
`Parser.FastString`	`lemma_parse_literal_datatype_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_datatype`, `parse_literal`, `parse_string_literal`, `rdf_dir_lang_string`, `rdf_lang_string`	no (has `requires`)
`Parser.FastString`	`lemma_parse_object_literal_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_literal`, `parse_object`	no (has `requires`)
`Parser.FastString`	`lemma_parse_graph_label_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_graph_label`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.FastString`	`lemma_parse_opt_graph_label_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_opt_graph_label`, `pws`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.FastString`	`lemma_parse_nquad_shift_generic`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri`, `parse_nquad`, `parse_object`, `parse_opt_graph_label`, `parse_subject`, `pws`	no (has `requires`)
`Parser.FastString`	`stream_parse_single_chunk_shape`	`RDF.NQuads.Streaming`	`dataset_finalise`, `fs_byte_length`, `parse_nquads_acc`	yes
`Parser.FastString`	`lemma_fs_byte_index_concat`	`RDF.NQuads.Streaming`	`fs_byte_index`, `fs_byte_length`	no (has `requires`)
`Parser.FastString`	`lemma_byte_index_at_middle`	`RDF.NQuads.Streaming`	`fs_byte_index`, `fs_byte_length`	no (has `requires`)
`Parser.FastString`	`parse_nquads_acc_concat_line_empty_complete`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	yes
`Parser.FastString`	`parse_nquads_acc_concat_line_empty_carry`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	yes
`Parser.FastString`	`lemma_skip_comment_shift`	`RDF.NQuads.Streaming`	`fs_byte_index`, `fs_byte_length`, `nt_skip_to_eol`, `skip_comment`	no (has `requires`)
`Parser.FastString`	`lemma_nq_skip_line_shift_exact`	`RDF.NQuads.Streaming`	`fs_byte_at`, `fs_byte_length`, `nq_skip_line`	no (has `requires`)
`Parser.FastString`	`stream_consume_single_chunk_shape`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	yes
`Parser.FastString`	`lemma_extract_middle`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `fs_byte_sub`	yes
`Parser.FastString`	`lemma_iri_bracket_shift_prereqs`	`RDF.NTriples.RoundTrip`	`fs_byte_index`, `fs_byte_length`, `is_iri_body_char`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_pws_one_space`	`RDF.NTriples.RoundTrip`	`fs_byte_index`, `fs_byte_length`, `is_nt_ws`, `pws`	no (has `requires`)
`Parser.FastString`	`lemma_build_string_byte_length_general`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `utf8_enc_char`	yes
`Parser.FastString`	`lemma_scan_iri_end_one_char_walk`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_scan_iri_end_build_string_utf8`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `scan_iri_end`	no (has `requires`)
`Parser.FastString`	`lemma_parse_iri_raw_build_string_utf8`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `parse_iri_raw`	yes
`Parser.FastString`	`lemma_parse_iri_build_string_utf8`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `parse_iri`	no (has `requires`)
`Parser.FastString`	`lemma_term_iri_round_trip_build_string_utf8`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `nq_term_to_string`, `parse_object`	no (has `requires`)
`Parser.FastString`	`lemma_term_iri_round_trip_utf8`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `nq_term_to_string`, `parse_object`	no (has `requires`)
`Parser.FastString`	`fs_sub_of_concat`	`SPARQL11.Parser.AskBgpRoundTrip`	`fs_byte_length`, `fs_byte_sub`	yes
`Parser.FastString`	`fs_sub_of_concat_literal`	`SPARQL11.Parser.AskBgpRoundTrip`	`fs_byte_length`, `fs_byte_sub`	yes
`Parser.FastString.Spec`	`utf8_decode_all_aux_unfold`	`Parser.FastString.Axioms`	`utf8_decode_all_aux`, `utf8_decode_at`	no (has `requires`)
`Parser.FastString.Spec`	`lemma_decode_all_aux_encode`	`Parser.FastString.Axioms`	`utf8_decode_all_aux`, `utf8_enc_char`	yes
`Parser.FastString.Spec`	`utf8_decode_all_utf8_bytes_identity`	`Parser.FastString.Axioms`	`utf8_bytes`, `utf8_decode_all`	yes
`Parser.FastString.Spec`	`lemma_ascii_utf8_bytes_at`	`Parser.FastString.RoundTripLemmas`	`nth_byte`, `utf8_enc_char`	yes
`Parser.FastString.Spec`	`fs_byte_sub_by_charcount`	`Parser.FastString.RoundTripLemmas`	`fs_byte_sub`, `slice_chars`, `take_chars`, `utf8_enc_char`	yes
`Parser.FastString.Spec`	`lemma_build_string_utf8_bytes_nth`	`Parser.FastString.RoundTripLemmas`	`nth_byte`, `utf8_bytes`	yes
`Parser.FastString.Spec`	`lemma_concatMap_utf8_enc_char_nth`	`Parser.FastString.RoundTripLemmas`	`nth_byte`, `utf8_enc_char`	yes
`Parser.FastString.Spec`	`lemma_utf8_bytes_build_string`	`Parser.FastString.RoundTripLemmas`	`utf8_bytes`, `utf8_enc_char`	yes
`Parser.FastString.Spec`	`utf8_bytes_singleton`	`Parser.FastString.Spec`	`utf8_bytes`, `utf8_enc_char`	no (has `requires`)
`Parser.FastString.Spec`	`utf8_decode_at_ascii`	`Parser.FastString.Spec`	`nth_byte`, `utf8_decode_at`	no (has `requires`)
`Parser.FastString.Spec`	`utf8_decode_encode_identity`	`Parser.FastString.Spec`	`utf8_decode_at`, `utf8_enc_char`	yes
`Parser.FastString.Spec`	`utf8_decode_all_aux_unfold`	`Parser.FastString.Spec`	`utf8_decode_all_aux`, `utf8_decode_at`	no (has `requires`)
`Parser.FastString.Spec`	`utf8_decode_all_aux_encode`	`Parser.FastString.Spec`	`utf8_decode_all_aux`, `utf8_enc_char`	yes
`Parser.FastString.Spec`	`utf8_decode_all_concatMap_identity`	`Parser.FastString.Spec`	`utf8_decode_all`, `utf8_enc_char`	yes
`Parser.FastString.Spec`	`utf8_decode_all_utf8_bytes_identity`	`Parser.FastString.Spec`	`utf8_bytes`, `utf8_decode_all`	yes
`Parser.FastString.Spec`	`chars_take_drop_append`	`Parser.FastString.Spec`	`drop_chars`, `take_chars`	yes
`Parser.FastString.Spec`	`chars_split3`	`Parser.FastString.Spec`	`drop_chars`, `slice_chars`, `take_chars`	yes
`Parser.FastString.Spec`	`utf8_decode_all_slice_by_charcount`	`Parser.FastString.Spec`	`slice_bytes`, `slice_chars`, `take_chars`, `utf8_decode_all`, `utf8_enc_char`	yes
`Parser.FastString.Spec`	`fs_byte_length_eq`	`Parser.FastString`	`fs_byte_length`, `utf8_bytes`	yes
`Parser.FastString.Spec`	`fs_byte_at_eq`	`Parser.FastString`	`fs_byte_at`, `nth_byte`, `utf8_bytes`	yes
`Parser.FastString.Spec`	`fs_byte_sub_eq`	`Parser.FastString`	`fs_byte_sub`, `slice_bytes`, `utf8_bytes`, `utf8_decode_all`	yes
`Parser.FastString.Spec`	`fs_find_byte_eq`	`Parser.FastString`	`find_byte`, `fs_find_byte`, `utf8_bytes`	yes
`Parser.FastString.Spec`	`fs_cp_at_eq`	`Parser.FastString`	`fs_cp_at`, `utf8_bytes`, `utf8_decode_at`	yes
`Parser.FastString.Spec`	`fs_cp_len_eq`	`Parser.FastString`	`fs_cp_len`, `utf8_bytes`, `utf8_decode_at`	yes
`Parser.FastString.Spec`	`utf8_decode_at_join`	`Parser.NTriples.Locality`	`is_continuation`, `utf8_decode_at`	no (has `requires`)
`Parser.FastString.Spec`	`lemma_cp_at_at_middle`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `fs_cp_at`, `is_continuation`	no (has `requires`)
`Parser.FastString.Spec`	`lemma_scan_bnode_body_cp_shift_headroom`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `is_continuation`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.FastString.Spec`	`lemma_parse_string_body_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `is_continuation`, `parse_string_body`	no (has `requires`)
`Parser.FastString.Spec`	`lemma_parse_string_literal_escapepath_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `is_continuation`, `parse_string_body`, `parse_string_literal`, `scan_string_fast`	no (has `requires`)
`Parser.FastString.Spec`	`lemma_parse_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_bnode`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.FastString.Spec`	`lemma_parse_subject_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_subject`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.FastString.Spec`	`lemma_parse_object_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_object`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.FastString.Spec`	`lemma_parse_graph_label_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_graph_label`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.FastString.Spec`	`lemma_parse_opt_graph_label_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_opt_graph_label`, `pws`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.FastString.Spec`	`lemma_build_string_utf8_bytes_general`	`RDF.NTriples.RoundTrip`	`utf8_bytes`, `utf8_enc_char`	yes
`Parser.FastString.Spec`	`lemma_build_string_byte_length_general`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `utf8_enc_char`	yes
`Parser.FastString.Spec`	`lemma_utf8_enc_char_iri_safe`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `is_iri_forbidden_codepoint`, `utf8_enc_char`	no (has `requires`)
`Parser.JSON`	`lemma_json_val_of_response_roundtrip`	`SPARQL.Protocol.RoundTrip`	`json_get_array`, `json_get_field`, `json_get_string_array`, `parse_binding_row`	yes
`Parser.JSONResults`	`lemma_json_val_of_response_roundtrip`	`SPARQL.Protocol.RoundTrip`	`json_get_array`, `json_get_field`, `json_get_string_array`, `parse_binding_row`	yes
`Parser.NQuads`	`lemma_parse_graph_label_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_graph_label`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_opt_graph_label_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri_raw`, `parse_opt_graph_label`, `pws`, `scan_iri_end`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_opt_graph_label_none_dot_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_opt_graph_label`, `pws`	no (has `requires`)
`Parser.NQuads`	`lemma_nq_skip_line_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `nq_skip_line`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_nquad_iri_nograph_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri`, `parse_iri_raw`, `parse_nquad`, `parse_object`, `parse_subject`, `pws`, `scan_iri_end`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_graph_label_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_graph_label`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_opt_graph_label_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_opt_graph_label`, `pws`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.NQuads`	`lemma_parse_nquad_shift_generic`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri`, `parse_nquad`, `parse_object`, `parse_opt_graph_label`, `parse_subject`, `pws`	no (has `requires`)
`Parser.NQuads`	`stream_parse_single_chunk_shape`	`RDF.NQuads.Streaming`	`dataset_finalise`, `fs_byte_length`, `parse_nquads_acc`	yes
`Parser.NQuads`	`parse_nquads_acc_concat_line_empty_complete`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	yes
`Parser.NQuads`	`parse_nquads_acc_concat_line_empty_carry`	`RDF.NQuads.Streaming`	`fs_byte_length`, `parse_nquads_acc`	yes
`Parser.NQuads`	`lemma_nq_skip_line_shift_exact`	`RDF.NQuads.Streaming`	`fs_byte_at`, `fs_byte_length`, `nq_skip_line`	no (has `requires`)
`Parser.NQuads`	`lw_ds_step_via_parse_nquad`	`RDF.NQuads.Streaming`	`dataset_add_quad`, `parse_nquad`	yes
`Parser.NQuads`	`stream_consume_single_chunk_shape`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `fs_byte_length`	yes
`Parser.NQuads`	`fold_nquads_acc_eq_parse_nquads_acc`	`RDF.NQuads.Streaming`	`fold_nquads_acc`, `parse_nquads_acc`	yes
`Parser.NTriples`	`lemma_scan_iri_end_shift`	`Parser.NTriples.Locality`	`fs_byte_length`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_scan_iri_end_shift_from_start`	`Parser.NTriples.Locality`	`fs_byte_length`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_scan_iri_end_shift_headroom`	`Parser.NTriples.Locality`	`fs_byte_length`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_pws_shift`	`Parser.NTriples.Locality`	`fs_byte_length`, `pws`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_iri_raw_fastpath_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_subject_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri_raw`, `parse_subject`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_object_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri_raw`, `parse_object`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_iri_body_acc_shift`	`Parser.NTriples.Locality`	`fs_byte_length`, `parse_iri_body_acc`	no (has `requires`)
`Parser.NTriples`	`lemma_scan_iri_end_success_bound`	`Parser.NTriples.Locality`	`fs_byte_length`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_iri_body_acc_success_bound`	`Parser.NTriples.Locality`	`fs_byte_length`, `parse_iri_body_acc`	no (has `requires`)
`Parser.NTriples`	`lemma_scan_bnode_body_cp_shift_headroom`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `is_continuation`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.NTriples`	`lemma_scan_string_fast_shift_headroom`	`Parser.NTriples.Locality`	`fs_byte_length`, `scan_string_fast`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_string_body_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `is_continuation`, `parse_string_body`	no (has `requires`)
`Parser.NTriples`	`lemma_scan_string_fast_shift_hasescapes`	`Parser.NTriples.Locality`	`fs_byte_length`, `scan_string_fast`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_string_literal_fastpath_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_string_literal`, `scan_string_fast`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_string_literal_escapepath_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `is_continuation`, `parse_string_body`, `parse_string_literal`, `scan_string_fast`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_lang_tag_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_alpha`, `is_lang_char`, `parse_lang_tag`, `ptake_while_scan`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_datatype_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_datatype`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_graph_label_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_graph_label`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_opt_graph_label_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri_raw`, `parse_opt_graph_label`, `pws`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_opt_graph_label_none_dot_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_opt_graph_label`, `pws`	no (has `requires`)
`Parser.NTriples`	`lemma_skip_eol_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `skip_eol`	no (has `requires`)
`Parser.NTriples`	`lemma_nt_skip_to_eol_shift`	`Parser.NTriples.Locality`	`fs_byte_length`, `nt_skip_to_eol`	no (has `requires`)
`Parser.NTriples`	`lemma_pws_noop`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_nt_ws`, `pws`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_nquad_iri_nograph_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri`, `parse_iri_raw`, `parse_nquad`, `parse_object`, `parse_subject`, `pws`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_bnode`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_subject_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_subject`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_object_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_object`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_literal_plain_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_literal`, `parse_string_literal`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_literal_lang_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_alpha`, `is_lang_char`, `parse_literal`, `parse_string_literal`, `ptake_while_scan`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_literal_datatype_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_datatype`, `parse_literal`, `parse_string_literal`, `rdf_dir_lang_string`, `rdf_lang_string`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_object_literal_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_literal`, `parse_object`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_graph_label_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_graph_label`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_opt_graph_label_bnode_shift`	`Parser.NTriples.Locality`	`fs_byte_at`, `fs_byte_index`, `fs_byte_length`, `fs_cp_at`, `is_bnode_start_cp`, `is_continuation`, `parse_opt_graph_label`, `pws`, `scan_bnode_body_cp`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_nquad_shift_generic`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri`, `parse_nquad`, `parse_object`, `parse_opt_graph_label`, `parse_subject`, `pws`	no (has `requires`)
`Parser.NTriples`	`lemma_skip_comment_shift`	`RDF.NQuads.Streaming`	`fs_byte_index`, `fs_byte_length`, `nt_skip_to_eol`, `skip_comment`	no (has `requires`)
`Parser.NTriples`	`checkpoint_a_closed_triple_round_trip`	`RDF.NTriples.RoundTrip`	`nq_line_for_triple_default_graph`, `parse_triple`	yes
`Parser.NTriples`	`lemma_scan_iri_end_build_string`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_iri_raw_build_string`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `parse_iri_raw`	yes
`Parser.NTriples`	`lemma_parse_iri_build_string`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `parse_iri`	no (has `requires`)
`Parser.NTriples`	`lemma_term_iri_round_trip_build_string`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `nq_term_to_string`, `parse_object`	no (has `requires`)
`Parser.NTriples`	`lemma_term_iri_round_trip`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `nq_term_to_string`, `parse_object`	no (has `requires`)
`Parser.NTriples`	`lemma_iri_round_trip`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `parse_iri`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_subject_iri_round_trip_build_string`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `nq_subject_to_string`, `parse_subject`	no (has `requires`)
`Parser.NTriples`	`lemma_subject_iri_round_trip`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `nq_subject_to_string`, `parse_subject`	no (has `requires`)
`Parser.NTriples`	`lemma_scan_iri_end_bracket_witness`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_iri_bracket_shift_prereqs`	`RDF.NTriples.RoundTrip`	`fs_byte_index`, `fs_byte_length`, `is_iri_body_char`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_pws_one_space`	`RDF.NTriples.RoundTrip`	`fs_byte_index`, `fs_byte_length`, `is_nt_ws`, `pws`	no (has `requires`)
`Parser.NTriples`	`lemma_utf8_enc_char_iri_safe`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `is_iri_forbidden_codepoint`, `utf8_enc_char`	no (has `requires`)
`Parser.NTriples`	`lemma_scan_iri_end_one_char_walk`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_scan_iri_end_build_string_utf8`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `scan_iri_end`	no (has `requires`)
`Parser.NTriples`	`lemma_parse_iri_raw_build_string_utf8`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `parse_iri_raw`	yes
`Parser.NTriples`	`lemma_parse_iri_build_string_utf8`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `parse_iri`	no (has `requires`)
`Parser.NTriples`	`lemma_term_iri_round_trip_build_string_utf8`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `nq_term_to_string`, `parse_object`	no (has `requires`)
`Parser.NTriples`	`lemma_term_iri_round_trip_utf8`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `nq_term_to_string`, `parse_object`	no (has `requires`)
`Parser.RIFXML`	`lemma_parse_none_yields_false`	`RIF.Core.Tests`	`parse_rif_program`, `run_rif_select_rows`	no (has `requires`)
`RDF.Bytes`	`lemma_int_of_byte_of_int`	`RDF.Bytes`	`byte_of_int`, `int_of_byte`	yes
`RDF.Bytes`	`lemma_map_byte_roundtrip`	`RDF.Bytes`	`byte_of_int`, `byte_to_spec_byte`	yes
`RDF.Bytes`	`lemma_bytes_to_string_of_bytes_of_string`	`RDF.Bytes`	`bytes_of_string`, `bytes_to_string`	yes
`RDF.Bytes`	`lemma_parse_write_u32_le_inverse`	`RDF.Bytes`	`parse_u32_le`, `write_u32_le`	yes
`RDF.Bytes`	`lemma_write_u64_le_decompose`	`RDF.Bytes`	`write_u32_le`, `write_u64_le`	no (has `requires`)
`RDF.Bytes`	`lemma_parse_u64_decompose`	`RDF.Bytes`	`parse_u32_le`, `parse_u64_le`	yes
`RDF.Bytes`	`lemma_parse_write_u64_le_inverse`	`RDF.Bytes`	`parse_u64_le`, `write_u64_le`	yes
`RDF.Bytes`	`lemma_parse_string_of_length_inverse`	`RDF.Bytes`	`bytes_of_string`, `parse_string_of_length`	yes
`RDF.Bytes`	`lemma_byte_to_hex_21`	`RDF.CottasStore.BaseWriter`	`byte_of_int`, `byte_to_hex`	yes
`RDF.Bytes`	`lemma_byte_to_hex_250`	`RDF.CottasStore.BaseWriter`	`byte_of_int`, `byte_to_hex`	yes
`RDF.Bytes`	`lemma_byte_to_hex_6`	`RDF.CottasStore.BaseWriter`	`byte_of_int`, `byte_to_hex`	yes
`RDF.Bytes`	`lemma_version_field_bytes_eq`	`RDF.CottasStore.BaseWriter`	`byte_of_int`, `version_field_bytes`	yes
`RDF.Bytes`	`lemma_bytes_to_hex_unfold`	`RDF.CottasStore.BaseWriter`	`byte_of_int`, `byte_to_hex`, `bytes_to_hex`	yes
`RDF.Bytes`	`lemma_version_field_hex_eq`	`RDF.CottasStore.BaseWriter`	`bytes_to_hex`, `version_field_bytes`	yes
`RDF.Bytes`	`lemma_version_field_roundtrip`	`RDF.CottasStore.BaseWriter`	`bytes_to_hex`, `cottas_format_version`, `parse_file_metadata_version_hex`, `version_field_bytes`	yes
`RDF.Bytes`	`lemma_parse_n_u64s_one`	`RDF.CottasStore.CompoundPresenceWriter`	`parse_n_u64s`, `write_u64_le`	yes
`RDF.Bytes`	`lemma_serialize_compound_presence_empty_shape`	`RDF.CottasStore.CompoundPresenceWriter`	`copo_magic`, `copo_version`, `serialize_compound_presence`, `write_u32_le`, `write_u64_le`	yes
`RDF.Bytes`	`lemma_build_offs_cons`	`RDF.CottasStore.DictWriter`	`build_offs`, `cum_final`, `tok_byte_len`, `write_u64_le`	no (has `requires`)
`RDF.Bytes`	`lemma_parse_n_u64s_one`	`RDF.CottasStore.OffsetsWriter`	`parse_n_u64s`, `write_u64_le`	yes
`RDF.Bytes`	`lemma_serialize_offsets_empty_shape`	`RDF.CottasStore.OffsetsWriter`	`coto_magic`, `coto_version`, `serialize_offsets`, `write_u32_le`, `write_u64_le`	yes
`RDF.CottasStore.BaseWriter`	`lemma_version_field_bytes_eq`	`RDF.CottasStore.BaseWriter`	`byte_of_int`, `version_field_bytes`	yes
`RDF.CottasStore.BaseWriter`	`lemma_version_field_hex_eq`	`RDF.CottasStore.BaseWriter`	`bytes_to_hex`, `version_field_bytes`	yes
`RDF.CottasStore.BaseWriter`	`lemma_version_field_roundtrip`	`RDF.CottasStore.BaseWriter`	`bytes_to_hex`, `cottas_format_version`, `parse_file_metadata_version_hex`, `version_field_bytes`	yes
`RDF.CottasStore.ColumnSeq`	`column_decode_sound`	`RDF.CottasStore.ColumnSeq`	`column_to_list`, `probe_parquet_column_decode_in_row_group_seq`	no (has `requires`)
`RDF.CottasStore.CompoundPresenceWriter`	`lemma_parse_n_u64s_one`	`RDF.CottasStore.CompoundPresenceWriter`	`parse_n_u64s`, `write_u64_le`	yes
`RDF.CottasStore.CompoundPresenceWriter`	`lemma_serialize_compound_presence_empty_shape`	`RDF.CottasStore.CompoundPresenceWriter`	`copo_magic`, `copo_version`, `serialize_compound_presence`, `write_u32_le`, `write_u64_le`	yes
`RDF.CottasStore.CompoundPresenceWriter`	`lemma_parse_serialize_compound_presence_empty_case`	`RDF.CottasStore.CompoundPresenceWriter`	`parse_compound_presence`, `serialize_compound_presence`	yes
`RDF.CottasStore.CompoundPresenceWriter`	`lemma_parse_n_u64s_serialize_u64_list`	`RDF.CottasStore.CompoundPresenceWriter`	`all_lt`, `parse_n_u64s`, `serialize_u64_list`	no (has `requires`)
`RDF.CottasStore.CompoundPresenceWriter`	`lemma_parse_serialize_compound_presence`	`RDF.CottasStore.CompoundPresenceWriter`	`all_lt`, `last_of_or`, `parse_compound_presence`, `serialize_compound_presence`	no (has `requires`)
`RDF.CottasStore.DictWriter`	`lemma_parse_serialize_dict_empty_case`	`RDF.CottasStore.DictWriter`	`parse_dict`, `serialize_dict`	yes
`RDF.CottasStore.DictWriter`	`lemma_build_offs_acc_final`	`RDF.CottasStore.DictWriter`	`build_offs_acc`, `cum_final`	no (has `requires`)
`RDF.CottasStore.DictWriter`	`lemma_parse_n_offsets_build_offs_acc`	`RDF.CottasStore.DictWriter`	`build_offs_acc`, `cum_final`, `cum_offs`, `parse_n_offsets`	no (has `requires`)
`RDF.CottasStore.DictWriter`	`lemma_parse_tokens_from_offsets_build_data`	`RDF.CottasStore.DictWriter`	`build_data`, `cum_final`, `cum_offs`, `parse_tokens_from_offsets`	no (has `requires`)
`RDF.CottasStore.DictWriter`	`lemma_cum_offs_length`	`RDF.CottasStore.DictWriter`	`cum_final`, `cum_offs`	no (has `requires`)
`RDF.CottasStore.DictWriter`	`lemma_build_offs_cons`	`RDF.CottasStore.DictWriter`	`build_offs`, `cum_final`, `tok_byte_len`, `write_u64_le`	no (has `requires`)
`RDF.CottasStore.DictWriter`	`lemma_cum_offs_cons`	`RDF.CottasStore.DictWriter`	`cum_offs`, `tok_byte_len`	no (has `requires`)
`RDF.CottasStore.DictWriter`	`lemma_cum_final_cons`	`RDF.CottasStore.DictWriter`	`cum_final`, `tok_byte_len`	no (has `requires`)
`RDF.CottasStore.DictWriter`	`lemma_parse_n_offsets_build_offs`	`RDF.CottasStore.DictWriter`	`build_offs`, `cum_final`, `cum_offs`, `parse_n_offsets`	no (has `requires`)
`RDF.CottasStore.DictWriter`	`lemma_parse_serialize_dict_cons`	`RDF.CottasStore.DictWriter`	`cum_final`, `header_size`, `id_size`, `offset_size`, `parse_dict`, `serialize_dict`	no (has `requires`)
`RDF.CottasStore.DictWriter`	`lemma_parse_serialize_dict`	`RDF.CottasStore.DictWriter`	`cum_final`, `header_size`, `id_size`, `offset_size`, `parse_dict`, `serialize_dict`	no (has `requires`)
`RDF.CottasStore.OffsetsWriter`	`lemma_parse_n_u64s_one`	`RDF.CottasStore.OffsetsWriter`	`parse_n_u64s`, `write_u64_le`	yes
`RDF.CottasStore.OffsetsWriter`	`lemma_serialize_offsets_empty_shape`	`RDF.CottasStore.OffsetsWriter`	`coto_magic`, `coto_version`, `serialize_offsets`, `write_u32_le`, `write_u64_le`	yes
`RDF.CottasStore.OffsetsWriter`	`lemma_parse_serialize_offsets_empty_case`	`RDF.CottasStore.OffsetsWriter`	`parse_offsets`, `serialize_offsets`	yes
`RDF.CottasStore.OffsetsWriter`	`lemma_parse_n_u64s_serialize_u64_list`	`RDF.CottasStore.OffsetsWriter`	`all_lt`, `parse_n_u64s`, `serialize_u64_list`	no (has `requires`)
`RDF.CottasStore.OffsetsWriter`	`lemma_parse_n_u32s_serialize_u32_list`	`RDF.CottasStore.OffsetsWriter`	`all_lt`, `parse_n_u32s`, `serialize_u32_list`	no (has `requires`)
`RDF.CottasStore.OffsetsWriter`	`lemma_parse_serialize_offsets`	`RDF.CottasStore.OffsetsWriter`	`all_lt`, `last_of_or`, `parse_offsets`, `serialize_offsets`	no (has `requires`)
`RDF.CottasStore.OffsetsWriter`	`lemma_flatten_all_lt`	`RDF.CottasStore.SubjectOffsetsWriter`	`all_lt`, `flatten_ranges`, `ranges_all_lt`	no (has `requires`)
`RDF.CottasStore.PageCache`	`find_oldest_aux_returns_present`	`RDF.CottasStore.PageCache.Bounds`	`find_oldest_aux`, `key_eq`	yes
`RDF.CottasStore.PageCache`	`entries_after_bound`	`RDF.CottasStore.PageCache.Bounds`	`lookup_entry`, `replace_entry`	no (has `requires`)
`RDF.CottasStore.PageCache`	`entries_capped_bound`	`RDF.CottasStore.PageCache.Bounds`	`drop_entry`, `find_oldest`	no (has `requires`)
`RDF.CottasStore.PresenceWriter`	`lemma_parse_serialize_presence_empty_case`	`RDF.CottasStore.PresenceWriter`	`parse_presence`, `serialize_presence`	yes
`RDF.CottasStore.PresenceWriter`	`lemma_parse_serialize_presence`	`RDF.CottasStore.PresenceWriter`	`parse_presence`, `serialize_presence`	no (has `requires`)
`RDF.CottasStore.SubjectOffsetsWriter`	`lemma_unflatten_flatten`	`RDF.CottasStore.SubjectOffsetsWriter`	`flatten_ranges`, `unflatten_ranges`	yes
`RDF.CottasStore.SubjectOffsetsWriter`	`lemma_flatten_all_lt`	`RDF.CottasStore.SubjectOffsetsWriter`	`all_lt`, `flatten_ranges`, `ranges_all_lt`	no (has `requires`)
`RDF.CottasStore.SubjectOffsetsWriter`	`lemma_parse_serialize_subject_offsets`	`RDF.CottasStore.SubjectOffsetsWriter`	`parse_subject_offsets`, `ranges_all_lt`, `serialize_subject_offsets`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_step_is_dedup_of_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`graph_dedup_sort`, `rho_df_closure_step`, `rho_df_closure_step_pre_dedup`	yes
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_rho_df_closure_iter_shift`	`RDF.Entailment.RDFS.RhoDFClosure`	`rho_df_closure_iter`, `rho_df_closure_step`	yes
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_after_row1_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_after_row2_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_after_row3_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_after_row4_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subClassOf`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_after_row5_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subClassOf`, `rdfs_rule_subClassOf_trans`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDF.Entailment.RDFS.RhoDFClosure`	`lemma_is_rho_df_frag_is_for_all`	`RDF.Entailment.RDFS.RhoDFClosure`	`is_rho_df_frag`, `is_rho_df_frag_triple`	yes
`RDF.Entailment.Simple`	`lemma_simple_entails_unfold`	`RDF.Entailment.Simple.Refinement`	`simple_entails`, `try_match`	yes
`RDF.Graph`	`lemma_step_is_dedup_of_pre_dedup`	`RDF.Entailment.RDFS.FixedPoint`	`graph_dedup_sort`, `rdfs_closure_step`	yes
`RDF.Graph`	`lemma_rho_df_step_is_dedup_of_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`graph_dedup_sort`, `rho_df_closure_step`, `rho_df_closure_step_pre_dedup`	yes
`RDF.Graph`	`lemma_subject_to_key_eq_term_to_key_opt`	`RDF.Indexed.KeyInjectivity`	`subject_to_key`, `subject_to_term`, `term_to_key_opt`	yes
`RDF.Graph`	`lemma_po_key_eq_po_key_opt`	`RDF.Indexed.KeyInjectivity`	`po_key`, `po_key_opt`, `subject_to_term`	yes
`RDF.Graph`	`lemma_term_to_subject_roundtrip`	`RDF.Indexed.KeyInjectivity`	`subject_to_term`, `term_to_subject`	no (has `requires`)
`RDF.Graph`	`lemma_po_key_opt_some_iff_term_to_subject_some`	`RDF.Indexed.KeyInjectivity`	`po_key_opt`, `term_to_subject`	yes
`RDF.Graph`	`lemma_literal_key_decomposes_1`	`RDF.Indexed.KeyInjectivity`	`lit_key_dir_part`, `lit_key_lang_part`, `term_to_key_total`, `unit_sep`	yes
`RDF.Graph`	`lemma_literal_key_decomposes_2`	`RDF.Indexed.KeyInjectivity`	`lit_key_dir_part`, `lit_key_lang_part`, `unit_sep`	yes
`RDF.Graph`	`lemma_literal_key_decomposes_3`	`RDF.Indexed.KeyInjectivity`	`lit_key_dir_part`, `lit_key_lang_part`, `unit_sep`	yes
`RDF.Graph`	`lemma_triple_term_key_decomposes_1`	`RDF.Indexed.KeyInjectivity`	`subject_to_key`, `term_to_key_total`, `unit_sep`	yes
`RDF.Graph`	`lemma_triple_term_key_decomposes_2`	`RDF.Indexed.KeyInjectivity`	`term_to_key_total`, `unit_sep`	yes
`RDF.Graph.Executable`	`stream_parse_single_chunk_shape`	`RDF.NQuads.Streaming`	`dataset_finalise`, `fs_byte_length`, `parse_nquads_acc`	yes
`RDF.Indexed`	`lemma_build_indexed_wf_pred`	`OWL.Semantics.MemLemmas`	`bucket_lookup`, `build_indexed`	yes
`RDF.Indexed`	`lemma_build_indexed_wf_subj_weak`	`OWL.Semantics.MemLemmas`	`bucket_key_subj`, `bucket_lookup`, `build_indexed`	yes
`RDF.Indexed`	`lemma_build_indexed_wf_obj_weak`	`OWL.Semantics.MemLemmas`	`bucket_key_obj`, `bucket_lookup`, `build_indexed`	yes
`RDF.Indexed`	`lemma_build_indexed_wf_sp_weak`	`OWL.Semantics.MemLemmas`	`bucket_key_sp`, `bucket_lookup`, `build_indexed`	yes
`RDF.Indexed`	`lemma_build_indexed_wf_po_weak`	`OWL.Semantics.MemLemmas`	`bucket_key_po`, `bucket_lookup`, `build_indexed`	yes
`RDF.Indexed`	`lemma_find_objects_complete`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `find_objects_indexed`	no (has `requires`)
`RDF.Indexed`	`lemma_after_row1_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDF.Indexed`	`lemma_after_row2_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDF.Indexed`	`lemma_after_row3_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDF.Indexed`	`lemma_after_row4_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subClassOf`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDF.Indexed`	`lemma_after_row5_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subClassOf`, `rdfs_rule_subClassOf_trans`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDF.Indexed`	`lemma_build_bucket_complete`	`RDF.Indexed.Completeness`	`bucket_lookup`, `build_bucket`	no (has `requires`)
`RDF.Indexed`	`lemma_build_indexed_complete_pred`	`RDF.Indexed.Completeness`	`bucket_lookup`, `build_indexed`	yes
`RDF.Indexed`	`lemma_build_indexed_complete_subj`	`RDF.Indexed.Completeness`	`bucket_lookup`, `build_indexed`, `subject_to_key`	yes
`RDF.Indexed`	`lemma_build_indexed_complete_sp`	`RDF.Indexed.Completeness`	`bucket_lookup`, `build_indexed`, `sp_key`	yes
`RDF.Indexed`	`lemma_build_indexed_complete_obj`	`RDF.Indexed.Completeness`	`bucket_lookup`, `build_indexed`, `term_to_key_opt`	yes
`RDF.Indexed`	`lemma_build_indexed_complete_po`	`RDF.Indexed.Completeness`	`bucket_lookup`, `build_indexed`, `po_key_opt`	yes
`RDF.Indexed`	`lemma_build_indexed_complete_so`	`RDF.Indexed.Completeness`	`bucket_lookup`, `build_indexed`, `so_key_opt`	yes
`RDF.Indexed`	`lemma_sp_key_decomposes`	`RDF.Indexed.KeyInjectivity`	`sp_key`, `subject_to_key`	yes
`RDF.Indexed`	`lemma_subject_to_key_eq_term_to_key_opt`	`RDF.Indexed.KeyInjectivity`	`subject_to_key`, `subject_to_term`, `term_to_key_opt`	yes
`RDF.Indexed`	`lemma_po_key_eq_po_key_opt`	`RDF.Indexed.KeyInjectivity`	`po_key`, `po_key_opt`, `subject_to_term`	yes
`RDF.Indexed`	`lemma_po_key_opt_some_iff_term_to_subject_some`	`RDF.Indexed.KeyInjectivity`	`po_key_opt`, `term_to_subject`	yes
`RDF.Indexed`	`lemma_po_key_decomposes`	`RDF.Indexed.KeyInjectivity`	`po_key`, `subject_to_key`	yes
`RDF.Indexed`	`lemma_literal_key_decomposes_1`	`RDF.Indexed.KeyInjectivity`	`lit_key_dir_part`, `lit_key_lang_part`, `term_to_key_total`, `unit_sep`	yes
`RDF.Indexed`	`lemma_literal_key_decomposes_2`	`RDF.Indexed.KeyInjectivity`	`lit_key_dir_part`, `lit_key_lang_part`, `unit_sep`	yes
`RDF.Indexed`	`lemma_literal_key_decomposes_3`	`RDF.Indexed.KeyInjectivity`	`lit_key_dir_part`, `lit_key_lang_part`, `unit_sep`	yes
`RDF.Indexed`	`lemma_triple_term_key_decomposes_1`	`RDF.Indexed.KeyInjectivity`	`subject_to_key`, `term_to_key_total`, `unit_sep`	yes
`RDF.Indexed`	`lemma_triple_term_key_decomposes_2`	`RDF.Indexed.KeyInjectivity`	`term_to_key_total`, `unit_sep`	yes
`RDF.List.Helpers`	`lemma_eval_bgp_store_unfold`	`SPARQL11.Algebra.BGPRefinement`	`choose_best_tp`, `concatMap_tr`, `eval_bgp_store_from_mu_fuel`, `eval_single_tp_store`	yes
`RDF.NQuads.Serialize`	`checkpoint_a_closed_triple_round_trip`	`RDF.NTriples.RoundTrip`	`nq_line_for_triple_default_graph`, `parse_triple`	yes
`RDF.NQuads.Serialize`	`lemma_term_iri_round_trip_build_string`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `nq_term_to_string`, `parse_object`	no (has `requires`)
`RDF.NQuads.Serialize`	`lemma_term_iri_round_trip`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `nq_term_to_string`, `parse_object`	no (has `requires`)
`RDF.NQuads.Serialize`	`lemma_parse_subject_iri_round_trip_build_string`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `nq_subject_to_string`, `parse_subject`	no (has `requires`)
`RDF.NQuads.Serialize`	`lemma_subject_iri_round_trip`	`RDF.NTriples.RoundTrip`	`is_iri_body_char`, `nq_subject_to_string`, `parse_subject`	no (has `requires`)
`RDF.NQuads.Serialize`	`lemma_term_iri_round_trip_build_string_utf8`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `nq_term_to_string`, `parse_object`	no (has `requires`)
`RDF.NQuads.Serialize`	`lemma_term_iri_round_trip_utf8`	`RDF.NTriples.RoundTrip`	`fs_byte_length`, `is_iri_body_char`, `nq_term_to_string`, `parse_object`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_u8_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`parse_u8`, `write_u8`	yes
`RDF.Store.Columnar.DeltaLog`	`lemma_lstring_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`field_byte_len`, `parse_lstring`, `serialize_lstring`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_lstring_length`	`RDF.Store.Columnar.DeltaLog`	`field_byte_len`, `max_field_chars`, `serialize_lstring`	yes
`RDF.Store.Columnar.DeltaLog`	`lemma_term_length`	`RDF.Store.Columnar.DeltaLog`	`max_field_chars`, `serialize_term`, `term_ok`	yes
`RDF.Store.Columnar.DeltaLog`	`lemma_term_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`parse_term`, `serialize_term`, `term_ok`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_subject_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`parse_subject`, `serialize_subject`, `subject_ok`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_triple_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`parse_triple`, `serialize_triple`, `triple_ok`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_graph_opt_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`graph_opt_ok`, `parse_graph_opt`, `serialize_graph_opt`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_delta_entry_payload_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`delta_entry_ok`, `parse_delta_entry_payload`, `serialize_delta_entry_payload`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_subject_length_bound`	`RDF.Store.Columnar.DeltaLog`	`max_field_chars`, `serialize_subject`, `subject_ok`	yes
`RDF.Store.Columnar.DeltaLog`	`lemma_graph_opt_length_bound`	`RDF.Store.Columnar.DeltaLog`	`graph_opt_ok`, `max_field_chars`, `serialize_graph_opt`	yes
`RDF.Store.Columnar.DeltaLog`	`lemma_triple_length_bound`	`RDF.Store.Columnar.DeltaLog`	`max_field_chars`, `serialize_triple`, `triple_ok`	yes
`RDF.Store.Columnar.DeltaLog`	`lemma_delta_entry_payload_length`	`RDF.Store.Columnar.DeltaLog`	`delta_entry_ok`, `serialize_delta_entry_payload`	yes
`RDF.Store.Columnar.DeltaLog`	`lemma_delta_entry_frame_ok`	`RDF.Store.Columnar.DeltaLog`	`delta_entry_frame_ok`, `delta_entry_ok`	yes
`RDF.Store.Columnar.DeltaLog`	`lemma_delta_entry_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`delta_entry_ok`, `parse_delta_entry`, `serialize_delta_entry`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_ops_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`delta_batch_ops_ok`, `parse_n_delta_entries`, `serialize_ops`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_batch_body_length`	`RDF.Store.Columnar.DeltaLog`	`delta_batch_ok`, `serialize_delta_batch_body`, `serialize_ops`	yes
`RDF.Store.Columnar.DeltaLog`	`lemma_delta_batch_frame_ok`	`RDF.Store.Columnar.DeltaLog`	`delta_batch_ok`, `serialize_delta_batch_body`	yes
`RDF.Store.Columnar.DeltaLog`	`lemma_delta_batch_body_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`delta_batch_ok`, `parse_delta_batch_body`, `serialize_delta_batch_body`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_delta_batch_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`delta_batch_ok`, `parse_delta_batch`, `serialize_delta_batch`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_log_header_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`parse_log_header`, `serialize_log_header`	yes
`RDF.Store.Columnar.DeltaLog`	`lemma_parse_log_batches_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`delta_batches_ok`, `parse_log_batches`, `serialize_delta_batches`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_log_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`delta_batches_ok`, `parse_log`, `serialize_log`	no (has `requires`)
`RDF.Store.Columnar.DeltaLog`	`lemma_compacted_epoch_roundtrip`	`RDF.Store.Columnar.DeltaLog`	`parse_compacted_epoch`, `serialize_compacted_epoch`	yes
`RDF.Store.Columnar.DeltaMerge`	`lemma_mem_matches_bound_acc`	`RDF.Store.Columnar.DeltaMerge`	`bound_matches`, `triple_matches_bound_acc`	yes
`RDF.Store.Columnar.DeltaMerge`	`lemma_mem_triple_matches_bound`	`RDF.Store.Columnar.DeltaMerge`	`bound_matches`, `triple_matches_bound`	yes
`RDF.Store.Columnar.DeltaMerge`	`lemma_merge_on_read_matches_apply_entries`	`RDF.Store.Columnar.DeltaMerge`	`apply_entries_ref`, `delta_resolved_empty`, `fold_entries_for_graph`, `merge_on_read`, `triple_matches_bound`	yes
`RDF.Term`	`lemma_parse_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`RDF.Term`	`lemma_parse_subject_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri_raw`, `parse_subject`, `scan_iri_end`	no (has `requires`)
`RDF.Term`	`lemma_parse_object_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri_raw`, `parse_object`, `scan_iri_end`	no (has `requires`)
`RDF.Term`	`lemma_parse_datatype_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_datatype`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`RDF.Term`	`lemma_parse_graph_label_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_graph_label`, `parse_iri_raw`, `scan_iri_end`	no (has `requires`)
`RDF.Term`	`lemma_parse_opt_graph_label_iri_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri_raw`, `parse_opt_graph_label`, `pws`, `scan_iri_end`	no (has `requires`)
`RDF.Term`	`lemma_parse_nquad_iri_nograph_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri`, `parse_iri_raw`, `parse_nquad`, `parse_object`, `parse_subject`, `pws`, `scan_iri_end`	no (has `requires`)
`RDF.Term`	`lemma_parse_literal_datatype_shift`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `parse_datatype`, `parse_literal`, `parse_string_literal`, `rdf_dir_lang_string`, `rdf_lang_string`	no (has `requires`)
`RDF.Term`	`lemma_parse_nquad_shift_generic`	`Parser.NTriples.Locality`	`fs_byte_index`, `fs_byte_length`, `is_iri`, `parse_iri`, `parse_nquad`, `parse_object`, `parse_opt_graph_label`, `parse_subject`, `pws`	no (has `requires`)
`RDF.Term`	`lemma_join_canon_term_eq`	`RDF.Term`	`join_canon_term`, `rdf_term_eq`	no (has `requires`)
`RDF.Term`	`theorem_sr2_witness_keys_now_agree`	`SPARQL11.Algebra.Refinement`	`rdf_term_eq`, `sm_compatible`, `sm_join_key`	no (has `requires`)
`RDF.Term`	`theorem_join_key_no_finer_than_compatibility`	`SPARQL11.Algebra.Refinement`	`rdf_term_eq`, `sm_join_key`	no (has `requires`)
`RDF.Term`	`lemma_sm_submap_lookup`	`SPARQL11.Algebra.Refinement`	`rdf_term_eq`, `sm_lookup`, `sm_submap`	no (has `requires`)
`RDF.Term`	`lemma_ebv_langstring_agrees`	`SPARQL11.Expression.Refinement`	`ebv`, `ebv_checked`, `rdf_lang_string`	no (has `requires`)
`RDF.Vocabulary.Axioms`	`lemma_rho_df_vocab_distinct`	`RDF.Entailment.RDFS.Completeness`	`i_rdf_type`, `i_rdfs_domain`, `i_rdfs_range`, `i_rdfs_subClassOf`, `i_rdfs_subPropertyOf`	yes
`RDF.Vocabulary.Axioms`	`lemma_vocab_agree`	`RDF.Entailment.RDFS.Refinement`	`i_rdf_Property`, `i_rdf_type`, `i_rdfs_Class`, `i_rdfs_ContainerMembershipProperty`, `i_rdfs_domain`, `i_rdfs_member`, `i_rdfs_range`, `i_rdfs_subClassOf`, `i_rdfs_subPropertyOf`, `rdf_Property`, `rdf_type`, `rdfs_Class`, `rdfs_ContainerMembershipProperty`, `rdfs_domain`, `rdfs_member`, `rdfs_range`, `rdfs_subClassOf`, `rdfs_subPropertyOf`	yes
`RDF.Vocabulary.Axioms`	`lemma_vocab_agree_rs2`	`RDF.Entailment.RDFS.Refinement`	`i_rdfs_Datatype`, `i_rdfs_Literal`, `i_rdfs_Resource`, `rdfs_Datatype`, `rdfs_Literal`, `rdfs_Resource`	yes
`RDFS.Closure`	`lemma_vocab_symp_agree`	`OWL.RL.Refinement`	`owl_SymmetricProperty`, `rdf_type`	yes
`RDFS.Closure`	`lemma_vocab_eqc_agree`	`OWL.RL.Refinement`	`owl_equivalentClass`, `rdfs_subClassOf`	yes
`RDFS.Closure`	`lemma_vocab_eqp_agree`	`OWL.RL.Refinement`	`owl_equivalentProperty`, `rdfs_subPropertyOf`	yes
`RDFS.Closure`	`lemma_vocab_trp_agree`	`OWL.RL.Refinement`	`owl_TransitiveProperty`, `rdf_type`	yes
`RDFS.Closure`	`lemma_vocab_dom_agree`	`OWL.RL.Refinement`	`rdfs_domain`, `rdfs_subClassOf`	yes
`RDFS.Closure`	`lemma_vocab_rng_agree`	`OWL.RL.Refinement`	`rdfs_range`, `rdfs_subClassOf`	yes
`RDFS.Closure`	`lemma_vocab_cls_oo_agree`	`OWL.RL.Refinement`	`owl_oneOf_iri`, `rdf_type`	yes
`RDFS.Closure`	`lemma_vocab_cls_int_agree`	`OWL.RL.Refinement`	`owl_intersectionOf_iri`, `rdf_type`	yes
`RDFS.Closure`	`lemma_vocab_cls_uni_agree`	`OWL.RL.Refinement`	`owl_unionOf_iri`, `rdfs_subClassOf`	yes
`RDFS.Closure`	`lemma_vocab_fp_agree`	`OWL.RL.Refinement`	`owl_FunctionalProperty`, `rdf_type`	yes
`RDFS.Closure`	`lemma_vocab_ifp_agree`	`OWL.RL.Refinement`	`owl_InverseFunctionalProperty`, `rdf_type`	yes
`RDFS.Closure`	`lemma_vocab_hv_agree`	`OWL.RL.Refinement`	`owl_hasValue_iri`, `owl_onProperty_iri`, `rdf_type`	yes
`RDFS.Closure`	`lemma_vocab_avf_agree`	`OWL.RL.Refinement`	`owl_allValuesFrom_iri`, `owl_onProperty_iri`, `rdf_type`	yes
`RDFS.Closure`	`lemma_vocab_clash_agree`	`OWL.RL.Refinement`	`owl_disjointWith_iri`, `owl_propertyDisjointWith`, `rdf_type`	yes
`RDFS.Closure`	`lemma_step_is_dedup_of_pre_dedup`	`RDF.Entailment.RDFS.FixedPoint`	`graph_dedup_sort`, `rdfs_closure_step`	yes
`RDFS.Closure`	`lemma_vocab_agree`	`RDF.Entailment.RDFS.Refinement`	`i_rdf_Property`, `i_rdf_type`, `i_rdfs_Class`, `i_rdfs_ContainerMembershipProperty`, `i_rdfs_domain`, `i_rdfs_member`, `i_rdfs_range`, `i_rdfs_subClassOf`, `i_rdfs_subPropertyOf`, `rdf_Property`, `rdf_type`, `rdfs_Class`, `rdfs_ContainerMembershipProperty`, `rdfs_domain`, `rdfs_member`, `rdfs_range`, `rdfs_subClassOf`, `rdfs_subPropertyOf`	yes
`RDFS.Closure`	`lemma_vocab_agree_rs2`	`RDF.Entailment.RDFS.Refinement`	`i_rdfs_Datatype`, `i_rdfs_Literal`, `i_rdfs_Resource`, `rdfs_Datatype`, `rdfs_Literal`, `rdfs_Resource`	yes
`RDFS.Closure`	`lemma_class_typing_rdfs`	`RDF.Entailment.RDFS.Refinement`	`is_class_type_object_rdfs`, `rdfs_Class`	no (has `requires`)
`RDFS.Closure`	`lemma_property_typing_rdfs`	`RDF.Entailment.RDFS.Refinement`	`is_property_type_object_rdfs`, `rdf_Property`	no (has `requires`)
`RDFS.Closure`	`lemma_after_row1_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDFS.Closure`	`lemma_after_row2_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDFS.Closure`	`lemma_after_row3_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDFS.Closure`	`lemma_after_row4_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subClassOf`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDFS.Closure`	`lemma_after_row5_pre_dedup`	`RDF.Entailment.RDFS.RhoDFClosure`	`build_indexed`, `rdfs_rule_domain`, `rdfs_rule_range`, `rdfs_rule_subClassOf`, `rdfs_rule_subClassOf_trans`, `rdfs_rule_subPropertyOf`, `rho_df_closure_step_pre_dedup`	no (has `requires`)
`RDFS.SchemaSplit`	`witness_stable_holds`	`RDFS.SchemaSplit`	`schema_stable_check`, `witness_stable`	yes
`RDFS.SchemaSplit`	`witness_reflective_violates`	`RDFS.SchemaSplit`	`schema_stable_check`, `witness_reflective`	yes
`RIF.Core.Tests`	`lemma_parse_none_yields_false`	`RIF.Core.Tests`	`parse_rif_program`, `run_rif_select_rows`	no (has `requires`)
`Regex.Derivative`	`cat_shift`	`Regex.Derivative`	`cat_try`, `deriv`, `mem`	no (has `requires`)
`Regex.Derivative`	`star_shift`	`Regex.Derivative`	`cat_try`, `deriv`, `mem`, `star_try`	no (has `requires`)
`Regex.Derivative`	`deriv_cat_w`	`Regex.Derivative`	`deriv`, `mem`	no (has `requires`)
`Regex.Derivative`	`deriv_star_w`	`Regex.Derivative`	`deriv`, `mem`	no (has `requires`)
`Regex.Derivative`	`deriv_correct`	`Regex.Derivative`	`deriv`, `mem`	yes
`Regex.Derivative`	`deriv_word_correct`	`Regex.Derivative`	`deriv_word`, `mem`	yes
`Regex.Derivative`	`matches_correct`	`Regex.Derivative`	`matches`, `mem`	yes
`Regex.Derivative`	`matches_norm_eq_proven`	`Regex.Exec`	`matches`, `matches_norm`	yes
`Regex.Exec`	`insert_regex_ok`	`Regex.Exec`	`insert_regex`, `mem`, `mem_alt_list`	yes
`Regex.Exec`	`alt_flatten_ok`	`Regex.Exec`	`alt_flatten`, `mem`, `mem_alt_list`	yes
`Regex.Exec`	`rebuild_alt_ok`	`Regex.Exec`	`mem`, `mem_alt_list`, `rebuild_alt`	yes
`Regex.Exec`	`has_universal_ok`	`Regex.Exec`	`has_universal`, `mem_alt_list`	no (has `requires`)
`Regex.Exec`	`ealt_ok`	`Regex.Exec`	`ealt`, `mem`	yes
`Regex.Exec`	`insert_regex_and_ok`	`Regex.Exec`	`insert_regex`, `mem`, `mem_and_list`	yes
`Regex.Exec`	`and_flatten_ok`	`Regex.Exec`	`and_flatten`, `mem`, `mem_and_list`	yes
`Regex.Exec`	`rebuild_and_ok`	`Regex.Exec`	`mem`, `mem_and_list`, `rebuild_and`	yes
`Regex.Exec`	`has_empty_ok`	`Regex.Exec`	`has_empty`, `mem_and_list`	no (has `requires`)
`Regex.Exec`	`eand_ok`	`Regex.Exec`	`eand`, `mem`	yes
`Regex.Exec`	`nderiv_cat_w`	`Regex.Exec`	`mem`, `nderiv`	no (has `requires`)
`Regex.Exec`	`nderiv_star_w`	`Regex.Exec`	`mem`, `nderiv`	no (has `requires`)
`Regex.Exec`	`nderiv_correct`	`Regex.Exec`	`mem`, `nderiv`	yes
`Regex.Exec`	`run_word_norm_correct`	`Regex.Exec`	`mem`, `run_word_norm`	yes
`Regex.Exec`	`matches_norm_correct`	`Regex.Exec`	`matches_norm`, `mem`	yes
`Regex.Exec`	`matches_norm_eq_proven`	`Regex.Exec`	`matches`, `matches_norm`	yes
`Regex.Syntax`	`cat_shift`	`Regex.Derivative`	`cat_try`, `deriv`, `mem`	no (has `requires`)
`Regex.Syntax`	`star_shift`	`Regex.Derivative`	`cat_try`, `deriv`, `mem`, `star_try`	no (has `requires`)
`Regex.Syntax`	`deriv_cat_w`	`Regex.Derivative`	`deriv`, `mem`	no (has `requires`)
`Regex.Syntax`	`deriv_star_w`	`Regex.Derivative`	`deriv`, `mem`	no (has `requires`)
`Regex.Syntax`	`deriv_correct`	`Regex.Derivative`	`deriv`, `mem`	yes
`Regex.Syntax`	`deriv_word_correct`	`Regex.Derivative`	`deriv_word`, `mem`	yes
`Regex.Syntax`	`matches_correct`	`Regex.Derivative`	`matches`, `mem`	yes
`Regex.Syntax`	`insert_regex_ok`	`Regex.Exec`	`insert_regex`, `mem`, `mem_alt_list`	yes
`Regex.Syntax`	`alt_flatten_ok`	`Regex.Exec`	`alt_flatten`, `mem`, `mem_alt_list`	yes
`Regex.Syntax`	`rebuild_alt_ok`	`Regex.Exec`	`mem`, `mem_alt_list`, `rebuild_alt`	yes
`Regex.Syntax`	`ealt_ok`	`Regex.Exec`	`ealt`, `mem`	yes
`Regex.Syntax`	`insert_regex_and_ok`	`Regex.Exec`	`insert_regex`, `mem`, `mem_and_list`	yes
`Regex.Syntax`	`and_flatten_ok`	`Regex.Exec`	`and_flatten`, `mem`, `mem_and_list`	yes
`Regex.Syntax`	`rebuild_and_ok`	`Regex.Exec`	`mem`, `mem_and_list`, `rebuild_and`	yes
`Regex.Syntax`	`eand_ok`	`Regex.Exec`	`eand`, `mem`	yes
`Regex.Syntax`	`cat_shift_gen`	`Regex.Exec`	`cat_try`, `mem`	no (has `requires`)
`Regex.Syntax`	`star_shift_gen`	`Regex.Exec`	`cat_try`, `mem`, `star_try`	no (has `requires`)
`Regex.Syntax`	`nderiv_cat_w`	`Regex.Exec`	`mem`, `nderiv`	no (has `requires`)
`Regex.Syntax`	`nderiv_star_w`	`Regex.Exec`	`mem`, `nderiv`	no (has `requires`)
`Regex.Syntax`	`nderiv_correct`	`Regex.Exec`	`mem`, `nderiv`	yes
`Regex.Syntax`	`run_word_norm_correct`	`Regex.Exec`	`mem`, `run_word_norm`	yes
`Regex.Syntax`	`matches_norm_correct`	`Regex.Exec`	`matches_norm`, `mem`	yes
`Regex.Syntax`	`nullable_correct`	`Regex.Syntax`	`mem`, `nullable`	yes
`Regex.Syntax`	`smart_alt_ok`	`Regex.Syntax`	`mem`, `smart_alt`	yes
`Regex.Syntax`	`smart_and_ok`	`Regex.Syntax`	`mem`, `smart_and`	yes
`Regex.Syntax`	`smart_not_ok`	`Regex.Syntax`	`mem`, `smart_not`	yes
`Regex.Syntax`	`cat_eps_left`	`Regex.Syntax`	`cat_try`, `mem`	yes
`Regex.Syntax`	`cat_eps_right`	`Regex.Syntax`	`cat_try`, `mem`	yes
`Regex.Syntax`	`smart_cat_ok`	`Regex.Syntax`	`mem`, `smart_cat`	yes
`Regex.Syntax`	`smart_star_ok`	`Regex.Syntax`	`mem`, `smart_star`	yes
`SPARQL.Eval.Limits`	`take_capped_aux_at_cap`	`SPARQL.Eval.Limits`	`is_enabled`, `take_capped_aux`	no (has `requires`)
`SPARQL.Eval.Limits`	`take_capped_aux_length_le`	`SPARQL.Eval.Limits`	`is_enabled`, `take_capped_aux`	no (has `requires`)
`SPARQL.Eval.Limits`	`take_capped_length_le_cap`	`SPARQL.Eval.Limits`	`is_enabled`, `take_capped`	no (has `requires`)
`SPARQL.Eval.Limits`	`take_capped_aux_unlimited`	`SPARQL.Eval.Limits`	`no_cap`, `take_capped_aux`	no (has `requires`)
`SPARQL.Eval.Limits`	`take_capped_unlimited_id`	`SPARQL.Eval.Limits`	`no_cap`, `take_capped`	yes
`SPARQL.Eval.TimeBudget`	`disabled_never_expires`	`SPARQL.Eval.TimeBudget`	`is_disabled`, `is_expired`	no (has `requires`)
`SPARQL.Eval.TimeBudget`	`enabled_expires_at_deadline`	`SPARQL.Eval.TimeBudget`	`is_disabled`, `is_expired`	no (has `requires`)
`SPARQL.FullText`	`lemma_parse_object_list_simple_1`	`SPARQL11.Parser.AskBgpRoundTrip`	`fulltext_query_pred`, `ggp_add_triple`, `group_graph_pattern`, `parse_object_list_simple`	no (has `requires`)
`SPARQL.FullText`	`lemma_parse_pred_obj_list_1`	`SPARQL11.Parser.AskBgpRoundTrip`	`fulltext_query_pred`, `ggp_add_triple`, `group_graph_pattern`, `parse_pred_obj_list`	no (has `requires`)
`SPARQL.Protocol`	`lemma_srj_single_row`	`SPARQL.Protocol.RoundTrip`	`json_row`, `json_var_list`, `serialise_response_json`	yes
`SPARQL.Protocol`	`lemma_srj_n_rows`	`SPARQL.Protocol.RoundTrip`	`json_var_list`, `serialise_response_json`	yes
`SPARQL11.Algebra`	`lemma_mem_matches_bound_acc`	`RDF.Store.Columnar.DeltaMerge`	`bound_matches`, `triple_matches_bound_acc`	yes
`SPARQL11.Algebra`	`lemma_mem_triple_matches_bound`	`RDF.Store.Columnar.DeltaMerge`	`bound_matches`, `triple_matches_bound`	yes
`SPARQL11.Algebra`	`lemma_merge_on_read_matches_apply_entries`	`RDF.Store.Columnar.DeltaMerge`	`apply_entries_ref`, `delta_resolved_empty`, `fold_entries_for_graph`, `merge_on_read`, `triple_matches_bound`	yes
`SPARQL11.Algebra`	`lemma_store_search_sound`	`SPARQL11.Algebra.BGPRefinement`	`graph_to_store`, `store_search`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_store_search_sound_for`	`SPARQL11.Algebra.BGPRefinement`	`graph_to_store_for`, `group_graph_pattern`, `store_search`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_bound_pred_from_obj`	`SPARQL11.Algebra.BGPRefinement`	`bound_object_of_pattern`, `bound_predicate_of_pattern`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_single_tp_store_default_eq`	`SPARQL11.Algebra.BGPRefinement`	`eval_single_tp_store`, `eval_single_tp_store_default`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_single_tp_sound`	`SPARQL11.Algebra.BGPRefinement`	`eval_single_tp_store_default`, `graph_to_store`, `tp_match`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_bgp_store_unfold`	`SPARQL11.Algebra.BGPRefinement`	`choose_best_tp`, `concatMap_tr`, `eval_bgp_store_from_mu_fuel`, `eval_single_tp_store`	yes
`SPARQL11.Algebra`	`lemma_eval_bgp_store_step`	`SPARQL11.Algebra.BGPRefinement`	`choose_best_tp`, `eval_bgp_store_from_mu_fuel`, `eval_single_tp_store`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_bound_obj_from_pred`	`SPARQL11.Algebra.BGPRefinement`	`bound_object_of_pattern`, `bound_predicate_of_pattern`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_bgp_store_step_intro`	`SPARQL11.Algebra.BGPRefinement`	`choose_best_tp`, `eval_bgp_store_from_mu_fuel`, `eval_single_tp_store`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_try_bind_subject_domain`	`SPARQL11.Algebra.BGPRefinement`	`pattern_subject_var`, `try_bind_subject`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_try_bind_term_domain`	`SPARQL11.Algebra.BGPRefinement`	`pattern_term_var`, `try_bind_term`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_tp_match_domain`	`SPARQL11.Algebra.BGPRefinement`	`tp_match`, `tp_vars`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_filter_sound`	`SPARQL11.Algebra.Refinement`	`eval_expr_ebv`, `filter_solutions`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_filter_complete`	`SPARQL11.Algebra.Refinement`	`eval_expr_ebv`, `filter_solutions`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_substitute_existentials_noop`	`SPARQL11.Algebra.Refinement`	`expr_has_existential`, `substitute_existentials`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_substitute_existentials_list_noop`	`SPARQL11.Algebra.Refinement`	`expr_list_has_existential`, `substitute_existentials_list`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_substitute_existentials_opt_noop`	`SPARQL11.Algebra.Refinement`	`expr_opt_has_existential`, `substitute_existentials_opt`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_filter_with_graph_is_filter_solutions`	`SPARQL11.Algebra.Refinement`	`expr_has_existential`, `filter_solutions`, `filter_solutions_with_graph`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_join_is_nested_loop_no_shared_vars`	`SPARQL11.Algebra.Refinement`	`join`, `join_nested_loop`, `sm_domain`, `vars_intersect`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_join_is_nested_loop_empty`	`SPARQL11.Algebra.Refinement`	`join`, `join_nested_loop`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_sr2_witness_keys_now_agree`	`SPARQL11.Algebra.Refinement`	`rdf_term_eq`, `sm_compatible`, `sm_join_key`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_join_key_no_finer_than_compatibility`	`SPARQL11.Algebra.Refinement`	`rdf_term_eq`, `sm_join_key`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_project_solutions_acc_memP`	`SPARQL11.Algebra.Refinement`	`project`, `project_solutions_acc`	yes
`SPARQL11.Algebra`	`theorem_project_solutions_spec`	`SPARQL11.Algebra.Refinement`	`project`, `project_solutions`	yes
`SPARQL11.Algebra`	`theorem_fx_bind_rows_rowwise`	`SPARQL11.Algebra.Refinement`	`er_to_term`, `eval_expr_fwd`, `fx_bind_rows`, `fx_ctx_put`, `sm_bind`	yes
`SPARQL11.Algebra`	`lemma_sort_solutions_permutation_pointwise`	`SPARQL11.Algebra.Refinement`	`order_condition`, `sort_solutions`	yes
`SPARQL11.Algebra`	`theorem_sort_solutions_permutation`	`SPARQL11.Algebra.Refinement`	`order_condition`, `sort_solutions`	yes
`SPARQL11.Algebra`	`lemma_sm_submap_extra_binding`	`SPARQL11.Algebra.Refinement`	`sm_domain`, `sm_submap`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_sm_submap_refl`	`SPARQL11.Algebra.Refinement`	`sm_domain`, `sm_submap`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_sm_equal_refl`	`SPARQL11.Algebra.Refinement`	`sm_domain`, `sm_equal`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_sm_submap_lookup`	`SPARQL11.Algebra.Refinement`	`rdf_term_eq`, `sm_lookup`, `sm_submap`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_sm_mem_witness`	`SPARQL11.Algebra.Refinement`	`sm_equal`, `sm_mem`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_dedup_core_complete`	`SPARQL11.Algebra.Refinement`	`list_deduplicate_sm_acc`, `sm_domain`, `sm_equal`	no (has `requires`)
`SPARQL11.Algebra`	`theorem_distinct_complete`	`SPARQL11.Algebra.Refinement`	`distinct_solutions`, `sm_domain`, `sm_equal`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_substitute_pattern_preserves_size`	`SPARQL11.Algebra`	`group_graph_pattern`, `pattern_size`, `substitute_pattern`	yes
`SPARQL11.Algebra`	`lemma_lateral_substitute_preserves_size`	`SPARQL11.Algebra`	`group_graph_pattern`, `lateral_substitute`, `pattern_size`	yes
`SPARQL11.Algebra`	`lemma_rewrite_query_bnodes_pattern_preserves_size`	`SPARQL11.Algebra`	`group_graph_pattern`, `pattern_size`, `rewrite_query_bnodes_pattern`	yes
`SPARQL11.Algebra`	`lemma_filter_union`	`SPARQL11.Algebra`	`filter_solutions`, `union`	yes
`SPARQL11.Algebra`	`lemma_sm_compatible_refl`	`SPARQL11.Algebra`	`sm_compatible`, `sm_domain`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_sm_merge_empty_l`	`SPARQL11.Algebra`	`sm_lookup`, `sm_merge`	yes
`SPARQL11.Algebra`	`lemma_store_search_empty`	`SPARQL11.Algebra`	`graph_to_store`, `store_search`	yes
`SPARQL11.Algebra`	`lemma_eval_single_tp_empty`	`SPARQL11.Algebra`	`eval_single_tp_store`, `graph_to_store`	yes
`SPARQL11.Algebra`	`lemma_eval_bgp_store_empty_fuel`	`SPARQL11.Algebra`	`eval_bgp_store_from_mu_fuel`, `graph_to_store`	yes
`SPARQL11.Algebra`	`lemma_eval_pattern_bgp_is_selective_store`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp_store`, `eval_pattern`, `graph_to_store_for`	yes
`SPARQL11.Algebra`	`lemma_ask_pattern_gives_solution`	`SPARQL11.EntailmentRegime.RDFS`	`eval_bgp_store`, `graph_to_store_for`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_eval_ask_query_bgp_shape`	`SPARQL11.EntailmentRegime.RDFS`	`eval_ask_query`, `query`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_ebv_langstring_agrees`	`SPARQL11.Expression.Refinement`	`ebv`, `ebv_checked`, `rdf_lang_string`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_parse_object_list_simple_1`	`SPARQL11.Parser.AskBgpRoundTrip`	`fulltext_query_pred`, `ggp_add_triple`, `group_graph_pattern`, `parse_object_list_simple`	no (has `requires`)
`SPARQL11.Algebra`	`lemma_parse_pred_obj_list_1`	`SPARQL11.Parser.AskBgpRoundTrip`	`fulltext_query_pred`, `ggp_add_triple`, `group_graph_pattern`, `parse_pred_obj_list`	no (has `requires`)
`SPARQL11.Algebra`	`parse_select_query_token_level_query`	`SPARQL11.Parser.AskBgpRoundTrip`	`default_modifier`, `parse_select_query`, `query`	no (has `requires`)
`SPARQL11.Parser`	`lemma_path_elt_iri`	`SPARQL11.Parser.AskBgpRoundTrip`	`parse_path_elt`, `parse_peek`	no (has `requires`)
`SPARQL11.Parser`	`lemma_path_elt_or_inverse_iri`	`SPARQL11.Parser.AskBgpRoundTrip`	`parse_path_elt_or_inverse`, `parse_peek`	no (has `requires`)
`SPARQL11.Parser`	`lemma_path_sequence_iri`	`SPARQL11.Parser.AskBgpRoundTrip`	`parse_path_sequence`, `parse_peek`	no (has `requires`)
`SPARQL11.Parser`	`lemma_path_alternative_iri`	`SPARQL11.Parser.AskBgpRoundTrip`	`parse_path_alternative`, `parse_peek`	no (has `requires`)
`SPARQL11.Parser`	`lemma_parse_verb_iri`	`SPARQL11.Parser.AskBgpRoundTrip`	`parse_peek`, `parse_verb`	no (has `requires`)
`SPARQL11.Parser`	`lemma_parse_verb_1`	`SPARQL11.Parser.AskBgpRoundTrip`	`parse_peek`, `parse_verb`	no (has `requires`)
`SPARQL11.Parser`	`lemma_parse_object_list_simple_1`	`SPARQL11.Parser.AskBgpRoundTrip`	`fulltext_query_pred`, `ggp_add_triple`, `group_graph_pattern`, `parse_object_list_simple`	no (has `requires`)
`SPARQL11.Parser`	`lemma_parse_pred_obj_list_1`	`SPARQL11.Parser.AskBgpRoundTrip`	`fulltext_query_pred`, `ggp_add_triple`, `group_graph_pattern`, `parse_pred_obj_list`	no (has `requires`)
`SPARQL11.Parser`	`lemma_triples_block_unfold_one_triple`	`SPARQL11.Parser.AskBgpRoundTrip`	`parse_peek`, `parse_triples_block`	no (has `requires`)
`SPARQL11.Parser`	`lemma_parse_ask_body_1`	`SPARQL11.Parser.AskBgpRoundTrip`	`default_modifier`, `parse_ask_body`	no (has `requires`)
`SPARQL11.Parser`	`lemma_parse_select_query_ask_bgp`	`SPARQL11.Parser.AskBgpRoundTrip`	`default_modifier`, `parse_select_query`, `resolve_relative_iri_tokens`	no (has `requires`)
`SPARQL11.Parser`	`parse_select_query_token_level`	`SPARQL11.Parser.AskBgpRoundTrip`	`default_modifier`, `parse_select_query`	no (has `requires`)
`SPARQL11.Parser`	`parse_select_query_token_level_query`	`SPARQL11.Parser.AskBgpRoundTrip`	`default_modifier`, `parse_select_query`, `query`	no (has `requires`)
`SPARQL11.Parser`	`peek_at_offset`	`SPARQL11.Parser.TokenRoundTrip`	`at_end`, `peek_char`	no (has `requires`)
`SPARQL11.Parser`	`peek_at_space`	`SPARQL11.Parser.TokenRoundTrip`	`at_end`, `peek_char`	no (has `requires`)
`SPARQL11.Parser`	`var_chars_end_stop`	`SPARQL11.Parser.TokenRoundTrip`	`at_end`, `peek_char`, `scan_var_chars_end`	no (has `requires`)
`SPARQL11.Parser`	`var_name_empty`	`SPARQL11.Parser.TokenRoundTrip`	`scan_var_chars_end`, `scan_var_name`	no (has `requires`)
`SPARQL11.Parser`	`next_token_skip_space`	`SPARQL11.Parser.TokenRoundTrip`	`at_end`, `char_code`, `is_ws`, `next_token`, `peek_char`	no (has `requires`)
`SPARQL11.Parser`	`next_token_at_end`	`SPARQL11.Parser.TokenRoundTrip`	`at_end`, `next_token`	no (has `requires`)
`SPARQL11.Parser`	`combine_step`	`SPARQL11.Parser.TokenRoundTrip`	`next_token`, `tokenize_loop`	no (has `requires`)
`SPARQL11.Parser`	`tokenize_loop_step_bridge`	`SPARQL11.Parser.TokenRoundTrip`	`next_token`, `tokenize_loop`	no (has `requires`)
`Tableau.CountingOracle`	`comb_len`	`Tableau.CountingOracle`	`all_len`, `comb_coeffs`	no (has `requires`)
`Tableau.CountingOracle`	`lin_dot_zeros`	`Tableau.CountingOracle`	`lin_dot`, `zeros`	yes
`Tableau.CountingOracle`	`lin_dot_vscale`	`Tableau.CountingOracle`	`lin_dot`, `vscale`	yes
`Tableau.CountingOracle`	`lin_dot_vadd`	`Tableau.CountingOracle`	`lin_dot`, `vadd`	no (has `requires`)
`Tableau.CountingOracle`	`comb_dot`	`Tableau.CountingOracle`	`all_len`, `comb_coeffs`, `lin_dot`, `weighted_lhs`	no (has `requires`)
`Tableau.CountingOracle`	`weighted_ge`	`Tableau.CountingOracle`	`lin_sat`, `valid_mults`, `weighted_lhs`, `weighted_rhs`	no (has `requires`)
`Tableau.CountingOracle`	`farkas_sound`	`Tableau.CountingOracle`	`farkas_check`, `lin_sat`	no (has `requires`)
`Tableau.CountingOracle`	`class_size_unsat_sound`	`Tableau.CountingOracle`	`build_lin_system`, `class_size_unsat`, `lin_sat`	no (has `requires`)

Full inventory (224 modules)

Module	Tier	Extraction	assume val	Local lemmas	Alg. corr.	Internal ref.	W3C ref.	Suites
`CSVW.Conversion`	merely Tot	extracted	0	0	0	0	0	csvw-nonnorm
`CSVW.Formats`	merely Tot	extracted	0	0	0	0	0	—
`CSVW.Json`	merely Tot	extracted	0	0	0	0	0	csvw-csv2json, csvw-nonnorm
`CSVW.Metadata`	merely Tot	extracted	0	0	0	0	0	—
`CSVW.URITemplate`	merely Tot	extracted	0	0	0	0	0	—
`CSVW.Validate`	merely Tot	extracted	0	0	0	0	0	csvw-validation
`DID.Key`	merely Tot	extracted	0	0	0	0	0	—
`Dep.Reachability`	algorithm-correctness theorem	extracted	0	2	1	0	0	—
`GRDDL.Discovery`	merely Tot	extracted	0	0	0	0	0	grddl
`HDT.Container`	algorithm-correctness theorem	extracted	0	0	2	0	0	—
`HDT.Dictionary`	merely Tot	extracted	0	0	0	0	0	—
`HDT.Triples`	merely Tot	extracted	0	0	0	0	0	—
`JSONLD.Compact`	merely Tot	extracted	0	0	0	0	0	jsonld-compact, jsonld-flatten, jsonld-frame
`JSONLD.Context`	merely Tot	extracted	0	0	0	0	0	jsonld-compact, jsonld-expand, jsonld-flatten
`JSONLD.Expand`	merely Tot	extracted	0	0	0	0	0	jsonld-compact, jsonld-expand, jsonld-flatten, jsonld-frame
`JSONLD.Flatten`	merely Tot	extracted	0	0	0	0	0	jsonld-flatten, jsonld-frame
`JSONLD.Frame`	merely Tot	extracted	0	0	0	0	0	jsonld-frame
`JSONLD.FromRdf`	merely Tot	extracted	0	0	0	0	0	—
`JSONLD.Loader`	merely Tot	extracted	1	0	0	0	0	—
`JSONSchema.Validate`	merely Tot	extracted	0	0	0	0	0	jsonschema
`LWS.Core.Spec`	unclassified (oracle unavailable)	not-in-build-list	0	28	0	0	0	—
`LWS.Solid.Registry`	unclassified (oracle unavailable)	not-in-build-list	0	0	0	0	0	—
`Math.Diff`	merely Tot	extracted	0	0	0	0	0	toan-matrix
`Math.Expr`	merely Tot	extracted	0	0	0	0	0	toan-matrix
`Math.Matrix`	local lemmas only	extracted	0	1	0	0	0	toan-matrix
`Math.Series`	merely Tot	extracted	0	0	0	0	0	toan-matrix
`Math.Sigmoid`	merely Tot	extracted	0	0	0	0	0	toan-matrix
`Math.Simplify`	merely Tot	extracted	0	0	0	0	0	toan-matrix
`Math.Subst`	merely Tot	extracted	0	0	0	0	0	toan-matrix
`MathML.Content`	merely Tot	extracted	0	0	0	0	0	toan-matrix
`MathML.Present`	merely Tot	extracted	0	0	0	0	0	toan-matrix
`OWL.Closure`	W3C-refinement theorem	extracted	0	0	13	11	108	local-negative-test-vacuity, owl-profile-el, owl-profile-ql, owl-semantics-direct, +4
`OWL.DirectMapping.Filter`	merely Tot	extracted	0	0	0	0	0	rif
`OWL.QueryEval`	merely Tot	extracted	0	0	0	0	0	rif, sparql11-entailment, sparql11-query
`OWL.QueryRewrite`	merely Tot	extracted	0	0	0	0	0	rif, sparql11-entailment, sparql11-query
`OWL.RL.Refinement`	specification / proof module	fully-erased	0	15	0	0	0	—
`OWL.RL.Spec`	specification / proof module	fully-erased	0	0	0	0	0	—
`OWL.Semantics`	specification / proof module	fully-erased	0	2	0	0	0	—
`OWL.Semantics.MemLemmas`	specification / proof module	fully-erased	0	11	0	0	0	—
`OWL.Semantics.Soundness`	specification / proof module	fully-erased	0	4	0	0	0	—
`OWL.Tests.Manifest`	merely Tot	extracted	0	0	0	0	0	—
`OWL.Vocabulary`	merely Tot	extracted	0	0	0	0	0	csvw-csv2json, csvw-nonnorm, csvw-validation, csvw, +77
`OWL2.SyntaxDL`	merely Tot	extracted	0	0	0	0	0	owl-syntax-dl
`Parquet.Footer`	algorithm-correctness theorem	extracted	3	0	2	0	0	local-cottas-corpus, local-cottas-row-order, local-parquet-footer-version-gate, local-parquet-footer
`Parser.BallyhooCOTTAS`	merely Tot	extracted	13	0	0	0	0	local-cottas-corpus, local-cottas-row-order
`Parser.BallyhooHDT`	merely Tot	extracted	0	0	0	0	0	—
`Parser.CSVResults`	local lemmas only	extracted	0	1	0	0	0	sparql11-federated-query, sparql11-query
`Parser.Combinators`	algorithm-correctness theorem	extracted	0	0	5	0	0	local-parser-unicode, local-sparql-parser, rdf-mt, rdf-n-quads, +6
`Parser.FastString`	internal-refinement theorem	extracted	0	0	78	31	0	csvw-csv2json, csvw-nonnorm, csvw-validation, csvw, +77
`Parser.FastString.Axioms`	unclassified (oracle unavailable)	not-in-build-list	0	12	0	0	0	—
`Parser.FastString.BaseCases`	unclassified (oracle unavailable)	not-in-build-list	0	31	0	0	0	—
`Parser.FastString.CharBoundary`	merely Tot	extracted	1	0	0	0	0	—
`Parser.FastString.ConcatSpec`	local lemmas only	extracted	0	6	0	0	0	—
`Parser.FastString.RoundTripLemmas`	unclassified (oracle unavailable)	not-in-build-list	0	20	0	0	0	—
`Parser.FastString.Spec`	algorithm-correctness theorem	extracted	0	15	37	0	0	—
`Parser.IRI`	merely Tot	extracted	0	0	0	0	0	csvw-csv2json, csvw-nonnorm, csvw-validation, csvw, +77
`Parser.JSON`	algorithm-correctness theorem	extracted	0	0	1	0	0	eecc-interop, jsonld-frame, jsonld-html, jsonld-tordf, +5
`Parser.JSONLD`	merely Tot	extracted	0	0	0	0	0	jsonld-compact, jsonld-expand, jsonld-flatten, jsonld-frame, +4
`Parser.JSONLD.Html`	merely Tot	extracted	0	0	0	0	0	jsonld-html
`Parser.JSONResults`	algorithm-correctness theorem	extracted	0	0	1	0	0	sparql11-federated-query, sparql11-query
`Parser.NQuads`	internal-refinement theorem	extracted	0	0	15	21	0	jsonld-html, jsonld-tordf, local-parser-unicode, rdf-n-quads, +3
`Parser.NTriples`	W3C-refinement theorem	extracted	0	0	56	2	1	local-parser-unicode, rdf-mt, rdf-n-quads, rdf-n-triples, +5
`Parser.NTriples.Locality`	unclassified (oracle unavailable)	not-in-build-list	0	4	0	0	0	—
`Parser.OWLFunctional`	merely Tot	extracted	0	0	0	0	0	owl-semantics-direct, owl-syntax-dl, owl-type-consistency, owl-type-inconsistency, +2
`Parser.RDFXML`	merely Tot	extracted	0	0	0	0	0	local-parser-unicode, owl-profile-el, owl-profile-ql, owl-profile-rl, +7
`Parser.RIFXML`	algorithm-correctness theorem	extracted	0	0	1	0	0	rif, sparql11-entailment
`Parser.SRX`	merely Tot	extracted	0	0	0	0	0	sparql11-federated-query, sparql11-query
`Parser.ShExC`	merely Tot	extracted	0	0	0	0	0	shex-negative-syntax
`Parser.TriG`	merely Tot	extracted	0	0	0	0	0	local-parser-unicode, rdf-trig, sparql11-query, sparql11-update
`Parser.Turtle`	merely Tot	extracted	0	0	0	0	0	local-parser-unicode, local-turtle-pretty, rdf-mt, rdf-trig, +10
`Parser.TurtleScanner`	merely Tot	extracted	0	0	0	0	0	local-parser-unicode, local-turtle-pretty, rdf-mt, rdf-trig, +6
`Parser.WKT`	merely Tot	extracted	0	0	0	0	0	geosparql
`Parser.XML`	merely Tot	extracted	0	0	0	0	0	local-parser-unicode, owl-profile-el, owl-profile-ql, owl-profile-rl, +7
`Parser.XPath`	merely Tot	extracted	0	0	0	0	0	xpath-unit
`RDF.Bytes`	algorithm-correctness theorem	extracted	0	8	20	0	0	local-parquet-footer-version-gate
`RDF.Canonical`	internal-refinement theorem	extracted	2	4	0	2	0	jsonld-html, jsonld-tordf, local-graphs-api, local-jsonld-regressions, +4
`RDF.Canonical.Manifest`	merely Tot	extracted	0	0	0	0	0	rdfc10
`RDF.CottasStore`	internal-refinement theorem	extracted	3	1	0	3	0	local-cottas-corpus, local-cottas-row-order, local-parquet-footer-version-gate
`RDF.CottasStore.BaseWriter`	algorithm-correctness theorem	extracted	0	6	3	0	0	local-parquet-footer-version-gate
`RDF.CottasStore.ColumnSeq`	algorithm-correctness theorem	extracted	4	0	1	0	0	local-cottas-ask-decode-failure
`RDF.CottasStore.CompoundPresenceBitmap`	internal-refinement theorem	extracted	0	0	0	1	0	—
`RDF.CottasStore.CompoundPresenceWriter`	algorithm-correctness theorem	extracted	0	2	5	0	0	—
`RDF.CottasStore.DictWriter`	algorithm-correctness theorem	extracted	0	6	11	0	0	—
`RDF.CottasStore.LazyDict`	merely Tot	extracted	9	0	0	0	0	local-cottas-ask-decode-failure
`RDF.CottasStore.LazyDictRegistry`	merely Tot	extracted	5	0	0	0	0	—
`RDF.CottasStore.OffsetsWriter`	algorithm-correctness theorem	extracted	0	2	7	0	0	—
`RDF.CottasStore.OnDiskIndex`	local lemmas only	extracted	7	1	0	0	0	local-cottas-row-order
`RDF.CottasStore.PageCache`	algorithm-correctness theorem	extracted	4	0	3	0	0	local-cottas-ask-decode-failure, local-cottas-groupby-counts
`RDF.CottasStore.PageCache.Bounds`	local lemmas only	fully-erased	0	12	0	0	0	—
`RDF.CottasStore.PresenceBitmap`	internal-refinement theorem	extracted	0	0	0	1	0	—
`RDF.CottasStore.PresenceWriter`	algorithm-correctness theorem	extracted	0	0	2	0	0	—
`RDF.CottasStore.SubjectOffsetsWriter`	algorithm-correctness theorem	extracted	0	1	3	0	0	—
`RDF.Dataset.Graphs`	merely Tot	extracted	0	0	0	0	0	local-graphs-api
`RDF.Dataset.Merge`	merely Tot	extracted	0	0	0	0	0	local-graph-default-semantics
`RDF.Entailment.RDF.Spec`	specification / proof module	fully-erased	0	0	0	0	0	—
`RDF.Entailment.RDFS.ChainWf`	local lemmas only	fully-erased	0	9	0	0	0	—
`RDF.Entailment.RDFS.Completeness`	unclassified (oracle unavailable)	not-in-build-list	0	25	0	0	0	—
`RDF.Entailment.RDFS.DatatypeClash`	merely Tot	extracted	0	0	0	0	0	—
`RDF.Entailment.RDFS.FixedPoint`	unclassified (oracle unavailable)	not-in-build-list	0	31	0	0	0	—
`RDF.Entailment.RDFS.ModelTheory`	specification / proof module	fully-erased	0	22	0	0	0	—
`RDF.Entailment.RDFS.Refinement`	specification / proof module	fully-erased	0	21	0	0	0	—
`RDF.Entailment.RDFS.RhoDFClosure`	W3C-refinement theorem	extracted	0	9	8	25	20	—
`RDF.Entailment.RDFS.SepFree`	specification / proof module	fully-erased	0	38	0	0	0	—
`RDF.Entailment.RDFS.Spec`	specification / proof module	fully-erased	0	0	0	0	0	—
`RDF.Entailment.RDFSPlus`	merely Tot	extracted	0	0	0	0	0	—
`RDF.Entailment.Regime`	merely Tot	extracted	0	0	0	0	0	local-negative-test-vacuity
`RDF.Entailment.RegimeDispatch`	merely Tot	extracted	0	0	0	0	0	—
`RDF.Entailment.Simple`	W3C-refinement theorem	extracted	0	0	1	3	21	—
`RDF.Entailment.Simple.Boundary`	local lemmas only	fully-erased	0	13	0	0	0	—
`RDF.Entailment.Simple.ModelTheory`	specification / proof module	fully-erased	0	30	0	0	0	—
`RDF.Entailment.Simple.Refinement`	specification / proof module	fully-erased	0	14	0	0	0	—
`RDF.Entailment.Simple.Spec`	specification / proof module	fully-erased	0	0	0	0	0	—
`RDF.Format`	merely Tot	extracted	0	0	0	0	0	csvw-csv2json, csvw-nonnorm, csvw-validation, csvw, +77
`RDF.Geo.BBox`	merely Tot	extracted	0	0	0	0	0	geosparql
`RDF.Geo.Functions`	merely Tot	extracted	0	0	0	0	0	geosparql
`RDF.Geo.Topology`	merely Tot	extracted	0	0	0	0	0	geosparql
`RDF.Geo.Types`	merely Tot	extracted	0	0	0	0	0	geosparql
`RDF.Graph`	W3C-refinement theorem	extracted	0	0	11	12	18	—
`RDF.Graph.Executable`	internal-refinement theorem	extracted	0	3	1	2	0	csvw-csv2json, csvw-nonnorm, csvw-validation, csvw, +77
`RDF.GraphIsomorphism`	merely Tot	extracted	0	0	0	0	0	—
`RDF.IRI`	merely Tot	extracted	0	0	0	0	0	—
`RDF.Indexed`	W3C-refinement theorem	extracted	0	0	28	11	72	—
`RDF.Indexed.Completeness`	unclassified (oracle unavailable)	not-in-build-list	0	18	0	0	0	—
`RDF.Indexed.KeyInjectivity`	specification / proof module	fully-erased	0	10	0	0	0	—
`RDF.Indexed.StringOrder`	unclassified (oracle unavailable)	not-in-build-list	0	3	0	0	0	—
`RDF.List.Helpers`	W3C-refinement theorem	extracted	0	6	1	0	1	sparql11-query
`RDF.NQuads.Serialize`	algorithm-correctness theorem	extracted	0	0	7	0	0	local-serializer-unicode, rdf-n-quads, rdfc10
`RDF.NQuads.Streaming`	unclassified (oracle unavailable)	not-in-build-list	0	34	0	0	0	—
`RDF.NTriples.RoundTrip`	unclassified (oracle unavailable)	not-in-build-list	0	12	0	0	0	—
`RDF.Pretty`	merely Tot	extracted	0	0	0	0	0	—
`RDF.Semantics.HypothesisWitness`	specification / proof module	fully-erased	0	32	0	0	0	—
`RDF.Store.Capabilities`	merely Tot	extracted	0	0	0	0	0	—
`RDF.Store.Capabilities.Cottas`	merely Tot	extracted	0	0	0	0	0	—
`RDF.Store.Capabilities.Delta`	merely Tot	extracted	0	0	0	0	0	—
`RDF.Store.Columnar.DeltaLog`	algorithm-correctness theorem	extracted	5	5	24	0	0	—
`RDF.Store.Columnar.DeltaMerge`	internal-refinement theorem	extracted	0	24	3	3	0	—
`RDF.Store.Columnar.OffsetIndex`	internal-refinement theorem	extracted	0	2	0	1	0	—
`RDF.Store.Columnar.SubjectOffsetIndex`	internal-refinement theorem	extracted	0	2	0	1	0	—
`RDF.Store.Combine`	merely Tot	extracted	0	0	0	0	0	—
`RDF.Store.LazyTermCache`	merely Tot	extracted	6	0	0	0	0	—
`RDF.Store.Loader`	merely Tot	extracted	0	0	0	0	0	—
`RDF.Term`	W3C-refinement theorem	extracted	0	5	14	2	3	—
`RDF.Triple`	local lemmas only	extracted	0	1	0	0	0	—
`RDF.Turtle.Serialize`	internal-refinement theorem	extracted	0	0	0	1	0	local-turtle-pretty
`RDF.Vocabulary`	merely Tot	extracted	0	0	0	0	0	—
`RDF.Vocabulary.Axioms`	W3C-refinement theorem	extracted	0	0	3	2	8	—
`RDFS.Closure`	W3C-refinement theorem	extracted	0	0	24	8	113	local-negative-test-vacuity
`RDFS.Closure.SemiNaive`	merely Tot	extracted	0	0	0	0	0	—
`RDFS.SchemaSplit`	algorithm-correctness theorem	extracted	0	5	2	0	0	—
`RIF.Core.Builtins`	merely Tot	extracted	0	0	0	0	0	rif
`RIF.Core.Conformance`	merely Tot	extracted	0	0	0	0	0	rif
`RIF.Core.Eval`	internal-refinement theorem	extracted	0	8	0	9	0	rif, sparql11-entailment
`RIF.Core.Refinement`	unclassified (oracle unavailable)	not-in-build-list	0	4	0	0	0	—
`RIF.Core.Syntax`	local lemmas only	extracted	0	2	0	0	0	rif, sparql11-entailment
`RIF.Core.Tests`	internal-refinement theorem	extracted	0	0	1	1	0	sparql11-entailment
`RIF.Core.Translation`	merely Tot	extracted	0	0	0	0	0	rif, sparql11-entailment
`RML.Eval`	merely Tot	extracted	0	0	0	0	0	rml
`RML.Mapping`	merely Tot	extracted	0	0	0	0	0	rml
`RML.Sources`	merely Tot	extracted	0	0	0	0	0	csvw-nonnorm, rml
`RML.VirtualSource`	merely Tot	extracted	0	0	0	0	0	—
`Regex.Derivative`	algorithm-correctness theorem	extracted	0	4	8	0	0	—
`Regex.Exec`	algorithm-correctness theorem	extracted	0	0	16	0	0	jsonschema
`Regex.Syntax`	algorithm-correctness theorem	extracted	0	12	30	0	0	—
`Regex.XSDPattern`	merely Tot	extracted	0	0	0	0	0	jsonschema
`SHACL.NodeExpr`	merely Tot	extracted	0	0	0	0	0	—
`SHACL.Rules`	merely Tot	extracted	0	0	0	0	0	—
`SHACL.Validation`	merely Tot	extracted	1	0	0	0	0	qudt, shacl-core, shacl-sparql
`SPARQL.Diagnostics`	merely Tot	extracted	0	0	0	0	0	sparql11-query
`SPARQL.Eval.Limits`	algorithm-correctness theorem	extracted	0	0	5	0	0	sparql11-entailment, sparql11-query, sparql11-update
`SPARQL.Eval.TimeBudget`	algorithm-correctness theorem	extracted	1	0	2	0	0	sparql11-entailment, sparql11-query, sparql11-update
`SPARQL.Explain`	merely Tot	extracted	0	0	0	0	0	—
`SPARQL.FullText`	algorithm-correctness theorem	extracted	0	0	2	0	0	—
`SPARQL.GraphStore`	merely Tot	extracted	0	0	0	0	0	sparql11-protocol
`SPARQL.HTTP`	merely Tot	extracted	0	0	0	0	0	sparql11-protocol, sparql11-service-description
`SPARQL.HTTP.Admin`	merely Tot	extracted	0	0	0	0	0	sparql11-protocol
`SPARQL.HTTP.BackendInfo`	merely Tot	extracted	0	0	0	0	0	sparql11-protocol, sparql11-service-description
`SPARQL.HTTP.Client`	merely Tot	extracted	0	0	0	0	0	sparql11-federated-query
`SPARQL.HTTP.QueriesIndex`	merely Tot	extracted	0	0	0	0	0	sparql11-protocol, sparql11-service-description
`SPARQL.HTTP.Response`	merely Tot	extracted	0	0	0	0	0	sparql11-protocol
`SPARQL.HTTP.Routes`	merely Tot	extracted	0	0	0	0	0	—
`SPARQL.HTTP.RunQuery`	merely Tot	extracted	0	0	0	0	0	—
`SPARQL.HTTP.StaticFiles`	merely Tot	extracted	0	0	0	0	0	sparql11-protocol
`SPARQL.JSON.Escape`	merely Tot	extracted	0	0	0	0	0	sparql11-protocol, sparql11-query, sparql11-update
`SPARQL.Plan.AccessPath`	local lemmas only	extracted	0	4	0	0	0	local-cottas-groupby-counts, sparql11-query
`SPARQL.Plan.Pruning`	local lemmas only	extracted	0	1	0	0	0	local-cottas-groupby-counts, sparql11-query
`SPARQL.Plan.Streamable`	merely Tot	extracted	0	0	0	0	0	—
`SPARQL.Protocol`	algorithm-correctness theorem	extracted	0	0	2	0	0	sparql11-protocol, sparql11-service-description
`SPARQL.Protocol.Client`	merely Tot	extracted	0	0	0	0	0	—
`SPARQL.Protocol.RoundTrip`	local lemmas only	fully-erased	0	11	0	0	0	—
`SPARQL.Query.Analysis`	merely Tot	extracted	0	0	0	0	0	sparql11-query
`SPARQL.ServiceDescription`	merely Tot	extracted	0	0	0	0	0	—
`SPARQL.Update.Analysis`	merely Tot	extracted	0	0	0	0	0	sparql11-update
`SPARQL.Update.Sandbox`	merely Tot	extracted	0	0	0	0	0	sparql11-update
`SPARQL11.Algebra`	W3C-refinement theorem	extracted	11	24	53	54	49	local-backend-parity-full, local-graph-default-semantics, local-sparql-negative, local-sparql-parser, +11
`SPARQL11.Algebra.BGPRefinement`	unclassified (oracle unavailable)	not-in-build-list	0	29	0	0	0	—
`SPARQL11.Algebra.Refinement`	specification / proof module	fully-erased	0	74	0	0	0	—
`SPARQL11.Algebra.Spec`	specification / proof module	fully-erased	0	36	0	0	0	—
`SPARQL11.EntailmentRegime.RDFS`	unclassified (oracle unavailable)	not-in-build-list	0	12	0	0	0	—
`SPARQL11.Expression.Refinement`	unclassified (oracle unavailable)	not-in-build-list	0	19	0	0	0	—
`SPARQL11.IRI.Resolve`	merely Tot	extracted	0	0	0	0	0	—
`SPARQL11.Parser`	algorithm-correctness theorem	extracted	0	0	21	0	0	local-sparql-negative, local-sparql-parser, rif, shacl-sparql, +6
`SPARQL11.Parser.AskBgpRoundTrip`	unclassified (oracle unavailable)	not-in-build-list	0	15	0	0	0	—
`SPARQL11.Parser.TokenRoundTrip`	unclassified (oracle unavailable)	not-in-build-list	0	45	0	0	0	—
`SPARQL11.Store`	merely Tot	extracted	0	0	0	0	0	local-backend-parity-full, local-backend-parity, local-graph-default-semantics, sparql11-entailment, +3
`Schematron.Validate`	merely Tot	extracted	0	0	0	0	0	—
`ShEx.Schema`	merely Tot	extracted	0	0	0	0	0	shex-negative-syntax, shex
`ShEx.SchemaEq`	merely Tot	extracted	0	0	0	0	0	—
`ShEx.Validation`	merely Tot	extracted	0	0	0	0	0	shex
`Solid.Protocol.Spec`	unclassified (oracle unavailable)	not-in-build-list	0	43	0	0	0	—
`Tableau`	merely Tot	extracted	0	0	0	0	0	owl-semantics-direct, owl-type-consistency, owl-type-inconsistency, owl-type-negative-entailment, +3
`Tableau.CountingOracle`	algorithm-correctness theorem	extracted	1	5	8	0	0	owl-semantics-direct, owl-type-consistency, owl-type-inconsistency, owl-type-negative-entailment, +1
`Tableau.Refute`	merely Tot	extracted	0	0	0	0	0	owl-semantics-direct, owl-type-consistency, owl-type-inconsistency, owl-type-negative-entailment, +1
`VC.Context`	merely Tot	extracted	0	0	0	0	0	eecc-interop
`VC.Credential`	merely Tot	extracted	0	0	0	0	0	eecc-interop, vc, vc20-api
`VC.DataIntegrity`	merely Tot	extracted	4	0	0	0	0	eecc-interop, vc-di-eddsa, vc20-api
`VC.Multibase`	merely Tot	extracted	0	0	0	0	0	vc-di-eddsa
`XForms.Bind`	local lemmas only	extracted	0	1	0	0	0	xforms
`XML.Namespaces`	merely Tot	extracted	0	0	0	0	0	—
`XML.Wellformedness`	merely Tot	extracted	0	0	0	0	0	—
`XPath.Eval`	merely Tot	extracted	0	0	0	0	0	grddl, xpath-unit
`XSD.Datatypes`	merely Tot	extracted	0	0	0	0	0	rif, shex
`XSD.Facets`	merely Tot	extracted	0	0	0	0	0	—
`XSD.IEEE754`	merely Tot	extracted	0	0	0	0	0	—
`XSLT.Transform`	merely Tot	extracted	0	0	0	0	0	grddl

Official suites and their exact coverage

Scores are read back from the committed runner logs, or from docs/test-results/latest.json when a log carries no matchable score line. Source records where each number came from. A suite with no numbers has a gap in its measurement chain, reported rather than filled in.

Suite	Pass	Fail	Skip	Total	Source
`csvw`	—	—	—	—	unresolved — no score line matched in formal/fstar/ocaml-output/csvw_results.log
`csvw-csv2json`	270	0	0	270	docs/test-results/latest.json:csvw_csv2json
`csvw-nonnorm`	—	—	—	—	unresolved — declared log_path missing: None
`csvw-validation`	281	1	0	282	docs/test-results/latest.json:csvw_validation
`did`	—	—	—	—	unresolved — no score line matched in formal/fstar/ocaml-output/did_results.log
`eecc-interop`	4	0	51	55	docs/test-results/latest.json:eecc_interop
`geosparql`	—	—	—	—	unresolved — no committed log carries score lines for geosparql_v0_unit
`grddl`	18	50	0	68	suite-log:named-line:formal/fstar/ocaml-output/grddl_results.log
`jsonld-compact`	245	0	0	245	suite-log:named-line:formal/fstar/ocaml-output/jsonld_compact_results.log
`jsonld-expand`	385	0	0	385	suite-log:named-line:formal/fstar/ocaml-output/jsonld_expand_results.log
`jsonld-flatten`	58	0	0	58	suite-log:named-line:formal/fstar/ocaml-output/jsonld_flatten_results.log
`jsonld-frame`	28	64	0	92	suite-log:named-line:formal/fstar/ocaml-output/jsonld_frame_results.log
`jsonld-fromrdf`	53	0	1	54	docs/test-results/latest.json:jsonld_fromrdf
`jsonld-html`	50	0	0	50	suite-log:named-line:formal/fstar/ocaml-output/jsonld_html_results.log
`jsonld-tordf`	467	0	0	467	suite-log:named-line:formal/fstar/ocaml-output/jsonld_results.log
`jsonschema`	770	0	0	770	docs/test-results/latest.json:jsonschema
`local-backend-parity`	—	—	—	—	unresolved — declared log_path missing: None
`local-backend-parity-full`	—	—	—	—	unresolved — declared log_path missing: None
`local-check-pages-links`	—	—	—	—	unresolved — declared log_path missing: None
`local-cottas-ask-decode-failure`	—	—	—	—	unresolved — declared log_path missing: None
`local-cottas-corpus`	—	—	—	—	unresolved — declared log_path missing: None
`local-cottas-groupby-counts`	—	—	—	—	unresolved — declared log_path missing: None
`local-cottas-row-order`	—	—	—	—	unresolved — declared log_path missing: None
`local-graph-default-semantics`	—	—	—	—	unresolved — declared log_path missing: None
`local-graphs-api`	—	—	—	—	unresolved — declared log_path missing: None
`local-jsonld-regressions`	—	—	—	—	unresolved — declared log_path missing: None
`local-negative-test-vacuity`	—	—	—	—	unresolved — declared log_path missing: None
`local-parquet-footer`	—	—	—	—	unresolved — declared log_path missing: None
`local-parquet-footer-version-gate`	—	—	—	—	unresolved — declared log_path missing: None
`local-parser-unicode`	—	—	—	—	unresolved — declared log_path missing: None
`local-serializer-unicode`	—	—	—	—	unresolved — declared log_path missing: None
`local-sparql-negative`	—	—	—	—	unresolved — declared log_path missing: None
`local-sparql-parser`	—	—	—	—	unresolved — declared log_path missing: None
`local-turtle-pretty`	—	—	—	—	unresolved — declared log_path missing: None
`mathml`	81	0	0	81	docs/test-results/latest.json:mathml
`owl-profile-el`	—	—	—	—	unresolved — no committed log carries score lines for rl
`owl-profile-ql`	—	—	—	—	unresolved — no committed log carries score lines for rl
`owl-profile-rl`	—	—	—	—	unresolved — declared log_path missing: formal/fstar/ocaml-output/owl_results.log
`owl-semantics-direct`	—	—	—	—	unresolved — no committed log carries score lines for dl
`owl-syntax-dl`	—	—	—	—	unresolved — no score line matched in formal/fstar/ocaml-output/owl_syntax_dl_results.log
`owl-type-consistency`	—	—	—	—	unresolved — no committed log carries score lines for dl
`owl-type-inconsistency`	—	—	—	—	unresolved — no committed log carries score lines for dl
`owl-type-negative-entailment`	—	—	—	—	unresolved — no committed log carries score lines for dl
`owl-type-positive-entailment`	—	—	—	—	unresolved — no committed log carries score lines for dl
`qudt`	—	—	—	—	unresolved — no score line matched in formal/fstar/ocaml-output/qudt_results.log
`rdf-mt`	38	0	0	38	suite-log:per-runner-arg:formal/fstar/ocaml-output/rdf_results.log (manifest log_path points at formal/fstar/ocaml-output/sparql_results.log, which does not carry this suite's score lines)
`rdf-n-quads`	87	0	0	87	suite-log:per-runner-arg:formal/fstar/ocaml-output/rdf_results.log (manifest log_path points at formal/fstar/ocaml-output/sparql_results.log, which does not carry this suite's score lines)
`rdf-n-triples`	70	0	0	70	suite-log:per-runner-arg:formal/fstar/ocaml-output/rdf_results.log (manifest log_path points at formal/fstar/ocaml-output/sparql_results.log, which does not carry this suite's score lines)
`rdf-trig`	356	0	0	356	suite-log:per-runner-arg:formal/fstar/ocaml-output/rdf_results.log (manifest log_path points at formal/fstar/ocaml-output/sparql_results.log, which does not carry this suite's score lines)
`rdf-turtle`	313	0	0	313	suite-log:per-runner-arg:formal/fstar/ocaml-output/rdf_results.log (manifest log_path points at formal/fstar/ocaml-output/sparql_results.log, which does not carry this suite's score lines)
`rdf-xml`	166	0	0	166	suite-log:per-runner-arg:formal/fstar/ocaml-output/rdf_results.log (manifest log_path points at formal/fstar/ocaml-output/sparql_results.log, which does not carry this suite's score lines)
`rdfc10`	86	0	0	86	docs/test-results/latest.json:rdfc10
`rif`	—	—	—	—	unresolved — no score line matched in formal/fstar/ocaml-output/rif_results.log
`rml`	—	—	—	—	unresolved — no score line matched in formal/fstar/ocaml-output/rml_results.log
`rml-io`	17	1	55	73	suite-log:named-line:formal/fstar/ocaml-output/rml_io_results.log
`schematron`	8	0	0	8	suite-log:named-line:formal/fstar/ocaml-output/schematron_results.log
`shacl-core`	98	0	0	98	suite-log:named-line:formal/fstar/ocaml-output/shacl_results.log
`shacl-sparql`	22	0	0	22	suite-log:named-line:formal/fstar/ocaml-output/shacl_sparql_results.log
`shacl12-core`	138	0	0	138	suite-log:TOTAL-line:formal/fstar/ocaml-output/shacl12_core_results.log
`shacl12-node-expr`	142	0	0	142	suite-log:TOTAL-line:formal/fstar/ocaml-output/shacl12_node_expr_results.log
`shacl12-rules`	11	0	0	11	suite-log:TOTAL-line:formal/fstar/ocaml-output/shacl12_rules_results.log
`shacl12-rules-syntax`	62	0	0	62	suite-log:TOTAL-line:formal/fstar/ocaml-output/shacl12_rules_syntax_results.log
`shacl12-sparql`	25	0	0	25	suite-log:TOTAL-line:formal/fstar/ocaml-output/shacl12_sparql_results.log
`shex`	1182	0	0	1182	docs/test-results/latest.json:shex
`shex-negative-syntax`	0	0	0	0	docs/test-results/latest.json:shex_negative_syntax
`sparql11-entailment`	70	0	0	70	suite-log:per-runner-arg:formal/fstar/ocaml-output/sparql_results.log
`sparql11-federated-query`	10	0	0	10	suite-log:per-runner-arg:formal/fstar/ocaml-output/sparql_results.log
`sparql11-protocol`	53	0	0	53	suite-log:per-runner-arg:formal/fstar/ocaml-output/sparql_results.log
`sparql11-query`	338	0	0	338	suite-log:per-runner-arg:formal/fstar/ocaml-output/sparql_results.log
`sparql11-service-description`	3	0	0	3	suite-log:per-runner-arg:formal/fstar/ocaml-output/sparql_results.log
`sparql11-update`	157	0	0	157	suite-log:per-runner-arg:formal/fstar/ocaml-output/sparql_results.log
`tests-unit`	19	28	0	47	docs/test-results/latest.json:tests_unit
`toan-matrix`	11	0	0	11	docs/test-results/latest.json:toan_matrix
`vc`	117	0	0	117	suite-log:TOTAL-line:formal/fstar/ocaml-output/vc_results.log
`vc-di-eddsa`	31	0	0	31	docs/test-results/latest.json:vc_di_eddsa
`vc20-api`	59	0	0	59	docs/test-results/latest.json:vc20_api
`xforms`	2	0	0	2	docs/test-results/latest.json:xforms
`xml-conformance`	1447	0	1138	2585	suite-log:named-line:formal/fstar/ocaml-output/xml_conformance_results.log
`xpath-unit`	—	—	—	—	unresolved — no committed log carries score lines for xpath_tests
`xslt`	87	0	1	88	docs/test-results/latest.json:xslt
`xslt1-xalan`	—	—	—	—	unresolved — declared log_path missing: formal/fstar/ocaml-output/xslt1_xalan_results.log

Regenerate with tools/assurance-inventory.sh. Machine-readable form: assurance-inventory.json. Filed as issue #315, sub-issue of the claim-discipline epic #313.