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__, emptyHRelation, reduction_sys, trans_of_subrelation, trans_of_subrelation_left, trans_of_subrelation_right	23
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, 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	51
Total	74

Relation

Definitions

Name	Category	Theorems
ChurchRosser 📖	MathDef	3 math math: SemiConfluent_iff_ChurchRosser, Confluent_iff_ChurchRosser, Confluent.toChurchRosser
Commute 📖	MathDef	4 math math: Commute.join_left, Commute.symmetric, Commute.toConfluent, StronglyCommute.toCommute
Confluent 📖	MathDef	17 math math: Cslib.SKI.MRed.diamond, Commute.join_confluent, 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, RightUnique.toConfluent, StronglyConfluent.toConfluent, Confluent_iff_SemiConfluent, Convergent.isConfluent, Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.confluent_beta_eta, Diamond.toConfluent, Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_confluence, Terminating.isConfluent_iff_all_unique_Normal
Convergent 📖	MathDef	—
Diamond 📖	MathDef	3 math math: Cslib.SKI.parallelReduction_diamond, 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	10 math math: Cslib.SKI.sk_nequiv, MJoin.single, MJoin.refl, Cslib.SKI.Y_correct, Cslib.SKI.mJoin_red_tail, Cslib.SKI.mJoin_red_equivalence, Cslib.SKI.TF_nequiv, Cslib.SKI.join_parallelReduction_equivalence, MJoin.symm, Cslib.SKI.mJoin_red_head
Normal 📖	MathDef	6 math math: Cslib.SKI.redexFree_iff, Cslib.SKI.RedexFree.normal_red, 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	2 math math: StronglyCommute.toStronglyConfluent, Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.stronglyCommute_eta_beta
StronglyConfluent 📖	MathDef	2 math math: Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.stronglyConfluent_eta, StronglyCommute.toStronglyConfluent
Terminating 📖	MathDef	5 math math: Terminating.toTransGen, Convergent.isTerminating, Terminating.subrelation, Terminating.iff_transGen, Terminating.ofTransGen
UpTo 📖	MathDef	—
command_Reduction_notation__ 📖	CompOp	—
emptyHRelation 📖	MathDef	1 math math: Cslib.LTS.IsBisimulation.bot
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 📖	mathematical	Relation.Confluent Relation.Commute	Relation.Confluent	—	join_left symmetric
join_left 📖	mathematical	Relation.Commute	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.RightUnique

Theorems

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

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 📖	mathematical	Relation.Terminating	Relation.Terminating	—	—
subrelation 📖	mathematical	Relation.Terminating	Relation.Terminating	—	eq_1
toTransGen 📖	mathematical	Relation.Terminating	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