Documentation Verification Report

Confluence

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

Statistics

Metric	Count
Definitions `ParallelReduction`, `«term_↠ₚ_»`, `«term_⭢ₚ_»`	3
Theorems `I_irreducible`, `K_irreducible`, `Ka_irreducible`, `diamond`, `S_irreducible`, `Sa_irreducible`, `Sab_irreducible`, `join_parallelReduction_equivalence`, `mJoin_red_equivalence`, `mRed_of_parallelReduction`, `parallelReduction_diamond`, `parallelReduction_of_red`, `reflTransGen_parallelReduction_mRed`	13
Total	16

Cslib.SKI

Definitions

Name	Category	Theorems
`ParallelReduction` 📖	CompData	7 math math: `Sab_irreducible`, `parallelReduction_diamond`, `parallelReduction_of_red`, `Ka_irreducible`, `join_parallelReduction_equivalence`, `Sa_irreducible`, `reflTransGen_parallelReduction_mRed`
`«term_↠ₚ_»` 📖	CompOp	—
`«term_⭢ₚ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`I_irreducible` 📖	mathematical	`ParallelReduction` `I`	`I`	—	—
`K_irreducible` 📖	mathematical	`ParallelReduction` `K`	`K`	—	—
`Ka_irreducible` 📖	mathematical	`ParallelReduction` `app` `K`	`Cslib.SKI` `ParallelReduction` `app` `K`	—	`K_irreducible`
`S_irreducible` 📖	mathematical	`ParallelReduction` `S`	`S`	—	—
`Sa_irreducible` 📖	mathematical	`ParallelReduction` `app` `S`	`Cslib.SKI` `ParallelReduction` `app` `S`	—	`S_irreducible`
`Sab_irreducible` 📖	mathematical	`ParallelReduction` `app` `S`	`Cslib.SKI` `ParallelReduction` `app` `S`	—	`Sa_irreducible`
`join_parallelReduction_equivalence` 📖	mathematical	—	`Cslib.SKI` `Relation.MJoin` `ParallelReduction`	—	`Relation.Confluent.equivalence_join_reflTransGen` `Relation.Diamond.toConfluent` `parallelReduction_diamond`
`mJoin_red_equivalence` 📖	mathematical	—	`Cslib.SKI` `Relation.MJoin` `Red`	—	`Relation.MJoin.eq_1` `reflTransGen_parallelReduction_mRed` `join_parallelReduction_equivalence`
`mRed_of_parallelReduction` 📖	mathematical	`ParallelReduction`	`Cslib.SKI` `Red`	—	`parallel_mRed`
`parallelReduction_diamond` 📖	mathematical	—	`Relation.Diamond` `Cslib.SKI` `ParallelReduction`	—	`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	—	`Relation.Confluent` `Cslib.SKI` `Cslib.SKI.Red`	—	`Cslib.SKI.mJoin_red_equivalence` `Relation.MJoin.single`

---

← Back to Index