Skip to content

Add 181 kernel-verified BB(6) halting and non-halting proofs #23

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 14 commits into from
Nov 6, 2026
+294,071 −1,743
Merged

Add 181 kernel-verified BB(6) halting and non-halting proofs #23

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
541b1da
feat(bb6): add 181 kernel-verified halting and non-halting proofs
Oct 31, 2026
5a39559
fix(bb6): restore Cfg.headRight/headLeft notation for existing holdouts
Oct 31, 2026
43f7449
refactor(bb6): address reviewer feedback and verify all 181 proofs
Nov 3, 2026
a762248
Merge branch 'main' into bb6-halting-proofs
Nov 3, 2026
6c0b73b
refactor(bb6): address all review comments on PR 23
Nov 4, 2026
cbf90e1
ci: pin action hashes in busy_beaver_ci.yml to satisfy blanket securi…
Nov 4, 2026
29b6c42
ci: update lean-action hash to match v1 tag
Nov 4, 2026
332dddf
ci: pin workflow action hashes, remove docs single-threading, and cle…
Nov 4, 2026
ff6fa4b
revert(ci): restore docs.yml and lean_action_ci.yml to match main
Nov 4, 2026
9c8b007
ci: configure 12GB swap space in busy_beaver_ci to prevent runner OOM…
Nov 4, 2026
6ef73a6
revert(ci): restore busy_beaver_ci to clean bubblewrap setup
Nov 4, 2026
fef63cd
ci: set LEAN_NUM_THREADS=1 in busy_beaver_ci and wrap halt theorems
Nov 5, 2026
11d81f8
Merge origin/main into bb6-halting-proofs resolving README.md conflict
Nov 6, 2026
1bcd4fb
Address review: close public sections, add license headers, compact c…
Nov 6, 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: 2 additions & 2 deletions .github/workflows/busy_beaver_ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,8 @@ jobs:
sudo apt-get install -y -qq bubblewrap >/dev/null
sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0

- uses: actions/checkout@v5
- uses: leanprover/lean-action@v1
- uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5
- uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1
with:
build-args: "BusyBeaver BusyBeaverChallenge"
env:
Expand Down
185 changes: 185 additions & 0 deletions BusyBeaver.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,191 @@ public import BusyBeaver.BB33.M_1RB2LA1LA_2LA0RA2RC_HHH1RB2RA
public import BusyBeaver.BB33.M_1RB2LC1RC_2LCHHH2RB_2LA0LB0RA
public import BusyBeaver.BB33.M_1RB2RA1LC_2LC1RB2RB_HHH2LA1LA


-- BB(6) Halt proofs
public import BusyBeaver.BB6.Halt.M_1RB0LB_0LC0RE_1LA1LD_0LB1LD_1RA0RF_1RAHHH
public import BusyBeaver.BB6.Halt.M_1RB0LB_0LC0RE_1LA1LD_0LB1LF_1RA1RD_0LBHHH
public import BusyBeaver.BB6.Halt.M_1RB0LB_0LC0RE_1LA1LD_0LB1RF_1RA1RD_HHH1LC
public import BusyBeaver.BB6.Halt.M_1RB0LC_1LC0RE_1RF1LD_1LA0LB_1RD1RA_1LBHHH
public import BusyBeaver.BB6.Halt.M_1RB0LD_1LC0RD_1RE0RA_1LE0RF_1LA1RC_0LBHHH
public import BusyBeaver.BB6.Halt.M_1RB0LD_1RC0RF_1LC1LA_0LEHHH_1LF0RB_0RC0RE
public import BusyBeaver.BB6.Halt.M_1RB0LE_0RC0RB_1LD0LD_1RA1LC_HHH1LF_1LA0LC
public import BusyBeaver.BB6.Halt.M_1RB0LF_1RCHHH_1LD0RF_1RA0LE_0LD1LD_0RD0RB
public import BusyBeaver.BB6.Halt.M_1RB0RA_1LC0RE_1LD0LC_1RA1LE_1LC0LF_0RAHHH
public import BusyBeaver.BB6.Halt.M_1RB0RB_1RC0RD_1LD1RC_1RF0LE_1LC1LE_HHH0RA
public import BusyBeaver.BB6.Halt.M_1RB0RC_1LC1RF_1RA1LD_1RD0LE_1LD1LC_0REHHH
public import BusyBeaver.BB6.Halt.M_1RB0RC_1RC0LD_1LD1RA_1LF0LE_HHH0RD_1LB0LA
public import BusyBeaver.BB6.Halt.M_1RB0RD_1LC0RA_HHH1RD_1RA1LE_1RC0LF_1LE0LB
public import BusyBeaver.BB6.Halt.M_1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LEHHH
public import BusyBeaver.BB6.Halt.M_1RB0RD_1RC0LC_1RE1RA_0LD1LA_0LF0LD_0REHHH
public import BusyBeaver.BB6.Halt.M_1RB0RE_1RC0RA_0LD0LB_0LA1LE_1LC1LF_0LAHHH
public import BusyBeaver.BB6.Halt.M_1RB0RF_0RC1RD_0LDHHH_1LE1RA_1LA0LF_0RD0RC
public import BusyBeaver.BB6.Halt.M_1RB0RF_1LC1RE_1LD0LC_0LE0RE_1RA1LD_1RBHHH
public import BusyBeaver.BB6.Halt.M_1RB0RF_1RC0RB_1LD1RA_1LE0LD_1RB0LA_0LDHHH
public import BusyBeaver.BB6.Halt.M_1RB1LA_0LB1LC_1RD0LD_0LA0RE_1RC1RF_0LDHHH
public import BusyBeaver.BB6.Halt.M_1RB1LC_1RC1RE_0LF1RD_0RA0LD_HHH1RC_1LA0LA
public import BusyBeaver.BB6.Halt.M_1RB1RA_1LC0RD_1LD1LB_1RA0LE_0LB1LF_1RCHHH
public import BusyBeaver.BB6.Halt.M_1RB1RA_1LC0RE_1LD1LB_1RA0LE_1RA0LF_0LBHHH
public import BusyBeaver.BB6.Halt.M_1RB1RC_1LC0LF_1RF0LD_0RE1LB_1RCHHH_1LD0RA
public import BusyBeaver.BB6.Halt.M_1RB1RC_1LC1RD_1LD0LE_1LA0LD_0LB1RF_HHH0LF
public import BusyBeaver.BB6.Halt.M_1RB1RE_1LC0LB_1LD1LC_0RA1RF_1RD1RE_HHH1LB
public import BusyBeaver.BB6.Halt.M_1RB1RE_1LC0RC_0RA0LD_1LB1LE_0RC1LF_HHH1RA
public import BusyBeaver.BB6.Halt.M_1RB1RE_1RC1LE_1LD0RA_1LF0LA_1LB0LC_HHH1RA
public import BusyBeaver.BB6.Halt.M_1RB1RF_0RC0RE_0RD1RA_1LE0LA_1LB0LD_0RDHHH
public import BusyBeaver.BB6.Halt.M_1RB1RF_1LC0RA_HHH0LD_1RE1LD_0LF0LB_1RA1LE
public import BusyBeaver.BB6.Halt.M_1RBHHH_1LC1RE_1LA0LD_0RE1LC_1LC1RF_1RB0RD

-- BB(6) NonHalt proofs
public import BusyBeaver.BB6.NonHalt.M_1RB0LA_0LC0RB_1RA0RD_1LE0LD_1LFHHH_1LA1LC
public import BusyBeaver.BB6.NonHalt.M_1RB0LA_0RC1LE_0RD1RE_1LA1RF_1RB0LD_1RCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0LB_1LC1LB_1RD1LA_0RE0RE_0RA1RF_HHH1RD
public import BusyBeaver.BB6.NonHalt.M_1RB0LC_0LC1RE_1LD1LC_1LA1RD_HHH1RF_0RA0RF
public import BusyBeaver.BB6.NonHalt.M_1RB0LC_1LA0RE_0RD0LA_1RE1RA_0LD1RF_0RBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0LC_1LC0RB_0LE0LD_1LCHHH_0RA1LF_1LA1LF
public import BusyBeaver.BB6.NonHalt.M_1RB0LC_1LC0RE_1LA1LD_1LA1LB_0RF1RA_HHH0RE
public import BusyBeaver.BB6.NonHalt.M_1RB0LC_1LC0RE_1LA1LD_1LA1LF_0RB1RA_1LCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0LD_1LC1RB_0LA0LD_1LE0RB_1RF0RE_HHH0RD
public import BusyBeaver.BB6.NonHalt.M_1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0LD_1RC1RF_0RD1RA_1LE1RC_0LA0LD_0RCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0LE_1LC1RA_HHH1LD_0RB1LF_1RD1LA_0LA0RD
public import BusyBeaver.BB6.NonHalt.M_1RB0LE_1LC1RD_1LA0LC_1RA1RE_0RF0RB_1LCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0LE_1RC0LF_0LD0RC_1RA1LD_1LB0LE_HHH0RE
public import BusyBeaver.BB6.NonHalt.M_1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LDHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0LE_1RC1LA_1LD1RE_1LB0LD_1RF0RC_1RBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0LF_0RCHHH_1RD0RA_1LE0RC_0LA0LE_1LE1LB
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_0LC0LA_1RF1LD_1LE0LD_1LC1LF_HHH1RA
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_0RC0LD_1LA1RF_1LE1LD_1LB1RE_HHH1RA
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_0RC0LE_1LD1RF_1LB1RD_1LD1LE_HHH1RA
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_0RC0RE_0LDHHH_1LE1LD_1LF0LD_1RA0RD
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_HHH0RA
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LB_HHH0RA
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1LC0LD_1LE1LD_0LB0RF_1RA1LB_1RAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1LC0LF_1LE0LD_1LBHHH_1RA1LB_0LB0RC
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1LC0LF_1LE0LD_1LBHHH_1RA1LB_0LD0RC
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1LC0RC_1LE0LD_1LC1LF_1RA1LC_0LCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1LC0RC_1LE0LD_1LC1LF_1RA1LC_1LBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1LC0RC_1LE0LD_1LC1LF_1RA1LC_1LCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1LC0RC_1LE0LD_1LC1LF_1RA1LC_1LDHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1RC0LC_0LD1RF_1RA1LE_1LD0LB_0REHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1RC0LE_1LD0RA_HHH1LE_0RE0LF_1LB1LC
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1RC0RC_1LD0LE_1RA1LC_1LC1LF_0LCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1RC0RD_1LD1LE_1LF0LC_0LDHHH_1RA1LD
public import BusyBeaver.BB6.NonHalt.M_1RB0RA_1RC0RE_1RDHHH_1LE1LD_1LF0LD_1RA1LE
public import BusyBeaver.BB6.NonHalt.M_1RB0RB_1LC0LE_1RD1LB_1RA0RD_1LB1LF_0LAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RB_1LC0LE_1RD1LB_1RA0RD_1LB1LF_0LBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RB_1LC0LE_1RD1LB_1RA0RD_1LB1LF_1LEHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RB_1RC1LC_0LD1RA_1LF1LE_0LA1LC_1LBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RC_1LC0LD_1RA1RC_1RA1LE_0LB1RE_HHH1RA
public import BusyBeaver.BB6.NonHalt.M_1RB0RC_1LC1LF_1LD0LB_1RE1LC_1RA0RE_0LCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RC_1LC1RA_0RF0LD_1LE0RB_1LB0LD_HHH1RD
public import BusyBeaver.BB6.NonHalt.M_1RB0RC_1LC1RD_1RA1LE_1LA0RD_0LE1RF_1LBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RD_0LC1RA_0RA1LB_1RE1LB_1LF1LB_HHH1LE
public import BusyBeaver.BB6.NonHalt.M_1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_HHH1LA
public import BusyBeaver.BB6.NonHalt.M_1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RD_1RCHHH_1LD1LC_1LE0LC_1RF0RC_1RA0RF
public import BusyBeaver.BB6.NonHalt.M_1RB0RD_1RCHHH_1LD1LE_1LE0LC_1RF1LD_1RA0RF
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1LC0LE_1LD0LC_1RA0LA_1RA1RF_1RAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1LC0RA_0RA0LD_1LEHHH_1RF0LF_0LC0RA
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1LC1RA_1LD0LC_1LA0LA_1RA1RF_0RAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1LC1RA_1LD0LC_1LA0LA_1RA1RF_0RDHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1LC1RA_1LD0LC_1RA0LA_1RA1RF_0LBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1LC1RA_1LD0LC_1RA0LA_1RA1RF_0RAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1LC1RA_1LD0LC_1RA0LA_1RA1RF_1RDHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1LC1RA_1LD0LC_1RA0LA_1RA1RF_1REHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1LC1RD_1LD0LC_1RA0RF_1RDHHH_0RD0LA
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1LC1RF_HHH0LD_0LE1LB_1LF1LD_1RD0RA
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1RC0RB_0RD0RF_0LEHHH_1LF1LE_1LA0LE
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1RC1LF_0LD0RE_HHH1LE_1RA0LB_1LB0LC
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1RC1RE_1LD1RA_1LA0LD_0RA0LF_1LDHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RE_1RCHHH_0LD1LE_0RE1LD_1RF0LC_0RA1RE
public import BusyBeaver.BB6.NonHalt.M_1RB0RF_1LC0LF_1LD0LC_0LE0LA_1LFHHH_1RA1RF
public import BusyBeaver.BB6.NonHalt.M_1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB0RF_1LC1RA_1LD0LC_0LE0LA_0RFHHH_1RA1RF
public import BusyBeaver.BB6.NonHalt.M_1RB0RF_1LC1RA_1LD0LC_0LE0LA_1RFHHH_1RA1RE
public import BusyBeaver.BB6.NonHalt.M_1RB0RF_1LC1RA_1LD0LC_1LE0LA_1LFHHH_1RA1RB
public import BusyBeaver.BB6.NonHalt.M_1RB0RF_1LC1RA_1LD0LC_1LE0LA_1LFHHH_1RA1RF
public import BusyBeaver.BB6.NonHalt.M_1RB0RF_1RC0RE_1LD1RA_1LA0LD_1RAHHH_0RA0LB
public import BusyBeaver.BB6.NonHalt.M_1RB0RF_1RC0RE_1LD1RA_1LA0LD_1RAHHH_0RE0LB
public import BusyBeaver.BB6.NonHalt.M_1RB0RF_1RC1RF_1LD0RE_HHH0LE_1LA0LE_0RA0LC
public import BusyBeaver.BB6.NonHalt.M_1RB0RF_1RC1RF_1LD1RA_HHH0LE_1LA0LE_0RA0LC
public import BusyBeaver.BB6.NonHalt.M_1RB1LA_0RC0RD_1LC1LA_1RE1RD_1LF0LA_HHH0LE
public import BusyBeaver.BB6.NonHalt.M_1RB1LA_1LA1RC_1RD0RB_1LE0LF_HHH1LD_0LE1LA
public import BusyBeaver.BB6.NonHalt.M_1RB1LA_1LC0RA_0LD1RC_HHH0LE_0LF1LE_1RF1LB
public import BusyBeaver.BB6.NonHalt.M_1RB1LA_1RC0LE_1RD0LF_0LA0RD_1LC0LE_HHH0RE
public import BusyBeaver.BB6.NonHalt.M_1RB1LB_1LC0LF_1LD0RC_1RE0LA_1RE1RC_HHH0LE
public import BusyBeaver.BB6.NonHalt.M_1RB1LB_1LC1RB_1RF1LD_0LE0LC_0RCHHH_1LA0RF
public import BusyBeaver.BB6.NonHalt.M_1RB1LB_1RC0LA_1LD1RF_1RB0LE_HHH1LA_1RD0RD
public import BusyBeaver.BB6.NonHalt.M_1RB1LC_1LA1RB_1LD0LA_1RE0RF_HHH1RD_0RE1RB
public import BusyBeaver.BB6.NonHalt.M_1RB1LC_1RC1LB_1LD0RB_0LE1RD_HHH0LF_0LA1LF
public import BusyBeaver.BB6.NonHalt.M_1RB1LD_0RC0RB_0LD1RE_0LA1LC_0RB0RF_1LCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1LD_0RC1RC_1LA1RE_HHH1LE_1RF0RC_0RB0LF
public import BusyBeaver.BB6.NonHalt.M_1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1LD_1RC0RB_1LA0RE_1LC1LE_1LF0LA_0REHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1LD_1RC0RB_1LA1RE_1LF0LA_1LA0RD_1LCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1LD_1RC0RB_1LD0RD_1LA0LE_1LD0LF_1RDHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1LD_1RC0RB_1LD0RD_1LA0LE_1LD1LF_0LDHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1LD_1RC0RB_1LD0RD_1LA0LE_1LD1LF_1LAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1LE_1LC0RF_1LA0RD_1LC1RC_1LB0LB_HHH1RD
public import BusyBeaver.BB6.NonHalt.M_1RB1LE_1LC1RD_0LA1LA_HHH1RE_1LF0LA_0LC0RF
public import BusyBeaver.BB6.NonHalt.M_1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LAHHH_1LA1LF
public import BusyBeaver.BB6.NonHalt.M_1RB1LF_1LC1RB_1RE1LD_1LB0LC_1LA0RE_1LDHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1LF_1RC0RB_1RD0RF_1REHHH_1LF1LA_1LA0LE
public import BusyBeaver.BB6.NonHalt.M_1RB1LF_1RC0RB_1RD0RF_1REHHH_1LF1LE_1LA0LE
public import BusyBeaver.BB6.NonHalt.M_1RB1RA_1LC1LE_0LD0LB_0RA0RF_0LC0RA_1RDHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_HHH0RC
public import BusyBeaver.BB6.NonHalt.M_1RB1RA_1LC1RE_0LD0LD_0LE1LF_1LA0RA_HHH1LC
public import BusyBeaver.BB6.NonHalt.M_1RB1RA_1RC0RA_1LD0LA_1LE0LD_1LF0LB_1REHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RA_1RC0RA_1LD1RB_1LE0LD_1LF0LB_1LAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RA_1RC1LB_0LD0RA_1RF1LE_HHH1LF_1LC0LF
public import BusyBeaver.BB6.NonHalt.M_1RB1RA_1RC1LB_1LD0RA_1LA0LE_HHH0LF_0RC0LB
public import BusyBeaver.BB6.NonHalt.M_1RB1RC_0LA1RF_1RD0LE_1LC0RB_0RA0LC_0RDHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RC_1LC0LE_0RA1RD_1RF1LB_1LD0LA_HHH0RC
public import BusyBeaver.BB6.NonHalt.M_1RB1RC_1LC0RA_1RA0LD_0RE0LF_0LBHHH_0RF0RE
public import BusyBeaver.BB6.NonHalt.M_1RB1RC_1LC0RF_1RE0LD_1LB0LD_HHH1RF_0LF0RA
public import BusyBeaver.BB6.NonHalt.M_1RB1RC_1LC1RE_HHH1LD_0LE0LD_1RA0RF_1LD1RB
public import BusyBeaver.BB6.NonHalt.M_1RB1RC_1RC0RA_1LD1RB_1LE0LD_1LF0LB_1LAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RD_1LC0RB_0RD0LC_1LB0LE_1RF0RE_1RAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RE_0RC0RA_0LD0LF_1LA1LD_0RB0LD_1LCHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RE_1LC1RB_1RA0LD_1RC0LB_0RFHHH_0LD1RA
public import BusyBeaver.BB6.NonHalt.M_1RB1RE_1LC1RD_1LD0LC_1RA0RF_0RDHHH_0RD0LB
public import BusyBeaver.BB6.NonHalt.M_1RB1RF_0RC1RE_1LD1RB_0LE0LC_1RA0LC_0RBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RDHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RF_1LC0LF_HHH0LD_0LE1LD_0RF0LB_1RA1RE
public import BusyBeaver.BB6.NonHalt.M_1RB1RF_1LC0RD_HHH0LD_1LE0LD_1RA0RF_0RE0LB
public import BusyBeaver.BB6.NonHalt.M_1RB1RF_1LC1RE_HHH0LD_1LE0LD_1RA0RF_0RE0LB
public import BusyBeaver.BB6.NonHalt.M_1RB1RF_1RC0RA_1LD1RB_1LE0LD_1LA0LB_0RBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RF_1RC0RA_1LD1RB_1LE0LD_1LB0LB_0RBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RF_1RC0RA_1LD1RB_1LE0LD_1RB0LB_0RBHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RF_1RC0RA_1LD1RB_1LE0LD_1RB0LB_1RAHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RF_1RC0RA_1LD1RB_1LE0LD_1RB0LB_1REHHH
public import BusyBeaver.BB6.NonHalt.M_1RB1RF_1RC1RA_1LD0LA_HHH0LE_0LF1LE_0RA0LC
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_0RC0LD_1RD1RC_1LB0LE_1LF0RA_0LD1LA
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_0RC0RA_1RD1RC_1LE1LF_0LB0LD_0LE0RC
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_0RC1LF_0RD1RB_1LE1RC_0LB0LE_0LE0LA
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_0RC1LF_1LC1LD_1RE0RA_0RD1RF_0LD0LF
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1LC0LF_1RD1LB_1RE0RD_1LB0RB_1LB0LA
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1LC0RC_0LD0LC_1RE1RA_0RD1LF_0LE0LF
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1LC1LB_1LD0LB_1RE1LC_1RF0RE_0RA0RC
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1LC1LB_1LD0LB_1RE1LC_1RF0RE_1RA0RC
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1LC1LD_1LD0LB_1RE1LC_1RF0RE_1RA0RC
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1RC0LC_1RD0RF_1LE1RC_1LB0LE_1RC1RA
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1RC0RF_1LD1RB_1LE0LD_1RB0LB_1RB1RA
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1RC0RF_1RD0RA_1LE1RB_1LB0LE_0RA0LC
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1RC0RF_1RD0RA_1LE1RB_1LB0LE_0RB0LC
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1RC1LF_1LD1RE_1LB0LD_1RA0RC_1RC0LE
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1RC1RA_1RD0RB_1LE1RC_1LF0LE_1RC0LC
public import BusyBeaver.BB6.NonHalt.M_1RBHHH_1RC1RE_1LD0RC_0RE0LD_1LC0LF_1RA0RF

/-!
# Busy Beaver Holdouts (`BusyBeaver`)

Expand Down
5 changes: 3 additions & 2 deletions BusyBeaver/BB33/M_1RB0LB0RC_2LC2LA1RA_1RA1LCHHH.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,9 @@ def start : State := .A 1 1
/-- Encoding of `State` into Turing machine configurations. -/
def encode : State → Cfg (Fin 3) (Fin 3)
| .A a c =>
((default <+ ([1, 0] : List (Fin 3)) ^ c) {{A}}>
(([1] : List (Fin 3)) ^ a +> ((2 : Fin 3) >> default)))
Cfg.headRight A
(default <+ ([1, 0] : List (Fin 3)) ^ c)
(([1] : List (Fin 3)) ^ a +> ((2 : Fin 3) >> default))

/-- Accelerated transition function on `State` (`none` indicates halting). -/
def next : State → Option State
Expand Down
3 changes: 2 additions & 1 deletion BusyBeaver/BB33/M_1RB2LC1RC_2LCHHH2RB_2LA0LB0RA.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,8 @@ def start : State := .A 0 1
/-- Encoding of `State` into Turing machine configurations. -/
def encode : State → Cfg (Fin 3) (Fin 3)
| .A a c =>
((default <+ ([1] : List (Fin 3))) <+ ([2] : List (Fin 3)) ^ a) <{{C}}
Cfg.headLeft C
(((default <+ ([1] : List (Fin 3))) <+ ([2] : List (Fin 3)) ^ a))
(([2, 0] : List (Fin 3)) ^ c +> default)

/-- Accelerated transition function on `State` (`none` indicates halting). -/
Expand Down
5 changes: 3 additions & 2 deletions BusyBeaver/BB33/M_1RB2RA1LC_2LC1RB2RB_HHH2LA1LA.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,8 +72,9 @@ def start : State := .A 2 0 0
@[simp]
def encode : State → Cfg (Fin 3) (Fin 3)
| .A a b c =>
(((default <+ ([2, 1] : List (Fin 3)) ^ a) <+ ([1] : List (Fin 3)) ^ (2 * b + 2)) <{{A}}
(([1] : List (Fin 3)) ^ (2 * (c + 2)) +> default))
Cfg.headLeft A
(((default <+ ([2, 1] : List (Fin 3)) ^ a) <+ ([1] : List (Fin 3)) ^ (2 * b + 2)))
(([1] : List (Fin 3)) ^ (2 * (c + 2)) +> default)

/-- Ligocki and savask's 7-rule mod-6 Collatz-like map for Bigfoot (`none` indicates halting at
$a = 0, b \equiv 1 \pmod 6$). -/
Expand Down
2 changes: 1 addition & 1 deletion BusyBeaver/BB6/Accelerations/M_1RB1RA_1LC0RC_HHH0LD_0LE0RF_1RE0RA_0LF1LB.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -974,7 +974,7 @@ private theorem mode_EB_n_00_closed (L R : List (ℕ × ℕ)) :

private theorem cfg_EL_n_00_nil_eq (R : List (ℕ × ℕ)) :
cfg_EL_n_00 [] R = cfg_EB_n_00 [] R := by
unfold cfg_EL_n_00 cfg_EB_n_00 Cfg.headLeft
unfold cfg_EL_n_00 cfg_EB_n_00; try unfold Cfg.headLeft
simp [encLeft_nil]

private theorem mode_EL_n_00_closed (L R : List (ℕ × ℕ)) :
Expand Down
4 changes: 2 additions & 2 deletions BusyBeaver/BB6/Accelerations/M_1RB1RE_1LC0RC_1RA1LD_1RB0LA_0LC1RF_HHH1RD.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -322,7 +322,7 @@ private theorem step_B_single_ge4 (L : List ℕ) (e₀ c : ℕ) :
ListBlank.append_pow_succ ([1] : List (Fin 2)) c]
simp only [list_pow_succ, list_pow_zero, List.cons_append, List.nil_append,
ListBlank.append_cons, ListBlank.append_nil]
rw [Cfg.headLeft_cons]
try rw [Cfg.headLeft_cons]
bb_steps
exact ((shift_B_cons L e₀ [] (c + 4)).trans hturn).trans
(reaches_drainD (4 :: bumpHeadBy (2 * e₀) L) [] c)
Expand Down Expand Up @@ -362,7 +362,7 @@ private theorem step_B_cons_ge2 (L : List ℕ) (e₀ e₁ : ℕ) (E₂ : List
ListBlank.append_pow_succ ([1] : List (Fin 2)) (2 * e₁)]
simp only [list_pow_succ, list_pow_zero, List.cons_append, List.nil_append,
ListBlank.append_cons, ListBlank.append_nil]
rw [Cfg.headLeft_cons]
try rw [Cfg.headLeft_cons]
bb_steps
exact ((shift_B_cons L e₀ ((e₁ + 2) :: E₂) c).trans hturn).trans
(reaches_drainD (4 :: bumpHeadBy (2 * e₀) L) (e₁ :: E₂) c)
Expand Down
Loading
Loading