1RB2LB---_1RC2RB1LC_0LA0RB1LB (u.h.id. 642) does not halt

Coq verification of "BB(2,4) = 3,932,964"

1RB2LA0LA_2LC---2RA_0RA2RC1LC doesn't halt

Coq-BB5 - Skelet #17 doesn't halt, Coq proof

Coq-BB5 - Complete Coq proof of "BB(5) = 47,176,870"

Coq-BB5

Coq-BB5 - Repeated block decider (RepWL_ES)

Coq-BB5 - Reproduction and improvements on NGramCPS

Skelet #26 and #15 don't halt

Skelet #33 doesn't halt

Reproduction, optimization, formal verification of savask's bouncers

Coq verification of Backward Reasoning

Skelet #1 is a translated cycler – Coq agrees

Coq verification of Translated Cyclers

Coq verification of Cyclers

busycoq