User:DrDisentangle/BB6 formal proofs: Difference between revisions
Jump to navigation
Jump to search
No edit summary |
No edit summary |
||
| Line 17: | Line 17: | ||
| [[1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/AntiHydra.v R] [https://github.com/rwst/bbchallenge/tree/main/Antihydra L] || [https://github.com/rwst/bbchallenge/tree/main/Antihydra L] || [https://github.com/rwst/bbchallenge/tree/main/Antihydra L] || || | | [[1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/AntiHydra.v R] [https://github.com/rwst/bbchallenge/tree/main/Antihydra L] || [https://github.com/rwst/bbchallenge/tree/main/Antihydra L] || [https://github.com/rwst/bbchallenge/tree/main/Antihydra L] || || | ||
|- | |- | ||
| [[1RB0RD_0RC1RE_1RD0LA_1LE1LC_1RF0LD_---0RA]] || || || || | | [[1RB0RD_0RC1RE_1RD0LA_1LE1LC_1RF0LD_---0RA]] || - || || || || | ||
|- | |- | ||
| [[1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC]] || || || || | | [[1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC]] || - || || || || | ||
|- | |- | ||
| [[1RB---_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA]] || || || || | | [[1RB---_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA]] || - || || || || | ||
|- | |- | ||
| [[1RB0RE_1LC0RA_1LA1LD_1LC1LF_0LC0LB_1LE---]] || || || || | | [[1RB0RE_1LC0RA_1LA1LD_1LC1LF_0LC0LB_1LE---]] || [https://github.com/int-y1/proofs/blob/1929f57df4dd7afcc11c3f458e20526fd1f991e0/BusyLean/Individual/1RB0RE%201LC0RA%201LA1LD%201LC1LF%200LC0LB%201LE---.lean L] || || || || | ||
|- | |- | ||
| [[1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE]] || || || || | | [[1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE]] || [https://github.com/int-y1/proofs/blob/1929f57df4dd7afcc11c3f458e20526fd1f991e0/BusyLean/Individual/1RB0LD%201RC1RA%201LD0RB%201LE1LA%201RF0RC%20---1RE.lean L] || || || || | ||
|- | |- | ||
| [[1RB0LC_1LC0RD_1LF1LA_1LB1RE_1RB1LE_---0LE]] || || || || | | [[1RB0LC_1LC0RD_1LF1LA_1LB1RE_1RB1LE_---0LE]] || - || || || || | ||
|- | |- | ||
| [[1RB0RE_1LC1LD_0RA0LD_1LB0LA_1RF1RA_---1LB]] || || || || | | [[1RB0RE_1LC1LD_0RA0LD_1LB0LA_1RF1RA_---1LB]] || - || || || || | ||
|- | |- | ||
| [[1RB1RE_1LC1LD_---1LA_1LB1LE_0RF0RA_1LD1RF]] || || || || | | [[1RB1RE_1LC1LD_---1LA_1LB1LE_0RF0RA_1LD1RF]] || - || || || || | ||
|- | |- | ||
| [[1RB0LC_0LC0RF_1RD1LC_0RA1LE_---0LD_1LF1LA]] || || || || | | [[1RB0LC_0LC0RF_1RD1LC_0RA1LE_---0LD_1LF1LA]] || - || || || || | ||
|- | |- | ||
| [[1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB1LD%201RC1RE%200LA1LB%200LD1LC%201RF0RA%20---0RC.v R] || || || || | | [[1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB1LD%201RC1RE%200LA1LB%200LD1LC%201RF0RA%20---0RC.v R] || || || || | ||
| Line 39: | Line 39: | ||
| [[1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LB%201LC0RE%201LA1LD%200LC---%200RB0RF%201RE1RB.v R] || || || | | [[1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LB%201LC0RE%201LA1LD%200LC---%200RB0RF%201RE1RB.v R] || || || | ||
|- | |- | ||
| [[1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_---1RE]] || || || || | | [[1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_---1RE]] || - || || || || | ||
|- | |- | ||
| c [[1RB0LD 1LC0RA 1RA1LB 1LA1LE 1RF0LC ---0RE]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE.v R] || || || || | | c [[1RB0LD 1LC0RA 1RA1LB 1LA1LE 1RF0LC ---0RE]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE.v R] || || || || | ||
|- | |- | ||
|} | |} | ||
Revision as of 10:33, 19 April 2026
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.