Ackermann

📁 Source: Mathlib/Computability/Ackermann.lean

Statistics

Metric	Count
Definitions `pappAck`, `step`, `ack`	3
Theorems `eval_pappAck`, `eval_pappAck_step_succ`, `eval_pappAck_step_zero`, `primrec_pappAck`, `primrec_pappAck_step`, `ack_ack_lt_ack_max_add_two`, `ack_add_one_sq_lt_ack_add_four`, `ack_add_one_sq_lt_ack_add_three`, `ack_inj_left`, `ack_inj_right`, `ack_injective_left`, `ack_injective_right`, `ack_le_ack`, `ack_le_iff_left`, `ack_le_iff_right`, `ack_lt_iff_left`, `ack_lt_iff_right`, `ack_mono_left`, `ack_mono_right`, `ack_one`, `ack_pair_lt`, `ack_pos`, `ack_strictMono_left`, `ack_strictMono_right`, `ack_succ_right_le_ack_succ_left`, `ack_succ_succ`, `ack_succ_zero`, `ack_three`, `ack_two`, `ack_zero`, `add_add_one_le_ack`, `add_lt_ack`, `computable₂_ack`, `exists_lt_ack_of_nat_primrec`, `lt_ack_left`, `lt_ack_right`, `max_ack_left`, `max_ack_right`, `not_nat_primrec_ack_self`, `not_primrec_ack_self`, `not_primrec₂_ack`, `one_lt_ack_succ_left`, `one_lt_ack_succ_right`	43
Total	46

Nat.Partrec.Code

Definitions

Name	Category	Theorems
`pappAck` 📖	CompOp	2 math math: `primrec_pappAck`, `eval_pappAck`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eval_pappAck` 📖	mathematical	—	`eval` `pappAck` `Part.some` `ack`	—	`ack.induct` `ack_zero` `eval_pappAck_step_zero` `ack_succ_zero` `eval_pappAck_step_succ` `Part.bind_some` `ack_succ_succ`
`eval_pappAck_step_succ` 📖	mathematical	—	`eval` `pappAck.step` `Part.bind`	—	`eval_curry` `Nat.unpair_pair` `eval_const` `Part.bind_some`
`eval_pappAck_step_zero` 📖	mathematical	—	`eval` `pappAck.step`	—	`eval_curry` `Nat.unpair_pair` `eval_const` `Part.bind_some`
`primrec_pappAck` 📖	mathematical	—	`Encodable.encode` `Nat.Partrec.Code` `Option.encodable` `Primcodable.toEncodable` `Primcodable.ofDenumerable` `instDenumerable` `pappAck` `Encodable.decode` `Denumerable.nat`	—	`Primrec.nat_rec₁` `Primrec.comp` `primrec_pappAck_step` `Primrec.snd`
`primrec_pappAck_step` 📖	mathematical	—	`Encodable.encode` `Nat.Partrec.Code` `Option.encodable` `Primcodable.toEncodable` `Primcodable.ofDenumerable` `instDenumerable` `pappAck.step` `Encodable.decode`	—	`Primrec₂.comp` `primrec₂_curry` `primrec₂_comp` `Primrec.id` `Nat.Primrec.const`

Nat.Partrec.Code.pappAck

Definitions

Name	Category	Theorems
`step` 📖	CompOp	3 math math: `Nat.Partrec.Code.primrec_pappAck_step`, `Nat.Partrec.Code.eval_pappAck_step_zero`, `Nat.Partrec.Code.eval_pappAck_step_succ`

(root)

Definitions

Name	Category	Theorems
`ack` 📖	CompOp	39 math math: `ack_add_one_sq_lt_ack_add_three`, `not_nat_primrec_ack_self`, `one_lt_ack_succ_left`, `ack_strictMono_left`, `ack_inj_right`, `ack_injective_right`, `not_primrec_ack_self`, `not_primrec₂_ack`, `ack_succ_zero`, `ack_pos`, `lt_ack_right`, `ack_le_iff_left`, `ack_three`, `ack_succ_succ`, `max_ack_right`, `ack_le_iff_right`, `ack_mono_right`, `ack_succ_right_le_ack_succ_left`, `one_lt_ack_succ_right`, `add_add_one_le_ack`, `ack_pair_lt`, `lt_ack_left`, `add_lt_ack`, `ack_add_one_sq_lt_ack_add_four`, `ack_injective_left`, `ack_one`, `ack_strictMono_right`, `max_ack_left`, `ack_two`, `ack_ack_lt_ack_max_add_two`, `ack_inj_left`, `ack_lt_iff_left`, `ack_zero`, `ack_lt_iff_right`, `ack_le_ack`, `computable₂_ack`, `exists_lt_ack_of_nat_primrec`, `ack_mono_left`, `Nat.Partrec.Code.eval_pappAck`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ack_ack_lt_ack_max_add_two` 📖	mathematical	—	`ack`	—	`ack_mono_left` `le_max_left` `ack_strictMono_right` `ack_strictMono_left` `le_max_right` `ack_succ_succ` `ack_succ_right_le_ack_succ_left`
`ack_add_one_sq_lt_ack_add_four` 📖	mathematical	—	`ack` `Monoid.toNatPow` `Nat.instMonoid`	—	`ack_strictMono_right` `lt_ack_right` `two_ne_zero` `ack_mono_right` `ack_add_one_sq_lt_ack_add_three` `ack_mono_left` `ack_succ_succ` `ack_succ_right_le_ack_succ_left`
`ack_add_one_sq_lt_ack_add_three` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid` `ack`	—	`ack_zero` `zero_add` `ack_three` `ack_succ_zero` `ack_succ_succ` `LE.le.trans` `ack_mono_right` `ack_mono_left`
`ack_inj_left` 📖	mathematical	—	`ack`	—	`ack_injective_left`
`ack_inj_right` 📖	mathematical	—	`ack`	—	`ack_injective_right`
`ack_injective_left` 📖	mathematical	—	`ack`	—	`StrictMono.injective` `ack_strictMono_left`
`ack_injective_right` 📖	mathematical	—	`ack`	—	`StrictMono.injective` `ack_strictMono_right`
`ack_le_ack` 📖	mathematical	—	`ack`	—	`LE.le.trans` `ack_mono_left` `ack_mono_right`
`ack_le_iff_left` 📖	mathematical	—	`ack`	—	`StrictMono.le_iff_le` `ack_strictMono_left`
`ack_le_iff_right` 📖	mathematical	—	`ack`	—	`StrictMono.le_iff_le` `ack_strictMono_right`
`ack_lt_iff_left` 📖	mathematical	—	`ack`	—	`StrictMono.lt_iff_lt` `ack_strictMono_left`
`ack_lt_iff_right` 📖	mathematical	—	`ack`	—	`StrictMono.lt_iff_lt` `ack_strictMono_right`
`ack_mono_left` 📖	mathematical	—	`Monotone` `Nat.instPreorder` `ack`	—	`StrictMono.monotone` `ack_strictMono_left`
`ack_mono_right` 📖	mathematical	—	`Monotone` `Nat.instPreorder` `ack`	—	`StrictMono.monotone` `ack_strictMono_right`
`ack_one` 📖	mathematical	—	`ack`	—	`ack_succ_zero` `ack_zero` `zero_add` `ack_succ_succ`
`ack_pair_lt` 📖	mathematical	—	`ack` `Nat.pair`	—	`LT.lt.trans` `ack_strictMono_right` `Nat.pair_lt_max_add_one_sq` `ack_add_one_sq_lt_ack_add_four`
`ack_pos` 📖	mathematical	—	`ack`	—	`ack_zero` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Nat.instZeroLEOneClass` `ack_succ_zero` `ack_succ_succ`
`ack_strictMono_left` 📖	mathematical	—	`StrictMono` `Nat.instPreorder` `ack`	—	—
`ack_strictMono_right` 📖	mathematical	—	`StrictMono` `Nat.instPreorder` `ack`	—	—
`ack_succ_right_le_ack_succ_left` 📖	mathematical	—	`ack`	—	`zero_add` `ack_succ_zero` `ack_succ_succ` `ack_mono_right` `le_trans` `add_add_one_le_ack`
`ack_succ_succ` 📖	mathematical	—	`ack`	—	`ack.eq_3`
`ack_succ_zero` 📖	mathematical	—	`ack`	—	`ack.eq_2`
`ack_three` 📖	mathematical	—	`ack` `Monoid.toNatPow` `Nat.instMonoid`	—	`ack_succ_zero` `ack_succ_succ` `zero_add` `ack_zero` `ack_two` `mul_comm` `mul_le_mul_right` `Nat.instMulLeftMono` `pow_le_pow_right'` `Nat.instAtLeastTwoHAddOfNat` `two_mul`
`ack_two` 📖	mathematical	—	`ack`	—	`ack_succ_zero` `ack_succ_succ` `zero_add` `ack_zero` `MulZeroClass.mul_zero` `ack_one`
`ack_zero` 📖	mathematical	—	`ack`	—	`ack.eq_1`
`add_add_one_le_ack` 📖	mathematical	—	`ack`	—	`add_lt_ack`
`add_lt_ack` 📖	mathematical	—	`ack`	—	—
`computable₂_ack` 📖	mathematical	—	`Computable₂` `Primcodable.ofDenumerable` `Denumerable.nat` `ack`	—	`Partrec.of_eq_tot` `Partrec₂.comp₂` `Nat.Partrec.Code.eval_part` `Computable.comp` `Primrec.to_comp` `Nat.Partrec.Code.primrec_pappAck` `Computable.fst` `Computable.snd` `Nat.Partrec.Code.eval_pappAck`
`exists_lt_ack_of_nat_primrec` 📖	mathematical	—	`ack`	—	`ack_pos` `add_lt_ack` `ack_zero` `Nat.unpair_left_le` `Nat.unpair_right_le` `Nat.pair_lt_max_add_one_sq` `max_ack_left` `pow_le_pow_left'` `Nat.instMulLeftMono` `covariant_swap_mul_of_covariant_mul` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `sup_le_sup` `LT.lt.le` `ack_add_one_sq_lt_ack_add_three` `LT.lt.trans` `ack_strictMono_right` `ack_ack_lt_ack_max_add_two` `ack_strictMono_left` `LE.le.trans_lt` `le_max_left` `LT.lt.trans_le` `ack_pair_lt` `lt_or_ge` `max_eq_left` `ack_le_ack` `max_eq_right` `LE.le.trans` `add_assoc` `le_max_right` `self_le_add_left` `Nat.instCanonicallyOrderedAdd` `ack_succ_succ` `ack_mono_left` `le_rfl` `ack_mono_right` `Nat.unpair_add_le`
`lt_ack_left` 📖	mathematical	—	`ack`	—	`LE.le.trans_lt` `self_le_add_right` `Nat.instCanonicallyOrderedAdd` `add_lt_ack`
`lt_ack_right` 📖	mathematical	—	`ack`	—	`LE.le.trans_lt` `self_le_add_left` `Nat.instCanonicallyOrderedAdd` `add_lt_ack`
`max_ack_left` 📖	mathematical	—	`ack`	—	`Monotone.map_max` `ack_mono_left`
`max_ack_right` 📖	mathematical	—	`ack`	—	`Monotone.map_max` `ack_mono_right`
`not_nat_primrec_ack_self` 📖	mathematical	—	`ack`	—	`LT.lt.false`
`not_primrec_ack_self` 📖	mathematical	—	`Encodable.encode` `Option.encodable` `Primcodable.toEncodable` `Primcodable.ofDenumerable` `Denumerable.nat` `ack` `Encodable.decode`	—	`Primrec.nat_iff` `not_nat_primrec_ack_self`
`not_primrec₂_ack` 📖	mathematical	—	`Primrec₂` `Primcodable.ofDenumerable` `Denumerable.nat` `ack`	—	`not_primrec_ack_self` `Primrec₂.comp` `Primrec.id`
`one_lt_ack_succ_left` 📖	mathematical	—	`ack`	—	`zero_add` `ack_one` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Nat.instZeroLEOneClass` `ack_succ_zero` `ack_succ_succ`
`one_lt_ack_succ_right` 📖	mathematical	—	`ack`	—	`ack_zero` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Nat.instZeroLEOneClass` `one_lt_ack_succ_left`

---

← Back to Index