Supporting results for pointwise provable equality.

PA graph laws for concrete minimization programs.

theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_rfind_code_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (f : Nat.Partrec.Code) (a y : M) : (FFL.FirstOrder.Semiformula.Evalb ![⟪a, 0⟫, y]) ↑(eventualGraph (Encodable.encode f.rfind')) ↔ (FFL.FirstOrder.Semiformula.Evalb ![⟪a, y⟫, 0]) ↑(eventualGraph (Encodable.encode f)) ∧ ∀ k < y, ∃ (z : M), z ≠ 0 ∧ (FFL.FirstOrder.Semiformula.Evalb ![⟪a, k⟫, z]) ↑(eventualGraph (Encodable.encode f))

The complete existential-stage graph of minimization from candidate zero. The candidate bound and every computation stage range over the PA model.