Documentation

LeanPool.PointwiseComposition.FailureOfComposition.ConcreteAdequacy

Supporting results for pointwise provable equality.

Standard-model adequacy of the concrete evaluator graph.

source
def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.stageComputation (s q x y : ℕ) :
Prop

The accepted computation formula interpreted over the natural numbers.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.stageComputation_iff_evaln (s : ℕ) (c : Nat.Partrec.Code) (x y : ℕ) :
    stageComputation s (Encodable.encode c) x y ↔ y ∈ Nat.Partrec.Code.evaln s c x

    Exact finite-stage correspondence with Mathlib's evaluator.

    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_adequate (q x y : ℕ) :
    (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(eventualGraph q) ↔ y ∈ Kleene.eval q x

    Standard-model adequacy of the PA-arithmetized graph for the actual Mathlib program numbering. Every direction is proved for every program index.

    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_normal_form (q x y : ℕ) :
    (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(eventualGraph q) ↔ ∃ (w : ℕ), Kleene.T₁ q x w ∧ Kleene.U w = y

    The graph arithmetized in PA has precisely the existing Kleene T₁,U normal form over the standard natural numbers.