Documentation Verification Report

Evaluation

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

Statistics

Metric	Count
Definitions `RedexFree`, `churchK`, `evalStep`, `instDecidablePredRedexFree`	4
Theorems `no_red`, `TF_nequiv`, `churchK_church`, `churchK_injective`, `churchK_redexFree`, `churchK_size`, `commonReduct_redexFree`, `confluent_redexFree`, `eq_of_commonReduct_redexFree`, `evalStep_right_correct`, `isBool_injective`, `isChurch_injective`, `redexFree_iff`, `redexFree_iff_evalStep`, `redexFree_iff_mred_eq`, `redexFree_of_no_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_of_no_red`, `redexFree_iff`, `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	—	`CommonReduct` `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`
`commonReduct_redexFree` 📖	mathematical	`RedexFree` `CommonReduct`	`Cslib.SKI` `Red`	—	`redexFree_iff_mred_eq`
`confluent_redexFree` 📖	—	`Cslib.SKI` `Red` `RedexFree`	—	—	`MRed.diamond` `redexFree_iff_mred_eq`
`eq_of_commonReduct_redexFree` 📖	—	`CommonReduct` `RedexFree`	—	—	`redexFree_iff_mred_eq` `commonReduct_redexFree`
`evalStep_right_correct` 📖	mathematical	`evalStep` `RedexFree` `Cslib.SKI`	`Red`	—	—
`isBool_injective` 📖	—	`IsBool` `CommonReduct`	—	—	`commonReduct_equivalence` `Relation.MJoin.single` `commonReduct_head` `sk_nequiv`
`isChurch_injective` 📖	—	`IsChurch` `CommonReduct`	—	—	`commonReduct_equivalence` `churchK_church` `Relation.MJoin.single` `commonReduct_head` `churchK_injective` `eq_of_commonReduct_redexFree` `churchK_redexFree`
`redexFree_iff` 📖	mathematical	—	`RedexFree` `Red`	—	`RedexFree.no_red` `redexFree_of_no_red`
`redexFree_iff_evalStep` 📖	mathematical	—	`RedexFree` `Cslib.SKI` `evalStep`	—	`RedexFree.no_red` `evalStep_right_correct`
`redexFree_iff_mred_eq` 📖	mathematical	—	`RedexFree` `Cslib.SKI` `Red`	—	`RedexFree.no_red` `redexFree_iff` `Red.ne`
`redexFree_of_no_red` 📖	mathematical	`Red`	`RedexFree`	—	`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'` 📖	—	`Cslib.SKI` `Red` `app` `TT` `FF`	—	—	`rice`
`sk_nequiv` 📖	mathematical	—	`CommonReduct` `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
`no_red` 📖	mathematical	`Cslib.SKI.RedexFree`	`Cslib.SKI.Red`	—	`eq_4` `eq_5`

---

← Back to Index