Skip to content

Prove a six-state A6 machine nonhalting from blank tape #21

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mo271 merged 3 commits into from
Oct 31, 2026
Merged

Prove a six-state A6 machine nonhalting from blank tape #21

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7898205
Prove BB6 A6 nonhalting from blank tape
Oct 29, 2026
77d8722
Replace generated A6 chunks with reflective RLE & affine certificate …
mo271 Oct 30, 2026
940616e
Merge branch 'main' into a6-nonhalting
mo271 Oct 31, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions BusyBeaver.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,9 @@ public import BusyBeaver.Defs
public import BusyBeaver.Basic
public import BusyBeaver.Bridge
public import BusyBeaver.Cert
public import BusyBeaver.WordRLE
public import BusyBeaver.AffRLE
public import BusyBeaver.ElabRLE
public import BusyBeaver.BB6.M_1RB0LB_1LC0RE_1LA1LD_0LCHHH_0RB0RF_1RE1RB
public import BusyBeaver.BB6.M_1RB0LC_0LC0RF_1RD1LC_0RA1LE_HHH0LD_1LF1LA
public import BusyBeaver.BB6.M_1RB0LC_0LC1RF_1LE1RD_0RC1RC_0LA1LA_HHH1RA
Expand All @@ -22,6 +25,7 @@ public import BusyBeaver.BB6.M_1RB0LE_0RC1RC_0RD1LA_1LD0LA_1LF1LC_HHH1LC
public import BusyBeaver.BB6.M_1RB0LE_1LC1RA_1RA1LD_0LC0LA_0RE1RF_0RCHHH
public import BusyBeaver.BB6.M_1RB0LF_1LC0LD_1RD1LB_HHH1RE_0RA1RE_1LA0LE
public import BusyBeaver.BB6.M_1RB0LF_1LC1RA_0RE0RD_HHH1LE_1LF1RC_1LC1LA
public import BusyBeaver.BB6.M_1RB0LF_1RC0RA_1LD0RB_0LE0LC_0LA0LC_0LBHHH
public import BusyBeaver.BB6.M_1RB0LF_1RC1RA_0RD0RB_1LEHHH_0LA1LE_1RD1LA
public import BusyBeaver.BB6.M_1RB0RB_1LB0LC_1RD1LC_1RE0RA_0RF1RA_HHH1LB
public import BusyBeaver.BB6.M_1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_HHH1LC
Expand Down
Loading
Loading