Documentation Verification Report

Evaluation

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

Statistics

Metric	Count
Definitions `RedexFree`, `churchK`, `evalStep`, `instDecidablePredRedexFree`	4
Theorems `normal_red`, `TF_nequiv`, `churchK_church`, `churchK_injective`, `churchK_redexFree`, `churchK_size`, `confluent_redexFree`, `eq_of_mJoin_red_redexFree`, `evalStep_right_correct`, `isBool_injective`, `isChurch_injective`, `mJoin_red_redexFree`, `redexFree_iff`, `redexFree_iff_evalStep`, `redexFree_iff_mred_eq`, `redexFree_of_normal_red`, `rice`, `rice'`, `sk_nequiv`, `unique_normal_form`	20
Total	24

Cslib.SKI

Definitions

Name	Category	Theorems
`RedexFree` 📖	MathDef	5 math math: `churchK_redexFree`, `redexFree_iff_mred_eq`, `redexFree_iff`, `redexFree_of_normal_red`, `redexFree_iff_evalStep`
`churchK` 📖	CompOp	4 math math: `churchK_redexFree`, `churchK_size`, `churchK_church`, `churchK_injective`
`evalStep` 📖	CompOp	1 math math: `redexFree_iff_evalStep`
`instDecidablePredRedexFree` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`TF_nequiv` 📖	mathematical	—	`Relation.MJoin` `Cslib.SKI` `Red` `TT` `FF`	—	`isBool_injective` `TT_correct` `FF_correct`
`churchK_church` 📖	mathematical	—	`churchK` `Church` `K`	—	—
`churchK_injective` 📖	mathematical	—	`Cslib.SKI` `churchK`	—	`churchK_size`
`churchK_redexFree` 📖	mathematical	—	`RedexFree` `churchK`	—	—
`churchK_size` 📖	mathematical	—	`size` `churchK`	—	`churchK.eq_2` `size.eq_4` `size.eq_2`
`confluent_redexFree` 📖	mathematical	`Cslib.SKI` `Red` `RedexFree`	`Cslib.SKI` `Red`	—	`MRed.diamond` `redexFree_iff_mred_eq`
`eq_of_mJoin_red_redexFree` 📖	—	`Relation.MJoin` `Cslib.SKI` `Red` `RedexFree`	—	—	`redexFree_iff_mred_eq` `mJoin_red_redexFree`
`evalStep_right_correct` 📖	mathematical	`evalStep` `RedexFree` `Cslib.SKI`	`Red`	—	—
`isBool_injective` 📖	—	`IsBool` `Relation.MJoin` `Cslib.SKI` `Red`	—	—	`mJoin_red_equivalence` `Relation.MJoin.single` `mJoin_red_head`
`isChurch_injective` 📖	—	`IsChurch` `Relation.MJoin` `Cslib.SKI` `Red`	—	—	`mJoin_red_equivalence` `churchK_church` `Relation.MJoin.single` `mJoin_red_head` `churchK_injective` `eq_of_mJoin_red_redexFree` `churchK_redexFree`
`mJoin_red_redexFree` 📖	mathematical	`RedexFree` `Relation.MJoin` `Cslib.SKI` `Red`	`Cslib.SKI` `Red`	—	`redexFree_iff_mred_eq`
`redexFree_iff` 📖	mathematical	—	`RedexFree` `Relation.Normal` `Cslib.SKI` `Red`	—	`RedexFree.normal_red` `redexFree_of_normal_red`
`redexFree_iff_evalStep` 📖	mathematical	—	`RedexFree` `Cslib.SKI` `evalStep`	—	`RedexFree.normal_red` `evalStep_right_correct`
`redexFree_iff_mred_eq` 📖	mathematical	—	`RedexFree` `Cslib.SKI` `Red`	—	`redexFree_iff` `Red.ne`
`redexFree_of_normal_red` 📖	mathematical	`Relation.Normal` `Cslib.SKI` `Red`	`RedexFree`	—	`Relation.Normal_iff` `evalStep_right_correct`
`rice` 📖	—	`Cslib.SKI` `Red` `app` `TT` `FF`	—	—	`Polynomial.toSKI_correct` `MRed.tail` `fixedPoint_correct` `MRed.head` `TT_correct` `TF_nequiv` `MRed.diamond` `FF_correct`
`rice'` 📖	mathematical	`Cslib.SKI` `Red` `app` `TT` `FF`	`Cslib.SKI` `Red` `app` `TT` `FF`	—	`rice`
`sk_nequiv` 📖	mathematical	—	`Relation.MJoin` `Cslib.SKI` `Red` `S` `K`	—	`redexFree_iff_mred_eq`
`unique_normal_form` 📖	—	`Cslib.SKI` `Red` `RedexFree`	—	—	`redexFree_iff_mred_eq` `confluent_redexFree`

Cslib.SKI.RedexFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normal_red` 📖	mathematical	`Cslib.SKI.RedexFree`	`Relation.Normal` `Cslib.SKI` `Cslib.SKI.Red`	—	`eq_4` `eq_5`

---

← Back to Index