BusyBeaver(1) — Verified in Coq

This repository contains a fully verified Coq proof for the Busy Beaver with 1 state,
written and proven as a small Test

---

📘 Overview

• File: Bb1.v
• Language: Coq 8.17+
• Goal: Prove termination of the 1-state Busy Beaver machine
• Method: Minimal inductive proof using structural recursion

---

🧩 Proof Concept

1. Define the single-state transition rules
2. Encode the halting configuration (None state)
3. Apply inductive termination lemma
4. Verify via minimalistic tactic sequence