Supporting results for pointwise provable equality.

The evaluator-cell code

One cell of the evaluation table. The table length names the pair (k, q): k is the fuel and q the partial-recursive index under evaluation. For positive fuel the constructor number of q selects a branch — 4 pairing, 5 composition, 6 primitive recursion, 7 minimization — and every other constructor number falls through to codeBaseEvaluatorCell, which decides the four base constructors. Branches 6 and 7 receive predecessor fuel and the whole index q; branch 7 reads the entire payload rather than its first component. No comparison of the argument with the fuel occurs.

The conditional is arithmetic and eager: codeIfPos evaluates both branches. Only the code constructions are given here. The standard computation theorems over the natural numbers are not part of this migration.

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

The cell for one of the four base constructors.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.Evaluator.codePairEvaluatorCell {r : ℕ} (dtable dk dcf dcg dn : Nat.ArithPart₁.Code r) : Nat.ArithPart₁.Code r

The cell for the pairing constructor.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.Evaluator.codeCompEvaluatorCell {r : ℕ} (dtable dk dcf dcg dn : Nat.ArithPart₁.Code r) : Nat.ArithPart₁.Code r

The cell for the composition constructor: the inner index dcg is applied to the argument, and the outer index dcf to the result.

Equations

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

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

The cell for the primitive-recursion constructor.

Equations

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

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

The cell for the minimization constructor.

Equations

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

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

One evaluator cell: fuel and index are read from the table length, and the constructor number of the index selects the branch.

Equations

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