inductive BusyBeasverTest.Γ : Type

• A : Γ
• B : Γ

instance BusyBeasverTest.instInhabitedΓ : Inhabited Γ

Equations

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

instance BusyBeasverTest.instFintypeΓ : Fintype Γ

Equations

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

inductive BusyBeasverTest.Λ : Type

• S : Λ
• T : Λ

instance BusyBeasverTest.instInhabitedΛ : Inhabited Λ

Equations

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

instance BusyBeasverTest.instFintypeΛ : Fintype Λ

Equations

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

def BusyBeasverTest.alwaysHaltingMachine : Turing.BusyBeaver.Machine Γ Λ

Equations

• BusyBeasverTest.alwaysHaltingMachine x✝¹ x✝ = none

def BusyBeasverTest.haltsAfterOne : Turing.BusyBeaver.Machine Γ Λ

Equations

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

instance BusyBeasverTest.instIsHaltingΓΛAlwaysHaltingMachine : alwaysHaltingMachine.IsHalting

instance BusyBeasverTest.instIsHaltingΓΛHaltsAfterOne : haltsAfterOne.IsHalting

theorem BusyBeasverTest.haltsAfterOne_haltingNumber : haltsAfterOne.haltingNumber = 1

def BusyBeasverTest.neverHalts : Turing.BusyBeaver.Machine Γ Λ

Equations

• BusyBeasverTest.neverHalts BusyBeasverTest.Λ.S BusyBeasverTest.Γ.A = some (some BusyBeasverTest.Λ.T, { symbol := default, dir := Turing.Dir.right })
• BusyBeasverTest.neverHalts BusyBeasverTest.Λ.T BusyBeasverTest.Γ.A = some (some BusyBeasverTest.Λ.S, { symbol := default, dir := Turing.Dir.right })
• BusyBeasverTest.neverHalts BusyBeasverTest.Λ.S BusyBeasverTest.Γ.B = some (some BusyBeasverTest.Λ.T, { symbol := default, dir := Turing.Dir.left })
• BusyBeasverTest.neverHalts BusyBeasverTest.Λ.T BusyBeasverTest.Γ.B = some (some BusyBeasverTest.Λ.T, { symbol := default, dir := Turing.Dir.left })

theorem BusyBeasverTest.not_isHalting_neverHalts : ¬neverHalts.IsHalting