Supporting results for pointwise provable equality.
Cantor pairing #
The pairing construction inverted by codeUnpair₁ and codeUnpair₂ in
CategoricalRiceShapiro.ArithmeticCode.Arithmetic. It needs only the
conditional, not minimization, and so does not depend on that module.
Only the code construction is given here. The standard computation theorem over the natural numbers is not part of this migration.
def
PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codePair
{n : ℕ}
(d₀ d₁ : Nat.ArithPart₁.Code n)
:
Cantor pairing of d₀ and d₁.
Equations
- One or more equations did not get rendered due to their size.