instFintypeΓ' — Mathlib

English

Specifies the behavior of the transformation tr on the successor state, equating it with a specified branching structure involving bit1 and cons/bit0 branches.

Русский

Определяется поведение преобразования tr на переходе к следующему состоянию, равному заданной структуре разветвления с bit1 и ветвями cons/bit0.

LaTeX

$$$\\forall q.\\; tr(\\Lambda'.succ\\ q) = pop' main\\; (branch(\\lambda s. s=some Γ'.bit1)\\; ( (push\\ rev\\ (\\lambda _=> Γ'.bit0))\\<|goto(\\lambda _=> Λ'.succ\\ q) ) \\; |\\; branch(\\lambda s. s=some Γ'.cons)\\; ( (push\\ main\\ (\\lambda x=> Γ'.cons))\\; (push\\ main\\ (\\lambda x=> Γ'.bit1))\\; (goto(\\lambda _=> unrev q)) )\\; ( (push\\ main\\ (\\lambda x=> Γ'.bit1))\\; (goto(\\lambda _=> unrev q)) ) )$$$

Lean4

instance : Fintype✝ Turing.PartrecToTM2.Γ'
    where
  elems✝ := Finset.mk✝ Turing.PartrecToTM2.Γ'.enumList Turing.PartrecToTM2.Γ'.enumList_nodup
  complete✝ := by
    intro x✝
    rw [Finset.mem_mk✝, Multiset.mem_coe✝, List.mem_iff_getElem?✝]
    exact ⟨Turing.PartrecToTM2.Γ'.ctorIdx x✝, Turing.PartrecToTM2.Γ'.enumList_getElem?_ctorIdx_eq x✝⟩

Похожие утверждения