namespace

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

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

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

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

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

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

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