Supporting results for pointwise provable equality.

Heterogeneous congruence for the evaluator cell

eval_codeEvaluatorCell_congr_at compares two evaluator cells written at different arities and read under different assignments. It is the analogue for codeEvaluatorCell of eval_codeBeta_congr_at, and is proved the same way: a relation saying that two codes have the same graph, each under its own assignment, is propagated through every constructor the cell is built from.

Every branch of the eager conditional is treated; none is discarded because its tag is unused. The derived constructors are delta-reduced as syntax trees only. No arithmetic meaning is attached to any of them, no totality is asserted, and the results hold in an arbitrary ORingStructure.

The partial-recursive index layer

The encoded-list layer

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.eval_codeListLength_congr_at {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} (A : Nat.ArithPart₁.Code k) (A' : Nat.ArithPart₁.Code l) (z : M) (v : Fin k → M) (v' : Fin l → M) (hA : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code A) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v')) (FFL.FirstOrder.Arithmetic.code A')) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (ArithmeticCode.codeListLength A)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v')) (FFL.FirstOrder.Arithmetic.code (ArithmeticCode.codeListLength A'))

Two encoded-list lengths agree whenever their list codes do, even at different arities and under different assignments.

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.eval_codeUnpair₁_congr_at {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} (A : Nat.ArithPart₁.Code k) (A' : Nat.ArithPart₁.Code l) (z : M) (v : Fin k → M) (v' : Fin l → M) (hA : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code A) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v')) (FFL.FirstOrder.Arithmetic.code A')) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (ArithmeticCode.codeUnpair₁ A)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v')) (FFL.FirstOrder.Arithmetic.code (ArithmeticCode.codeUnpair₁ A'))

Two first Cantor components agree whenever their argument codes do, even at different arities and under different assignments.

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.eval_codeTableLookup_congr_at {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} (dtable dk dq dn : Nat.ArithPart₁.Code k) (dtable' dk' dq' dn' : Nat.ArithPart₁.Code l) (z : M) (v : Fin k → M) (v' : Fin l → M) (hT : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code dtable) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v')) (FFL.FirstOrder.Arithmetic.code dtable')) (hK : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code dk) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v')) (FFL.FirstOrder.Arithmetic.code dk')) (hQ : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code dq) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v')) (FFL.FirstOrder.Arithmetic.code dq')) (hN : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code dn) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v')) (FFL.FirstOrder.Arithmetic.code dn')) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeTableLookup dtable dk dq dn)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v')) (FFL.FirstOrder.Arithmetic.code (codeTableLookup dtable' dk' dq' dn'))

Two table lookups agree whenever their four argument codes do, even at different arities and under different assignments.

This is the public form of the private closure above; the chain is not duplicated.

The evaluator-cell branches

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.eval_codeEvaluatorCell_congr_at {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} (dtable dn : Nat.ArithPart₁.Code k) (dtable' dn' : Nat.ArithPart₁.Code l) (z : M) (v : Fin k → M) (v' : Fin l → M) (hT : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code dtable) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v')) (FFL.FirstOrder.Arithmetic.code dtable')) (hN : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code dn) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v')) (FFL.FirstOrder.Arithmetic.code dn')) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeEvaluatorCell dtable dn)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v')) (FFL.FirstOrder.Arithmetic.code (codeEvaluatorCell dtable' dn'))

Two evaluator cells agree whenever their table and index codes do, even at different arities and under different assignments.

Every branch of the eager conditional is compared; none is discarded.