Confluence

📁 Source: Cslib/Languages/CombinatoryLogic/Confluence.lean

Statistics

Metric	Count
Definitions ParallelReduction, «term_⇒ₚ_»	2
Theorems I_irreducible, K_irreducible, Ka_irreducible, diamond, S_irreducible, Sa_irreducible, Sab_irreducible, commonReduct_equivalence, join_parallelReduction_equivalence, mRed_of_parallelReduction, parallelReduction_diamond, parallelReduction_of_red, reflTransGen_parallelReduction_mRed	13
Total	15

Cslib.SKI

Definitions

Name	Category	Theorems
ParallelReduction 📖	CompData	3 math math: parallelReduction_of_red, join_parallelReduction_equivalence, reflTransGen_parallelReduction_mRed
«term_⇒ₚ_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
I_irreducible 📖	—	ParallelReduction I	—	—	—
K_irreducible 📖	—	ParallelReduction K	—	—	—
Ka_irreducible 📖	—	ParallelReduction app K	—	—	K_irreducible
S_irreducible 📖	—	ParallelReduction S	—	—	—
Sa_irreducible 📖	—	ParallelReduction app S	—	—	S_irreducible
Sab_irreducible 📖	—	ParallelReduction app S	—	—	Sa_irreducible
commonReduct_equivalence 📖	mathematical	—	Cslib.SKI CommonReduct	—	reflTransGen_parallelReduction_mRed join_parallelReduction_equivalence
join_parallelReduction_equivalence 📖	mathematical	—	Cslib.SKI ParallelReduction	—	Relation.Confluent.equivalence_join_reflTransGen Relation.Diamond.toConfluent parallelReduction_diamond
mRed_of_parallelReduction 📖	mathematical	ParallelReduction	Cslib.SKI Red	—	parallel_mRed
parallelReduction_diamond 📖	mathematical	ParallelReduction	Cslib.SKI	—	I_irreducible Ka_irreducible Sab_irreducible
parallelReduction_of_red 📖	mathematical	Red	ParallelReduction	—	—
reflTransGen_parallelReduction_mRed 📖	mathematical	—	Cslib.SKI ParallelReduction Red	—	mRed_of_parallelReduction parallelReduction_of_red

Cslib.SKI.MRed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diamond 📖	mathematical	Cslib.SKI Cslib.SKI.Red	Cslib.SKI.CommonReduct	—	Cslib.SKI.commonReduct_equivalence Relation.MJoin.single

---

← Back to Index