Turing.PartrecToTM2.tr_supports
theorem Turing.PartrecToTM2.tr_supports :
∀ (c : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
Turing.TM2.Supports Turing.PartrecToTM2.tr (Turing.PartrecToTM2.codeSupp c k)
The theorem `Turing.PartrecToTM2.tr_supports` states that for any given partial recursive function `c` and a continuation `k`, the Turing machine transition function `tr` is supported by the finite set `codeSupp c k`. In other words, when the Turing machine starts from the initial state `trNormal c k`, it only transitions to states within the set `codeSupp c k`, hence effectively behaving as a finite state machine. This is despite the fact that the underlying type of state labels, denoted as `Λ'`, is infinite. The states accessed correspond approximately to the subterms of `c`, and hence are finite for any specific `c` and `k`.
More concisely: The theorem `Turing.PartrecToTM2.tr_supports` guarantees that for any partial recursive function `c` and continuation `k`, the Turing machine transition function `tr` starting from state `trNormal c k` only visits states in the finite set `codeSupp c k`.
|
Mathlib.Computability.TMToPartrec._auxLemma.18
theorem Mathlib.Computability.TMToPartrec._auxLemma.18 :
∀ {α : Sort u_1} {β : α → Sort u} {f₁ f₂ : (x : α) → β x}, (f₁ = f₂) = ∀ (a : α), f₁ a = f₂ a
This theorem, named `Mathlib.Computability.TMToPartrec._auxLemma.18`, states that for any arbitrary types `α` and `β` (where `β` is a type-dependent on `α`), and any two functions `f₁` and `f₂` (both of which take an element of type `α` and return an element of type `β`), the equality of `f₁` and `f₂` is equivalent to the statement that for every element of type `α`, `f₁` of that element equals `f₂` of that element. Essentially, it asserts that two functions are equal if and only if they produce the same output for every input.
More concisely: For functions `f₁` and `f₂` from type `α` to type `β` dependent on `α`, the equality of `f₁` and `f₂` holds if and only if for all `x : α`, `f₁ x = f₂ x`.
|
Turing.ToPartrec.stepNormal_then
theorem Turing.ToPartrec.stepNormal_then :
∀ (c : Turing.ToPartrec.Code) (k k' : Turing.ToPartrec.Cont) (v : List ℕ),
Turing.ToPartrec.stepNormal c (k.then k') v = (Turing.ToPartrec.stepNormal c k v).then k'
The `stepNormal_then` theorem states that for any given Partrec Turing code `c`, continuation `k`, another continuation `k'`, and a list of natural numbers `v`, the function `stepNormal` exhibits a specific property: applying `stepNormal` to `c`, the composition of `k` and `k'`, and `v` is equivalent to first applying `stepNormal` to `c`, `k`, and `v` and then applying the `then` operation with `k'`. In other words, the `stepNormal` function respects the `then k'` homomorphism. This is an exact equality, not a simulation, indicating that the original and embedded machines move in sync until the embedded machine reaches the halt state.
More concisely: For any Partrec Turing code `c`, continuations `k` and `k'`, and a list of natural numbers `v`, `stepNormal c (k '' k') v = stepNormal c k v ^^ k'`.
|
Turing.PartrecToTM2.supports_union
theorem Turing.PartrecToTM2.supports_union :
∀ {K₁ K₂ S : Finset Turing.PartrecToTM2.Λ'},
Turing.PartrecToTM2.Supports (K₁ ∪ K₂) S ↔
Turing.PartrecToTM2.Supports K₁ S ∧ Turing.PartrecToTM2.Supports K₂ S
This theorem in the Lean theorem prover language states that for any three finite sets `K₁`, `K₂`, and `S` of Turing.PartrecToTM2.Λ' (which is a type that represents a Turing machine's states), the Turing machine's set of supports `S` supports the union of `K₁` and `K₂` if and only if `S` supports `K₁` and `S` supports `K₂`. This theorem is an essential part of understanding how supports work in the context of Turing machines.
More concisely: For any finite sets `K₁`, `K₂`, and `S` of Turing machine states, the set `S` supports the union of `K₁` and `K₂` if and only if it supports both `K₁` and `K₂`.
|
Turing.ToPartrec.stepRet_then
theorem Turing.ToPartrec.stepRet_then :
∀ {k k' : Turing.ToPartrec.Cont} {v : List ℕ},
Turing.ToPartrec.stepRet (k.then k') v = (Turing.ToPartrec.stepRet k v).then k'
This theorem states that for any two computation continuations `k` and `k'` and a list of natural numbers `v`, the `stepRet` function applied to the composition of `k` and `k'` and `v` is equivalent to the composition of the `stepRet` function applied to `k` and `v` and `k'`. In other words, the function `stepRet` respects the composition operation `then`. This is an exact equality, indicating that the original and the embedded computation processes move together until the embedded one reaches the halt state.
More concisely: For any computation continuations `k` and `k'` and list of natural numbers `v`, `stepRet(k ∘ k') v = stepRet k (k' v)`.
|
Mathlib.Computability.TMToPartrec._auxLemma.34
theorem Mathlib.Computability.TMToPartrec._auxLemma.34 :
∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, (s ∪ t ⊆ u) = (s ⊆ u ∧ t ⊆ u)
This theorem, `Mathlib.Computability.TMToPartrec._auxLemma.34`, states that for any type `α` that has decidable equality, and any three finite sets `s`, `t`, and `u` of `α`, the set union of `s` and `t` is a subset of `u` if and only if both `s` and `t` are individually subsets of `u`. This theorem is a formalisation of a basic set theory property.
More concisely: For any type `α` with decidable equality, sets `s`, `t`, and `u` of `α` are such that `s ∪ t ⊆ u` if and only if `s ⊆ u` and `t ⊆ u`.
|