Recursion

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

Statistics

Metric	Count
Definitions `Add`, `AddPoly`, `Church`, `IsChurch`, `IsChurchPair`, `IsZero`, `IsZeroPoly`, `LE`, `LEPoly`, `Mul`, `MulPoly`, `NatPair`, `NatPairPoly`, `NatUnpairLeft`, `NatUnpairLeftPoly`, `NatUnpairRight`, `NatUnpairRightPoly`, `One`, `Pred`, `PredAux`, `PredAuxPoly`, `PredPoly`, `RFind`, `RFindAbove`, `RFindAboveAux`, `RFindAboveAuxPoly`, `Rec`, `RecAux`, `RecAuxPoly`, `Sqrt`, `SqrtCond`, `SqrtCondPoly`, `SqrtPoly`, `Sub`, `SubPoly`, `Succ`, `Zero`, `toChurch`	38
Theorems `Church_succ`, `Church_zero`, `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`, `natPair_correct`, `natPair_def`, `natUnpairLeft_correct`, `natUnpairLeft_def`, `natUnpairRight_correct`, `natUnpairRight_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`, `sqrtCond_def`, `sqrt_correct`, `sqrt_def`, `sub_correct`, `sub_def`, `succ_correct`, `toChurch_correct`, `toChurch_succ`, `toChurch_zero`, `zero_correct`	44
Total	82

Cslib.SKI

Definitions

Name	Category	Theorems
`Add` 📖	CompOp	4 math math: `add_correct`, `natPair_def`, `mul_def`, `add_def`
`AddPoly` 📖	CompOp	—
`Church` 📖	CompOp	5 math math: `church_red`, `Church_zero`, `churchK_church`, `predAux_correct'`, `Church_succ`
`IsChurch` 📖	MathDef	17 math math: `natUnpairLeft_correct`, `mul_correct`, `natPair_correct`, `pred_correct`, `add_correct`, `List.headD_correct`, `sub_correct`, `zero_correct`, `sqrt_correct`, `RFindAbove_correct`, `natUnpairRight_correct`, `toChurch_correct`, `one_correct`, `RFind_correct`, `succ_correct`, `List.head_correct`, `isChurch_trans`
`IsChurchPair` 📖	MathDef	3 math math: `predAux_correct`, `predAux_correct'`, `isChurchPair_trans`
`IsZero` 📖	CompOp	6 math math: `isZero_def`, `isZero_correct`, `le_def`, `rec_def`, `rfindAboveAux_def`, `recAux_def`
`IsZeroPoly` 📖	CompOp	—
`LE` 📖	CompOp	6 math math: `natUnpairRight_def`, `natUnpairLeft_def`, `le_correct`, `le_def`, `natPair_def`, `sqrtCond_def`
`LEPoly` 📖	CompOp	—
`Mul` 📖	CompOp	6 math math: `natUnpairRight_def`, `natUnpairLeft_def`, `mul_correct`, `natPair_def`, `mul_def`, `sqrtCond_def`
`MulPoly` 📖	CompOp	—
`NatPair` 📖	CompOp	2 math math: `natPair_correct`, `natPair_def`
`NatPairPoly` 📖	CompOp	—
`NatUnpairLeft` 📖	CompOp	2 math math: `natUnpairLeft_correct`, `natUnpairLeft_def`
`NatUnpairLeftPoly` 📖	CompOp	—
`NatUnpairRight` 📖	CompOp	2 math math: `natUnpairRight_def`, `natUnpairRight_correct`
`NatUnpairRightPoly` 📖	CompOp	—
`One` 📖	CompOp	2 math math: `one_correct`, `sqrtCond_def`
`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	2 math math: `sqrt_def`, `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	—
`Sqrt` 📖	CompOp	4 math math: `natUnpairRight_def`, `natUnpairLeft_def`, `sqrt_def`, `sqrt_correct`
`SqrtCond` 📖	CompOp	2 math math: `sqrt_def`, `sqrtCond_def`
`SqrtCondPoly` 📖	CompOp	—
`SqrtPoly` 📖	CompOp	—
`Sub` 📖	CompOp	5 math math: `natUnpairRight_def`, `natUnpairLeft_def`, `sub_correct`, `le_def`, `sub_def`
`SubPoly` 📖	CompOp	—
`Succ` 📖	CompOp	7 math math: `predAux_def`, `toChurch_succ`, `rfindAboveAux_def`, `rfindAboveAux_step`, `sqrtCond_def`, `add_def`, `succ_correct`
`Zero` 📖	CompOp	8 math math: `pred_def`, `List.prependZero_def`, `List.head_def`, `zero_correct`, `predAux_correct'`, `toChurch_zero`, `mul_def`, `sqrtCond_def`
`toChurch` 📖	CompOp	4 math math: `toChurch_succ`, `toChurch_zero`, `List.toChurch_cons`, `toChurch_correct`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Church_succ` 📖	mathematical	—	`Church` `app`	—	—
`Church_zero` 📖	mathematical	—	`Church`	—	—
`RFindAbove_correct` 📖	mathematical	`IsChurch` `app`	`IsChurch` `app` `RFindAbove`	—	`isChurch_trans` `MRed.head` `fixedPoint_correct` `rfindAboveAux_step` `succ_correct`
`RFind_correct` 📖	mathematical	`IsChurch` `app`	`IsChurch` `app` `RFind`	—	`RFindAbove_correct` `zero_correct`
`add_correct` 📖	mathematical	`IsChurch`	`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`	`Cslib.SKI` `Red` `Church`	—	`parallel_mRed`
`isChurchPair_trans` 📖	mathematical	`Cslib.SKI` `Red` `IsChurchPair`	`IsChurchPair`	—	`isChurch_trans` `MRed.tail`
`isChurch_trans` 📖	mathematical	`Cslib.SKI` `Red` `IsChurch`	`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`	`IsChurch` `app` `Mul`	—	`isChurch_trans` `mul_def` `zero_correct` `add_correct`
`mul_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Mul` `Add` `Zero`	—	`Polynomial.toSKI_correct`
`natPair_correct` 📖	mathematical	`IsChurch`	`IsChurch` `app` `NatPair`	—	`isChurch_trans` `natPair_def` `neg_correct` `le_correct` `cond_correct`
`natPair_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `NatPair` `Cond` `Add` `Mul` `Neg` `LE`	—	`Polynomial.toSKI_correct`
`natUnpairLeft_correct` 📖	mathematical	`IsChurch`	`IsChurch` `app` `NatUnpairLeft`	—	`isChurch_trans` `natUnpairLeft_def` `neg_correct` `le_correct` `cond_correct`
`natUnpairLeft_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `NatUnpairLeft` `Cond` `Sub` `Mul` `Sqrt` `Neg` `LE`	—	`Polynomial.toSKI_correct`
`natUnpairRight_correct` 📖	mathematical	`IsChurch`	`IsChurch` `app` `NatUnpairRight`	—	`isChurch_trans` `natUnpairRight_def` `neg_correct` `le_correct` `cond_correct`
`natUnpairRight_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `NatUnpairRight` `Cond` `Sqrt` `Sub` `Mul` `Neg` `LE`	—	`Polynomial.toSKI_correct`
`one_correct` 📖	mathematical	—	`IsChurch` `One`	—	`MRed.head`
`predAux_correct` 📖	mathematical	`IsChurchPair`	`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`	`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` `app` `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` `app` `RFindAboveAux` `Succ`	—	`rfindAboveAux_def` `cond_correct` `isZero_correct`
`sqrtCond_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `SqrtCond` `Cond` `Zero` `One` `Neg` `LE` `Mul` `Succ`	—	`Polynomial.toSKI_correct`
`sqrt_correct` 📖	mathematical	`IsChurch`	`IsChurch` `app` `Sqrt`	—	`isChurch_trans` `sqrt_def` `RFind_correct` `sqrtCond_def` `succ_correct` `le_correct` `mul_correct` `neg_correct` `cond_correct`
`sqrt_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Sqrt` `RFind` `SqrtCond`	—	`Polynomial.toSKI_correct`
`sub_correct` 📖	mathematical	`IsChurch`	`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`	`IsChurch` `app` `Succ`	—	`B_def` `MRed.tail`
`toChurch_correct` 📖	mathematical	—	`IsChurch` `toChurch`	—	`zero_correct` `succ_correct`
`toChurch_succ` 📖	mathematical	—	`toChurch` `app` `Succ`	—	—
`toChurch_zero` 📖	mathematical	—	`toChurch` `Zero`	—	—
`zero_correct` 📖	mathematical	—	`IsChurch` `Zero`	—	`Church.eq_def`

---

← Back to Index