Relation

📁 Source: Cslib/Foundations/Data/Relation.lean

Statistics

Metric	Count
Definitions `ChurchRosser`, `Commute`, `Confluent`, `Convergent`, `Diamond`, `DiamondCommute`, `LocallyConfluent`, `MJoin`, `Normal`, `Normalizable`, `Normalizing`, `Reducible`, `SemiConfluent`, `StronglyCommute`, `StronglyConfluent`, `Terminating`, `UpTo`, `command_Reduction_notation__`, `reduction_sys`, `trans_of_subrelation`, `trans_of_subrelation_left`, `trans_of_subrelation_right`	22
Theorems `normal_eq`, `normal_eqvGen_reflTransGen`, `join_confluent`, `join_left`, `symmetric`, `toConfluent`, `equivalence_join_reflTransGen`, `toChurchRosser`, `toLocallyConfluent`, `Confluent_iff_ChurchRosser`, `Confluent_iff_SemiConfluent`, `Confluent_of_unique_end`, `isConfluent`, `isNormalizing`, `isTerminating`, `unique_Normal`, `extend`, `toConfluent`, `toDiamond`, `Terminating_toConfluent`, `refl`, `single`, `symm`, `reflTransGen_eq`, `Normal_iff`, `compRel_symm`, `to_eqvGen`, `to_eqvGen`, `toConfluent`, `SemiConfluent_iff_ChurchRosser`, `extend`, `toCommute`, `toStronglyConfluent`, `toConfluent`, `to_eqvGen`, `iff_transGen`, `isConfluent_iff_all_unique_Normal`, `isNormalizing`, `ofTransGen`, `subrelation`, `toTransGen`, `to_eqvGen`, `join_inl`, `join_inl_reflTransGen`, `join_inr`, `join_inr_reflTransGen`, `reflTransGen_compRel`, `reflTransGen_mono_closed`, `iff_transGen`, `ofTransGen`	50
Total	72

Relation

Definitions

Name	Category	Theorems
`ChurchRosser` 📖	MathDef	3 math math: `SemiConfluent_iff_ChurchRosser`, `Confluent_iff_ChurchRosser`, `Confluent.toChurchRosser`
`Commute` 📖	MathDef	3 math math: `Commute.symmetric`, `Commute.toConfluent`, `StronglyCommute.toCommute`
`Confluent` 📖	MathDef	13 math math: `LocallyConfluent.Terminating_toConfluent`, `Confluent_of_unique_end`, `SemiConfluent.toConfluent`, `Confluent_iff_ChurchRosser`, `Cslib.URM.step_confluent`, `Commute.toConfluent`, `Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.confluence_beta`, `StronglyConfluent.toConfluent`, `Confluent_iff_SemiConfluent`, `Convergent.isConfluent`, `Diamond.toConfluent`, `Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_confluence`, `Terminating.isConfluent_iff_all_unique_Normal`
`Convergent` 📖	MathDef	—
`Diamond` 📖	MathDef	2 math math: `Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_diamond`, `DiamondCommute.toDiamond`
`DiamondCommute` 📖	MathDef	1 math math: `DiamondCommute.toDiamond`
`LocallyConfluent` 📖	MathDef	1 math math: `Confluent.toLocallyConfluent`
`MJoin` 📖	MathDef	3 math math: `MJoin.single`, `MJoin.refl`, `MJoin.symm`
`Normal` 📖	MathDef	4 math math: `Convergent.unique_Normal`, `Normal_iff`, `Cslib.URM.isHalted_iff_normal`, `Terminating.isConfluent_iff_all_unique_Normal`
`Normalizable` 📖	MathDef	1 math math: `Cslib.URM.halts_iff_normalizable`
`Normalizing` 📖	MathDef	2 math math: `Terminating.isNormalizing`, `Convergent.isNormalizing`
`Reducible` 📖	MathDef	—
`SemiConfluent` 📖	MathDef	2 math math: `SemiConfluent_iff_ChurchRosser`, `Confluent_iff_SemiConfluent`
`StronglyCommute` 📖	MathDef	1 math math: `StronglyCommute.toStronglyConfluent`
`StronglyConfluent` 📖	MathDef	1 math math: `StronglyCommute.toStronglyConfluent`
`Terminating` 📖	MathDef	2 math math: `Convergent.isTerminating`, `Terminating.iff_transGen`
`UpTo` 📖	MathDef	1 math math: `Cslib.LTS.IsBisimulationUpTo.isBisimulation`
`command_Reduction_notation__` 📖	CompOp	—
`reduction_sys` 📖	CompOp	—
`trans_of_subrelation` 📖	CompOp	—
`trans_of_subrelation_left` 📖	CompOp	—
`trans_of_subrelation_right` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Confluent_iff_ChurchRosser` 📖	mathematical	—	`Confluent` `ChurchRosser`	—	—
`Confluent_iff_SemiConfluent` 📖	mathematical	—	`Confluent` `SemiConfluent`	—	—
`Confluent_of_unique_end` 📖	mathematical	—	`Confluent`	—	—
`Normal_iff` 📖	mathematical	—	`Normal`	—	`Normal.eq_1`
`SemiConfluent_iff_ChurchRosser` 📖	mathematical	—	`SemiConfluent` `ChurchRosser`	—	—
`join_inl` 📖	—	—	—	—	—
`join_inl_reflTransGen` 📖	—	—	—	—	—
`join_inr` 📖	—	—	—	—	—
`join_inr_reflTransGen` 📖	—	—	—	—	—
`reflTransGen_compRel` 📖	—	—	—	—	—
`reflTransGen_mono_closed` 📖	—	—	—	—	—

Relation.ChurchRosser

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normal_eq` 📖	—	`Relation.ChurchRosser` `Relation.Normal`	—	—	—
`normal_eqvGen_reflTransGen` 📖	—	`Relation.ChurchRosser` `Relation.Normal`	—	—	—

Relation.Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`join_confluent` 📖	—	`Relation.Confluent` `Relation.Commute`	—	—	`join_left` `symmetric`
`join_left` 📖	—	`Relation.Commute`	—	—	—
`symmetric` 📖	mathematical	—	`Relation.Commute`	—	—
`toConfluent` 📖	mathematical	—	`Relation.Commute` `Relation.Confluent`	—	—

Relation.Confluent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivalence_join_reflTransGen` 📖	—	`Relation.Confluent`	—	—	—
`toChurchRosser` 📖	mathematical	`Relation.Confluent`	`Relation.ChurchRosser`	—	—
`toLocallyConfluent` 📖	mathematical	`Relation.Confluent`	`Relation.LocallyConfluent`	—	—

Relation.Convergent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isConfluent` 📖	mathematical	`Relation.Convergent`	`Relation.Confluent`	—	—
`isNormalizing` 📖	mathematical	`Relation.Convergent`	`Relation.Normalizing`	—	`Relation.Terminating.isNormalizing` `isTerminating`
`isTerminating` 📖	mathematical	`Relation.Convergent`	`Relation.Terminating`	—	—
`unique_Normal` 📖	mathematical	`Relation.Convergent`	`Relation.Normal`	—	`Relation.Terminating.isConfluent_iff_all_unique_Normal` `isTerminating` `isConfluent`

Relation.Diamond

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extend` 📖	—	`Relation.Diamond`	—	—	—
`toConfluent` 📖	mathematical	`Relation.Diamond`	`Relation.Confluent`	—	`extend`

Relation.DiamondCommute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toDiamond` 📖	mathematical	—	`Relation.DiamondCommute` `Relation.Diamond`	—	—

Relation.LocallyConfluent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Terminating_toConfluent` 📖	mathematical	`Relation.LocallyConfluent` `Relation.Terminating`	`Relation.Confluent`	—	—

Relation.MJoin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`refl` 📖	mathematical	—	`Relation.MJoin`	—	—
`single` 📖	mathematical	—	`Relation.MJoin`	—	—
`symm` 📖	mathematical	—	`Relation.MJoin`	—	—

Relation.Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reflTransGen_eq` 📖	—	`Relation.Normal`	—	—	—

Relation.ReflGen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compRel_symm` 📖	—	—	—	—	—
`to_eqvGen` 📖	—	—	—	—	—

Relation.ReflTransGen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_eqvGen` 📖	—	—	—	—	—

Relation.SemiConfluent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toConfluent` 📖	mathematical	`Relation.SemiConfluent`	`Relation.Confluent`	—	—

Relation.StronglyCommute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extend` 📖	—	`Relation.StronglyCommute`	—	—	—
`toCommute` 📖	mathematical	`Relation.StronglyCommute`	`Relation.Commute`	—	`extend`
`toStronglyConfluent` 📖	mathematical	—	`Relation.StronglyCommute` `Relation.StronglyConfluent`	—	—

Relation.StronglyConfluent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toConfluent` 📖	mathematical	`Relation.StronglyConfluent`	`Relation.Confluent`	—	`Relation.StronglyCommute.toCommute`

Relation.SymmGen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_eqvGen` 📖	—	—	—	—	—

Relation.Terminating

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_transGen` 📖	mathematical	—	`Relation.Terminating`	—	`ofTransGen` `toTransGen`
`isConfluent_iff_all_unique_Normal` 📖	mathematical	`Relation.Terminating`	`Relation.Confluent` `Relation.Normal`	—	`isNormalizing` `Relation.Normal.reflTransGen_eq`
`isNormalizing` 📖	mathematical	`Relation.Terminating`	`Relation.Normalizing`	—	—
`ofTransGen` 📖	—	`Relation.Terminating`	—	—	—
`subrelation` 📖	—	`Relation.Terminating`	—	—	`eq_1`
`toTransGen` 📖	—	`Relation.Terminating`	—	—	—

Relation.TransGen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_eqvGen` 📖	—	—	—	—	—

WellFounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_transGen` 📖	—	—	—	—	`ofTransGen`
`ofTransGen` 📖	—	—	—	—	—

---

← Back to Index