Supporting results for pointwise provable equality.

Concrete natural-number indices for the direct computation-search construction. The graph equations proved here are standard-model equations. Their PA-provable counterparts for the repository's arithmetized evaluator remain a separate task.

noncomputable def PointwiseComposition.FailureOfComposition.Kleene.indexOf (f : ℕ → Part ℕ) (hf : Partrec f) : ℕ

The index Of construction in FailureOfComposition.Kleene.

Equations

• PointwiseComposition.FailureOfComposition.Kleene.indexOf f hf = Encodable.encode (Classical.choose ⋯)

theorem PointwiseComposition.FailureOfComposition.Kleene.eval_indexOf (f : ℕ → Part ℕ) (hf : Partrec f) (x : ℕ) : eval (indexOf f hf) x = f x

def PointwiseComposition.FailureOfComposition.Kleene.guardEval (d n : ℕ) : Part ℕ

The guard Eval construction in FailureOfComposition.Kleene.

Equations

• PointwiseComposition.FailureOfComposition.Kleene.guardEval d n = ↑(if PointwiseComposition.FailureOfComposition.Kleene.T₁ d d n then none else some n)

def PointwiseComposition.FailureOfComposition.Kleene.searchEval (d _x : ℕ) : Part ℕ

The search Eval construction in FailureOfComposition.Kleene.

Equations

• PointwiseComposition.FailureOfComposition.Kleene.searchEval d _x = Nat.rfind fun (n : ℕ) => Part.some (decide (PointwiseComposition.FailureOfComposition.Kleene.T₁ d d n))

theorem PointwiseComposition.FailureOfComposition.Kleene.check_primrec (d : ℕ) : PrimrecPred (T₁ d d)

theorem PointwiseComposition.FailureOfComposition.Kleene.guardEval_partrec (d : ℕ) : Partrec (guardEval d)

theorem PointwiseComposition.FailureOfComposition.Kleene.searchEval_partrec (d : ℕ) : Partrec (searchEval d)

noncomputable def PointwiseComposition.FailureOfComposition.Kleene.guardIndex (d : ℕ) : ℕ

The guard Index construction in FailureOfComposition.Kleene.

Equations

• PointwiseComposition.FailureOfComposition.Kleene.guardIndex d = PointwiseComposition.FailureOfComposition.Kleene.indexOf (PointwiseComposition.FailureOfComposition.Kleene.guardEval d) ⋯

noncomputable def PointwiseComposition.FailureOfComposition.Kleene.searchIndex (d : ℕ) : ℕ

The search Index construction in FailureOfComposition.Kleene.

Equations

• PointwiseComposition.FailureOfComposition.Kleene.searchIndex d = PointwiseComposition.FailureOfComposition.Kleene.indexOf (PointwiseComposition.FailureOfComposition.Kleene.searchEval d) ⋯

def PointwiseComposition.FailureOfComposition.Kleene.identityIndex : ℕ

The identity Index construction in FailureOfComposition.Kleene.

Equations

• PointwiseComposition.FailureOfComposition.Kleene.identityIndex = Encodable.encode Nat.Partrec.Code.id

noncomputable def PointwiseComposition.FailureOfComposition.Kleene.emptyIndex : ℕ

The empty Index construction in FailureOfComposition.Kleene.

Equations

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

@[simp]

theorem PointwiseComposition.FailureOfComposition.Kleene.guardIndex_spec (d x y : ℕ) : y ∈ eval (guardIndex d) x ↔ ¬T₁ d d x ∧ y = x

@[simp]

theorem PointwiseComposition.FailureOfComposition.Kleene.searchIndex_spec (d x y : ℕ) : y ∈ eval (searchIndex d) x ↔ T₁ d d y ∧ ∀ r < y, ¬T₁ d d r

@[simp]

theorem PointwiseComposition.FailureOfComposition.Kleene.identityIndex_spec (x : ℕ) : eval identityIndex x = Part.some x

@[simp]

theorem PointwiseComposition.FailureOfComposition.Kleene.emptyIndex_spec (x : ℕ) : eval emptyIndex x = Part.none

theorem PointwiseComposition.FailureOfComposition.Kleene.guard_after_search (d x : ℕ) : eval (compIndex (guardIndex d) (searchIndex d)) x = Part.none

theorem PointwiseComposition.FailureOfComposition.Kleene.identity_after_search (d x : ℕ) : eval (compIndex identityIndex (searchIndex d)) x = eval (searchIndex d) x

theorem PointwiseComposition.FailureOfComposition.Kleene.guard_eq_identity_of_divergence (d : ℕ) (hd : ¬diagonalHalts d) (x : ℕ) : eval (guardIndex d) x = eval identityIndex x

theorem PointwiseComposition.FailureOfComposition.Kleene.search_diverges_of_divergence (d : ℕ) (hd : ¬diagonalHalts d) (x : ℕ) : eval (searchIndex d) x = Part.none