inductive Γ : Type

• A : Γ
• B : Γ

instance instInhabitedΓ : Inhabited Γ

Equations

• instInhabitedΓ = { default := Γ.A }

instance instFintypeΓ : Fintype Γ

Equations

• instFintypeΓ = { elems := { val := ↑Γ.enumList, nodup := Γ.enumList_nodup }, complete := instFintypeΓ.proof_1 }

inductive Λ : Type

• S : Λ
• T : Λ

instance instInhabitedΛ : Inhabited Λ

Equations

• instInhabitedΛ = { default := Λ.S }

instance instFintypeΛ : Fintype Λ

Equations

• instFintypeΛ = { elems := { val := ↑Λ.enumList, nodup := Λ.enumList_nodup }, complete := instFintypeΛ.proof_1 }

def alwaysHaltingMachine : Turing.BusyBeaver.Machine Γ Λ

Equations

• alwaysHaltingMachine x✝¹ x✝ = none

def haltsAfterOne : Turing.BusyBeaver.Machine Γ Λ

Equations

• haltsAfterOne Λ.S x✝ = some (some Λ.T, { symbol := default, dir := Turing.Dir.right })
• haltsAfterOne Λ.T x✝ = none

instance instIsHaltingΓΛAlwaysHaltingMachine : alwaysHaltingMachine.IsHalting

instance instIsHaltingΓΛHaltsAfterOne : haltsAfterOne.IsHalting