Supporting results for pointwise provable equality.

The table-lookup code

codeTableLookup dtable dk dq dn reads entry dn of the row of the encoded table dtable indexed by the Cantor pair of dk and dq.

A row is stored as an encoded Option (List (Option ℕ)), so the row read out of the table is an encoded Option (Option ℕ), and the two layers are flattened by codeOptionJoin. Subtracting 1 before the second lookup replaces an absent row by the empty row.

The literal construction matters: later results reason about this code itself, not only about the function it realizes over the natural numbers, so it must not be replaced by an extensionally equivalent one.

def PointwiseComposition.CategoricalRiceShapiro.Evaluator.codeOptionJoin {r : ℕ} (d : Nat.ArithPart₁.Code r) : Nat.ArithPart₁.Code r

Flatten an encoded Option (Option ℕ) to an encoded Option ℕ.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.CategoricalRiceShapiro.Evaluator.codeTableLookup {r : ℕ} (dtable dk dq dn : Nat.ArithPart₁.Code r) : Nat.ArithPart₁.Code r

Entry dn of the row of dtable indexed by the pair of dk and dq.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.codeTableLookup_eq {r : ℕ} (dtable dk dq dn : Nat.ArithPart₁.Code r) : codeTableLookup dtable dk dq dn = ArithmeticCode.codeSub (ArithmeticCode.codeListGetOptional (ArithmeticCode.codeSub (ArithmeticCode.codeListGetOptional dtable (ArithmeticCode.codePair dk dq)) (ArithmeticCode.codeConst 1)) dn) (ArithmeticCode.codeConst 1)

The table-lookup code written out without the private flattening helper.