Supporting results for pointwise provable equality.
Compatibility results for Foundation's arithmetic codes #
Foundation defines FFL.FirstOrder.Arithmetic.code, the arithmetic formula
associated with a partial-recursive code Nat.ArithPart₁.Code k, together with
its auxiliary formula codeAux. Foundation's own uniqueness statements for
these formulas are dormant source at the recorded revision, so this module
supplies the corresponding active result.
eval_unique states that the evaluation relation of an arithmetic code is
functional in every model of 𝐏𝐀⁻, under an arbitrary assignment.
theorem
PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_unique
{M : Type u_1}
[FFL.ORingStructure M]
[M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻]
{k : ℕ}
{c : Nat.ArithPart₁.Code k}
{v : Fin k → M}
{z z' : M}
(hz : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code c))
(hz' : (FFL.FirstOrder.Semiformula.Evalb (z' :> v)) (FFL.FirstOrder.Arithmetic.code c))
: