Index

CoMuAmadioCardelli No external references.

JCoMuAmadioCardelli No references.

anti_frame_disabled Progress. Subtyping. Typing.

anti_frame_enabled Typing. WeakRefWithAffineContent.

anti_frame_switch No external references.

anti_frame_switch_contradiction Progress.

gt_succ No external references.

le_succ No external references.

lt_a_fortiori RawSemantics.

CanonicalVAbs No references.

CanonicalVBang No references.

CanonicalVInhabitant No references.

CanonicalVLoc No references.

CanonicalVPack No references.

CanonicalVPair No references.

CanonicalVRegionCap No references.

CanonicalVRegionCapPunched No references.

CanonicalVTyAbs No references.

CanonicalVUnit No references.

CanonicalVVar No references.

EachCons No references.

EachNil No references.

canonical CanonicalValuesDoNotReduce. Focus. InversionClassification. Progress. ProgressValues. ValueReductionTerminates.

canonical_induction CanonicalValuesDoNotReduce. ValueReductionTerminates.

canonical_lift No references.

each_canonical CanonicalValuesDoNotReduce. InversionClassification. ProgressValues. ValueReductionTerminates.

each_canonical_member Progress. ValueReductionTerminates.

each_canonical_singleton_inversion No external references.

canonical_values_do_not_reduce No references.

canonical_values_do_not_reduce_preliminary No external references.

subst_term_overshoot TermSubstitution.

well_typed_closed_value RegionAllocation. SubjectReduction.

well_typed_well_scoped No external references.

measure_coercion ValueReductionTerminates.

measure_cunfold ValueReductionTerminates.

measure_subst_co No external references.

jco_substitution No external references.

jco_substitution_0 SubjectReductionValues.

CoArrow CoercionMeasure. DerivedSubtyping. Intuitionistic. SemanticsValues. Subtyping.

CoAtBang CoercionMeasure. SemanticsValues. Subtyping. WeakRefWithAffineContent.

CoBang CoercionMeasure. DerivedSubtyping. Intuitionistic. SemanticsValues. Subtyping. ValueReductionTerminates.

CoBangExists CoercionMeasure. SemanticsValues. Subtyping.

CoBangIdempotent CoercionMeasure. SemanticsValues. Subtyping.

CoBangPair CoercionMeasure. SemanticsValues. Subtyping.

CoBangPairReversed DerivedSubtyping.

CoBangRef CoercionMeasure. Subtyping.

CoBangRegionCap CoercionMeasure. Subtyping.

CoBangRegionCapPunched CoercionMeasure. Subtyping.

CoComposExchange DerivedSubtyping. RevelationDefinition.

CoComposExchangeUnder Revelation. SemanticsValues.

CoDefocus CoercionMeasure. DerivedTyping. SemanticsValues. Subtyping. ValueReductionTerminates. WeakRefWithAffineContent.

CoDefocusGroup CoercionMeasure. SemanticsValues. Subtyping.

CoDereliction CoercionMeasure. SemanticsValues. Subtyping. WeakRefWithAffineContent.

CoDistrib CoercionMeasure. SemanticsValues. Subtyping.

CoExists CoercionMeasure. DerivedSubtyping. SemanticsValues. Subtyping. ValueReductionTerminates.

CoExistsCap DerivedSubtyping.

CoExistsElim CoercionMeasure. SemanticsValues. Subtyping.

CoExistsIntro CoercionMeasure. DerivedSubtyping. SemanticsValues. Subtyping.

CoExistsIntrusion DerivedSubtyping.

CoExistsLeftIntro CoercionMeasure. DerivedSubtyping. SemanticsValues. Subtyping.

CoExistsLeftIntroReversed DerivedSubtyping.

CoExistsPairDistrib DerivedSubtyping.

CoExistsPairIntrusion DerivedSubtyping.

CoExistsScopeRestrictionLeft DerivedSubtyping.

CoExistsScopeRestrictionRight DerivedSubtyping.

CoForall CoercionMeasure. DerivedSubtyping. SemanticsValues. Subtyping. ValueReductionTerminates.

CoForallBang CoercionMeasure. SemanticsValues. Subtyping.

CoForallElim CoercionMeasure. DerivedSubtyping. SemanticsValues. Subtyping.

CoForallExtrusion DerivedSubtyping.

CoForallIntro CoercionMeasure. SemanticsValues. Subtyping.

CoForallPair CoercionMeasure. SemanticsValues. Subtyping.

CoForallPairExtrusion DerivedSubtyping.

CoForallPairExtrusionLeft DerivedSubtyping.

CoForallPairLeft DerivedSubtyping. RevelationDefinition.

CoForallRef CoercionMeasure. SemanticsValues. Subtyping.

CoForallRegionCap CoercionMeasure. SemanticsValues. Subtyping. ValueReductionTerminates.

CoForallRegionCapPunched CoercionMeasure. SemanticsValues. Subtyping. ValueReductionTerminates.

CoId CoercionMeasure. DerivedSubtyping. RevelationDefinition. SemanticsValues. Subtyping.

CoMixPair RevelationDefinition.

CoMixPairComposExchange DerivedSubtyping. RevelationDefinition.

CoMixPairExchange DerivedSubtyping. RevelationDefinition.

CoMu AdmissibleSubtyping. CoercionMeasure. SemanticsValues. Subtyping. ValueReductionTerminates.

CoPair CoercionMeasure. DerivedSubtyping. SemanticsValues. Subtyping. ValueReductionTerminates.

CoPairBang CoercionMeasure. DerivedSubtyping. SemanticsValues. Subtyping.

CoPairBangReversed DerivedSubtyping.

CoPairExistsLeft CoercionMeasure. SemanticsValues. Subtyping.

CoPairExistsRight CoercionMeasure. SemanticsValues. Subtyping.

CoRef CoercionMeasure. DerivedSubtyping. SemanticsValues. Subtyping. ValueReductionTerminates. WeakRefWithAffineContent.

CoRefExists CoercionMeasure. SemanticsValues. Subtyping.

CoRefStar CoercionMeasure. SemanticsValues. Subtyping.

CoRegionCap CoercionMeasure. DerivedSubtyping. SemanticsValues. Subtyping. ValueReductionTerminates. WeakRefWithAffineContent.

CoRegionCapPunched CoercionMeasure. DerivedSubtyping. SemanticsValues. Subtyping. ValueReductionTerminates.

CoSeq CoercionMeasure. SemanticsValues. Subtyping. ValueReductionTerminates.

CoSingletonRegionCapExists CoercionMeasure. DerivedSubtyping. SemanticsValues. Subtyping.

CoSingletonStar CoercionMeasure. SemanticsValues. Subtyping.

CoSingletonToGroup CoercionMeasure. SemanticsValues. Subtyping.

CoStarAssociative CoercionMeasure. SemanticsValues. Subtyping.

CoStarAssociativeReversed DerivedSubtyping.

CoStarCommutative CoercionMeasure. SemanticsValues. Subtyping.

CoStarRef CoercionMeasure. SemanticsValues. Subtyping.

CoStarSingleton CoercionMeasure. SemanticsValues. Subtyping.

CoTensorExchange CoercionMeasure. RevelationDefinition. SemanticsValues. Subtyping. ValueReductionTerminates.

CoTyEq AdmissibleSubtyping. DerivedSubtyping.

CoUnitBang CoercionMeasure. SemanticsValues. Subtyping.

CoVar CoercionMeasure. Subtyping.

ContractiveCoArrow No references.

ContractiveCoAtBang No references.

ContractiveCoBang No references.

ContractiveCoBangExists No references.

ContractiveCoBangIdempotent No references.

ContractiveCoBangPair No references.

ContractiveCoBangRef No references.

ContractiveCoBangRegionCap No references.

ContractiveCoBangRegionCapPunched No references.

ContractiveCoDefocus No references.

ContractiveCoDefocusGroup No references.

ContractiveCoDereliction No references.

ContractiveCoDistrib No references.

ContractiveCoExists No references.

ContractiveCoExistsElim No references.

ContractiveCoExistsIntro No references.

ContractiveCoExistsLeftIntro No references.

ContractiveCoForall No references.

ContractiveCoForallBang No references.

ContractiveCoForallElim No references.

ContractiveCoForallIntro No references.

ContractiveCoForallPair No references.

ContractiveCoForallPairExtrusionLeft No external references.

ContractiveCoForallPairLeft No external references.

ContractiveCoForallRef No references.

ContractiveCoForallRegionCap No references.

ContractiveCoForallRegionCapPunched No references.

ContractiveCoId No references.

ContractiveCoMu No references.

ContractiveCoPairBang No references.

ContractiveCoPairExistsLeft No references.

ContractiveCoPairExistsRight No references.

ContractiveCoPairOtherwise No references.

ContractiveCoPairPhysical No references.

ContractiveCoRef No references.

ContractiveCoRefExists No references.

ContractiveCoRefStar No references.

ContractiveCoRegionCap No references.

ContractiveCoRegionCapPunched No references.

ContractiveCoSeq No references.

ContractiveCoSingletonRegionCapExists No references.

ContractiveCoSingletonStar No references.

ContractiveCoSingletonToGroup No references.

ContractiveCoStarAssociaative No references.

ContractiveCoStarCommutative No references.

ContractiveCoStarRef No references.

ContractiveCoStarSingleton No references.

ContractiveCoTensorExchange No references.

ContractiveCoTyEq No external references.

ContractiveCoUnitBang No references.

ContractiveCoVar No references.

WfCoArrow No references.

WfCoAtBang No references.

WfCoBang No references.

WfCoBangExists No references.

WfCoBangIdempotent No references.

WfCoBangPair No references.

WfCoBangRef No references.

WfCoBangRegionCap No references.

WfCoBangRegionCapPunched No references.

WfCoDefocus No references.

WfCoDefocusGroup No references.

WfCoDereliction No references.

WfCoDistrib No references.

WfCoExists No references.

WfCoExistsElim No references.

WfCoExistsIntro No references.

WfCoExistsLeftIntro No references.

WfCoForall No references.

WfCoForallBang No references.

WfCoForallElim No references.

WfCoForallIntro No references.

WfCoForallPair No references.

WfCoForallPairExtrusionLeft No external references.

WfCoForallPairLeft No external references.

WfCoForallRef No references.

WfCoForallRegionCap No references.

WfCoForallRegionCapPunched No references.

WfCoId No references.

WfCoMu No references.

WfCoPair No references.

WfCoPairBang No references.

WfCoPairExistsLeft No references.

WfCoPairExistsRight No references.

WfCoRef No references.

WfCoRefExists No references.

WfCoRefStar No references.

WfCoRegionCap No references.

WfCoRegionCapPunched No references.

WfCoSeq No references.

WfCoSingletonRegionCapExists No references.

WfCoSingletonStar No references.

WfCoSingletonToGroup No references.

WfCoStarAssociative No references.

WfCoStarCommutative No references.

WfCoStarRef No references.

WfCoStarSingleton No references.

WfCoTensorExchange No references.

WfCoTyEq No external references.

WfCoUnitBang No references.

WfCoVar No references.

ccontractive CoercionMeasure. SemanticsValues. ValueReductionTerminates.

ccontractive_cunfold No references.

ccontractive_lift_1 No external references.

ccontractive_lift_2 No external references.

ccontractive_lift_3 No external references.

ccontractive_subst_1 No external references.

ccontractive_subst_2 No external references.

co_compos Revelation.

co_composs Revelation. RevelationDefinition. Semantics.

co_tensor Revelation. RevelationDefinition.

coercion CoercionMeasure. DerivedSubtyping. Programs. Semantics. Subtyping. ValueReductionTerminates.

contractive_co_tensor No external references.

cunfold CoercionMeasure. SemanticsValues. ValueReductionTerminates.

cunfold_lift No references.

cunfold_subst No external references.

cunfold_subst_mu No references.

cwf LittleFacts. SubjectReductionValues. Typing.

cwf_CoComposExchange No external references.

cwf_CoComposExchangeUnder Revelation.

cwf_CoMixPairComposExchange Revelation.

cwf_CoMixPairExchange No external references.

cwf_CoStarAssociativeReversed No external references.

cwf_co_compos No external references.

cwf_co_composs Revelation. SubjectReduction.

cwf_co_tensor Revelation.

cwf_cunfold SubjectReductionValues.

cwf_lift No external references.

cwf_mu ProgressValues.

cwf_subst No external references.

lift_co PreliminaryLemmas.

lift_lift_co No external references.

lift_subst_1_co No external references.

lift_subst_2_co No external references.

lift_zero_lift_co No references.

subst_co CoercionMeasure. CoercionSubstitution.

subst_lift_co No external references.

subst_subst_co No external references.

closed Programs.

lift_injective Types.

lift_lift Coercions. Programs. RawPrograms. TypeContexts. Types.

lift_lift_var No external references.

lift_subst_1 Coercions. Programs. RawPrograms. TypeContexts. Types.

lift_subst_2 Coercions. Programs. RawPrograms. Types.

lift_subst_var_1 No external references.

lift_subst_var_2 No external references.

lift_var Coercions. Environments. Programs. RawPrograms. RevelationDefinition. Types.

lift_var_injective RawPrograms. TypeEquality.

lift_var_old Environments.

lift_var_recent Revelation. RevelationDefinition.

lift_var_succ Environments.

lift_zero_lift Coercions. Programs. RawPrograms. Types.

pun_1 Programs. Types.

pun_1_var Programs. RawPrograms.

pun_2 Programs. Types.

pun_2_var Programs. RawPrograms.

rotate Types.

rotate1_self_inverse No external references.

rotate1_self_inverse_holds Types.

rotate_var No external references.

rotate_var_characterization No references.

subst_lift Coercions. Environments. Programs. RawPrograms. Types.

subst_lift_var No external references.

subst_subst Coercions. Programs. RawPrograms. Types.

subst_subst_var No external references.

subst_var Coercions. Environments. Programs. RawPrograms. Types.

subst_var_identity DerivedSubtyping. ErasureSimulation. Focus. MoreTypeEquality. SubjectReduction. TypeContexts.

subst_var_miss_1 ErasureSimulation.

subst_var_miss_2 No external references.

well_scoped_lift Closed. RevelationDefinition.

well_scoped_lift_monotonic Closed.

well_scoped_lift_subst Closed. Programs.

well_scoped_subst No external references.

tyapproxeq_decompose_inert_tensor_1 No external references.

tyapproxeq_decompose_inert_tensor_2 No external references.

tyeq_decompose_inert_tensor_1 No references.

tyeq_decompose_inert_tensor_2 No references.

CoExistsExists No external references.

CoExistsForall No external references.

CoForallForall No external references.

JCoBangPairReversed No references.

JCoComposExchange No external references.

JCoExistsCap No external references.

JCoExistsExists No external references.

JCoExistsExists_alternate_formulation No references.

JCoExistsForall No external references.

JCoExistsForall_alternate_formulation No references.

JCoExistsIntroPun No external references.

JCoExistsIntrusion No external references.

JCoExistsLeftIntroReversed No external references.

JCoExistsPairDistrib No external references.

JCoExistsPairIntrusion No references.

JCoExistsScopeRestrictionLeft No references.

JCoExistsScopeRestrictionRight No references.

JCoForallElimPun SubjectReductionValues.

JCoForallElimTrivial No external references.

JCoForallExtrusion No external references.

JCoForallForall No external references.

JCoForallForall_alternate_formulation No references.

JCoForallPairExtrusion No references.

JCoForallPairExtrusionLeft Revelation.

JCoForallPairLeft Revelation.

JCoIdentity No external references.

JCoMixPairComposExchange Revelation.

JCoMixPairExchange Revelation.

JCoPairBangReversed No external references.

JCoStarAssociativeReversed No external references.

JCoTyEq AdmissibleSubtyping. Revelation.

VarianceArrow No references.

VarianceBang No references.

VarianceConstant No references.

VarianceExists No references.

VarianceForall No references.

VarianceHole No references.

VariancePair No references.

VarianceRef No references.

VarianceRegionCap No references.

VarianceRegionCapPunched No references.

coerce No external references.

coerce_negb No external references.

inverse No external references.

jco_coerce_lift No external references.

jco_coerce_negb No external references.

variance No external references.

variance_fill No external references.

variance_lift No external references.

variance_wf No external references.

wf_rotate_ty No external references.

JCoDefocusRoot WeakRefWithAffineContent.

JPSngCreate No references.

JTLet WeakRefWithAffineContent.

JVPack_eq Revelation.

JVPairDelayedSplit WeakRefWithAffineContent.

JVPairDupLeft ReferenceAccess. SubjectReduction.

JVPairDupRight No references.

JVRegionCap_flexible Focus. Progress.

JVRegionCap_flexible_singleton Focus. ProgressValues. ReferenceAccess. SubjectReductionValues.

JVVarInfinity WeakRefWithAffineContent.

ji_singleton_construction SubjectReductionValues.

duplicable_capabilities_have_zero_weight No references.

zero_plus_zero No external references.

EnvEqCons No references.

EnvEqNil No references.

JEnvCons No references.

JEnvNil No references.

env Subtyping. Typing.

env_inclusion WellLayeredness.

env_inclusion_extension WellLayeredness.

env_inclusion_nil WellLayeredness.

env_lift_lift PreliminaryLemmas.

env_subst_lift TypeSubstitution.

env_tensor Revelation.

env_tensor_remove_env_entry No references.

enveq PreliminaryLemmas.

enveq_env_tensor No references.

enveq_lift PreliminaryLemmas.

insert_env MultiplicityEnvironments. PreliminaryLemmas. Revelation. WellLayeredness.

jenv Closed. CoercionSubstitution. DerivedTyping. MultiplicityEnvironments. Subtyping. TermSubstitution. Typing. WellLayeredness.

jenv_env_tensor No references.

jenv_enveq No external references.

jenv_insert Revelation. WellLayeredness.

jenv_lift CoercionSubstitution. PreliminaryLemmas. TermSubstitution.

jenv_map MultiplicityEnvironments. Revelation.

jenv_nil InversionClassification. WellLayeredness.

jenv_substitution CoercionSubstitution. WellLayeredness.

jenv_substitution_old MultiplicityEnvironments. TermSubstitution.

jenv_substitution_recent MultiplicityEnvironments. TermSubstitution.

jenv_type_substitution No external references.

jenv_uniqueness No external references.

jenv_weakening PreliminaryLemmas. WellLayeredness.

jenv_well_scoped Closed.

le_length_map Revelation.

lift_env_tensor PreliminaryLemmas. Revelation.

lift_insert_env Revelation.

lift_ty_env DerivedSubtyping. PreliminaryLemmas.

lift_ty_env_preserves_length Closed.

lift_ty_env_preserves_length_le Revelation.

map_remove MultiplicityEnvironments.

remove_env_entry CoercionSubstitution. MultiplicityEnvironments. PreliminaryLemmas. TermSubstitution. WellLayeredness.

remove_env_entry_simpl TermSubstitution.

remove_insert_env PreliminaryLemmas. WellLayeredness.

remove_lift_env CoercionSubstitution. PreliminaryLemmas. TermSubstitution.

subst_lift_env AdmissibleSubtyping. TypeSubstitution.

subst_ty_env TypeSubstitution.

PweCons No references.

PweNil No references.

erase_lift ErasureSimulation. RevelationDefinition.

erase_store ErasureSimulation. TypeErasure. Typing.

erase_subst ErasureSimulation. RevelationDefinition.

erase_term ErasureSimulation. RevelationDefinition. TypeErasure.

erase_value DerivedTyping. ErasureSimulation. ErasureSimulationValues. Focus. InversionClassification. LittleFacts. PathSemantics. ReferenceAccess. ReferenceAllocation. RegionAllocation. RevelationDefinition. Semantics. TypeErasure. Typing. WeakRefWithAffineContent. WellLayeredness.

pwe DerivedTyping. ErasureSimulationValues. LittleFacts. RevelationDefinition.

pwe_count LittleFacts.

pwe_reflexive ErasureSimulationValues. Focus. Progress.

pwe_some LittleFacts.

pwe_vmap_coapp SubjectReductionValues.

pwe_vmap_vtyabs SubjectReductionValues.

erasure_simulation TypeErasure.

erasure_simulation_nonzero No external references.

erasure_simulation_zero No external references.

hideous No external references.

hideous_CoMixPairCompossExchange No external references.

hideous_redvt No external references.

hideous_subst No external references.

measure No external references.

measure_redvt No external references.

measure_subst No external references.

mredvt TypeErasure.

mredvt_wf TypeErasure.

values_stutter ErasureSimulation. SubjectReductionValues.

values_stutter_yup SubjectReductionValues.

defocus_duplicable_progress_plug Progress.

defocus_duplicable_sr SubjectReduction.

defocus_group_sr SubjectReductionValues.

defocus_progress_plug ProgressValues.

defocus_progress_select Progress. ProgressValues.

defocus_sr SubjectReductionValues.

focus_progress Progress.

focus_sr SubjectReduction.

focus_sr_preliminary No external references.

ji_focus SubjectReduction.

JPathPairLeft No references.

JPathPairRight No references.

JPathRef No references.

JPathRegionCapSingleton No references.

JPathRoot DerivedTyping.

PathPairLeft PathSemantics. Revelation. WellLayeredness.

PathPairRight PathSemantics. Revelation. WeakRefWithAffineContent. WellLayeredness.

PathRef PathSemantics. Revelation. WeakRefWithAffineContent. WellLayeredness.

PathRegionCapSingleton PathSemantics. Revelation. WeakRefWithAffineContent. WellLayeredness.

PathRoot DerivedTyping. Focus. PathSemantics. Revelation. SubjectReduction. WeakRefWithAffineContent. WellLayeredness.

jpath Focus. Revelation. Subtyping. Typing.

jpath_lift PreliminaryLemmas. Revelation.

jpath_subst TypeSubstitution.

jpath_wf_1 Focus.

jpath_wf_2 No references.

path Coercions. PathSemantics. Programs. Revelation. WeakRefWithAffineContent. WellLayeredness.

ccAbs No external references.

ccArrow No external references.

co_ccArrow No external references.

jco_ccArrow No references.

jv_ccAbs No references.

classification_arrow No external references.

classification_at No external references.

classification_at_neutral LittleFacts. SubjectReductionValues.

classification_bang No external references.

classification_exists No external references.

classification_forall No external references.

classification_loc No external references.

classification_pair No external references.

classification_regioncap No external references.

classification_regioncappunched No external references.

classification_unit No external references.

group_inhabitation Focus. Progress.

inversion_tval No external references.

inversion_vabs No external references.

inversion_vbang No external references.

inversion_vinhabitant No external references.

inversion_vloc No external references.

inversion_vpack No external references.

inversion_vpair No external references.

inversion_vregioncap No external references.

inversion_vregioncappunched No external references.

inversion_vtyabs No external references.

inversion_vunit No external references.

ji_singleton_inversion No external references.

prediction_vabs No external references.

prediction_vbang No external references.

prediction_vinhabitant No external references.

prediction_vloc No external references.

prediction_vpack No external references.

prediction_vpair No external references.

prediction_vregioncap No external references.

prediction_vregioncappunched No external references.

prediction_vtyabs No external references.

prediction_vunit No external references.

singleton_inhabitation Focus.

singleton_inhabitation_preliminary No external references.

singleton_inhabitation_preliminary_variant Progress.

toplevel_var ProgressValues.

Logical Coercions. DerivedSubtyping. DupCapZeroWeight. Erasure. ErasureSimulation. Programs. RevelationDefinition. SemanticsValues. Subtyping. Types. WeakRefWithAffineContent. WellLayeredness.

Physical CoercionMeasure. Coercions. DerivedSubtyping. Erasure. ErasureSimulation. Programs. RevelationDefinition. Types. ValueReductionTerminates. WeakRefWithAffineContent. WellLayeredness.

layer Coercions. FocusPaths. MoreTypeEquality. Programs. Types. WellLayeredness.

layer_conj Coercions. DerivedSubtyping. SemanticsValues. Subtyping. WellLayeredness.

layer_conj_associative WellLayeredness.

layer_conj_commutative DerivedSubtyping. WellLayeredness.

layer_logical_neutral_left No references.

layer_logical_neutral_right WellLayeredness.

LexprodLeft No external references.

LexprodRight No external references.

lexicographic_product No external references.

lexicographic_product.A No external references.

lexicographic_product.B No external references.

lexicographic_product.eqA No external references.

lexicographic_product.eqA_lessA_compatible No references.

lexicographic_product.eqA_reflexive No references.

lexicographic_product.eqA_symmetric No references.

lexicographic_product.eqA_transitive No references.

lexicographic_product.lessA No external references.

lexicographic_product.lessA_eqA_compatible No references.

lexicographic_product.lessA_transitive No references.

lexicographic_product.lessB No external references.

lexicographic_product.lessB_transitive No references.

lexicographic_product.wfA No references.

lexicographic_product.wfB No references.

lexprod ErasureSimulation. MyMultisets. ValueReductionTerminates.

lexprod_accessibility No external references.

lexprod_intro No external references.

lexprod_transitive MyMultisets.

lexprod_wf ErasureSimulation. MyMultisets. ValueReductionTerminates.

Args No external references.

Boxer No external references.

Hnts No external references.

Hyps No external references.

LibTacticsCompatibility No references.

Vars No external references.

boxer No external references.

dup_lemma No external references.

equatesLemma No external references.

equatesLemma.A0 No external references.

equatesLemma.A1 No external references.

equatesLemma.A2 No external references.

equatesLemma.A3 No external references.

equatesLemma.A4 No external references.

equatesLemma.A5 No external references.

equatesLemma.A6 No references.

equates_0 No external references.

equates_1 No external references.

equates_2 No external references.

equates_3 No external references.

equates_4 No external references.

equates_5 No external references.

equates_6 No external references.

iff_intro_swap No external references.

inj_pair2 No external references.

ltac_Mark No external references.

ltac_No_arg No external references.

ltac_Wild No external references.

ltac_Wilds No external references.

ltac_database No external references.

ltac_database_provide No external references.

ltac_inst No external references.

ltac_mark No external references.

ltac_no_arg No references.

ltac_tag_subst No external references.

ltac_to_generalize No external references.

ltac_wild No external references.

ltac_wilds No external references.

skip_axiom No external references.

fictitious_jsto SubjectReduction.

inhabitant_compatible SubjectReduction.

ji_coapp SubjectReductionValues.

ji_vtyabs SubjectReductionValues.

jsto_inversion Progress.

jsto_inversion_preliminary No external references.

jv_duplicable No external references.

pair_inhabitant No external references.

region_compatibility_1 No external references.

region_compatibility_1b DerivedTyping.

region_compatibility_1bs No external references.

region_compatibility_2 No external references.

region_compatibility_2b DerivedTyping.

region_compatibility_3b No external references.

j_rio Focus. ReferenceAllocation. RegionAllocation. SubjectReduction.

j_rio_term No references.

discrete_add No external references.

discrete_add_associative No external references.

discrete_add_commutative No external references.

discrete_add_default No external references.

discrete_add_default_symmetric No external references.

discrete_add_eq No external references.

discrete_add_matches_discrete_star No external references.

discrete_add_neq No external references.

discrete_add_spec No external references.

discrete_add_spec_eq No external references.

discrete_add_spec_neq No external references.

discrete_resource No external references.

discrete_star No external references.

store_typing No external references.

store_typing_duplicable No references.

store_typing_resource No external references.

ExhibitsTyCon No references.

HasArrow No references.

HasAt No references.

HasBang No references.

HasPair No references.

HasQ No references.

HasRef No references.

HasRegionCap No references.

HasRegionCapPunched No references.

HasUnit No references.

InertRegion No references.

InertTensor No references.

InertVar No references.

TmoMu No references.

TmoTensor No references.

TyConArrow InversionClassification.

TyConAt InversionClassification.

TyConBang InversionClassification.

TyConPair InversionClassification.

TyConQ InversionClassification.

TyConRef InversionClassification.

TyConRegionCap InversionClassification.

TyConRegionCapPunched InversionClassification.

TyConUnit InversionClassification.

commutative_pair DerivedSubtyping. Revelation. Subtyping.

commutative_pair_existence Revelation.

commutative_pair_symmetric DerivedSubtyping.

commutative_pair_wf_first DerivedSubtyping.

commutative_pair_wf_second DerivedSubtyping.

composs Revelation. SubjectReduction. Typing.

composs_app SubjectReduction.

composs_snoc No references.

composs_ssopmoc No external references.

exhibits_tensor No external references.

exhibits_tycon InversionClassification.

exhibits_tycon_inert No external references.

exhibits_tyeq No external references.

exploit_commutative_pair DerivedSubtyping.

exploit_commutative_pair_2 Revelation.

fold_composs No references.

fold_tensors SubjectReductionValues.

has_exhibits No external references.

has_tycon No external references.

if_tensor_exhibits_arrow No references.

if_tensor_exhibits_tycon No external references.

if_tensor_exhibits_tycon_preliminary No external references.

inert DecidableTypeEquality.

inert_tensors No external references.

lift_commutative_pair No external references.

lift_tensors PreliminaryLemmas.

srosnet No external references.

ssopmoc No external references.

subst_commutative_pair No external references.

subst_tensors SubjectReductionValues. TypeSubstitution.

tensors ProveTypeEquality. Revelation. Subtyping.

tensors_arrow SubjectReduction.

tensors_at No external references.

tensors_bang No external references.

tensors_pair No external references.

tensors_q No external references.

tensors_ref No external references.

tensors_regioncap No external references.

tensors_regioncappunched No external references.

tensors_snoc Revelation.

tensors_srosnet No external references.

tensors_unit No external references.

tmo No external references.

tmo_tto No external references.

tmo_well_founded No external references.

tycon No external references.

tyeq_composs SubjectReduction.

tyeq_tensors ProveTypeEquality.

tyred_inert DecidableTypeEquality.

wf_composs No external references.

wf_tensors SubjectReductionValues.

MInfinity DerivedTyping. MultiplicityEnvironments. TermSubstitution. Typing. WeakRefWithAffineContent.

MOne DerivedTyping. Intuitionistic. InversionClassification. MultiplicityEnvironments. Revelation. SubjectReductionValues. TermSubstitution. Typing. WeakRefWithAffineContent.

MStarInfinity No references.

MStarOneLeft Revelation.

MStarOneRight No references.

MStarZero No references.

MZero MultiplicityEnvironments. SubjectReductionValues. TermSubstitution. WeakRefWithAffineContent.

NonzeroInfinity No references.

NonzeroOne No references.

StarInfinity No external references.

StarOneLeft Revelation.

StarOneRight Revelation.

StarZero No external references.

invert_menv_star_nil No external references.

le_length_neutral Revelation.

madd No external references.

menv LittleFacts. MultiplicityEnvironments. Revelation. SubjectReduction. SubjectReductionValues. TermSubstitution. Typing.

menv_star_cons Revelation.

menv_star_nil No external references.

mneutral No external references.

mstar No external references.

multiplicity MultiplicityEnvironments.

multiplicity_resource No references.

neutral_length Revelation.

nonzero MultiplicityEnvironments. TermSubstitution. Typing.

nonzero_star MultiplicityEnvironments.

insert_star Revelation.

j_term_substitution_infinity_bang TermSubstitution.

jenv_neutral No external references.

jenv_neutral_infinity TermSubstitution.

jenv_neutral_one TermSubstitution.

jenv_neutral_zero TermSubstitution.

jenv_star No external references.

neutral_remove PreliminaryLemmas. TermSubstitution.

permute_left_remove No external references.

present No external references.

present_star PreliminaryLemmas.

present_substitution_old TermSubstitution.

present_substitution_recent TermSubstitution.

rotate_right_remove No external references.

split_as_dictated TermSubstitution.

split_as_you_like PreliminaryLemmas.

split_infinity TermSubstitution.

split_one No external references.

split_zero TermSubstitution.

binary_choice Resources.

MyLPO No references.

MyLeFEqual No references.

MyLeFOtherTensor No references.

MyVLPO No references.

MyVLPO.LPO.S.LO.lex1 No external references.

MyVLPO.LPO.lpo1 No external references.

MyVLPO.LPO.lpo2 No external references.

MyVLPO.LPO.lpo3 No external references.

MyVLPO.LPO.lt_lpo TypeEquality.

Precedence No references.

Precedence.Sig No external references.

Precedence.eqF No references.

Precedence.leF No external references.

Precedence.leF_dec No references.

Precedence.leF_preorder No references.

Precedence.leF_reflexive No external references.

Precedence.leF_transitive No external references.

Precedence.ltF No external references.

Precedence.ltF_wf No references.

Precedence.myLeF No external references.

Precedence.mySig No external references.

SOther No external references.

STensor No external references.

VRPO_Results No references.

VRPO_Results.wf_lt No external references.

beq_symb No external references.

beq_symb_ok No external references.

fact1 No external references.

fact2 No external references.

in2 No external references.

in3 No external references.

myLPO_wf TypeEquality.

myLeF No external references.

mySig No external references.

other No external references.

other0 TypeEquality.

other1 TypeEquality.

other2 TypeEquality.

other3 TypeEquality.

other_tensor_lt_tensor_other_left No external references.

other_tensor_lt_tensor_other_right No external references.

subterm No external references.

subterm_11 No external references.

subterm_21 No external references.

subterm_22 No external references.

subterm_31 No external references.

subterm_32 No external references.

subterm_33 No external references.

symbol No external references.

tensor TypeEquality.

tensor_arrow_reduction No external references.

tensor_distribution No external references.

tensor_selective_distribution_2_2 No external references.

tensor_selective_distribution_3_2 No external references.

tensor_simplification_left No external references.

tensor_simultaneous_distribution No external references.

tensor_simultaneous_distribution_arity_0 No external references.

tensor_simultaneous_distribution_arity_1 No external references.

tensor_simultaneous_distribution_arity_2 No external references.

CaDesc No references.

CaDesc.A No references.

CaDesc.cadesc No external references.

CaDescSet No references.

CaDescSet_dec No references.

CaDescSet_dec.Eq No references.

CaDescSet_dec.cadesc No external references.

CaDescSet_dec.eqA_dec No references.

Demo No external references.

MSetCore No references.

MSetCore.Multiset ValueReductionTerminates.

MSetCore.empty ValueReductionTerminates.

MSetCore.meq No external references.

MSetCore.singleton No external references.

MSetCore.union No external references.

MSetOrd No references.

MSetOrd.MSetGT No external references.

MSetOrd.MultisetGT ValueReductionTerminates.

MSetOrd.MultisetLT ValueReductionTerminates.

MSetOrd.mOrd_trans No external references.

MSetOrd.mOrd_wf No external references.

MSetTheory No references.

MSetTheory.empty_dec No external references.

MSetTheory.member No external references.

MSetTheory.member_notempty No external references.

MSetTheory.member_union No external references.

MSetTheory.member_union_l No external references.

MSetTheory.meq_refl No external references.

MSetTheory.meq_sym ValueReductionTerminates.

MSetTheory.meq_trans ValueReductionTerminates.

MSetTheory.not_empty No external references.

MSetTheory.singleton_member No external references.

MSetTheory.singleton_member_eqA No external references.

MSetTheory.singleton_notempty No external references.

MSetTheory.union_assoc ValueReductionTerminates.

MSetTheory.union_comm No external references.

MSetTheory.union_empty No external references.

MSetTheory.union_notempty No external references.

MultisetGE ValueReductionTerminates.

MultisetGE_reflexive ValueReductionTerminates.

MultisetGE_transitive No references.

MultisetGTGE_transitive ValueReductionTerminates.

MultisetGTLT ValueReductionTerminates.

MultisetGT_transitive No external references.

MultisetLT_wf ValueReductionTerminates.

cadesc No external references.

demo_multiset_union_permut_simpl_1 No references.

demo_multiset_union_permut_simpl_2 No references.

demo_multiset_union_permut_simpl_3 No references.

eqmul_simplify_left ValueReductionTerminates.

ge No external references.

ge_covariant_union ValueReductionTerminates.

ge_excess ValueReductionTerminates.

ge_intro ValueReductionTerminates.

ge_singleton_singleton ValueReductionTerminates.

gt ValueReductionTerminates.

gt_excess_l No external references.

gt_excess_r No references.

gt_ge_gt ValueReductionTerminates.

gt_singleton_singleton No external references.

in_singleton No external references.

lt No external references.

max_left No references.

max_right No references.

permut_get_1 No external references.

permut_get_2 No external references.

permut_get_3 No external references.

permut_get_4 No external references.

permut_get_5 No external references.

permut_get_6 No external references.

permut_get_7 No external references.

permut_get_8 No external references.

permut_tactic_keep No external references.

permut_tactic_setup No external references.

permut_tactic_simpl_eq No external references.

permut_tactic_simpl_incl No external references.

permut_tactic_trans No external references.

singleton_empty_gt No external references.

singleton_multiset_ordering ValueReductionTerminates.

union_comm_assoc ValueReductionTerminates.

union_comm_assoc_variant ValueReductionTerminates.

union_covariant_ge_gt ValueReductionTerminates.

union_covariant_gt_ge ValueReductionTerminates.

union_covariant_gt_ge_singleton_empty No references.

union_covariant_l No external references.

union_covariant_l_empty No external references.

union_covariant_lr No external references.

union_covariant_r No external references.

union_covariant_r_empty No external references.

union_empty_l No external references.

union_empty_r ValueReductionTerminates.

union_singleton_gt No external references.

well_founded_gt No external references.

well_founded_lt No external references.

mark_ih TermSubstitution. ValueReductionTerminates.

pi1 Erasure. ErasureSimulation. PreliminaryLemmas. ProgressValues. Revelation. RevelationDefinition. SubjectReductionValues. WellLayeredness.

pi2 PreliminaryLemmas. RevelationDefinition.

pi3 Closed. Erasure. ErasureSimulation. PreliminaryLemmas. Revelation. RevelationDefinition. WellLayeredness.

transpose ErasureSimulation. MyMultisets. TypeEquality. ValueReductionTerminates.

PlugPairLeft No references.

PlugPairRight No references.

PlugRef No references.

PlugRegionCapSingleton No references.

PlugRoot No references.

SelectPairLeft No references.

SelectPairRight No references.

SelectRef No references.

SelectRegionCapSingleton No references.

SelectRoot No references.

plug ErasureSimulation. Focus. Semantics. SemanticsValues. ValueReductionTerminates. WellLayeredness.

plugging_respects_erasure ErasureSimulation. ErasureSimulationValues. Focus.

select Focus. Semantics. SemanticsValues. WellLayeredness.

j_multiplicity_weakening No external references.

j_resource_multiplicity_weakening SubjectReduction. SubjectReductionValues. TermSubstitution.

j_resource_multiplicity_weakening_term No references.

j_resource_weakening SubjectReduction.

j_term_resource_weakening SubjectReduction. TermSubstitution.

j_term_weakening SubjectReductionValues.

j_term_weakening_2 Revelation.

j_term_weakening_general Revelation. SubjectReductionValues.

j_term_weakening_insert Revelation.

j_ty_weakening_general No external references.

j_ty_weakening_term No references.

j_ty_weakening_value SubjectReductionValues.

j_ty_weakening_value_remove TermSubstitution.

j_value_resource_weakening Focus. InversionClassification. LittleFacts. RegionAccess. TermSubstitution.

j_value_weakening SubjectReduction.

j_value_weakening_insert Revelation.

j_value_weakening_remove TermSubstitution.

jco_ty_weakening CoercionSubstitution.

jco_ty_weakening_arrow DerivedSubtyping.

jco_ty_weakening_nil_arrow No external references.

jco_weakening CoercionSubstitution.

jco_weakening_general No external references.

jco_wf No external references.

jco_wf_left No external references.

jco_wf_right No external references.

ji_tyeq InversionClassification.

jp_ty_weakening No external references.

jp_wf_1 No external references.

jp_wf_2 No external references.

jvit_enveq InversionClassification.

jvit_wf No external references.

PAdopt Erasure. Semantics. Typing. WellLayeredness.

PDefocusDuplicable Erasure. Revelation. Semantics. Typing. WellLayeredness.

PFocus DerivedTyping. Erasure. Revelation. Semantics. Typing. WeakRefWithAffineContent. WellLayeredness.

PFocusGroup Erasure. Semantics. Typing. WellLayeredness.

PNewAffine Erasure. Semantics. Typing. WellLayeredness.

PNewCap Erasure. Semantics. Typing. WeakRefWithAffineContent. WellLayeredness.

PNewGroup Erasure. Semantics. Typing. WellLayeredness.

PReadAffine Erasure. Semantics. Typing. WellLayeredness.

PReadCap Erasure. Semantics. Typing. WeakRefWithAffineContent. WellLayeredness.

PWriteAffine Erasure. Semantics. Typing. WellLayeredness.

PWriteCap Erasure. Semantics. Typing. WeakRefWithAffineContent. WellLayeredness.

TApp Erasure. ErasureSimulation. RevelationDefinition. Semantics. Typing. ValueReductionTerminates. WellLayeredness.

TCoApp Erasure. ErasureSimulation. RevelationDefinition. Semantics. SemanticsValues. Typing. ValueReductionTerminates. WellLayeredness.

THide Erasure. ErasureSimulation. RevelationDefinition. Semantics. TermSubstitution. Typing. ValueReductionTerminates. WeakRefWithAffineContent. WellLayeredness.

TLet DerivedTyping. WeakRefWithAffineContent.

TLetBang Erasure. ErasureSimulation. RevelationDefinition. Semantics. Typing. ValueReductionTerminates. WeakRefWithAffineContent. WellLayeredness.

TLetMixPair RevelationDefinition. WeakRefWithAffineContent.

TLetPair Erasure. ErasureSimulation. RevelationDefinition. Semantics. Typing. ValueReductionTerminates. WellLayeredness.

TLetUnpack Erasure. ErasureSimulation. RevelationDefinition. Semantics. SemanticsValues. Typing. ValueReductionTerminates. WeakRefWithAffineContent. WellLayeredness.

TMixPair Erasure. ErasureSimulation. RevelationDefinition. Semantics. Typing. ValueReductionTerminates. WellLayeredness.

TPrimApp Erasure. ErasureSimulation. Revelation. RevelationDefinition. Semantics. Typing. ValueReductionTerminates. WeakRefWithAffineContent. WellLayeredness.

TTyAbs Erasure. ErasureSimulation. RevelationDefinition. Semantics. SemanticsValues. Typing. ValueReductionTerminates. WellLayeredness.

TVal Erasure. ErasureSimulation. InversionClassification. Progress. ReferenceAccess. ReferenceAllocation. RevelationDefinition. Semantics. TypeErasure. Typing. ValueReductionTerminates. WeakRefWithAffineContent. WellLayeredness.

VAbs Canonical. Erasure. Intuitionistic. InversionClassification. RevelationDefinition. Semantics. SemanticsValues. Typing. ValueReductionTerminates. WeakRefWithAffineContent. WellLayeredness.

VBang Canonical. Erasure. Focus. Intuitionistic. InversionClassification. RevelationDefinition. Semantics. SemanticsValues. TermSubstitution. Typing. ValueReductionTerminates. WeakRefWithAffineContent. WellLayeredness.

VCoApp Erasure. LittleFacts. RevelationDefinition. Semantics. SemanticsValues. Typing. ValueReductionTerminates. WeakRefWithAffineContent. WellLayeredness.

VCons Canonical. DerivedTyping. Erasure. Focus. InversionClassification. LittleFacts. PathSemantics. ReferenceAccess. RegionAllocation. RevelationDefinition. Semantics. SemanticsValues. Typing. ValueLists. ValueReductionTerminates. WellLayeredness.

VInhabitant Canonical. Erasure. Focus. InversionClassification. LittleFacts. ReferenceAccess. RegionAllocation. RevelationDefinition. Semantics. SemanticsValues. TermSubstitution. Typing. ValueReductionTerminates. WellLayeredness.

VLoc Canonical. Erasure. InversionClassification. PathSemantics. ReferenceAccess. ReferenceAllocation. RevelationDefinition. Semantics. SemanticsValues. TermSubstitution. Typing. ValueReductionTerminates. WellLayeredness.

VLogPair Focus. Semantics. SemanticsValues.

VLogUnit No references.

VMixPair Focus. ReferenceAccess. RevelationDefinition. Semantics. SemanticsValues. ValueReductionTerminates. WeakRefWithAffineContent.

VNil Canonical. DerivedTyping. Erasure. Focus. InversionClassification. LittleFacts. PathSemantics. ReferenceAccess. RegionAllocation. RevelationDefinition. Semantics. SemanticsValues. Typing. ValueLists. ValueReductionTerminates. WellLayeredness.

VPack Canonical. DerivedTyping. Erasure. Focus. InversionClassification. RevelationDefinition. Semantics. SemanticsValues. Typing. ValueReductionTerminates. WellLayeredness.

VPair Canonical. DerivedTyping. Erasure. InversionClassification. PathSemantics. RevelationDefinition. Semantics. SemanticsValues. Typing. ValueReductionTerminates. WellLayeredness.

VPhyPair ReferenceAccess. Semantics. WeakRefWithAffineContent.

VPhyUnit ReferenceAccess. Semantics.

VRegionCap Canonical. DerivedTyping. Erasure. Focus. InversionClassification. PathSemantics. ReferenceAccess. RegionAllocation. RevelationDefinition. Semantics. SemanticsValues. SubjectReduction. TermSubstitution. Typing. ValueReductionTerminates. WellLayeredness.

VRegionCapPunched Canonical. Erasure. Focus. InversionClassification. RevelationDefinition. Semantics. SemanticsValues. TermSubstitution. Typing. ValueReductionTerminates. WellLayeredness.

VTyAbs Canonical. Erasure. InversionClassification. LittleFacts. RevelationDefinition. Semantics. SemanticsValues. Typing. ValueReductionTerminates. WeakRefWithAffineContent. WellLayeredness.

VUnit Canonical. InversionClassification. RevelationDefinition. SemanticsValues. Typing. ValueReductionTerminates. WellLayeredness.

VVar Canonical. DerivedTyping. Erasure. InversionClassification. PreliminaryLemmas. Revelation. RevelationDefinition. SemanticsValues. TermSubstitution. Typing. ValueReductionTerminates. WeakRefWithAffineContent. WellLayeredness.

closed_value Closed. InversionClassification. LittleFacts. RevelationDefinition. Typing.

closed_value_lift PreliminaryLemmas.

closed_value_subst TermSubstitution.

eq_coercion_dec No external references.

eq_layer_dec No external references.

eq_path_dec No external references.

eq_primitive_dec No external references.

eq_term_dec No references.

eq_value_dec ValueLists. WellLayeredness.

eq_values_dec No references.

lift_lift_term RevelationDefinition.

lift_lift_value RevelationDefinition.

lift_lift_value_term No external references.

lift_subst_1_term No external references.

lift_subst_1_value No external references.

lift_subst_1_value_term No external references.

lift_subst_2_term RevelationDefinition.

lift_subst_2_value No external references.

lift_subst_2_value_term No external references.

lift_term Closed. Erasure. PreliminaryLemmas. Revelation. RevelationDefinition. SemanticsValues. WellLayeredness.

lift_value Canonical. Closed. Erasure. PreliminaryLemmas. Revelation. RevelationDefinition. Semantics. WellLayeredness.

lift_zero_lift_term No references.

lift_zero_lift_value No references.

primitive Typing. WellLayeredness.

pun_1_term No references.

pun_1_value No references.

pun_1_value_term No external references.

pun_2_term No references.

pun_2_value No references.

pun_2_value_term No external references.

store Erasure. Progress. Semantics. Typing. WellLayeredness.

subst_lift_term Closed.

subst_lift_value No external references.

subst_lift_value_term No external references.

subst_subst_term No references.

subst_subst_value No references.

subst_subst_value_term No external references.

subst_term Closed. Erasure. ErasureSimulation. RevelationDefinition. Semantics. SemanticsValues. TermSubstitution. WellLayeredness.

subst_value Erasure. TermSubstitution. WellLayeredness.

term Erasure. ErasureSimulation. Progress. RevelationDefinition. Semantics. Typing. ValueReductionTerminates. WellLayeredness.

value Canonical. Erasure. PathSemantics. RevelationDefinition. Semantics. SemanticsValues. TermSubstitution. Typing. ValueLists. ValueReductionTerminates. WellLayeredness.

value_term_ind Erasure. RevelationDefinition.

values Canonical. Erasure. RevelationDefinition. SemanticsValues. Typing. ValueLists. ValueReductionTerminates. WellLayeredness.

AcceptableStep No external references.

AcceptableValue No references.

acceptable No external references.

progress No external references.

progress_configurations TypeErasure.

progress_values Progress.

progress_values_preliminary No external references.

prop_ext Resources.

RawTApp Erasure. RawSemantics.

RawTFirst Erasure.

RawTLet Erasure.

RawTLetPair Erasure. RawSemantics.

RawTNew Erasure. RawSemantics.

RawTRead Erasure. RawSemantics.

RawTVal Erasure. RawSemantics. TypeErasure.

RawTWrite Erasure. RawSemantics.

RawVAbs Erasure. RawSemantics.

RawVErased Erasure. WellLayeredness.

RawVLoc Erasure. ErasureSimulation. RawSemantics. Semantics.

RawVPair Erasure. RawSemantics.

RawVUnit Erasure. RawSemantics. ResourcesContinued.

RawVVar Erasure. RevelationDefinition.

lift_raw_term Erasure. RevelationDefinition.

lift_raw_value Erasure. RawSemantics. RevelationDefinition.

lift_raw_value_term_injective No references.

raw_lift_lift_term RevelationDefinition.

raw_lift_lift_value Erasure. RevelationDefinition.

raw_lift_lift_value_term No external references.

raw_lift_subst_1_term No external references.

raw_lift_subst_1_value Erasure.

raw_lift_subst_1_value_term No external references.

raw_lift_subst_2_term Erasure. RevelationDefinition.

raw_lift_subst_2_term_rawverased RevelationDefinition.

raw_lift_subst_2_value No external references.

raw_lift_subst_2_value_term No external references.

raw_lift_zero_lift_term No references.

raw_lift_zero_lift_value No references.

raw_pun_1 Erasure.

raw_pun_2 Erasure. RevelationDefinition.

raw_store Erasure. RawSemantics. TypeErasure.

raw_subst_lift_term RevelationDefinition.

raw_subst_lift_value ErasureSimulation.

raw_subst_lift_value_term No external references.

raw_subst_subst_term Erasure.

raw_subst_subst_value No external references.

raw_subst_subst_value_term No external references.

raw_term Erasure. RawSemantics. TypeErasure.

raw_value Erasure. ResourcesContinued.

raw_value_term_ind No external references.

subst_raw_term Erasure. RawSemantics.

subst_raw_value Erasure.

DivergesCons No references.

RawRedAppContext No references.

RawRedBeta No references.

RawRedLetPair No references.

RawRedNew No references.

RawRedRead No references.

RawRedWriteCap No references.

RawRedplusAppContext No external references.

RredplusMore ErasureSimulation.

RredplusOne ErasureSimulation.

RredstarMore No references.

RredstarZero No references.

SensibleRawStore No references.

diverges TypeErasure.

empty_raw_store_is_sensible No references.

raw_reduction_preserves_sensible No references.

rred TypeErasure.

rred_and_rredplus TypeErasure.

rred_and_rredstar TypeErasure.

rred_deterministic No external references.

rredplus ErasureSimulation.

rredplus_implies_rredstar No external references.

rredstar TypeErasure.

sensible_raw_store No external references.

values_do_not_reduce TypeErasure.

controlled_reference_write SubjectReduction.

reference_write SubjectReduction.

new_reference_allocation SubjectReduction.

ji_inversion Focus. Progress.

adoption SubjectReduction.

group_region_allocation SubjectReduction.

region_compatibility_extend_group No external references.

singleton_region_allocation Focus. SubjectReduction.

Inhabited MoreResources. ResourcesContinued.

ListForall2Cons No references.

ListForall2Nil No references.

ListStarCons No references.

ListStarNil No references.

OptionStarLeft No references.

OptionStarRight No references.

STAR MoreResources. Multiplicity.

Void No external references.

Void_mset No references.

Void_pair_resource No references.

aMap MoreResources. ResourcesContinued.

add MoreResources. Multiplicity. ResourcesReconfiguration.

add_associative ResourcesReconfiguration.

add_commutative ResourcesReconfiguration.

alimit ResourcesContinued.

allocate ResourcesContinued.

allocate_rio ResourcesContinued.

allocate_rxo ResourcesContinued.

amap ResourcesContinued.

amap_update ResourcesContinued.

compatible_implies_common_core ResourcesContinued.

compatible_split ResourcesReconfiguration.

core_implies_duplicable No references.

duplicable DupCapZeroWeight. LittleFacts. MultiplicityEnvironments. ResourcesContinued. TermSubstitution. WeakRefWithAffineContent.

duplicable_implies_core LittleFacts. MultiplicityEnvironments. WeakRefWithAffineContent.

duplicable_neutral DupCapZeroWeight. Multiplicity.

duplicable_split LittleFacts. ProgressValues.

duplicable_split_2 LittleFacts.

duplicable_split_left DupCapZeroWeight.

duplicable_split_right DupCapZeroWeight.

duplicable_void WeakRefWithAffineContent.

empty_mset ResourcesContinued.

extend_mset ResourcesContinued.

inhabitant MoreResources. ResourcesContinued.

inhabited_unit No references.

list_add No external references.

list_forall2 No external references.

list_resource No external references.

list_star No external references.

mSet ResourcesContinued.

map_resource MoreResources.

mkaMap No external references.

mkmSet No external references.

monotonic_set_resource No external references.

mset ResourcesContinued.

nat_resource No external references.

nat_void No references.

neutral DerivedTyping. Intuitionistic. InversionClassification. LittleFacts. MoreResources. Multiplicity. MultiplicityEnvironments. RegionAllocation. ResourcesContinued. Revelation. SubjectReductionValues. TermSubstitution. Typing.

neutral_idempotent No external references.

option_add No external references.

option_resource No external references.

option_rxo No external references.

option_star ResourcesContinued.

option_star_duplicable_implies_core No external references.

option_star_notowned_left No external references.

option_star_notowned_right No external references.

option_star_owned_exclusive No external references.

option_star_owned_left No external references.

option_star_owned_right No external references.

option_void No references.

owned ResourcesContinued.

pair_resource No external references.

rio Monotonicity. MoreResources. Multiplicity. ReferenceAccess. ReferenceAllocation. ResourcesContinued. SubjectReduction.

rio_extend_mset ResourcesContinued.

rio_neutral ResourcesContinued.

rio_reflexive ReferenceAccess. ResourcesContinued. SubjectReduction.

rio_star No external references.

rio_transitive SubjectReduction.

rio_update ResourcesContinued.

rxo MoreResources. Multiplicity. ResourcesContinued.

rxo_extend_mset ResourcesContinued.

rxo_reflexive ResourcesContinued.

rxo_star ResourcesContinued.

rxo_transitive No external references.

rxo_update ResourcesContinued.

send_down_both_ways TermSubstitution.

singleton_mset ResourcesContinued.

star DerivedTyping. Focus. InversionClassification. LittleFacts. MoreResources. Multiplicity. MultiplicityEnvironments. PreliminaryLemmas. Progress. ReferenceAccess. ReferenceAllocation. RegionAllocation. ResourcesContinued. ResourcesReconfiguration. SubjectReduction. TermSubstitution. Typing.

star_allocate ResourcesContinued.

star_amap ResourcesContinued.

star_associative MultiplicityEnvironments. ResourcesReconfiguration.

star_associative_reverse No external references.

star_commutative DerivedTyping. Focus. LittleFacts. MultiplicityEnvironments. Progress. RegionAccess. RegionAllocation. ResourcesContinued. ResourcesReconfiguration. Revelation. SubjectReduction. SubjectReductionValues. TermSubstitution. WeakRefWithAffineContent.

star_deterministic ResourcesReconfiguration.

star_extend_mset ResourcesContinued.

star_length_eq No external references.

star_length_le Revelation.

star_neutral DerivedTyping. Focus. MultiplicityEnvironments. Progress. RegionAllocation. ResourcesContinued. Revelation. SubjectReduction. SubjectReductionValues. TermSubstitution.

star_neutral_bang TermSubstitution.

star_neutral_generalized SubjectReduction.

star_neutral_map Multiplicity. MultiplicityEnvironments. ResourcesContinued.

star_update ResourcesContinued.

star_update_owned ResourcesContinued.

update ResourcesContinued.

void ResourcesContinued. WeakRefWithAffineContent.

void_list_resource No references.

void_map_resource No references.

allocate_group RegionAllocation.

allocate_reference ReferenceAllocation.

allocate_reference_unowned ReferenceAllocation.

allocate_singleton RegionAllocation.

allocate_singleton_R1 RegionAllocation.

allocate_singleton_R2 RegionAllocation.

duplicable_own_location DupCapZeroWeight. ProgressValues.

duplicable_own_region DupCapZeroWeight. ProgressValues.

empty_allocate_group No external references.

extend_group RegionAllocation.

fictitious Focus. LittleFacts. RegionAllocation.

fictitious_rxo No references.

fictitious_star No external references.

fictitious_star_symmetric No external references.

inhabited_raw_value No references.

location_map InversionClassification. LittleFacts. Typing.

location_map_allocate_reference_1 No external references.

location_map_allocate_reference_2 No external references.

location_map_rio No external references.

location_map_update_reference_1 No external references.

location_map_update_reference_2 No external references.

permission_map DerivedTyping. Focus. InversionClassification. ReferenceAccess. Typing.

permission_map_allocate_group No external references.

permission_map_allocate_singleton No external references.

permission_map_extend_group No external references.

reference_resource No external references.

reflimit InversionClassification. LittleFacts. Typing.

reflimit_allocate_reference_1 No external references.

reflimit_allocate_reference_2 No external references.

reflimit_neutral No external references.

reflimit_reflimit_neutral No external references.

reflimit_rio No external references.

reflimit_update_reference_1 No external references.

reflimit_update_reference_2 No external references.

region_map DerivedTyping. Focus. InversionClassification. LittleFacts. RegionAllocation. Typing.

region_map_allocate_singleton No external references.

region_map_allocate_singleton_uniqueness No external references.

region_map_extend_group_1 No external references.

region_map_extend_group_2 No external references.

region_map_extend_group_reverse RegionAllocation.

region_map_fictitious No external references.

region_map_neutral SubjectReduction.

region_map_neutral_1 No external references.

region_map_neutral_2 No external references.

region_map_rio No external references.

region_map_rio_reverse SubjectReduction.

region_resource No external references.

reglimit DerivedTyping. InversionClassification. RegionAllocation. Typing.

reglimit_allocate_group No external references.

reglimit_allocate_singleton No external references.

reglimit_extend_group No external references.

reglimit_fictitious No external references.

reglimit_neutral No external references.

reglimit_neutral_simplify No external references.

reglimit_rio No external references.

resource DerivedTyping. Focus. LittleFacts. Progress. ProgressValues. RegionAccess. RegionAllocation. ResourcesReconfiguration. SubjectReduction. SubjectReductionValues. TermSubstitution. Typing.

rio_allocate_reference_unowned No external references.

rio_allocate_singleton No external references.

rio_extend_group No external references.

rio_owned_region ReferenceAccess.

rxo_allocate_group No external references.

rxo_allocate_reference No external references.

rxo_allocate_singleton No external references.

rxo_extend_group No external references.

rxo_star_symmetric No external references.

star_allocate_reference_1 No external references.

star_allocate_reference_2 No external references.

star_allocate_singleton No external references.

star_extend_group RegionAllocation.

star_owned_exclusive No external references.

star_owned_exclusive_locations No external references.

star_owned_exclusive_locations_symmetric No external references.

star_owned_left No external references.

star_owned_left_locations No external references.

star_owned_right_locations No external references.

star_update_reference No external references.

star_update_reference_preliminary No external references.

update_reference ReferenceAccess.

Leaf Focus. Progress. ReferenceAccess. RegionAllocation. SubjectReduction.

LeafLeaf No references.

LeafNodeLeft No references.

LeafNodeRight No references.

Node Focus. Progress. ReferenceAccess. RegionAllocation. SubjectReduction.

ValidLeaf No references.

ValidNode No references.

ac_fold_permutation No external references.

ac_fold_permutation_nonempty No external references.

compatible No external references.

compatible_commutative No external references.

compatible_star_add No external references.

compatible_trees_leaves No external references.

compatible_trees_via_sons_left No external references.

compatible_trees_via_sons_right No external references.

compatible_via_ancestor No external references.

compatible_via_ancestors No external references.

compatible_via_father_left No external references.

compatible_via_father_right No external references.

compatible_via_sons_left No external references.

compatible_via_sons_right No external references.

equivalence_1 No external references.

equivalence_2 No external references.

fringe No external references.

fringe_permutation No external references.

interpret No external references.

interpret_fringe No external references.

interpret_fringe_correct No external references.

interpret_is_up_to_permutation No external references.

interpret_tree No external references.

leaf No external references.

leaves_determine_root No external references.

permut_append No external references.

permutation_cons_nil No external references.

permute_left No external references.

reconfiguration No external references.

rotate_left No external references.

rotate_right No external references.

star_compatible No external references.

tree No external references.

tree_predicate No external references.

valid_inversion_left No external references.

valid_inversion_right No external references.

valid_node No external references.

valid_tree No external references.

valid_trees_have_compatible_leaves No external references.

JCoComposExchangeUnder_nil No external references.

JCoCompos_nil No external references.

JCoComposs_nil SubjectReduction.

JCoMixPairCompossExchange SubjectReduction.

cenv_tensor No external references.

cenv_tensor_def No external references.

ct_tensor No external references.

ct_tensor_def No references.

fill_tensor No external references.

fill_tensor_flexible No external references.

fill_tensor_invariant No external references.

fold_revelation_values_nil SubjectReduction.

lift_cenv_tensor No external references.

lift_ct_tensor No external references.

lift_pair No external references.

lift_path_tensor No external references.

lift_tensor No external references.

path_tensor No external references.

revelation_path No external references.

revelation_primitive No external references.

revelation_subtyping No external references.

revelation_subtyping_nil No external references.

revelation_terms No references.

revelation_typing No external references.

revelation_values No external references.

revelation_values_nil SubjectReduction.

use_the_new_variable No external references.

wf_path_tensor No external references.

CoMixPairCompossExchange ErasureSimulation. Revelation. Semantics. WellLayeredness.

closed_reveal Revelation.

erase_CoMixPairCompossExchange ErasureSimulation.

erase_reveal No external references.

erase_reveal_term No references.

erase_reveal_value ErasureSimulation. Revelation.

fold_erase_reveal ErasureSimulation.

fold_reveal_value Revelation. Semantics. WellLayeredness.

lift_reveal No external references.

reveal_term Revelation. WellLayeredness.

reveal_value Revelation. Semantics. WellLayeredness.

reveal_values Revelation. WellLayeredness.

well_scoped_reveal No external references.

EAppRight No external references.

ECoApp No external references.

EMixPairLeft No external references.

RedAdopt No references.

RedAppContextLeft No references.

RedBeta No references.

RedCoApp No references.

RedContext No external references.

RedContextEAppRight No external references.

RedContextECoApp No external references.

RedContextEMixPairLeft No external references.

RedDefocusDuplicable No references.

RedFocus No references.

RedFocusGroup No references.

RedLetBang No references.

RedLetPair No references.

RedMixPair No references.

RedNewAffine No references.

RedNewCap No references.

RedNewGroup No references.

RedReadAffine No references.

RedReadCap No references.

RedTHide No references.

RedTLetBangContext No references.

RedTLetPairContext No references.

RedTLetUnpackContext No references.

RedTPrimAppContext No references.

RedTTyAbsContext No references.

RedTyAbs No references.

RedUnpack No references.

RedVal No references.

RedWriteAffine No references.

RedWriteCap No references.

RedstarRefl No references.

RedstarStep No references.

RedstarTrans No references.

ectx No external references.

efill SubjectReduction.

red ErasureSimulation. Progress. SubjectReduction. TypeErasure. WellLayeredness.

redstar TypeErasure.

reveal_ectx SubjectReduction.

RedCoArrow No references.

RedCoAtBang No references.

RedCoBang No references.

RedCoBangExists No references.

RedCoBangIdempotent No references.

RedCoBangPair No references.

RedCoDefocus No references.

RedCoDefocusGroup No references.

RedCoDereliction No references.

RedCoDistrib No references.

RedCoExists No references.

RedCoExistsElim No references.

RedCoExistsIntro No references.

RedCoExistsLeftIntro No references.

RedCoForall No references.

RedCoForallBang No references.

RedCoForallElim No references.

RedCoForallIntro No references.

RedCoForallPair No references.

RedCoForallRef No references.

RedCoForallRegionCap No references.

RedCoForallRegionCapPunched No references.

RedCoId No references.

RedCoMu No references.

RedCoPair No references.

RedCoPairBang No references.

RedCoPairExistsLeft No references.

RedCoPairExistsRight No references.

RedCoRef No references.

RedCoRefExists No references.

RedCoRefStar No references.

RedCoRegionCap No references.

RedCoRegionCapPunched No references.

RedCoSeq No references.

RedCoSingletonRegionCapExists No references.

RedCoSingletonStar No references.

RedCoSingletonToGroup No references.

RedCoStarAssociative No references.

RedCoStarCommutative No references.

RedCoStarRef No references.

RedCoStarSingleton No references.

RedCoTensorExchangeVAbs No references.

RedCoTensorExchangeVBang No references.

RedCoTensorExchangeVInhabitant No references.

RedCoTensorExchangeVLoc No references.

RedCoTensorExchangeVPack No references.

RedCoTensorExchangeVPair No references.

RedCoTensorExchangeVRegionCap No references.

RedCoTensorExchangeVRegionCapPunched No references.

RedCoTensorExchangeVTyAbs No references.

RedCoTensorExchangeVUnit No references.

RedCoUnitBang No references.

RedPairContextLeft No references.

RedPairContextRight No references.

RedVBangContext No references.

RedVCoAppContext No references.

RedVLocContext No references.

RedVPackContext No references.

RedVRegionCapContext No references.

RedVRegionCapPunchedContext No references.

RedVTyAbsContext No references.

RedvsHere No references.

RedvsThere No references.

VCoApps ValueReductionTerminates.

VTyAbss ValueReductionTerminates.

redv CanonicalValuesDoNotReduce. ErasureSimulation. ErasureSimulationValues. ProgressValues. Semantics. SubjectReduction. SubjectReductionValues. ValueReductionTerminates. WellLayeredness.

redv_redvs_ind ValueReductionTerminates. WellLayeredness.

redvs CanonicalValuesDoNotReduce. ErasureSimulationValues. ProgressValues. SubjectReductionValues. ValueReductionTerminates. WellLayeredness.

Everywhere No references.

Store Erasure. LittleFacts. RawSemantics. ReferenceAccess. ReferenceAllocation. Semantics.

everywhere WellLayeredness.

everywhere_extend WellLayeredness.

everywhere_read No references.

everywhere_write WellLayeredness.

extend RawSemantics. ReferenceAccess. ReferenceAllocation. Semantics.

gstore Programs. RawPrograms.

location Programs. RawPrograms. ResourcesContinued.

patch No external references.

patch_extensional No references.

patch_extensional_new No references.

transform Erasure. LittleFacts.

transform_extend ErasureSimulation. ReferenceAccess. ReferenceAllocation.

transform_extensional No external references.

transform_none No external references.

transform_some No external references.

evaluation_contexts No external references.

subject_reduction No external references.

subject_reduction_configurations TypeErasure.

subject_reduction_value SubjectReduction.

subject_reduction_value_preliminary No external references.

JCoArrow No references.

JCoAtBang No references.

JCoBang No references.

JCoBangExists No references.

JCoBangIdempotent No references.

JCoBangPair No references.

JCoBangRef No references.

JCoBangRegionCap No references.

JCoBangRegionCapPunched No references.

JCoDefocus DerivedTyping.

JCoDefocusGroup No references.

JCoDereliction No references.

JCoDistrib No references.

JCoExists No references.

JCoExistsElim DerivedSubtyping.

JCoExistsIntro No references.

JCoExistsLeftIntro No references.

JCoForall No references.

JCoForallBang No references.

JCoForallElim No references.

JCoForallIntro No references.

JCoForallPair DerivedSubtyping.

JCoForallRef No references.

JCoForallRegionCap No references.

JCoForallRegionCapPunched No references.

JCoId No references.

JCoMu No references.

JCoPair No references.

JCoPairBang No references.

JCoPairExistsLeft Revelation.

JCoPairExistsRight No references.

JCoRef No references.

JCoRefExists No references.

JCoRefStar No references.

JCoRegionCap No references.

JCoRegionCapPunched No references.

JCoSeq No references.

JCoSingletonRegionCapExists No references.

JCoSingletonStar No references.

JCoSingletonToGroup No references.

JCoStarAssociative DerivedSubtyping.

JCoStarCommutative No references.

JCoStarRef No references.

JCoStarSingleton No references.

JCoTensorExchange Revelation.

JCoTensorExchangeZero DerivedSubtyping.

JCoUnitBang No references.

JCoVar No references.

jco AdmissibleSubtyping. CoercionSubstitution. DerivedSubtyping. DerivedTyping. Intuitionistic. LittleFacts. PreliminaryLemmas. ProgressValues. Revelation. SubjectReductionValues. TypeSubstitution. Typing.

j_term_substitution_infinity_0 SubjectReduction.

j_term_substitution_one_0 SubjectReduction.

j_term_substitution_one_1 Revelation.

j_term_substitution_one_1_rebind SubjectReductionValues.

j_term_substitution_zero No external references.

j_term_substitution_zero_0 No references.

j_value_substitution_infinity_0 No references.

j_value_substitution_zero No external references.

j_value_term_substitution_infinity No external references.

j_value_term_substitution_infinity_backward No external references.

j_value_term_substitution_one No external references.

j_value_term_substitution_one_backward SubjectReductionValues.

j_value_term_substitution_zero No external references.

constant FocusPaths. Revelation. WeakRefWithAffineContent.

fill Focus. FocusPaths. Revelation. Subtyping. Typing. WeakRefWithAffineContent.

fill_constant No references.

fill_hole SubjectReduction.

fill_pair_1 No external references.

fill_pair_2 No external references.

fill_ref No external references.

fill_tyregioncap_2 No external references.

hole FocusPaths. Revelation. WeakRefWithAffineContent.

lift_fill PreliminaryLemmas.

lift_hole No references.

lift_lift_ty_ctx PreliminaryLemmas.

lift_subst_1_ty_ctx TypeSubstitution.

lift_ty_ctx Focus. FocusPaths. Revelation. Typing. WeakRefWithAffineContent.

subst_fill TypeSubstitution.

subst_fill_lift Focus.

subst_ty_ctx FocusPaths.

tensor_constant Revelation.

ty_ctx FocusPaths. Revelation.

wf_constant No external references.

wf_fill Focus.

wf_fill_inverse No references.

wf_lift_ty_ctx Focus.

ContractiveTyArrow No references.

ContractiveTyAt No references.

ContractiveTyBang No references.

ContractiveTyMu No references.

ContractiveTyPair No references.

ContractiveTyQ No references.

ContractiveTyRef No references.

ContractiveTyRegion No references.

ContractiveTyRegionCap No references.

ContractiveTyRegionCapPunched No references.

ContractiveTyTensor No references.

ContractiveTyUnit No references.

ContractiveTyVar No references.

FiniteTyArrow No references.

FiniteTyAt No references.

FiniteTyBang No references.

FiniteTyPair No references.

FiniteTyQ No references.

FiniteTyRef No references.

FiniteTyRegion No references.

FiniteTyRegionCap No references.

FiniteTyRegionCapPunched No references.

FiniteTyTensor No references.

FiniteTyUnit No references.

FiniteTyVar No references.

FtoArrow1 No references.

FtoArrow2 No references.

FtoAt No references.

FtoBang No references.

FtoPair1 No references.

FtoPair2 No references.

FtoQ No references.

FtoRed No references.

FtoRef No references.

FtoRegionCap1 No references.

FtoRegionCap2 No references.

FtoRegionCapPunched1 No references.

FtoRegionCapPunched2 No references.

FtoRegionCapPunched3 No references.

FtoTensor1 No references.

FtoTensor2 No references.

TtoArrow1 No references.

TtoArrow2 No references.

TtoAt No references.

TtoBang No references.

TtoPair1 No references.

TtoPair2 No references.

TtoQ No references.

TtoRed No references.

TtoRef No references.

TtoRegionCap1 No references.

TtoRegionCap2 No references.

TtoRegionCapPunched1 No references.

TtoRegionCapPunched2 No references.

TtoRegionCapPunched3 No references.

TtoTensor1 No references.

TtoTensor2 No references.

TyApproxEqArrow No references.

TyApproxEqAt No references.

TyApproxEqBang No references.

TyApproxEqPair No references.

TyApproxEqQ No references.

TyApproxEqRedLeft No references.

TyApproxEqRedRight No external references.

TyApproxEqRef No references.

TyApproxEqRegion No references.

TyApproxEqRegionCap No references.

TyApproxEqRegionCapPunched No references.

TyApproxEqTensor No references.

TyApproxEqUnit No references.

TyApproxEqVar No references.

TyApproxEqZero No references.

TyRedMu No references.

TyRedMuCContext No references.

TyRedMuCInject No references.

TyRedMuInject No references.

TyRedStarCons No references.

TyRedStarNil No references.

TyRedTensorArrow No references.

TyRedTensorAt No references.

TyRedTensorBang No references.

TyRedTensorContext No references.

TyRedTensorPair No references.

TyRedTensorQ No references.

TyRedTensorRef No references.

TyRedTensorRegionCap No references.

TyRedTensorRegionCapPunched No references.

TyRedTensorUnit No references.

WfTyArrow No references.

WfTyAt No references.

WfTyBang No references.

WfTyMu No references.

WfTyPair No references.

WfTyQ No references.

WfTyRef No references.

WfTyRegion No references.

WfTyRegionCap No references.

WfTyRegionCapPunched No references.

WfTyTensor No references.

WfTyUnit No references.

WfTyVar No references.

WfsCons No references.

WfsNil No references.

acc_tto_zero No external references.

acc_tyredmuc_subst No external references.

acc_tyredmuc_tensor No external references.

contractive No external references.

contractive_lift_1 No external references.

contractive_lift_2 No external references.

contractive_lift_3 MoreTypeEquality.

contractive_lift_inverse No external references.

contractive_subst_1 No external references.

contractive_subst_2 No external references.

contractive_subst_inverse No external references.

contractive_type_equations_have_solution_mu MoreTypeEquality.

contractive_type_equations_have_unique_solutions No external references.

contractive_tyred No external references.

contractive_tyredmu No external references.

contractive_unfold No external references.

finite No external references.

finite_lift No external references.

finite_subst No external references.

frozen No external references.

frozen_lift No external references.

frozen_subst No external references.

fto No external references.

fto2lpo No external references.

fto_finite No external references.

fto_lpo No external references.

fto_well_founded No external references.

lift_ty_injective_tyapproxeq No external references.

lift_ty_injective_tyeq No external references.

skeleton No external references.

skeleton_lift No external references.

tensor_subst ProveTypeEquality.

tto MoreTypeEquality.

tto2fto No external references.

tto_well_founded MoreTypeEquality.

tto_wf No external references.

two_regions No external references.

tyapproxeq DecidableTypeEquality.

tyapproxeq_mu No external references.

tyapproxeq_redstar_right No external references.

tyapproxeq_reflexive No external references.

tyapproxeq_symmetric No external references.

tyapproxeq_transitive No external references.

tyapproxeq_tyred No external references.

tyapproxeq_unfold No external references.

tyapproxeqrr No external references.

tyapproxeqrr_decreases No external references.

tyapproxeqrr_lift No external references.

tyapproxeqrr_subst No external references.

tyapproxeqrr_subst_contractive No external references.

tyeq DecidableTypeEquality. DerivedSubtyping. DerivedTyping. Environments. InversionClassification. MoreTypeEquality. PreliminaryLemmas. ProveTypeEquality. RegionAllocation. Revelation. Sigma. SubjectReduction. Subtyping. Typing. WeakRefWithAffineContent.

tyeq_arrow ProveTypeEquality.

tyeq_at InversionClassification. ProveTypeEquality. Sigma.

tyeq_bang ProveTypeEquality.

tyeq_decompose_arrow No external references.

tyeq_decompose_at No external references.

tyeq_decompose_bang No external references.

tyeq_decompose_pair No external references.

tyeq_decompose_q No external references.

tyeq_decompose_ref No external references.

tyeq_decompose_region No external references.

tyeq_decompose_regioncap No external references.

tyeq_decompose_regioncappunched No external references.

tyeq_decompose_unit No external references.

tyeq_decompose_var No external references.

tyeq_fold AdmissibleSubtyping. WeakRefWithAffineContent.

tyeq_impossible_example No references.

tyeq_lift Environments. MoreTypeEquality. PreliminaryLemmas.

tyeq_mu No references.

tyeq_mu_mu No external references.

tyeq_pair DerivedSubtyping. MoreTypeEquality. ProveTypeEquality. Revelation. WeakRefWithAffineContent.

tyeq_q ProveTypeEquality. Revelation.

tyeq_ref ProveTypeEquality.

tyeq_reflexive DerivedSubtyping. MoreTypeEquality. PreliminaryLemmas. ProveTypeEquality. Revelation. SubjectReductionValues. WeakRefWithAffineContent.

tyeq_region ProveTypeEquality.

tyeq_region_lift No external references.

tyeq_regioncap ProveTypeEquality. Sigma. SubjectReductionValues. WeakRefWithAffineContent.

tyeq_regioncappunched ProveTypeEquality. Sigma. SubjectReductionValues.

tyeq_subst Environments. InversionClassification. MoreTypeEquality. Revelation.

tyeq_symmetric DerivedSubtyping. InversionClassification. MoreTypeEquality. ProveTypeEquality. Revelation. Sigma. SubjectReductionValues. Typing. WeakRefWithAffineContent.

tyeq_tensor Environments. MoreTypeEquality. ProveTypeEquality. Revelation.

tyeq_tensor_arrow ProveTypeEquality.

tyeq_tensor_at ProveTypeEquality.

tyeq_tensor_bang ProveTypeEquality.

tyeq_tensor_pair DerivedSubtyping. MoreTypeEquality. ProveTypeEquality.

tyeq_tensor_q ProveTypeEquality.

tyeq_tensor_ref ProveTypeEquality. WeakRefWithAffineContent.

tyeq_tensor_regioncap ProveTypeEquality. WeakRefWithAffineContent.

tyeq_tensor_regioncappunched ProveTypeEquality.

tyeq_tensor_unit ProveTypeEquality.

tyeq_transitive InversionClassification. MoreTypeEquality. ProveTypeEquality. Revelation. WeakRefWithAffineContent.

tyeq_unfold MoreTypeEquality.

tyeq_unfold_unfold No external references.

tyeq_var ProveTypeEquality.

tyred MoreTypeEquality.

tyred_deterministic No external references.

tyred_finite No external references.

tyred_lift No external references.

tyred_lift_inverse No external references.

tyred_lpo No external references.

tyred_reveals_arrow No external references.

tyred_reveals_at No external references.

tyred_reveals_bang No external references.

tyred_reveals_pair No external references.

tyred_reveals_q No external references.

tyred_reveals_ref No external references.

tyred_reveals_regioncap No external references.

tyred_reveals_regioncappunched No external references.

tyred_reveals_unit No external references.

tyred_subst No external references.

tyred_tensor No external references.

tyred_tyeq No external references.

tyred_unfolding No external references.

tyred_wf No external references.

tyredmu MoreTypeEquality.

tyredmu_finite No external references.

tyredmu_lift No external references.

tyredmu_lift_inverse No external references.

tyredmu_subst No external references.

tyredmuc No external references.

tyredmuc_subst No external references.

tyredmuc_well_founded No external references.

tyredstar No external references.

tyredstar_tensor_context No external references.

unfold No external references.

unfold_lift No external references.

unfold_subst No external references.

unfold_subst_mu No references.

unfolding No external references.

unfolding_exists No external references.

unfolding_tyredmuc No external references.

wf AdmissibleSubtyping. DerivedSubtyping. DerivedTyping. Environments. FocusPaths. Intuitionistic. InversionClassification. MoreTypeEquality. PreliminaryLemmas. ProveTypeEquality. RegionAllocation. Revelation. Subtyping. TypeContexts. TypeSubstitution. Typing. WeakRefWithAffineContent.

wf_lift AdmissibleSubtyping. Focus.

wf_lift_inverse PreliminaryLemmas.

wf_subst DerivedSubtyping.

wf_subst_inverse TypeContexts.

wf_unfold MoreTypeEquality. WeakRefWithAffineContent.

wfs MoreTypeEquality. Revelation. SubjectReduction. Subtyping. Typing.

wfs_app No external references.

wfs_append_invert No references.

wfs_map SubjectReductionValues.

WellTypedCons No references.

erasure_reverse_simulation No external references.

erasure_value_reduces_value No references.

erasure_value_stutter No external references.

raw_progress No external references.

raw_progress_preliminary No external references.

raw_subject_reduction No external references.

type_soundness No references.

type_soundness_preliminary No external references.

well_typed No external references.

j_term_type_substitution_unpack SubjectReduction.

j_type_substitution No external references.

j_type_substitution_0 SubjectReductionValues.

j_type_substitution_0_term No references.

jco_type_substitution AdmissibleSubtyping.

jco_type_substitution_nil_arrow SubjectReductionValues.

jp_type_substitution No external references.

Group Focus. RegionAllocation. Subtyping. Typing.

QExists InversionClassification.

QForall InversionClassification.

Singleton DerivedTyping. Focus. FocusPaths. InversionClassification. LittleFacts. ReferenceAccess. RegionAllocation. Revelation. Subtyping. Typing. WeakRefWithAffineContent.

TyArrow DerivedSubtyping. Intuitionistic. InversionClassification. MoreTypeEquality. Subtyping. TypeEquality. Typing. WeakRefWithAffineContent.

TyAt DerivedTyping. Focus. InversionClassification. LittleFacts. MoreTypeEquality. ReferenceAccess. RegionAllocation. Sigma. Subtyping. TermSubstitution. TypeEquality. Typing. WeakRefWithAffineContent.

TyBang DerivedSubtyping. Focus. Intuitionistic. InversionClassification. MoreTypeEquality. Subtyping. TypeEquality. Typing. WeakRefWithAffineContent.

TyCompos DerivedSubtyping. MoreTypeEquality. Revelation. SubjectReduction. TypeEquality. Typing.

TyExists DerivedSubtyping. DerivedTyping. Focus. InversionClassification. Subtyping. Typing. WeakRefWithAffineContent.

TyForall DerivedSubtyping. InversionClassification. LittleFacts. SubjectReductionValues. Subtyping. Typing. WeakRefWithAffineContent.

TyLogPair Focus. Subtyping. Typing.

TyLogUnit No references.

TyMixPair DerivedSubtyping. DerivedTyping. Focus. MoreTypeEquality. ReferenceAccess. Revelation. Subtyping. Typing. WeakRefWithAffineContent.

TyMu AdmissibleSubtyping. MoreTypeEquality. TypeEquality. WeakRefWithAffineContent.

TyPair DerivedSubtyping. DerivedTyping. FocusPaths. InversionClassification. MoreTypeEquality. Revelation. Subtyping. TypeContexts. TypeEquality. Typing.

TyPhyPair ReferenceAccess. Typing.

TyPhyUnit DerivedSubtyping. ReferenceAccess. TypeEquality. Typing.

TyQ MoreTypeEquality. TypeEquality.

TyRef DerivedSubtyping. FocusPaths. InversionClassification. MoreTypeEquality. ReferenceAccess. ReferenceAllocation. Revelation. Subtyping. TypeContexts. TypeEquality. Typing. WeakRefWithAffineContent.

TyRegion DerivedTyping. Focus. InversionClassification. LittleFacts. MoreTypeEquality. RegionAllocation. Sigma. SubjectReduction. TypeEquality. Typing.

TyRegionCap DerivedSubtyping. DerivedTyping. Focus. FocusPaths. InversionClassification. MoreTypeEquality. ReferenceAccess. RegionAllocation. Revelation. Sigma. Subtyping. TypeContexts. TypeEquality. Typing. WeakRefWithAffineContent.

TyRegionCapPunched DerivedSubtyping. Focus. InversionClassification. MoreTypeEquality. Sigma. Subtyping. TypeEquality. Typing.

TyTensor DecidableTypeEquality. DerivedSubtyping. Environments. MoreTypeEquality. ProveTypeEquality. Revelation. Subtyping. TypeContexts. TypeEquality. Typing. WeakRefWithAffineContent.

TyUnit InversionClassification. MoreTypeEquality. Subtyping. TypeEquality. Typing.

TyVar AdmissibleSubtyping. DerivedSubtyping. DerivedTyping. Focus. MoreResources. MoreTypeEquality. TypeContexts. TypeEquality. Typing. WeakRefWithAffineContent.

lift_lift_ty DerivedSubtyping. Environments. FocusPaths. PreliminaryLemmas. Revelation. TypeContexts. TypeEquality. WeakRefWithAffineContent.

lift_subst_1_ty DerivedSubtyping. Environments. FocusPaths. TypeContexts. TypeEquality. TypeSubstitution.

lift_subst_2_ty AdmissibleSubtyping. PreliminaryLemmas. TypeContexts. TypeEquality.

lift_ty AdmissibleSubtyping. DerivedSubtyping. DerivedTyping. Environments. Focus. MoreTypeEquality. PreliminaryLemmas. Revelation. SubjectReductionValues. Subtyping. TypeContexts. TypeEquality. TypeSubstitution. Typing. WeakRefWithAffineContent.

lift_ty_injective No references.

lift_zero_lift_ty No references.

pun_1_ty No external references.

pun_1_ty_explicit No references.

pun_2_ty DerivedSubtyping.

pun_2_ty_explicit No references.

quantifier MoreTypeEquality.

region ResourcesContinued.

region_kind MoreTypeEquality.

rotate_ty DerivedSubtyping.

rotate_ty_1_self_inverse DerivedSubtyping.

subst_lift_ty AdmissibleSubtyping. DerivedSubtyping. Environments. Focus. MoreTypeEquality. Revelation. SubjectReduction. SubjectReductionValues. TypeContexts. TypeEquality. TypeSubstitution. WeakRefWithAffineContent.

subst_subst_ty TypeContexts. TypeEquality. TypeSubstitution.

subst_ty DerivedSubtyping. DerivedTyping. Environments. InversionClassification. MoreTypeEquality. SubjectReductionValues. Subtyping. TypeContexts. TypeEquality. TypeSubstitution. Typing.

ty DerivedSubtyping. Environments. MoreResources. MoreTypeEquality. Revelation. SubjectReduction. Subtyping. TypeContexts. TypeEquality. TypeErasure. Typing.

JConfCons No references.

JICons No references.

JINil No references.

JPAdopt No references.

JPDefocusDuplicable No references.

JPFocus DerivedTyping.

JPFocusGroup No references.

JPNewAffine No references.

JPNewCap No references.

JPNewGroup No references.

JPReadAffine No references.

JPReadCap No references.

JPWriteAffine No references.

JPWriteCap No references.

JTApp No references.

JTCoApp No references.

JTEq InversionClassification. Revelation.

JTHide Revelation.

JTLetBang No references.

JTLetPair No references.

JTLetUnpack SubjectReductionValues.

JTMixPair No references.

JTPrimApp No references.

JTTyAbs No references.

JTVal No references.

JVAbs No references.

JVAtRegion No references.

JVBang No references.

JVCoApp No references.

JVEq Revelation. Sigma. SubjectReduction. SubjectReductionValues. WeakRefWithAffineContent.

JVLoc No references.

JVPack Focus. SubjectReduction.

JVPair No references.

JVRegionCap RegionAllocation.

JVRegionCapPunched SubjectReduction.

JVTyAbs No references.

JVUnit No references.

JVVar No references.

jconf Progress. SubjectReduction. TypeErasure.

ji Closed. DerivedTyping. Focus. InversionClassification. LittleFacts. Monotonicity. PreliminaryLemmas. ProgressValues. RegionAccess. Revelation. SubjectReductionValues. TermSubstitution. TypeSubstitution.

jp DerivedTyping. InversionClassification. PreliminaryLemmas. Revelation. TypeSubstitution. WeakRefWithAffineContent.

jsto LittleFacts. Progress. ReferenceAccess. ReferenceAllocation. SubjectReduction.

jt Closed. DerivedTyping. Intuitionistic. InversionClassification. Monotonicity. PreliminaryLemmas. Progress. ProgressValues. ReferenceAccess. ReferenceAllocation. Revelation. SubjectReduction. SubjectReductionValues. TermSubstitution. TypeSubstitution. WeakRefWithAffineContent.

jv Closed. DerivedTyping. DupCapZeroWeight. Focus. Intuitionistic. InversionClassification. LittleFacts. Monotonicity. PreliminaryLemmas. Progress. ProgressValues. ReferenceAccess. ReferenceAllocation. RegionAccess. RegionAllocation. Revelation. Sigma. SubjectReduction. SubjectReductionValues. TermSubstitution. TypeSubstitution. WeakRefWithAffineContent.

jvit_ind Closed. Monotonicity. PreliminaryLemmas. ProgressValues. Revelation. SubjectReductionValues. TermSubstitution. TypeSubstitution.

count DerivedTyping. Erasure. InversionClassification. LittleFacts. Typing. ValueReductionTerminates.

head_member No external references.

member Canonical. DerivedTyping. Focus. InversionClassification. LittleFacts. RegionAccess. Semantics. Typing. ValueReductionTerminates. WellLayeredness.

member_cons_elim No references.

member_further Focus.

member_singleton RegionAllocation.

member_some No external references.

member_tail No external references.

remove Focus. Semantics. WellLayeredness.

remove_cases Focus.

reordering_1 SubjectReduction.

reordering_2 SubjectReduction.

singleton_list No external references.

singleton_some RegionAllocation.

some DerivedTyping. Erasure. InversionClassification. LittleFacts. RegionAllocation. SubjectReduction. Typing.

some_member InversionClassification.

some_remove No external references.

some_singleton Focus. InversionClassification.

vmap Erasure. LittleFacts. SemanticsValues. ValueReductionTerminates. WellLayeredness.

RedvtAppContextLeft No references.

RedvtAppContextRight No references.

RedvtMixPairContextLeft No references.

RedvtTCoAppContext No references.

RedvtTLetBangContext No references.

RedvtTLetPairContext No references.

RedvtTLetUnpackContext No references.

RedvtTPrimAppContext No references.

RedvtTTyAbsContext No references.

RedvtVal No references.

canonical_values_have_empty_descs No external references.

collect_descs No external references.

collect_descs_vcoapps No external references.

collect_descs_vmap No external references.

desc No external references.

descs No external references.

fold_desc No external references.

in_collect_descs_vcoapps No external references.

in_fold_desc No external references.

member_weight No references.

okCoBang No external references.

okCoDefocus No external references.

okCoExists No external references.

okCoForall No external references.

okCoForallRegionCap No external references.

okCoForallRegionCapPunched No external references.

okCoMu No external references.

okCoPair No external references.

okCoRef No external references.

okCoRegionCap No external references.

okCoRegionCapPunched No external references.

okCoSeq No external references.

okLeafCoercion No external references.

okRedCoTensorExchangeVRegionCap No external references.

plug_preserves_descs No external references.

plug_preserves_weight No external references.

poly No external references.

polys No external references.

polys_vcoapps No external references.

redv_preserves_desc No external references.

redv_preserves_weight No external references.

redv_redvo No external references.

redv_wf No external references.

redvo No external references.

redvso No external references.

redvt ErasureSimulation.

redvt_TApp No external references.

redvt_TCoApp No external references.

redvt_THide No external references.

redvt_TLetBang No external references.

redvt_TLetPair No external references.

redvt_TLetUnpack No external references.

redvt_TMixPair No external references.

redvt_TPrimApp No external references.

redvt_TTyAbs No external references.

redvt_TVal No external references.

redvt_wf ErasureSimulation.

sum_weight No external references.

sum_weight_vmap No external references.

vo No external references.

weight DupCapZeroWeight.

equation1 No external references.

equation2 No external references.

focus_pair_cap_ref No external references.

invariant No external references.

mkwref No external references.

mkwref_well_layered No references.

mkwref_well_typed No references.

pair_cap_ref No external references.

swap No external references.

swap_well_typed No external references.

well_founded_inclusion MyMultisets.

WlConf No references.

WlPAdopt No references.

WlPDefocusDuplicable No references.

WlPFocus No references.

WlPFocusGroup No references.

WlPNewAffine No references.

WlPNewCap No references.

WlPNewGroup No references.

WlPReadAffine No references.

WlPReadCap No references.

WlPWriteAffine No references.

WlPWriteCap No references.

WlPathPairLeft No references.

WlPathPairRight No references.

WlPathRef No references.

WlPathRegionCapSingleton No references.

WlPathRoot No references.

WlTApp No references.

WlTCoApp No references.

WlTLetBang No references.

WlTLetPair No references.

WlTLetUnpack No references.

WlTMixPair No references.

WlTPrimApp No references.

WlTTyAbs No references.

WlTVal No references.

WlVAbs No references.

WlVBang No references.

WlVCoApp No references.

WlVInhabitant No references.

WlVLoc No references.

WlVPack No references.

WlVPair No references.

WlVRegionCap No references.

WlVRegionCapPunched No references.

WlVTyAbs No references.

WlVUnit No references.

WlVVar No references.

WlVsCons No references.

WlVsNil No references.

WltTHide No references.

erase_logical_value No external references.

wl_CoMixPairCompossExchange No external references.

wl_env_inclusion No external references.

wl_fold_reveal No external references.

wl_lift No external references.

wl_preserved No external references.

wl_reveal No external references.

wl_subst No external references.

wlconf ErasureSimulation. TypeErasure.

wlconf_preserved TypeErasure.

wlpath No external references.

wlprim No external references.

wls ErasureSimulation.

wlt ErasureSimulation.

wlt_lift_zero No external references.

wlt_subst_one No external references.

wlt_subst_zero No external references.

wlv DupCapZeroWeight. WeakRefWithAffineContent.

wlv_lift_zero No external references.

wlv_nil No external references.

wlv_plug No external references.

wlv_preserved No external references.

wlv_preserved_preliminary No external references.

wlv_select No external references.

wlv_select_plug No external references.

wlv_subst_zero No external references.

wlvs No external references.

wlvs_member No external references.

wlvs_remove No external references.

wlvs_vmap No external references.

wlvt_ind No external references.

AdmissibleSubtyping

AntiFrameSwitch

Arithmetic

Canonical

CanonicalValuesDoNotReduce

Closed

CoercionMeasure

CoercionSubstitution

Coercions

DeBruijn

DecidableTypeEquality

DerivedSubtyping

DerivedTyping

DupCapZeroWeight

Environments

Erasure

ErasureSimulation

ErasureSimulationValues

Focus

FocusPaths

Intuitionistic

InversionClassification

Layers

Lexicographic

LibTactics

LittleFacts

Monotonicity

MoreResources

MoreTypeEquality

Multiplicity

MultiplicityEnvironments

MyClassicalChoice

MyLPO

MyMultisets

MyTactics

PathSemantics

PreliminaryLemmas

Programs

Progress

ProgressValues

PropositionalExtensionality

RawPrograms

RawSemantics

ReferenceAccess

ReferenceAllocation

RegionAccess

RegionAllocation

Resources

ResourcesContinued

ResourcesReconfiguration

Revelation

RevelationDefinition

Semantics

SemanticsValues

Store

SubjectReduction

SubjectReductionValues

Subtyping

TermSubstitution

TypeContexts

TypeEquality

TypeErasure

TypeSubstitution

Types

Typing

ValueLists

ValueReductionTerminates

WeakRefWithAffineContent

WellFoundedInclusion

WellLayeredness