Supporting results for pointwise provable equality.

Evaluation of arithmetic codes in an arbitrary model

Every result in this module describes Semiformula.Evalb for the arithmetic formula FFL.FirstOrder.Arithmetic.code c under an arbitrary assignment in an arbitrary structure.

Two results assume a model of 𝐏𝐀⁻. eval_codeConst states the value of a constant code, and needs that assumption already for the numeral cast (m : M). eval_codeConst_iff characterises that value, and additionally uses evaluator functionality (eval_unique, proved in CategoricalRiceShapiro.ArithmeticCode.FoundationCompat, which also assumes 𝐏𝐀⁻). Every other evaluation result in this module assumes only ORingStructure M.

The equivalences for the primitive constructors and for composition are the reusable core; the derived constructors and the congruence law under a composed-code context are proved from them.

Primitive constructors

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_zero_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (Nat.ArithPart₁.Code.zero k)) ↔ z = 0

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_one_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (Nat.ArithPart₁.Code.one k)) ↔ z = 1

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_proj_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (i : Fin k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (Nat.ArithPart₁.Code.proj i)) ↔ z = v i

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_add_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (i j : Fin k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (Nat.ArithPart₁.Code.add i j)) ↔ z = v i + v j

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_mul_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (i j : Fin k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (Nat.ArithPart₁.Code.mul i j)) ↔ z = v i * v j

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_equal_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (i j : Fin k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (Nat.ArithPart₁.Code.equal i j)) ↔ v i = v j ∧ z = 1 ∨ ¬v i = v j ∧ z = 0

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_lt_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (i j : Fin k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (Nat.ArithPart₁.Code.lt i j)) ↔ v i < v j ∧ z = 1 ∨ ¬v i < v j ∧ z = 0

Composition

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_comp_iff {M : Type u_1} [FFL.ORingStructure M] {m k : ℕ} (c : Nat.ArithPart₁.Code m) (d : Fin m → Nat.ArithPart₁.Code k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (c.comp d)) ↔ ∃ (w : Fin m → M), (FFL.FirstOrder.Semiformula.Evalb (z :> w)) (FFL.FirstOrder.Arithmetic.code c) ∧ ∀ (i : Fin m), (FFL.FirstOrder.Semiformula.Evalb (w i :> v)) (FFL.FirstOrder.Arithmetic.code (d i))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_comp₂_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (c : Nat.ArithPart₁.Code 2) (A B : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (c.comp ![A, B])) ↔ ∃ (e : Fin 2 → M), (FFL.FirstOrder.Semiformula.Evalb (z :> e)) (FFL.FirstOrder.Arithmetic.code c) ∧ (FFL.FirstOrder.Semiformula.Evalb (e 0 :> v)) (FFL.FirstOrder.Arithmetic.code A) ∧ (FFL.FirstOrder.Semiformula.Evalb (e 1 :> v)) (FFL.FirstOrder.Arithmetic.code B)

Derived constructors

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeAdd_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A B : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeAdd A B)) ↔ ∃ (a : M) (b : M), (FFL.FirstOrder.Semiformula.Evalb (a :> v)) (FFL.FirstOrder.Arithmetic.code A) ∧ (FFL.FirstOrder.Semiformula.Evalb (b :> v)) (FFL.FirstOrder.Arithmetic.code B) ∧ z = a + b

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeMul_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A B : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeMul A B)) ↔ ∃ (a : M) (b : M), (FFL.FirstOrder.Semiformula.Evalb (a :> v)) (FFL.FirstOrder.Arithmetic.code A) ∧ (FFL.FirstOrder.Semiformula.Evalb (b :> v)) (FFL.FirstOrder.Arithmetic.code B) ∧ z = a * b

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeEq_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A B : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeEq A B)) ↔ ∃ (a : M) (b : M), (FFL.FirstOrder.Semiformula.Evalb (a :> v)) (FFL.FirstOrder.Arithmetic.code A) ∧ (FFL.FirstOrder.Semiformula.Evalb (b :> v)) (FFL.FirstOrder.Arithmetic.code B) ∧ (a = b ∧ z = 1 ∨ ¬a = b ∧ z = 0)

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeLt_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A B : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeLt A B)) ↔ ∃ (a : M) (b : M), (FFL.FirstOrder.Semiformula.Evalb (a :> v)) (FFL.FirstOrder.Arithmetic.code A) ∧ (FFL.FirstOrder.Semiformula.Evalb (b :> v)) (FFL.FirstOrder.Arithmetic.code B) ∧ (a < b ∧ z = 1 ∨ ¬a < b ∧ z = 0)

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeSucc_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeSucc A)) ↔ ∃ (a : M), (FFL.FirstOrder.Semiformula.Evalb (a :> v)) (FFL.FirstOrder.Arithmetic.code A) ∧ z = a + 1

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codePos_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codePos A)) ↔ ∃ (a : M), (FFL.FirstOrder.Semiformula.Evalb (a :> v)) (FFL.FirstOrder.Arithmetic.code A) ∧ (0 < a ∧ z = 1 ∨ ¬0 < a ∧ z = 0)

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeInv_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeInv A)) ↔ ∃ (a : M), (FFL.FirstOrder.Semiformula.Evalb (a :> v)) (FFL.FirstOrder.Arithmetic.code A) ∧ (a = 0 ∧ z = 1 ∨ ¬a = 0 ∧ z = 0)

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeAnd_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A B : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeAnd A B)) ↔ ∃ (a : M) (b : M), (FFL.FirstOrder.Semiformula.Evalb (a :> v)) (FFL.FirstOrder.Arithmetic.code A) ∧ (FFL.FirstOrder.Semiformula.Evalb (b :> v)) (FFL.FirstOrder.Arithmetic.code B) ∧ (0 < a * b ∧ z = 1 ∨ ¬0 < a * b ∧ z = 0)

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeOr_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A B : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeOr A B)) ↔ ∃ (a : M) (b : M), (FFL.FirstOrder.Semiformula.Evalb (a :> v)) (FFL.FirstOrder.Arithmetic.code A) ∧ (FFL.FirstOrder.Semiformula.Evalb (b :> v)) (FFL.FirstOrder.Arithmetic.code B) ∧ (0 < a + b ∧ z = 1 ∨ ¬0 < a + b ∧ z = 0)

Weakening and constants

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeHead_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (z : M) (w : Fin (k + 1) → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> w)) (FFL.FirstOrder.Arithmetic.code codeHead) ↔ z = w 0

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeLift_iff {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (d : Nat.ArithPart₁.Code k) (z t : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> t :> v)) (FFL.FirstOrder.Arithmetic.code (codeLift d)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code d)

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeConst {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} (m : ℕ) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (↑m :> v)) (FFL.FirstOrder.Arithmetic.code (codeConst m))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeConst_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} (m : ℕ) (z : M) (v : Fin k → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeConst m)) ↔ z = ↑m

Bridges between a graph and a constant

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_iff_codeConst_of_eval {M : Type u_2} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {r : ℕ} (d : Nat.ArithPart₁.Code r) (m : ℕ) (v : Fin r → M) (hd : (FFL.FirstOrder.Semiformula.Evalb (↑m :> v)) (FFL.FirstOrder.Arithmetic.code d)) (z : M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code d) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeConst m))

A code whose graph holds at the standard value m under the assignment v has, at that same assignment, exactly the graph of the constant code m.

The hypothesis is one instance of the graph; functionality of evaluation turns it into the full equivalence.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeLift_codeConst_iff {M : Type u_2} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {r : ℕ} (m : ℕ) (z t : M) (v : Fin r → M) : (FFL.FirstOrder.Semiformula.Evalb (z :> t :> v)) (FFL.FirstOrder.Arithmetic.code (codeLift (codeConst m))) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> t :> v)) (FFL.FirstOrder.Arithmetic.code (codeConst m))

Lifting a constant code past one argument is the constant code of the larger arity.

Graph agreement across arities and assignments

@[reducible, inline]

abbrev PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.EvalEq {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} (A : Nat.ArithPart₁.Code k) (v : Fin k → M) (A' : Nat.ArithPart₁.Code l) (v' : Fin l → M) : Prop

Two codes have the same graph, each under its own assignment.

Equations

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

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_proj {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} (i : Fin k) (j : Fin l) (v : Fin k → M) (v' : Fin l → M) (h : v i = v' j) : EvalEq (Nat.ArithPart₁.Code.proj i) v (Nat.ArithPart₁.Code.proj j) v'

Projections agree when the selected assignment entries agree.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_zero {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} (v : Fin k → M) (v' : Fin l → M) : EvalEq (Nat.ArithPart₁.Code.zero k) v (Nat.ArithPart₁.Code.zero l) v'

Zero codes have the same graph under any two assignments.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_codeHead {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} (t : M) (v : Fin k → M) (v' : Fin l → M) : EvalEq codeHead (t :> v) codeHead (t :> v')

Head codes agree under assignments with the same head.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_codeSucc {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} {A : Nat.ArithPart₁.Code k} {A' : Nat.ArithPart₁.Code l} {v : Fin k → M} {v' : Fin l → M} (hA : EvalEq A v A' v') : EvalEq (codeSucc A) v (codeSucc A') v'

Successor-code construction preserves heterogeneous graph agreement.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_codePos {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} {A : Nat.ArithPart₁.Code k} {A' : Nat.ArithPart₁.Code l} {v : Fin k → M} {v' : Fin l → M} (hA : EvalEq A v A' v') : EvalEq (codePos A) v (codePos A') v'

Positive-test code construction preserves heterogeneous graph agreement.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_codeInv {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} {A : Nat.ArithPart₁.Code k} {A' : Nat.ArithPart₁.Code l} {v : Fin k → M} {v' : Fin l → M} (hA : EvalEq A v A' v') : EvalEq (codeInv A) v (codeInv A') v'

Boolean-inverse code construction preserves heterogeneous graph agreement.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_codeAdd {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} {A B : Nat.ArithPart₁.Code k} {A' B' : Nat.ArithPart₁.Code l} {v : Fin k → M} {v' : Fin l → M} (hA : EvalEq A v A' v') (hB : EvalEq B v B' v') : EvalEq (codeAdd A B) v (codeAdd A' B') v'

Addition-code construction preserves heterogeneous graph agreement.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_codeMul {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} {A B : Nat.ArithPart₁.Code k} {A' B' : Nat.ArithPart₁.Code l} {v : Fin k → M} {v' : Fin l → M} (hA : EvalEq A v A' v') (hB : EvalEq B v B' v') : EvalEq (codeMul A B) v (codeMul A' B') v'

Multiplication-code construction preserves heterogeneous graph agreement.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_codeEq {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} {A B : Nat.ArithPart₁.Code k} {A' B' : Nat.ArithPart₁.Code l} {v : Fin k → M} {v' : Fin l → M} (hA : EvalEq A v A' v') (hB : EvalEq B v B' v') : EvalEq (codeEq A B) v (codeEq A' B') v'

Equality-test code construction preserves heterogeneous graph agreement.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_codeLt {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} {A B : Nat.ArithPart₁.Code k} {A' B' : Nat.ArithPart₁.Code l} {v : Fin k → M} {v' : Fin l → M} (hA : EvalEq A v A' v') (hB : EvalEq B v B' v') : EvalEq (codeLt A B) v (codeLt A' B') v'

Order-test code construction preserves heterogeneous graph agreement.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_codeAnd {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} {A B : Nat.ArithPart₁.Code k} {A' B' : Nat.ArithPart₁.Code l} {v : Fin k → M} {v' : Fin l → M} (hA : EvalEq A v A' v') (hB : EvalEq B v B' v') : EvalEq (codeAnd A B) v (codeAnd A' B') v'

Conjunction-code construction preserves heterogeneous graph agreement.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_codeOr {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} {A B : Nat.ArithPart₁.Code k} {A' B' : Nat.ArithPart₁.Code l} {v : Fin k → M} {v' : Fin l → M} (hA : EvalEq A v A' v') (hB : EvalEq B v B' v') : EvalEq (codeOr A B) v (codeOr A' B') v'

Disjunction-code construction preserves heterogeneous graph agreement.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_codeLift {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} {A : Nat.ArithPart₁.Code k} {A' : Nat.ArithPart₁.Code l} {v : Fin k → M} {v' : Fin l → M} (t t' : M) (hA : EvalEq A v A' v') : EvalEq (codeLift A) (t :> v) (codeLift A') (t' :> v')

A lift ignores its head, so the two heads need not agree.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_one {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} (v : Fin k → M) (v' : Fin l → M) : EvalEq (Nat.ArithPart₁.Code.one k) v (Nat.ArithPart₁.Code.one l) v'

One codes have the same graph under any two assignments.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_comp {M : Type u_1} [FFL.ORingStructure M] {k l m : ℕ} (c : Nat.ArithPart₁.Code m) (ds : Fin m → Nat.ArithPart₁.Code k) (ds' : Fin m → Nat.ArithPart₁.Code l) {v : Fin k → M} {v' : Fin l → M} (h : ∀ (i : Fin m), EvalEq (ds i) v (ds' i) v') : EvalEq (c.comp ds) v (c.comp ds') v'

Composition with a shared outer code.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.evalEq_codeConst {M : Type u_1} [FFL.ORingStructure M] {k l : ℕ} (m : ℕ) (v : Fin k → M) (v' : Fin l → M) : EvalEq (codeConst m) v (codeConst m) v'

Constant codes agree under assignments of any arities.

Valuation-local congruence for the derived constructors

Each lemma below fixes one assignment v and transports an equivalence of the argument codes, quantified over the possible argument values, to an equivalence of the constructed codes. No assignment other than v occurs, and no model assumption beyond ORingStructure M is used. Composition is already covered by eval_comp_congr.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_comp_congr {M : Type u_1} [FFL.ORingStructure M] {m k : ℕ} (c : Nat.ArithPart₁.Code m) (d e : Fin m → Nat.ArithPart₁.Code k) (z : M) (v : Fin k → M) (h : ∀ (i : Fin m) (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code (d i)) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code (e i))) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (c.comp d)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (c.comp e))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeSucc_congr {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A A' : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → 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 (codeSucc A)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeSucc A'))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codePos_congr {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A A' : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → 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 (codePos A)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codePos A'))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeInv_congr {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A A' : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → 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 (codeInv A)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeInv A'))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeAdd_congr {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A A' B B' : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → 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')) (hB : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code B) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code B')) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeAdd A B)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeAdd A' B'))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeMul_congr {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A A' B B' : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → 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')) (hB : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code B) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code B')) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeMul A B)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeMul A' B'))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeEq_congr {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A A' B B' : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → 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')) (hB : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code B) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code B')) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeEq A B)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeEq A' B'))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeLt_congr {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A A' B B' : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → 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')) (hB : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code B) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code B')) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeLt A B)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeLt A' B'))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeAnd_congr {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A A' B B' : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → 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')) (hB : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code B) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code B')) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeAnd A B)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeAnd A' B'))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeOr_congr {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A A' B B' : Nat.ArithPart₁.Code k) (z : M) (v : Fin k → 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')) (hB : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code B) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code B')) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeOr A B)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeOr A' B'))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeLift_congr {M : Type u_1} [FFL.ORingStructure M] {k : ℕ} (A A' : Nat.ArithPart₁.Code k) (z t : M) (v : Fin k → 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 :> t :> v)) (FFL.FirstOrder.Arithmetic.code (codeLift A)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> t :> v)) (FFL.FirstOrder.Arithmetic.code (codeLift A'))

An equivalence at v lifts to an equivalence at every assignment extending v by one value.