Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `SKI`, `CommonReduct`, `Red`, `applyList`, `size`, `«term_↠_»`, `«term_⬝_»`, `«term_⭢_»`, `instDecidableEqSKI`, `decEq`, `instReprSKI`, `repr`	12
Theorems `I`, `K`, `S`, `head`, `tail`, `ne`, `applyList_concat`, `commonReduct_head`, `commonReduct_tail`, `parallel_mRed`, `parallel_red`	11
Total	23

Cslib

Definitions

Name	Category	Theorems
`SKI` 📖	CompData	47 math math: `SKI.pred_def`, `SKI.ThAux_def`, `SKI.isZero_def`, `SKI.pair_def`, `SKI.fixedPoint_correct`, `SKI.mRed_of_parallelReduction`, `SKI.rec_zero`, `SKI.MRed.S`, `SKI.predAux_def`, `SKI.unpaired_def`, `SKI.or_def`, `SKI.B_def`, `SKI.applyList_concat`, `SKI.redexFree_iff_mred_eq`, `SKI.cond_correct`, `SKI.and_def`, `SKI.rec_succ`, `SKI.snd_correct`, `SKI.le_def`, `SKI.R_def`, `SKI.parallelReduction_diamond`, `SKI.H_def`, `SKI.rec_def`, `SKI.commonReduct_redexFree`, `SKI.fst_correct`, `SKI.unpaired_correct`, `SKI.Th_correct`, `SKI.rfindAboveAux_def`, `SKI.MRed.K`, `SKI.rfindAboveAux_base`, `SKI.join_parallelReduction_equivalence`, `SKI.MRed.I`, `SKI.rotL_def`, `SKI.del_def`, `SKI.mul_def`, `SKI.recAux_def`, `SKI.rfindAboveAux_step`, `SKI.C_def`, `SKI.rotR_def`, `SKI.churchK_injective`, `SKI.add_def`, `SKI.parallel_red`, `SKI.Y_def`, `SKI.sub_def`, `SKI.commonReduct_equivalence`, `SKI.redexFree_iff_evalStep`, `SKI.reflTransGen_parallelReduction_mRed`
`instDecidableEqSKI` 📖	CompOp	—
`instReprSKI` 📖	CompOp	—

Cslib.SKI

Definitions

Name	Category	Theorems
`CommonReduct` 📖	MathDef	5 math math: `sk_nequiv`, `MRed.diamond`, `Y_correct`, `TF_nequiv`, `commonReduct_equivalence`
`Red` 📖	CompData	45 math math: `pred_def`, `ThAux_def`, `Polynomial.toSKI_correct`, `isZero_def`, `pair_def`, `fixedPoint_correct`, `mRed_of_parallelReduction`, `rec_zero`, `MRed.S`, `predAux_def`, `unpaired_def`, `or_def`, `B_def`, `RedexFree.no_red`, `redexFree_iff_mred_eq`, `cond_correct`, `and_def`, `rec_succ`, `snd_correct`, `redexFree_iff`, `le_def`, `R_def`, `H_def`, `rec_def`, `commonReduct_redexFree`, `fst_correct`, `unpaired_correct`, `Th_correct`, `rfindAboveAux_def`, `MRed.K`, `rfindAboveAux_base`, `MRed.I`, `rotL_def`, `del_def`, `mul_def`, `recAux_def`, `rfindAboveAux_step`, `C_def`, `rotR_def`, `add_def`, `Y_def`, `sub_def`, `evalStep_right_correct`, `Polynomial.elimVar_correct`, `reflTransGen_parallelReduction_mRed`
`applyList` 📖	CompOp	2 math math: `Polynomial.toSKI_correct`, `applyList_concat`
`size` 📖	CompOp	1 math math: `churchK_size`
`«term_↠_»` 📖	CompOp	—
`«term_⬝_»` 📖	CompOp	—
`«term_⭢_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`applyList_concat` 📖	mathematical	—	`applyList` `Cslib.SKI` `app`	—	—
`commonReduct_head` 📖	mathematical	`CommonReduct`	`app`	—	`MRed.head`
`commonReduct_tail` 📖	mathematical	`CommonReduct`	`app`	—	`MRed.tail`
`parallel_mRed` 📖	mathematical	`Cslib.SKI` `Red`	`app`	—	`MRed.head` `MRed.tail`
`parallel_red` 📖	mathematical	`Red`	`Cslib.SKI` `app`	—	—

Cslib.SKI.MRed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`I` 📖	mathematical	—	`Cslib.SKI` `Cslib.SKI.Red` `Cslib.SKI.app` `Cslib.SKI.I`	—	—
`K` 📖	mathematical	—	`Cslib.SKI` `Cslib.SKI.Red` `Cslib.SKI.app` `Cslib.SKI.K`	—	—
`S` 📖	mathematical	—	`Cslib.SKI` `Cslib.SKI.Red` `Cslib.SKI.app` `Cslib.SKI.S`	—	—
`head` 📖	mathematical	`Cslib.SKI` `Cslib.SKI.Red`	`Cslib.SKI.app`	—	—
`tail` 📖	mathematical	`Cslib.SKI` `Cslib.SKI.Red`	`Cslib.SKI.app`	—	—

Cslib.SKI.Red

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ne` 📖	—	`Cslib.SKI.Red`	—	—	—

Cslib.instDecidableEqSKI

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

Cslib.instReprSKI

Definitions

Name	Category	Theorems
`repr` 📖	CompOp	—

---

← Back to Index