Supporting results for pointwise provable equality.

Extracting an output from a semidecision program for a functional arithmetic graph. The search ranges over candidate outputs together with computation stages, so divergent rejected candidates do not block later outputs.

def PointwiseComposition.FailureOfComposition.SigmaOneRealization.reorderProgram (c : ProgramGraph.PCode) : ProgramGraph.PCode

Convert a candidate/input pair into the graph's input/output vector.

Equations

• PointwiseComposition.FailureOfComposition.SigmaOneRealization.reorderProgram c = Nat.Partrec.Code.comp c (Nat.Partrec.Code.right.pair (Nat.Partrec.Code.left.pair Nat.Partrec.Code.zero))

def PointwiseComposition.FailureOfComposition.SigmaOneRealization.graphProgram (c : ProgramGraph.PCode) : ProgramGraph.PCode

Search the graph semidecision program and return its successful output.

Equations

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

theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.computes_reorder {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : ProgramGraph.PCode) (x y z : M) : ProgramGraph.Computes (reorderProgram c) ⟪y, x⟫ z ↔ ProgramGraph.Computes c (ArithmeticCodeCompiler.encodeVector ![x, y]) z

theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.realize_of_semidecides (F : ProofSearch.Graph) (hF : ProofSearch.Functional F) (c : ProgramGraph.PCode) (hc : Semidecides (↑F) c) : ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph (Encodable.encode (graphProgram c))) F

A semidecision program for a PA-functional graph yields an actual program whose graph PA proves uniformly equivalent to the original graph.