From e0247617d9d75e1ccb21819e889544c93b0b2ec2 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Wed, 16 Oct 2024 11:49:37 +0800
Subject: [PATCH] namespace

---
 GoldbachTm/Tm31/Content.lean         | 4 ++++
 GoldbachTm/Tm31/PBP.lean             | 4 ++++
 GoldbachTm/Tm31/Prime.lean           | 4 ++++
 GoldbachTm/Tm31/Search0.lean         | 3 +++
 GoldbachTm/Tm31/Sim31.lean           | 2 ++
 GoldbachTm/Tm31/Transition.lean      | 4 ++++
 GoldbachTm/Tm31/TuringMachine31.lean | 4 ++++
 7 files changed, 25 insertions(+)

diff --git a/GoldbachTm/Tm31/Content.lean b/GoldbachTm/Tm31/Content.lean
index b63a56e..cb06ff3 100644
--- a/GoldbachTm/Tm31/Content.lean
+++ b/GoldbachTm/Tm31/Content.lean
@@ -2,6 +2,8 @@ import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.PBP
 import Mathlib.Data.Nat.Prime.Defs
 
+namespace Tm31
+
 theorem lemma_25 (n : ℕ) (i : ℕ)
 (g :
 nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4) Γ.one), Turing.ListBlank.mk []⟩⟩ )
@@ -111,3 +113,5 @@ intros h
 by_contra! g
 apply halt_lemma_rev' at g
 tauto
+
+end Tm31
diff --git a/GoldbachTm/Tm31/PBP.lean b/GoldbachTm/Tm31/PBP.lean
index a212f0b..4e44bbe 100644
--- a/GoldbachTm/Tm31/PBP.lean
+++ b/GoldbachTm/Tm31/PBP.lean
@@ -4,6 +4,8 @@ import GoldbachTm.Tm31.Search0
 import GoldbachTm.Tm31.Prime
 import Mathlib.Data.Nat.Prime.Defs
 
+namespace Tm31
+
 -- l1 : count of 1 on the left
 -- r1 : count of 1 on the right
 theorem lemma_26 (i l1 r1: ℕ)
@@ -283,3 +285,5 @@ induction l1 with
       simp at hpp
       ring_nf
       by_cases Nat.Prime (2+l1) <;> tauto
+
+end Tm31
diff --git a/GoldbachTm/Tm31/Prime.lean b/GoldbachTm/Tm31/Prime.lean
index e0a59c2..19b33b2 100644
--- a/GoldbachTm/Tm31/Prime.lean
+++ b/GoldbachTm/Tm31/Prime.lean
@@ -5,6 +5,8 @@ import GoldbachTm.Tm31.Transition
 import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Data.Nat.ModEq
 
+namespace Tm31
+
 -- c1++, c2++
 --    l 0 [la 11] 0  [lb 11] 0 [ra 11111] 0  [(rb+1) 1] 0 r
 --                c1         ^            c2
@@ -466,3 +468,5 @@ match r1 with
     have g : 1 + r1.succ.succ.succ = 4+r1 := by omega
     rw [g] at h
     exact h
+
+end Tm31
diff --git a/GoldbachTm/Tm31/Search0.lean b/GoldbachTm/Tm31/Search0.lean
index 33cb84a..7a5dbab 100644
--- a/GoldbachTm/Tm31/Search0.lean
+++ b/GoldbachTm/Tm31/Search0.lean
@@ -2,6 +2,7 @@
 -- all these states' usage is to search 0
 import GoldbachTm.Tm31.TuringMachine31
 
+namespace Tm31
 
 -- left
 theorem rec5 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
@@ -197,3 +198,5 @@ induction k with intros i l r h
             rw [g, induction_step]
             . simp [List.replicate_succ' (k+1)]
             . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+
+end Tm31
diff --git a/GoldbachTm/Tm31/Sim31.lean b/GoldbachTm/Tm31/Sim31.lean
index e3f837e..4d14c6e 100644
--- a/GoldbachTm/Tm31/Sim31.lean
+++ b/GoldbachTm/Tm31/Sim31.lean
@@ -1,6 +1,8 @@
 import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Basic
 
+open Tm31
+
 unsafe def foo (cfg : Cfg) : IO Unit :=
 match (step machine cfg) with
 | some cfg => do
diff --git a/GoldbachTm/Tm31/Transition.lean b/GoldbachTm/Tm31/Transition.lean
index 705a4f1..ed267ad 100644
--- a/GoldbachTm/Tm31/Transition.lean
+++ b/GoldbachTm/Tm31/Transition.lean
@@ -1,6 +1,8 @@
 import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.Search0
 
+namespace Tm31
+
 theorem lemma_12_to_13 (i : ℕ) (r1: ℕ) (l r : List Γ)
 (h :
 nth_cfg i = some ⟨⟨12, by omega⟩, ⟨Γ.zero,
@@ -107,3 +109,5 @@ cases l1 with
              simp [h]
              rw [List.append_cons, ← List.replicate_succ']
              ring_nf
+
+end Tm31
diff --git a/GoldbachTm/Tm31/TuringMachine31.lean b/GoldbachTm/Tm31/TuringMachine31.lean
index 6792902..6ccb8c4 100644
--- a/GoldbachTm/Tm31/TuringMachine31.lean
+++ b/GoldbachTm/Tm31/TuringMachine31.lean
@@ -5,6 +5,8 @@ import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank
 
+namespace Tm31
+
 def Machine := Fin 31 → Γ → Option (Fin 31 × Stmt)
 
 structure Cfg where
@@ -127,3 +129,5 @@ forward h h 3
 forward h h 4
 forward h h 5
 assumption
+
+end Tm31