User:DrDisentangle/BB6 formal proofs

This page is a draft of something to be added to BB(6). The goal is to keep track of which BB(6) cryptids (or candidates) have Rocq/Lean proofs of specific stages up to halting/nonhalting proofs.

Machine	Rules Proved	Math Derived	BMO	Prob. Model	H/NH Proof attempt	Final Proof
1RB1RE 1LC0RA 0RD1LB ---1RC 1LF1RE 0LB0LE	L	L	#1
1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA	R L	L	#2	L
1RB0LD 1LC0RA 1RA1LB 1LA1LE 1RF0LC ---0RE	R		#5
1RB1LA_1LC0RE_1LF1LD_0RB0LA_1RC1RE_---0LD	-		#6
1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA	-		#8
1RB0RD_0RC1RE_1RD0LA_1LE1LC_1RF0LD_---0RA	L	L
1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC	L	L
1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC	R L	L		L
1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE	L	L
1RB0RE_1LC1LD_0RA0LD_1LB0LA_1RF1RA_---1LB	L	L
1RB1RE_1LC1LD_---1LA_1LB1LE_0RF0RA_1LD1RF	L	L
1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_---1RE	L	L
1RB1RC_1LC1LE_1RA1RD_0RF0RE_1LA0LB_---1RA	R
1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---	R
1RB---_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA	-
1RB0RE_1LC0RA_1LA1LD_1LC1LF_0LC0LB_1LE---	L
1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE	L
1RB0LC_0LC0RF_1RD1LC_0RA1LE_---0LD_1LF1LA	-
1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC	R
1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB	R
c 1RB0LC_1LC0RD_1LF1LA_1LB1RE_1RB1LE_---0LE	*L
c 1RB1LD_1RC0LE_1LA1RE_0LF1LA_1RB0RB_---0LB	*L
c 1RB1LA 1RC0RF 1RD--- 0LE1RB ---0LA 1LD1RF	L				L
c 1RB1RF_1LC1LF_0RE1LD_0LB1LD_---1RC_1RA0RD	*L
c 1RB---_0RC0RD_1LD1RB_0LE0LC_1RA0LF_1LD1LE	-

(*) incomplete