Supporting results for pointwise provable equality.

Functional Sigma-one witnesses for adjoining composition to pointwise equality. The first witness records the least successful evaluator stage and the input; the other two read that computation, with an optional second graph condition.

def PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.stageGraph (e : ℕ) : Σ₁.Semisentence 3

The stage Graph construction in FailureOfComposition.GeneratedWitnessGraphs.

Equations

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

def PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.failureGraph (e : ℕ) : ProofSearch.Graph

The failure Graph construction in FailureOfComposition.GeneratedWitnessGraphs.

Equations

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

def PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.leastGraph (e : ℕ) : ProofSearch.Graph

The least Graph construction in FailureOfComposition.GeneratedWitnessGraphs.

Equations

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

def PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.HGraph (e : ℕ) : ProofSearch.Graph

The HGraph construction in FailureOfComposition.GeneratedWitnessGraphs.

Equations

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

def PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.BGraph (e : ℕ) : ProofSearch.Graph

The BGraph construction in FailureOfComposition.GeneratedWitnessGraphs.

Equations

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

def PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.AGraph (e : ℕ) (G : ProofSearch.Graph) : ProofSearch.Graph

The AGraph construction in FailureOfComposition.GeneratedWitnessGraphs.

Equations

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

def PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.intersection (F G : ProofSearch.Graph) : ProofSearch.Graph

The intersection construction in FailureOfComposition.GeneratedWitnessGraphs.

Equations

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

@[simp]

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.stageGraph_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (s x y : M) : (FFL.FirstOrder.Semiformula.Evalb ![s, x, y]) ↑(stageGraph e) ↔ (FFL.FirstOrder.Semiformula.Evalb ![s, ↑e, x, y]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula

@[simp]

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.failureGraph_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (s x : M) : (FFL.FirstOrder.Semiformula.Evalb ![s, x]) ↑(failureGraph e) ↔ (FFL.FirstOrder.Semiformula.Evalb ![0, s, ↑e, x]) (FFL.FirstOrder.Arithmetic.code CategoricalRiceShapiro.Evaluator.codeHistoryEvaluator)

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.stage_of_history {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (s x y : M) : (FFL.FirstOrder.Semiformula.Evalb ![s, x, y]) ↑(stageGraph e) ↔ (FFL.FirstOrder.Semiformula.Evalb ![y + 1, s, ↑e, x]) (FFL.FirstOrder.Arithmetic.code CategoricalRiceShapiro.Evaluator.codeHistoryEvaluator)

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

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.stage_implies_eventual {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (s x y : M) (h : (FFL.FirstOrder.Semiformula.Evalb ![s, x, y]) ↑(stageGraph e)) : (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(ConcreteEvaluator.eventualGraph e)

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

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.failure_iff_no_stage {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (s x : M) : (FFL.FirstOrder.Semiformula.Evalb ![s, x]) ↑(failureGraph e) ↔ ¬∃ (y : M), (FFL.FirstOrder.Semiformula.Evalb ![s, x, y]) ↑(stageGraph e)

@[simp]

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.leastGraph_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (x s : M) : (FFL.FirstOrder.Semiformula.Evalb ![x, s]) ↑(leastGraph e) ↔ (∃ (y : M), (FFL.FirstOrder.Semiformula.Evalb ![s, x, y]) ↑(stageGraph e)) ∧ ∀ r < s, (FFL.FirstOrder.Semiformula.Evalb ![r, x]) ↑(failureGraph e)

@[simp]

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.HGraph_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (x n : M) : (FFL.FirstOrder.Semiformula.Evalb ![x, n]) ↑(HGraph e) ↔ ∃ (s : M), (FFL.FirstOrder.Semiformula.Evalb ![x, s]) ↑(leastGraph e) ∧ n = ⟪s, x⟫

@[simp]

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.BGraph_pair_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (s x y : M) : (FFL.FirstOrder.Semiformula.Evalb ![⟪s, x⟫, y]) ↑(BGraph e) ↔ (FFL.FirstOrder.Semiformula.Evalb ![s, x, y]) ↑(stageGraph e)

@[simp]

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.AGraph_pair_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (G : ProofSearch.Graph) (s x y : M) : (FFL.FirstOrder.Semiformula.Evalb ![⟪s, x⟫, y]) ↑(AGraph e G) ↔ (FFL.FirstOrder.Semiformula.Evalb ![s, x, y]) ↑(stageGraph e) ∧ (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑G

@[simp]

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.intersection_eval {M : Type u_1} [FFL.ORingStructure M] (F G : ProofSearch.Graph) (x y : M) : (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(intersection F G) ↔ (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑F ∧ (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑G

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.leastGraph_unique {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (x s t : M) (hs : (FFL.FirstOrder.Semiformula.Evalb ![x, s]) ↑(leastGraph e)) (ht : (FFL.FirstOrder.Semiformula.Evalb ![x, t]) ↑(leastGraph e)) : s = t

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.leastGraph_exists {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (x y : M) (hy : (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(ConcreteEvaluator.eventualGraph e)) : ∃ (s : M), (FFL.FirstOrder.Semiformula.Evalb ![x, s]) ↑(leastGraph e) ∧ (FFL.FirstOrder.Semiformula.Evalb ![s, x, y]) ↑(stageGraph e)

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.B_comp_H_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (x y : M) : (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(ProofSearch.comp (BGraph e) (HGraph e)) ↔ (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(ConcreteEvaluator.eventualGraph e)

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.A_comp_H_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (e : ℕ) (G : ProofSearch.Graph) (x y : M) : (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(ProofSearch.comp (AGraph e G) (HGraph e)) ↔ (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(intersection (ConcreteEvaluator.eventualGraph e) G)

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.intersection_functional (F G : ProofSearch.Graph) (hF : ProofSearch.Functional F) : ProofSearch.Functional (intersection F G)

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.intersection_comm_uniform (F G : ProofSearch.Graph) : ProofSearch.Uniform 𝐏𝐀 (intersection F G) (intersection G F)

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.HGraph_functional (e : ℕ) : ProofSearch.Functional (HGraph e)

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.BGraph_functional (e : ℕ) : ProofSearch.Functional (BGraph e)

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.AGraph_functional (e : ℕ) (G : ProofSearch.Graph) : ProofSearch.Functional (AGraph e G)

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.B_comp_H (e : ℕ) : ProofSearch.Uniform 𝐏𝐀 (ProofSearch.comp (BGraph e) (HGraph e)) (ConcreteEvaluator.eventualGraph e)

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.A_comp_H (e : ℕ) (G : ProofSearch.Graph) : ProofSearch.Uniform 𝐏𝐀 (ProofSearch.comp (AGraph e G) (HGraph e)) (intersection (ConcreteEvaluator.eventualGraph e) G)