Recursion

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

Statistics

Metric	Count
Definitions `Add`, `AddPoly`, `Church`, `IsChurch`, `IsChurchPair`, `IsZero`, `IsZeroPoly`, `LE`, `LEPoly`, `Mul`, `MulPoly`, `One`, `Pred`, `PredAux`, `PredAuxPoly`, `PredPoly`, `RFind`, `RFindAbove`, `RFindAboveAux`, `RFindAboveAuxPoly`, `Rec`, `RecAux`, `RecAuxPoly`, `Sub`, `SubPoly`, `Succ`, `Zero`	27
Theorems `RFindAbove_correct`, `RFind_correct`, `add_correct`, `add_def`, `church_red`, `isChurchPair_trans`, `isChurch_trans`, `isZero_correct`, `isZero_def`, `le_correct`, `le_def`, `mul_correct`, `mul_def`, `one_correct`, `predAux_correct`, `predAux_correct'`, `predAux_def`, `pred_correct`, `pred_def`, `recAux_def`, `rec_def`, `rec_succ`, `rec_zero`, `rfindAboveAux_base`, `rfindAboveAux_def`, `rfindAboveAux_step`, `sub_correct`, `sub_def`, `succ_correct`, `zero_correct`	30
Total	57

Cslib.SKI

Definitions

Name	Category	Theorems
`Add` 📖	CompOp	3 math math: `add_correct`, `mul_def`, `add_def`
`AddPoly` 📖	CompOp	—
`Church` 📖	CompOp	3 math math: `church_red`, `churchK_church`, `predAux_correct'`
`IsChurch` 📖	MathDef	2 math math: `zero_correct`, `one_correct`
`IsChurchPair` 📖	MathDef	1 math math: `predAux_correct'`
`IsZero` 📖	CompOp	6 math math: `isZero_def`, `isZero_correct`, `le_def`, `rec_def`, `rfindAboveAux_def`, `recAux_def`
`IsZeroPoly` 📖	CompOp	—
`LE` 📖	CompOp	2 math math: `le_correct`, `le_def`
`LEPoly` 📖	CompOp	—
`Mul` 📖	CompOp	2 math math: `mul_correct`, `mul_def`
`MulPoly` 📖	CompOp	—
`One` 📖	CompOp	1 math math: `one_correct`
`Pred` 📖	CompOp	6 math math: `pred_def`, `pred_correct`, `rec_succ`, `rec_def`, `recAux_def`, `sub_def`
`PredAux` 📖	CompOp	4 math math: `pred_def`, `predAux_def`, `predAux_correct`, `predAux_correct'`
`PredAuxPoly` 📖	CompOp	—
`PredPoly` 📖	CompOp	—
`RFind` 📖	CompOp	1 math math: `RFind_correct`
`RFindAbove` 📖	CompOp	1 math math: `RFindAbove_correct`
`RFindAboveAux` 📖	CompOp	3 math math: `rfindAboveAux_def`, `rfindAboveAux_base`, `rfindAboveAux_step`
`RFindAboveAuxPoly` 📖	CompOp	—
`Rec` 📖	CompOp	3 math math: `rec_zero`, `rec_succ`, `rec_def`
`RecAux` 📖	CompOp	1 math math: `recAux_def`
`RecAuxPoly` 📖	CompOp	—
`Sub` 📖	CompOp	3 math math: `sub_correct`, `le_def`, `sub_def`
`SubPoly` 📖	CompOp	—
`Succ` 📖	CompOp	5 math math: `predAux_def`, `rfindAboveAux_def`, `rfindAboveAux_step`, `add_def`, `succ_correct`
`Zero` 📖	CompOp	4 math math: `pred_def`, `zero_correct`, `predAux_correct'`, `mul_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`RFindAbove_correct` 📖	mathematical	`IsChurch` `app`	`RFindAbove`	—	`isChurch_trans` `MRed.head` `fixedPoint_correct` `rfindAboveAux_base` `rfindAboveAux_step` `succ_correct`
`RFind_correct` 📖	mathematical	`IsChurch` `app`	`RFind`	—	`RFindAbove_correct` `zero_correct`
`add_correct` 📖	mathematical	`IsChurch`	`app` `Add`	—	`isChurch_trans` `add_def` `succ_correct`
`add_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Add` `Succ`	—	`Polynomial.toSKI_correct`
`church_red` 📖	mathematical	`Cslib.SKI` `Red`	`Church`	—	`parallel_mRed`
`isChurchPair_trans` 📖	—	`Cslib.SKI` `Red` `IsChurchPair`	—	—	`isChurch_trans` `MRed.tail`
`isChurch_trans` 📖	—	`Cslib.SKI` `Red` `IsChurch`	—	—	`MRed.head`
`isZero_correct` 📖	mathematical	`IsChurch`	`IsBool` `app` `IsZero`	—	`isBool_trans` `isZero_def` `TT_correct` `FF_correct`
`isZero_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `IsZero` `K` `FF` `TT`	—	`Polynomial.toSKI_correct`
`le_correct` 📖	mathematical	`IsChurch`	`IsBool` `app` `LE`	—	`isBool_trans` `le_def` `isZero_correct` `sub_correct`
`le_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `LE` `IsZero` `Sub`	—	`Polynomial.toSKI_correct`
`mul_correct` 📖	mathematical	`IsChurch`	`app` `Mul`	—	`isChurch_trans` `mul_def` `zero_correct` `add_correct`
`mul_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Mul` `Add` `Zero`	—	`Polynomial.toSKI_correct`
`one_correct` 📖	mathematical	—	`IsChurch` `One`	—	`MRed.head`
`predAux_correct` 📖	mathematical	`IsChurchPair`	`app` `PredAux`	—	`isChurchPair_trans` `predAux_def` `isChurch_trans` `fst_correct` `snd_correct` `succ_correct`
`predAux_correct'` 📖	mathematical	—	`IsChurchPair` `Church` `PredAux` `app` `MkPair` `Zero`	—	`isChurchPair_trans` `isChurch_trans` `fst_correct` `zero_correct` `snd_correct` `predAux_correct`
`predAux_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `PredAux` `MkPair` `Snd` `Succ`	—	`Polynomial.toSKI_correct`
`pred_correct` 📖	mathematical	`IsChurch`	`app` `Pred`	—	`isChurch_trans` `pred_def` `MRed.tail` `predAux_correct'`
`pred_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Pred` `Fst` `PredAux` `MkPair` `Zero`	—	`Polynomial.toSKI_correct`
`recAux_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `RecAux` `Cond` `Pred` `IsZero`	—	`Polynomial.toSKI_correct`
`rec_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Rec` `Cond` `Pred` `IsZero`	—	`MRed.head` `fixedPoint_correct` `recAux_def`
`rec_succ` 📖	mathematical	`IsChurch`	`Cslib.SKI` `Red` `app` `Rec` `Pred`	—	`rec_def` `cond_correct` `isZero_correct`
`rec_zero` 📖	mathematical	`IsChurch`	`Cslib.SKI` `Red` `app` `Rec`	—	`rec_def` `cond_correct` `isZero_correct`
`rfindAboveAux_base` 📖	mathematical	`IsChurch` `app`	`Cslib.SKI` `Red` `RFindAboveAux`	—	`rfindAboveAux_def` `cond_correct` `isZero_correct`
`rfindAboveAux_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `RFindAboveAux` `Cond` `Succ` `IsZero`	—	`Polynomial.toSKI_correct`
`rfindAboveAux_step` 📖	mathematical	`IsChurch` `app`	`Cslib.SKI` `Red` `RFindAboveAux` `Succ`	—	`rfindAboveAux_def` `cond_correct` `isZero_correct`
`sub_correct` 📖	mathematical	`IsChurch`	`app` `Sub`	—	`isChurch_trans` `sub_def` `pred_correct`
`sub_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Sub` `Pred`	—	`Polynomial.toSKI_correct`
`succ_correct` 📖	mathematical	`IsChurch`	`app` `Succ`	—	`B_def` `MRed.tail`
`zero_correct` 📖	mathematical	—	`IsChurch` `Zero`	—	`Church.eq_def`

---

← Back to Index