Skip to content

feat(busy_beaver): Port 11 single-file BB(6) proofs and SegCount #28

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
TomZahavy merged 1 commit into from
Nov 11, 2026
Merged

feat(busy_beaver): Port 11 single-file BB(6) proofs and SegCount #28

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
11 changes: 11 additions & 0 deletions BusyBeaver.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,7 @@ 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_1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LCHHH
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
Expand Down Expand Up @@ -157,6 +158,7 @@ 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_1RB0LC_1RC0RA_1RD0RF_0LEHHH_1LB1LA_1LD1RA
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
Expand All @@ -166,6 +168,7 @@ 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_1RB0LE_1RCHHH_0RD0RB_1RE0LA_1RF0LF_1LD1RF
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
Expand All @@ -181,9 +184,11 @@ 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_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LEHHH
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_1RC0RC_1LD1RF_HHH1LE_1RF0LF_1RA0LE
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
Expand All @@ -194,6 +199,7 @@ 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_1LC1RB_0RE1LD_0LC1LA_1RF1RA_HHH0RB
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
Expand All @@ -217,12 +223,14 @@ 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_0LCHHH_1LE1LD_1RE0LA_1RA0RD_1LB1RD
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_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LAHHH
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
Expand All @@ -247,9 +255,11 @@ 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_0RCHHH_1RD1RF_1LE0LF_1LB0LA_1LD0RE
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_0LC0RA_1RC1LD_0LB1LE_1LF0RC_HHH0LD
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
Expand Down Expand Up @@ -283,6 +293,7 @@ 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_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD
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
Expand Down
Loading
Loading