Supporting results for pointwise provable equality.

Program graphs indexed by actual Mathlib program descriptions.

@[reducible, inline]

abbrev PointwiseComposition.FailureOfComposition.ProgramGraph.PCode : Type

The PCode construction in FailureOfComposition.ProgramGraph.

Equations

• PointwiseComposition.FailureOfComposition.ProgramGraph.PCode = Nat.Partrec.Code

def PointwiseComposition.FailureOfComposition.ProgramGraph.Computes {M : Type u_1} [FFL.ORingStructure M] (c : PCode) (x y : M) : Prop

The Computes construction in FailureOfComposition.ProgramGraph.

Equations

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

theorem PointwiseComposition.FailureOfComposition.ProgramGraph.computes_comp {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (f g : PCode) (x z : M) : Computes (Nat.Partrec.Code.comp f g) x z ↔ ∃ (y : M), Computes g x y ∧ Computes f y z

theorem PointwiseComposition.FailureOfComposition.ProgramGraph.computes_zero {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (x y : M) : Computes Nat.Partrec.Code.zero x y ↔ y = 0

theorem PointwiseComposition.FailureOfComposition.ProgramGraph.computes_succ {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (x y : M) : Computes Nat.Partrec.Code.succ x y ↔ y = x + 1

theorem PointwiseComposition.FailureOfComposition.ProgramGraph.computes_left {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (x y : M) : Computes Nat.Partrec.Code.left x y ↔ y = π₁ x

theorem PointwiseComposition.FailureOfComposition.ProgramGraph.computes_right {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (x y : M) : Computes Nat.Partrec.Code.right x y ↔ y = π₂ x

theorem PointwiseComposition.FailureOfComposition.ProgramGraph.computes_id {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (x y : M) : Computes Nat.Partrec.Code.id x y ↔ y = x

theorem PointwiseComposition.FailureOfComposition.ProgramGraph.computes_pair {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (f g : PCode) (x z : M) : Computes (Nat.Partrec.Code.pair f g) x z ↔ ∃ (a : M) (b : M), Computes f x a ∧ Computes g x b ∧ z = ⟪a, b⟫

theorem PointwiseComposition.FailureOfComposition.ProgramGraph.computes_const {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (n : ℕ) (x y : M) : Computes (Nat.Partrec.Code.const n) x y ↔ y = ↑n

theorem PointwiseComposition.FailureOfComposition.ProgramGraph.computes_unique {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (c : PCode) (x y z : M) (hy : Computes c x y) (hz : Computes c x z) : y = z