Supporting results for pointwise provable equality.

Arithmetic programs for the direct computation-search obstruction. The checked function is the existing history evaluator at the diagonal input. All graph equations in this file concern arbitrary PA-model inputs, not only numerals.

def PointwiseComposition.FailureOfComposition.HistoryWitnesses.historyCode (d : ℕ) : Nat.ArithPart₁.Code 1

The history Code construction in FailureOfComposition.HistoryWitnesses.

Equations

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

def PointwiseComposition.FailureOfComposition.HistoryWitnesses.guardCode (d : ℕ) : Nat.ArithPart₁.Code 1

The guard Code construction in FailureOfComposition.HistoryWitnesses.

Equations

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

def PointwiseComposition.FailureOfComposition.HistoryWitnesses.searchCode (d : ℕ) : Nat.ArithPart₁.Code 1

The search Code construction in FailureOfComposition.HistoryWitnesses.

Equations

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

def PointwiseComposition.FailureOfComposition.HistoryWitnesses.rawHistoryGraph (d : ℕ) : ProofSearch.Graph

The raw History Graph construction in FailureOfComposition.HistoryWitnesses.

Equations

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

def PointwiseComposition.FailureOfComposition.HistoryWitnesses.historyGraph (d : ℕ) : ProofSearch.Graph

The history Graph construction in FailureOfComposition.HistoryWitnesses.

Equations

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

def PointwiseComposition.FailureOfComposition.HistoryWitnesses.guardGraph (d : ℕ) : ProofSearch.Graph

The guard Graph construction in FailureOfComposition.HistoryWitnesses.

Equations

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

def PointwiseComposition.FailureOfComposition.HistoryWitnesses.searchGraph (d : ℕ) : ProofSearch.Graph

The search Graph construction in FailureOfComposition.HistoryWitnesses.

Equations

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

@[simp]

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.guardGraph_eval {M : Type u_1} [FFL.ORingStructure M] (d : ℕ) (v : Fin 2 → M) : (FFL.FirstOrder.Semiformula.Evalb v) ↑(guardGraph d) ↔ (FFL.FirstOrder.Semiformula.Evalb ![v 0, 0]) ↑(historyGraph d) ∧ v 1 = v 0

@[simp]

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.searchGraph_eval {M : Type u_1} [FFL.ORingStructure M] (d : ℕ) (v : Fin 2 → M) : (FFL.FirstOrder.Semiformula.Evalb v) ↑(searchGraph d) ↔ (∃ (z : M), 0 < z ∧ (FFL.FirstOrder.Semiformula.Evalb ![v 1, z]) ↑(historyGraph d)) ∧ ∀ r < v 1, (FFL.FirstOrder.Semiformula.Evalb ![r, 0]) ↑(historyGraph d)

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.eval_rfind_iff {M : Type u_1} [FFL.ORingStructure M] {n : ℕ} (c : Nat.ArithPart₁.Code (n + 1)) (y : M) (v : Fin n → M) : (FFL.FirstOrder.Semiformula.Evalb (y :> v)) (FFL.FirstOrder.Arithmetic.code c.rfind) ↔ (FFL.FirstOrder.Semiformula.Evalb (0 :> y :> v)) (FFL.FirstOrder.Arithmetic.code c) ∧ ∀ r < y, ∃ (z : M), z ≠ 0 ∧ (FFL.FirstOrder.Semiformula.Evalb (z :> r :> v)) (FFL.FirstOrder.Arithmetic.code c)

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.historyCode_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (d : ℕ) (s z : M) : (FFL.FirstOrder.Semiformula.Evalb ![z, s]) (FFL.FirstOrder.Arithmetic.code (historyCode d)) ↔ (FFL.FirstOrder.Semiformula.Evalb ![z, s, ↑d, ↑d]) (FFL.FirstOrder.Arithmetic.code CategoricalRiceShapiro.Evaluator.codeHistoryEvaluator)

@[simp]

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.historyGraph_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (d : ℕ) (s z : M) : (FFL.FirstOrder.Semiformula.Evalb ![s, z]) ↑(historyGraph d) ↔ (FFL.FirstOrder.Semiformula.Evalb ![z, s, ↑d, ↑d]) (FFL.FirstOrder.Arithmetic.code CategoricalRiceShapiro.Evaluator.codeHistoryEvaluator)

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.history_total {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (d : ℕ) (s : M) : ∃ (z : M), (FFL.FirstOrder.Semiformula.Evalb ![s, z]) ↑(historyGraph d)

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.history_unique {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (d : ℕ) (s a b : M) (ha : (FFL.FirstOrder.Semiformula.Evalb ![s, a]) ↑(historyGraph d)) (hb : (FFL.FirstOrder.Semiformula.Evalb ![s, b]) ↑(historyGraph d)) : a = b

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.headHistory_eval {M : Type u_1} [FFL.ORingStructure M] (d : ℕ) (s x z : M) : (FFL.FirstOrder.Semiformula.Evalb ![z, s, x]) (FFL.FirstOrder.Arithmetic.code ((historyCode d).comp ![Nat.ArithPart₁.Code.proj 0])) ↔ (FFL.FirstOrder.Semiformula.Evalb ![z, s]) (FFL.FirstOrder.Arithmetic.code (historyCode d))

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.guardCode_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (d : ℕ) (x y : M) : (FFL.FirstOrder.Semiformula.Evalb ![y, x]) (FFL.FirstOrder.Arithmetic.code (guardCode d)) ↔ (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(guardGraph d)

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.searchCode_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (d : ℕ) (x y : M) : (FFL.FirstOrder.Semiformula.Evalb ![y, x]) (FFL.FirstOrder.Arithmetic.code (searchCode d)) ↔ (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(searchGraph d)

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.guard_functional (d : ℕ) : ProofSearch.Functional (guardGraph d)

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.search_functional (d : ℕ) : ProofSearch.Functional (searchGraph d)

theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.guard_search_empty (d : ℕ) : ProofSearch.Uniform 𝐏𝐀 (ProofSearch.comp (guardGraph d) (searchGraph d)) ProofSearch.empty