Supporting results for pointwise provable equality.

The evaluator-history codes

The evaluation table is extended one row at a time. codeEvaluatorRow builds the row of a table by primitive recursion on the fuel read from the table length, codeEvaluatorTableStep appends that row, and codeEvaluatorHistory iterates the step from the empty table. codeHistoryEvaluator looks one entry up in the history one step past the pair of its first two arguments, and codeEvaluatorHistoryBeforeCell names the history one step earlier.

Only the code constructions are given here. The standard computation theorems over the natural numbers are not part of this migration, and no arithmetic property of the encoding is asserted.

def PointwiseComposition.CategoricalRiceShapiro.Evaluator.codeEvaluatorRowCore {r : ℕ} (dtable : Nat.ArithPart₁.Code r) : Nat.ArithPart₁.Code (r + 1)

The recursion that builds one row of the evaluation table: at recursion argument i the cell at index k - (i + 1) is consed onto the row built so far, where k is the fuel read from the table length.

Equations

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

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

One row of the evaluation table of dtable.

Equations

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

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.codeEvaluatorRow_eq_bind {r : ℕ} (dtable : Nat.ArithPart₁.Code r) : codeEvaluatorRow dtable = ArithmeticCode.codeBind (ArithmeticCode.codeUnpair₁ (ArithmeticCode.codeListLength dtable)) (ArithmeticCode.codePrec ArithmeticCode.codeListNil (ArithmeticCode.codeListCons (codeEvaluatorCell (ArithmeticCode.codeLift (ArithmeticCode.codeLift dtable)) (ArithmeticCode.codeSub (ArithmeticCode.codeUnpair₁ (ArithmeticCode.codeListLength (ArithmeticCode.codeLift (ArithmeticCode.codeLift dtable)))) (ArithmeticCode.codeSucc (Nat.ArithPart₁.Code.proj 0)))) (Nat.ArithPart₁.Code.proj 1)))

codeEvaluatorRow binds the fuel read from the table length as the recursion argument of one fixed arity-r + 1 code.

The recursion is an implementation detail and stays private; a proof reaches it by rewriting with this equation.

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

Extend the evaluation table by one row.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.Evaluator.codeEvaluatorHistory : Nat.ArithPart₁.Code 1

The evaluation table after the number of steps given by the argument.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.Evaluator.codeEvaluatorHistoryBeforeCell : Nat.ArithPart₁.Code 3

The evaluation history one step before the one codeHistoryEvaluator reads: the history at the pair of the first two arguments.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.Evaluator.codeHistoryEvaluator : Nat.ArithPart₁.Code 3

Look up entry n of the row of k and q in the history one step past the pair of k and q.

Equations

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