Skelet #26 and #15 don't halt

Jan 2024 · Jason Yuen ,mei ,Shawn Ligocki

Formal Verification Individual Machine Write-up Coq bb5

Featured Links

Github	https://github.com/meithecatte/busycoq/commit/8550d7db7ef88e90330e6fb66bd1d98275438f89
Chat about it	https://discord.com/channels/960643023006490684/1242208042460647575
Forum Link	https://discuss.bbchallenge.org/t/skelet-26-and-15-do-not-halt-coq-proof/183
Proof sketch (incomplete)	https://www.sligocki.com/2023/02/05/shift-overflow.html
Coq proof for Skelet #15	https://github.com/meithecatte/busycoq/commit/095c22b0a28a8f9b24f45aa08b2e31d1364063de

Description

Jason Yuen - Wrote Coq proof for Skelet #26. Wrote forum post with a complete proof. mei - Suggested improvements to Coq proof. Wrote Coq proof for Skelet #15. Shawn Ligocki - Wrote an incomplete proof sketch.