Talk:BitChanger Busy beaver/Proof

From Esolang
Jump to navigation Jump to search

AProVE can solve some programs without the use of aproximating rules, If we substitute }<} with > and maybe }< with *. i will work on some code to generate a string rewriting system from bitchanger code. C++DSUCKER (talk) 08:45, 8 April 2025 (UTC)

It turns out AProVE can prove more about term rewriting systems than string rewriting systems, so i will be using it instead. C++DSUCKER (talk) 12:05, 11 April 2025 (UTC)
AProVE produces proofs for complex programs of length 17, BB(17) is close. I will work on the page soon. C++DSUCKER (talk) 12:18, 11 April 2025 (UTC)

Someone on the bbchallange dicsord ran TM deciders on bitchanger programs, and verified the 17th busy beaver to be 346 and the 18th to be 367. there are 3 undetermined programs for length 19 and 9 for length 20. C++DSUCKER (talk) 23:53, 14 April 2025 (UTC)