Skelet #33 doesn't halt

Dec 2023 · Jason Yuen ,mei ,Shawn Ligocki

Formal Verification Individual Machine Coq bb5 Write-up

Featured Links

Github	https://github.com/meithecatte/busycoq/commit/7bb7c754e8b601020dd60c621b60836d90717e14
Chat about it	https://discord.com/channels/960643023006490684/1242208042460647575
Forum Link	https://discuss.bbchallenge.org/t/skelet-33-doesnt-halt-coq-proof/180
Proof sketch (incomplete)	https://www.sligocki.com/2023/02/05/shift-overflow.html

Description

Jason Yuen - Wrote most of Coq proof. Wrote forum post with a complete proof. mei - Filled in a missing lemma in Coq proof. Suggested improvements to Coq proof. Shawn Ligocki - Wrote an incomplete proof sketch.