From 66c8f85fb2bd2999e5da628962865e63f8652c64 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Sun, 17 Nov 2024 08:27:40 +0800
Subject: [PATCH] 25 states is enough

no 16

merge 16 to 4
---
 GoldbachTm.lean                               | 14 ++--
 GoldbachTm/Basic.lean                         |  2 +-
 GoldbachTm/{Tm26 => Tm25}/Content.lean        | 30 ++++----
 GoldbachTm/{Tm26 => Tm25}/Miscellaneous.lean  | 10 +--
 GoldbachTm/{Tm26 => Tm25}/PBP.lean            | 62 ++++++++---------
 GoldbachTm/{Tm26 => Tm25}/Prime.lean          | 40 +++++------
 GoldbachTm/{Tm26 => Tm25}/Search0.lean        | 48 ++++++-------
 .../{Tm26/Sim26.lean => Tm25/Sim25.lean}      |  4 +-
 GoldbachTm/{Tm26 => Tm25}/Transition.lean     | 14 ++--
 .../TuringMachine25.lean}                     | 68 +++++++++----------
 README.md                                     |  6 +-
 lakefile.lean                                 |  4 +-
 12 files changed, 151 insertions(+), 151 deletions(-)
 rename GoldbachTm/{Tm26 => Tm25}/Content.lean (83%)
 rename GoldbachTm/{Tm26 => Tm25}/Miscellaneous.lean (96%)
 rename GoldbachTm/{Tm26 => Tm25}/PBP.lean (85%)
 rename GoldbachTm/{Tm26 => Tm25}/Prime.lean (95%)
 rename GoldbachTm/{Tm26 => Tm25}/Search0.lean (94%)
 rename GoldbachTm/{Tm26/Sim26.lean => Tm25/Sim25.lean} (84%)
 rename GoldbachTm/{Tm26 => Tm25}/Transition.lean (81%)
 rename GoldbachTm/{Tm26/TuringMachine26.lean => Tm25/TuringMachine25.lean} (77%)

diff --git a/GoldbachTm.lean b/GoldbachTm.lean
index a80127a..9dfbdbf 100644
--- a/GoldbachTm.lean
+++ b/GoldbachTm.lean
@@ -4,13 +4,13 @@ import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank
 
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Search0
-import GoldbachTm.Tm26.Transition
-import GoldbachTm.Tm26.Miscellaneous
-import GoldbachTm.Tm26.Prime
-import GoldbachTm.Tm26.PBP
-import GoldbachTm.Tm26.Content
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Search0
+import GoldbachTm.Tm25.Transition
+import GoldbachTm.Tm25.Miscellaneous
+import GoldbachTm.Tm25.Prime
+import GoldbachTm.Tm25.PBP
+import GoldbachTm.Tm25.Content
 
 import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.Search0
diff --git a/GoldbachTm/Basic.lean b/GoldbachTm/Basic.lean
index 8e069c6..622ba79 100644
--- a/GoldbachTm/Basic.lean
+++ b/GoldbachTm/Basic.lean
@@ -129,7 +129,7 @@ induction n with
 
 /-
 P i => nth_cfg i ≠ none
-Q i n => nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
+Q i n => nth_cfg i = some ⟨⟨24, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
 -/
 theorem propagating_induction (P : ℕ → Prop) (Q : ℕ → ℕ → Prop)
                (base : ℕ) (hbase : Q base 0)
diff --git a/GoldbachTm/Tm26/Content.lean b/GoldbachTm/Tm25/Content.lean
similarity index 83%
rename from GoldbachTm/Tm26/Content.lean
rename to GoldbachTm/Tm25/Content.lean
index d584c1d..6d4781e 100644
--- a/GoldbachTm/Tm26/Content.lean
+++ b/GoldbachTm/Tm25/Content.lean
@@ -1,20 +1,20 @@
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Search0
-import GoldbachTm.Tm26.PBP
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Search0
+import GoldbachTm.Tm25.PBP
 import Mathlib.Data.Nat.Prime.Defs
 
-namespace Tm26
+namespace Tm25
 
-theorem lemma_22 (n : ℕ) (i : ℕ)
+theorem lemma_21 (n : ℕ) (i : ℕ)
 (even_n : Even (n+2))
 (g :
-nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4) Γ.one), Turing.ListBlank.mk []⟩⟩ )
+nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4) Γ.one), Turing.ListBlank.mk []⟩⟩ )
 ( hpp : Goldbach (n+4)) :
-∃ j>i, nth_cfg j = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4+2) Γ.one), Turing.ListBlank.mk []⟩⟩
+∃ j>i, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4+2) Γ.one), Turing.ListBlank.mk []⟩⟩
 := by
 forward g
 repeat rw [← List.replicate_succ] at g
-apply (leap_18 _ _ 0) at g
+apply (leap_17 _ _ 0) at g
 any_goals omega
 any_goals assumption
 refine (?_ ∘ g) ?_
@@ -40,7 +40,7 @@ refine (?_ ∘ g) ?_
 
 lemma never_halt_step (n : ℕ) :
 (∀ i < n, Goldbach (2*i+4)) ->
-∃ j, nth_cfg j = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
+∃ j, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
  := by
 induction n with
 | zero =>
@@ -54,7 +54,7 @@ refine (?_ ∘ induction_step) ?_
 . intros g
   obtain ⟨j, g⟩ := g
   specialize h n (by omega)
-  apply lemma_22 at g
+  apply lemma_21 at g
   . specialize g h
     obtain ⟨k, g⟩ := g
     use k
@@ -73,7 +73,7 @@ apply never_halt_step at IH
 obtain ⟨j, g⟩ := IH
 forward g
 repeat rw [← List.replicate_succ] at g
-apply (leap_18_halt _ _ 0) at g
+apply (leap_17_halt _ _ 0) at g
 any_goals omega
 by_contra! h
 refine (?_ ∘ g) ?_
@@ -88,10 +88,10 @@ refine (?_ ∘ g) ?_
 
 theorem halt_lemma_rev' (h : ∀ n, Goldbach (2*n+4)) :
 ∀ i, nth_cfg i ≠ none := by
-apply propagating_induction (fun i => nth_cfg i ≠ none) (fun i n => nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩) 45
+apply propagating_induction (fun i => nth_cfg i ≠ none) (fun i n => nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩) 45
 . simp [cfg45]; tauto
 . intros i n g
-  apply (lemma_22 (2*n)) at g
+  apply (lemma_21 (2*n)) at g
   . specialize g (h _)
     obtain ⟨j, g⟩ := g
     use j
@@ -120,7 +120,7 @@ by rw [← Mathlib.Tactic.PushNeg.not_not_eq (Goldbach (2*i+4))]
 )
 forward hj
 repeat rw [← List.replicate_succ] at hj
-apply (leap_18_halt _ _ 0) at hj
+apply (leap_17_halt _ _ 0) at hj
 any_goals omega
 apply hj
 intros x y _
@@ -135,4 +135,4 @@ by_contra! g
 apply halt_lemma_rev' at g
 tauto
 
-end Tm26
+end Tm25
diff --git a/GoldbachTm/Tm26/Miscellaneous.lean b/GoldbachTm/Tm25/Miscellaneous.lean
similarity index 96%
rename from GoldbachTm/Tm26/Miscellaneous.lean
rename to GoldbachTm/Tm25/Miscellaneous.lean
index e11a600..b21fdf0 100644
--- a/GoldbachTm/Tm26/Miscellaneous.lean
+++ b/GoldbachTm/Tm25/Miscellaneous.lean
@@ -1,9 +1,9 @@
 -- some lemmas tm31 doesn't contain
 
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Transition
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Transition
 
-namespace Tm26
+namespace Tm25
 
 theorem lemma7 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
 nth_cfg i = some ⟨⟨7, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
@@ -39,7 +39,7 @@ induction k with (intros i l r h; simp_all)
 
 theorem lemma5 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
 nth_cfg i = some ⟨⟨5, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
-nth_cfg (i + k + 2) = some ⟨⟨4, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate k Γ.zero ++ r)⟩⟩ := by
+nth_cfg (i + k + 2) = some ⟨⟨7, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate k Γ.zero ++ r)⟩⟩ := by
 induction k with (intros i l r h; simp_all)
 | zero => iterate 2 forward h
           rw [← h]
@@ -111,4 +111,4 @@ cases r1 with simp_all
              simp [h]
              omega
 
-end Tm26
+end Tm25
diff --git a/GoldbachTm/Tm26/PBP.lean b/GoldbachTm/Tm25/PBP.lean
similarity index 85%
rename from GoldbachTm/Tm26/PBP.lean
rename to GoldbachTm/Tm25/PBP.lean
index 31a4131..6191f6a 100644
--- a/GoldbachTm/Tm26/PBP.lean
+++ b/GoldbachTm/Tm25/PBP.lean
@@ -1,24 +1,24 @@
 -- PDP is short for "prime board prime"
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Search0
-import GoldbachTm.Tm26.Prime
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Search0
+import GoldbachTm.Tm25.Prime
 import Mathlib.Data.Nat.Prime.Defs
 
-namespace Tm26
+namespace Tm25
 
 -- l1 : count of 1 on the left
 -- r1 : count of 1 on the right
-theorem lemma_18 (i l1 r1: ℕ)
+theorem lemma_17 (i l1 r1: ℕ)
 (hp : ¬ Nat.Prime (l1+1) \/ ¬ Nat.Prime (r1+1))
 (g :
-nth_cfg i = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩
+nth_cfg i = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩
 ):
-∃ j>i, nth_cfg j = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate l1 Γ.one), Turing.ListBlank.mk (List.replicate (r1+2) Γ.one)⟩⟩ := by
+∃ j>i, nth_cfg j = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate l1 Γ.one), Turing.ListBlank.mk (List.replicate (r1+2) Γ.one)⟩⟩ := by
 forward g
 forward g
 forward g
 by_cases hr1 : Nat.Prime (r1+1)
-. refine (?_ ∘ (prime_21 (3+i) r1 (Γ.one :: List.replicate l1 Γ.one) [])) ?_
+. refine (?_ ∘ (prime_20 (3+i) r1 (Γ.one :: List.replicate l1 Γ.one) [])) ?_
   . intros g
     specialize g hr1
     obtain ⟨j, _, g⟩ := g
@@ -30,10 +30,10 @@ by_cases hr1 : Nat.Prime (r1+1)
       use 1
       tauto
     rw [h] at g
-    apply (rec24 l1 (1+j) []) at g
+    apply (rec23 l1 (1+j) []) at g
     forward g
     have h : ¬ Nat.Prime (l1+1) := by tauto
-    apply n_prime_17 at h
+    apply n_prime_16 at h
     pick_goal 5
     . rw [g]
       simp
@@ -41,7 +41,7 @@ by_cases hr1 : Nat.Prime (r1+1)
       all_goals rfl
     obtain ⟨m, _, h⟩ := h
     iterate 3 forward h
-    apply rec22 at h
+    apply rec21 at h
     forward h
     use (5+m+l1)
     constructor
@@ -61,7 +61,7 @@ by_cases hr1 : Nat.Prime (r1+1)
     left
     use 1
     tauto
-. apply n_prime_17 at hr1
+. apply n_prime_16 at hr1
   pick_goal 5
   . rw [g]
     simp
@@ -95,13 +95,13 @@ theorem both_prime (i l1 r1: ℕ)
 (hpr : Nat.Prime (r1+1))
 (even_sum : Even (l1+r1))
 (g :
-nth_cfg i = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩
+nth_cfg i = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩
 ) :
-∃ j>i, nth_cfg j = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (l1+r1+4) Γ.one), Turing.ListBlank.mk []⟩⟩ := by
+∃ j>i, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (l1+r1+4) Γ.one), Turing.ListBlank.mk []⟩⟩ := by
 forward g
 forward g
 forward g
-apply prime_21 at hpr
+apply prime_20 at hpr
 pick_goal 5
 . rw [g]
   simp
@@ -122,9 +122,9 @@ have h : Turing.ListBlank.mk (List.replicate l1 Γ.one) = Turing.ListBlank.mk (L
   use 1
   tauto
 rw [h] at g
-apply (rec24 l1 (1+j) []) at g
+apply (rec23 l1 (1+j) []) at g
 forward g
-apply prime_21 at hpl
+apply prime_20 at hpl
 pick_goal 5
 . rw [g]
   simp
@@ -133,7 +133,7 @@ obtain ⟨m, _, g⟩ := hpl
 forward g
 forward g
 forward g
-apply rec23 at g
+apply rec22 at g
 forward g
 rw [← List.cons_append] at g
 rw [← List.replicate_succ] at g
@@ -141,7 +141,7 @@ rw [← List.cons_append] at g
 rw [← List.replicate_succ] at g
 rw [List.append_cons] at g
 rw [← List.replicate_succ'] at g
-apply rec24 at g
+apply rec23 at g
 forward g
 rw [← List.cons_append] at g
 rw [← List.replicate_succ] at g
@@ -151,7 +151,7 @@ rw [List.append_cons] at g
 rw [← List.replicate_succ'] at g
 rw [← List.append_assoc] at g
 rw [← List.replicate_add] at g
-apply n_prime_17 at g
+apply n_prime_16 at g
 refine (?_ ∘ g) ?_
 . clear g
   intros g
@@ -161,7 +161,7 @@ refine (?_ ∘ g) ?_
   forward g
   rw [← List.cons_append] at g
   rw [← List.replicate_succ] at g
-  apply rec22 at g
+  apply rec21 at g
   use (3 + n + (2 + l1 + r1 + 1) + 1)
   constructor
   . omega
@@ -182,12 +182,12 @@ refine (?_ ∘ g) ?_
     assumption
 
 
-theorem leap_18 (l1 : ℕ) : ∀ (i r1: ℕ),
+theorem leap_17 (l1 : ℕ) : ∀ (i r1: ℕ),
 l1 + r1 ≥ 2 →
 Even (l1+r1) →
-nth_cfg i = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩ →
+nth_cfg i = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩ →
 (∃ x y, x + y = l1 + r1 + 2 /\ Nat.Prime x /\ Nat.Prime y /\ (r1+1) ≤ x /\ x ≤ y) →
-∃ j>i, nth_cfg j = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (l1+r1+4) Γ.one), Turing.ListBlank.mk []⟩⟩
+∃ j>i, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (l1+r1+4) Γ.one), Turing.ListBlank.mk []⟩⟩
 := by
 induction l1 with
 | zero => omega
@@ -195,7 +195,7 @@ induction l1 with
   intros i r1 h _ g hpp
   by_cases hp : ¬ Nat.Prime (l1+2) \/ ¬ Nat.Prime (r1+1)
   . -- induction step
-    apply lemma_18 at g
+    apply lemma_17 at g
     any_goals tauto
     obtain ⟨j, _, g⟩ := g
     apply induction_step at g
@@ -231,9 +231,9 @@ induction l1 with
     all_goals tauto
 
 
-theorem leap_18_halt (l1 : ℕ) : ∀ (i r1: ℕ),
+theorem leap_17_halt (l1 : ℕ) : ∀ (i r1: ℕ),
 l1 + r1 ≥ 2 →
-nth_cfg i = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩ →
+nth_cfg i = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩ →
 (∀ x y, x + y = l1 + r1 + 2 /\ Nat.Prime x /\ Nat.Prime y → False) →
 ∃ j, nth_cfg j = none
 := by
@@ -249,7 +249,7 @@ induction l1 with
   rw [← List.replicate_succ] at g
   rw [← List.replicate_succ] at g
   by_cases hp : Nat.Prime (r2+3)
-  . apply prime_21 at hp
+  . apply prime_20 at hp
     pick_goal 5
     . rw [g]
       simp
@@ -263,7 +263,7 @@ induction l1 with
     obtain ⟨j, _, h⟩ := hp
     iterate 13 forward h
     use (13+j)
-  . apply n_prime_17 at hp
+  . apply n_prime_16 at hp
     pick_goal 5
     . rw [g]
       simp
@@ -279,7 +279,7 @@ induction l1 with
     use (3+j)
 | succ l1 induction_step =>
     intros i r1 h g hpp
-    apply lemma_18 at g
+    apply lemma_17 at g
     . obtain ⟨j, _, g⟩ := g
       apply induction_step at g
       any_goals omega
@@ -293,4 +293,4 @@ induction l1 with
       ring_nf
       tauto
 
-end Tm26
+end Tm25
diff --git a/GoldbachTm/Tm26/Prime.lean b/GoldbachTm/Tm25/Prime.lean
similarity index 95%
rename from GoldbachTm/Tm26/Prime.lean
rename to GoldbachTm/Tm25/Prime.lean
index 62a554e..3b8cfc1 100644
--- a/GoldbachTm/Tm26/Prime.lean
+++ b/GoldbachTm/Tm25/Prime.lean
@@ -1,8 +1,10 @@
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Transition
-import GoldbachTm.Tm26.Miscellaneous
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Transition
+import GoldbachTm.Tm25.Miscellaneous
+import Mathlib.Data.Nat.ModEq
+import Mathlib.Data.Nat.Prime.Basic
 
-namespace Tm26
+namespace Tm25
 
 -- c1++, c2++
 --    l 0 [la 11] 0  [lb 11] 0 [ra 11111] 0  [(rb+1) 1] 0 r
@@ -147,10 +149,10 @@ cases lb' with (simp! [*, -nth_cfg] at g; simp_all)
           ring_nf at *
           apply Nat.ModEq.trans h₁
           rw [Nat.modEq_zero_iff_dvd]
-| succ lb' => apply lemma_15_to_19 at g
+| succ lb' => apply lemma_15_to_18 at g
               obtain ⟨m, g⟩ := g
               forward g
-              apply rec20 at g
+              apply rec19 at g
               forward g
               forward g
               forward g
@@ -184,13 +186,13 @@ cases lb' with (simp! [*, -nth_cfg] at g; simp_all)
 --
 --    l 0 1 1  [lb 11]    1  1  [rb 1] 0 r
 --      ^
---      17
+--      16
 theorem step_10_dvd (i lb rb: ℕ) (l r : List Γ) :
 nth_cfg i = some ⟨⟨10, by omega⟩, ⟨Γ.one,
   Turing.ListBlank.mk (List.replicate lb Γ.one ++ Γ.zero :: Γ.one :: Γ.zero :: l),
   Turing.ListBlank.mk (List.cons Γ.zero (List.replicate rb Γ.one ++ List.cons Γ.zero r))⟩⟩ →
   (lb + 2) ∣ (rb + 2) →
-∃ j>i, nth_cfg j = some ⟨⟨17, by omega⟩, ⟨Γ.zero,
+∃ j>i, nth_cfg j = some ⟨⟨16, by omega⟩, ⟨Γ.zero,
   Turing.ListBlank.mk l,
   Turing.ListBlank.mk (List.replicate (lb+rb+4) Γ.one ++ List.cons Γ.zero r)⟩⟩
 := by
@@ -211,7 +213,7 @@ cases lb' with (simp! [*, -nth_cfg] at g; simp_all)
 | zero => subst la'
           forward g
           forward g
-          apply rec17 at g
+          apply rec16 at g
           use (6 + k + j + rb + (1+lb)+1)
           constructor
           . omega
@@ -272,11 +274,11 @@ induction rb with intros i lb l r g p
                 rw [← List.replicate_succ]
                 ring_nf
 
-theorem prime_21 (i r1: ℕ) (l r : List Γ)
+theorem prime_20 (i r1: ℕ) (l r : List Γ)
 (g :
 nth_cfg i = some ⟨⟨0, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩)
 (p : Nat.Prime (r1+1)) :
-∃ j>i, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (r1+1) Γ.one ++ List.cons Γ.zero r)⟩⟩ :=
+∃ j>i, nth_cfg j = some ⟨⟨20, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (r1+1) Γ.one ++ List.cons Γ.zero r)⟩⟩ :=
 match h : r1 with
 | Nat.zero => by subst r1
                  exfalso
@@ -327,10 +329,10 @@ match h : r1 with
   | zero => exfalso
             have g : ¬ Nat.Prime 4 := by decide
             apply g p
-  | succ r1 => apply lemma_15_to_19 at g
+  | succ r1 => apply lemma_15_to_18 at g
                obtain ⟨k, g⟩ := g
                forward g
-               apply rec20 at g
+               apply rec19 at g
                forward g
                forward g
                forward g
@@ -339,7 +341,7 @@ match h : r1 with
                rw [List.append_cons, ← List.replicate_succ'] at g
                rw [← List.cons_append] at g
                rw [← List.replicate_succ] at g
-               apply rec21 at g
+               apply rec20 at g
                use (11 + k + j + r1 + (r1 + 1 + 1 + 1) + 1)
                constructor
                . omega
@@ -354,13 +356,13 @@ match h : r1 with
 --
 --    l 0 1 1  [lb 11]    1  1  [rb 1] 0 r
 --      ^
---      17
+--      16
 theorem leap_10_dvd  (rb : ℕ) : ∀ (i lb: ℕ) (l r : List Γ),
 nth_cfg i = some ⟨⟨10, by omega⟩, ⟨Γ.one,
   Turing.ListBlank.mk (List.replicate lb Γ.one ++ Γ.zero :: Γ.one :: Γ.zero :: l),
   Turing.ListBlank.mk (List.cons Γ.zero (List.replicate rb Γ.one ++ List.cons Γ.zero r))⟩⟩ →
 (∃ divisor, divisor ≥ (lb+2) /\ divisor < lb + rb + 4 /\ divisor ∣ (lb + rb + 4)) →
-∃ j>i, nth_cfg j = some ⟨⟨17, by omega⟩, ⟨Γ.zero,
+∃ j>i, nth_cfg j = some ⟨⟨16, by omega⟩, ⟨Γ.zero,
   Turing.ListBlank.mk l,
   Turing.ListBlank.mk (List.replicate (lb+rb+4) Γ.one ++ List.cons Γ.zero r)⟩⟩
 := by
@@ -415,11 +417,11 @@ induction rb with intros i lb l r g hd
                     assumption
                   . omega
 
-theorem n_prime_17 (i r1: ℕ) (l r : List Γ)
+theorem n_prime_16 (i r1: ℕ) (l r : List Γ)
 (g :
 nth_cfg i = some ⟨⟨0, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩)
 (hp : ¬ Nat.Prime (r1+1)) :
-∃ j>i, nth_cfg j = some ⟨⟨17, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (r1+1) Γ.one ++ List.cons Γ.zero r)⟩⟩ :=
+∃ j>i, nth_cfg j = some ⟨⟨16, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (r1+1) Γ.one ++ List.cons Γ.zero r)⟩⟩ :=
 match r1 with
 | Nat.zero => by simp_all
                  forward g
@@ -462,4 +464,4 @@ match r1 with
     rw [g] at h
     exact h
 
-end Tm26
+end Tm25
diff --git a/GoldbachTm/Tm26/Search0.lean b/GoldbachTm/Tm25/Search0.lean
similarity index 94%
rename from GoldbachTm/Tm26/Search0.lean
rename to GoldbachTm/Tm25/Search0.lean
index eca6143..a68d8b2 100644
--- a/GoldbachTm/Tm26/Search0.lean
+++ b/GoldbachTm/Tm25/Search0.lean
@@ -1,8 +1,8 @@
 -- theorem of recursive states
 -- all these states' usage is to search 0
-import GoldbachTm.Tm26.TuringMachine26
+import GoldbachTm.Tm25.TuringMachine25
 
-namespace Tm26
+namespace Tm25
 
 -- left
 theorem rec13 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
@@ -29,9 +29,9 @@ induction k with intros i l r h
             . simp [List.replicate_succ' (k+1)]
             . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 
-theorem rec17 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
-nth_cfg i = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
-nth_cfg (i + k + 1) = some ⟨⟨17, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
+theorem rec16 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨16, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨16, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
 induction k with intros i l r h
 | zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 | succ k induction_step =>
@@ -41,9 +41,9 @@ induction k with intros i l r h
             . simp [List.replicate_succ' (k+1)]
             . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 
-theorem rec19 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
-nth_cfg i = some ⟨⟨19, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
-nth_cfg (i + k + 1) = some ⟨⟨19, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
+theorem rec18 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨18, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
 induction k with intros i l r h
 | zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 | succ k induction_step =>
@@ -53,9 +53,9 @@ induction k with intros i l r h
             . simp [List.replicate_succ' (k+1)]
             . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 
-theorem rec21 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
-nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
-nth_cfg (i + k + 1) = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
+theorem rec20 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨20, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨20, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
 induction k with intros i l r h
 | zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 | succ k induction_step =>
@@ -65,9 +65,9 @@ induction k with intros i l r h
             . simp [List.replicate_succ' (k+1)]
             . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 
-theorem rec24 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
-nth_cfg i = some ⟨⟨24, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
-nth_cfg (i + k + 1) = some ⟨⟨24, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
+theorem rec23 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨23, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨23, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
 induction k with intros i l r h
 | zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 | succ k induction_step =>
@@ -90,9 +90,9 @@ induction k with intros i l r h
             . simp [List.replicate_succ' (k+1)]
             . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 
-theorem rec20 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
-nth_cfg i = some ⟨⟨20, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
-nth_cfg (i + k + 1) = some ⟨⟨20, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ l), Turing.ListBlank.mk r⟩⟩ := by
+theorem rec19 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨19, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨19, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ l), Turing.ListBlank.mk r⟩⟩ := by
 induction k with intros i l r h
 | zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 | succ k induction_step =>
@@ -102,9 +102,9 @@ induction k with intros i l r h
             . simp [List.replicate_succ' (k+1)]
             . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 
-theorem rec23 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
-nth_cfg i = some ⟨⟨23, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
-nth_cfg (i + k + 1) = some ⟨⟨23, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ l), Turing.ListBlank.mk r⟩⟩ := by
+theorem rec22 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ l), Turing.ListBlank.mk r⟩⟩ := by
 induction k with intros i l r h
 | zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 | succ k induction_step =>
@@ -114,9 +114,9 @@ induction k with intros i l r h
             . simp [List.replicate_succ' (k+1)]
             . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 
-theorem rec22 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
-nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
-nth_cfg (i + k + 1) = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ l), Turing.ListBlank.mk r⟩⟩ := by
+theorem rec21 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ l), Turing.ListBlank.mk r⟩⟩ := by
 induction k with intros i l r h
 | zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 | succ k induction_step =>
@@ -126,4 +126,4 @@ induction k with intros i l r h
             . simp [List.replicate_succ' (k+1)]
             . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 
-end Tm26
+end Tm25
diff --git a/GoldbachTm/Tm26/Sim26.lean b/GoldbachTm/Tm25/Sim25.lean
similarity index 84%
rename from GoldbachTm/Tm26/Sim26.lean
rename to GoldbachTm/Tm25/Sim25.lean
index 03bdaf2..8d943c0 100644
--- a/GoldbachTm/Tm26/Sim26.lean
+++ b/GoldbachTm/Tm25/Sim25.lean
@@ -1,7 +1,7 @@
-import GoldbachTm.Tm26.TuringMachine26
+import GoldbachTm.Tm25.TuringMachine25
 import GoldbachTm.Basic
 
-open Tm26
+open Tm25
 
 unsafe def foo (cfg : Cfg) : IO Unit :=
 match (step machine cfg) with
diff --git a/GoldbachTm/Tm26/Transition.lean b/GoldbachTm/Tm25/Transition.lean
similarity index 81%
rename from GoldbachTm/Tm26/Transition.lean
rename to GoldbachTm/Tm25/Transition.lean
index 0f313f1..82de13e 100644
--- a/GoldbachTm/Tm26/Transition.lean
+++ b/GoldbachTm/Tm25/Transition.lean
@@ -1,7 +1,7 @@
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Search0
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Search0
 
-namespace Tm26
+namespace Tm25
 
 theorem lemma_10_to_11 (i : ℕ) (r1: ℕ) (l r : List Γ)
 (h :
@@ -20,13 +20,13 @@ cases r1 with
              rw [← h]
              ring_nf
 
-theorem lemma_15_to_19 (i : ℕ) (l1: ℕ) (l r : List Γ)
+theorem lemma_15_to_18 (i : ℕ) (l1: ℕ) (l r : List Γ)
 (h :
 nth_cfg i = some ⟨⟨15, by omega⟩, ⟨Γ.one,
   Turing.ListBlank.mk (List.replicate l1 Γ.one ++ List.cons Γ.zero l),
   Turing.ListBlank.mk r,
   ⟩⟩) :
-∃ j, nth_cfg (j + i) = some ⟨⟨19, by omega⟩, ⟨Γ.zero,
+∃ j, nth_cfg (j + i) = some ⟨⟨18, by omega⟩, ⟨Γ.zero,
     Turing.ListBlank.mk l,
     Turing.ListBlank.mk (List.replicate (l1+1) Γ.one ++ r),
     ⟩⟩
@@ -35,11 +35,11 @@ forward h
 cases l1 with simp! [*, -nth_cfg] at h
 | zero => use 1
           simp [h]
-| succ r1 =>  apply rec19 at h
+| succ r1 =>  apply rec18 at h
               use (r1+2)
               ring_nf at *
               simp [h]
               rw [List.append_cons, ← List.replicate_succ']
               ring_nf
 
-end Tm26
+end Tm25
diff --git a/GoldbachTm/Tm26/TuringMachine26.lean b/GoldbachTm/Tm25/TuringMachine25.lean
similarity index 77%
rename from GoldbachTm/Tm26/TuringMachine26.lean
rename to GoldbachTm/Tm25/TuringMachine25.lean
index acf6fa2..3c1ede9 100644
--- a/GoldbachTm/Tm26/TuringMachine26.lean
+++ b/GoldbachTm/Tm25/TuringMachine25.lean
@@ -1,19 +1,19 @@
 -- inspired by https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Computability/TuringMachine.lean
 import Mathlib.Computability.TuringMachine
-import Mathlib.Data.Real.Sqrt
+import Mathlib.Tactic.Ring.RingNF
 import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank
 
-namespace Tm26
+namespace Tm25
 
 open Lean Meta Elab Tactic Std Term
 
-def Machine := Fin 26 → Γ → Option (Fin 26 × Stmt)
+def Machine := Fin 25 → Γ → Option (Fin 25 × Stmt)
 
 structure Cfg where
   /-- The current machine state. -/
-  q : Fin 26
+  q : Fin 25
   /-- The current state of the tape: current symbol, left and right parts. -/
   Tape : Turing.Tape Γ
 
@@ -38,17 +38,17 @@ def step (M : Machine) : Cfg → Option Cfg :=
 
 
 def machine : Machine
-| ⟨ 0, _⟩, Γ.zero => some ⟨⟨23, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
+| ⟨ 0, _⟩, Γ.zero => some ⟨⟨22, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
 | ⟨ 0, _⟩, Γ.one  => some ⟨⟨ 1, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
-| ⟨ 1, _⟩, Γ.zero => some ⟨⟨17, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
+| ⟨ 1, _⟩, Γ.zero => some ⟨⟨16, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
 | ⟨ 1, _⟩, Γ.one  => some ⟨⟨ 2, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
-| ⟨ 2, _⟩, Γ.zero => some ⟨⟨21, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
+| ⟨ 2, _⟩, Γ.zero => some ⟨⟨20, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
 | ⟨ 2, _⟩, Γ.one  => some ⟨⟨ 3, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
-| ⟨ 3, _⟩, Γ.zero => some ⟨⟨21, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
+| ⟨ 3, _⟩, Γ.zero => some ⟨⟨20, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
 | ⟨ 3, _⟩, Γ.one  => some ⟨⟨ 4, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
-| ⟨ 4, _⟩, Γ.zero => some ⟨⟨ 9, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
+| ⟨ 4, _⟩, Γ.zero => some ⟨⟨16, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
 | ⟨ 4, _⟩, Γ.one  => some ⟨⟨ 5, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
-| ⟨ 5, _⟩, Γ.zero => some ⟨⟨ 4, by omega⟩, ⟨Turing.Dir.right, Γ.zero⟩⟩
+| ⟨ 5, _⟩, Γ.zero => some ⟨⟨ 7, by omega⟩, ⟨Turing.Dir.right, Γ.zero⟩⟩
 | ⟨ 5, _⟩, Γ.one  => some ⟨⟨ 5, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
 | ⟨ 6, _⟩, Γ.zero => some ⟨⟨ 8, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
 | ⟨ 6, _⟩, Γ.one  => some ⟨⟨ 7, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
@@ -57,7 +57,7 @@ def machine : Machine
 | ⟨ 8, _⟩, Γ.zero => some ⟨⟨ 9, by omega⟩, ⟨Turing.Dir.right, Γ.zero⟩⟩
 | ⟨ 8, _⟩, Γ.one  => some ⟨⟨ 8, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
 | ⟨ 9, _⟩, Γ.zero => some ⟨⟨10, by omega⟩, ⟨Turing.Dir.right, Γ.zero⟩⟩
-| ⟨ 9, _⟩, Γ.one  => some ⟨⟨22, by omega⟩, ⟨Turing.Dir.right, Γ.zero⟩⟩
+| ⟨ 9, _⟩, Γ.one  => some ⟨⟨21, by omega⟩, ⟨Turing.Dir.right, Γ.zero⟩⟩
 | ⟨10, _⟩, Γ.zero => some ⟨⟨10, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
 | ⟨10, _⟩, Γ.one  => some ⟨⟨11, by omega⟩, ⟨Turing.Dir.right, Γ.zero⟩⟩
 | ⟨11, _⟩, Γ.zero => some ⟨⟨12, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
@@ -68,29 +68,27 @@ def machine : Machine
 | ⟨13, _⟩, Γ.one  => some ⟨⟨13, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
 | ⟨14, _⟩, Γ.zero => some ⟨⟨15, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
 | ⟨14, _⟩, Γ.one  => some ⟨⟨14, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
-| ⟨15, _⟩, Γ.zero => some ⟨⟨16, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
-| ⟨15, _⟩, Γ.one  => some ⟨⟨19, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
+| ⟨15, _⟩, Γ.zero => some ⟨⟨ 4, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
+| ⟨15, _⟩, Γ.one  => some ⟨⟨18, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
 | ⟨16, _⟩, Γ.zero => some ⟨⟨17, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
-| ⟨16, _⟩, Γ.one  => none -- unreachable
-| ⟨17, _⟩, Γ.zero => some ⟨⟨18, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
-| ⟨17, _⟩, Γ.one  => some ⟨⟨17, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
-| ⟨18, _⟩, Γ.zero => some ⟨⟨ 9, by omega⟩, ⟨Turing.Dir.right, Γ.zero⟩⟩
-| ⟨18, _⟩, Γ.one  => some ⟨⟨25, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
-| ⟨19, _⟩, Γ.zero => some ⟨⟨20, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
-| ⟨19, _⟩, Γ.one  => some ⟨⟨19, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
-| ⟨20, _⟩, Γ.zero => some ⟨⟨ 2, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
-| ⟨20, _⟩, Γ.one  => some ⟨⟨20, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
-| ⟨21, _⟩, Γ.zero => some ⟨⟨24, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
-| ⟨21, _⟩, Γ.one  => some ⟨⟨21, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
-| ⟨22, _⟩, Γ.zero => some ⟨⟨18, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
+| ⟨16, _⟩, Γ.one  => some ⟨⟨16, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
+| ⟨17, _⟩, Γ.zero => some ⟨⟨ 9, by omega⟩, ⟨Turing.Dir.right, Γ.zero⟩⟩
+| ⟨17, _⟩, Γ.one  => some ⟨⟨24, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
+| ⟨18, _⟩, Γ.zero => some ⟨⟨19, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
+| ⟨18, _⟩, Γ.one  => some ⟨⟨18, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
+| ⟨19, _⟩, Γ.zero => some ⟨⟨ 2, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
+| ⟨19, _⟩, Γ.one  => some ⟨⟨19, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
+| ⟨20, _⟩, Γ.zero => some ⟨⟨23, by omega⟩, ⟨Turing.Dir.left, Γ.zero⟩⟩
+| ⟨20, _⟩, Γ.one  => some ⟨⟨20, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
+| ⟨21, _⟩, Γ.zero => some ⟨⟨17, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
+| ⟨21, _⟩, Γ.one  => some ⟨⟨21, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
+| ⟨22, _⟩, Γ.zero => some ⟨⟨23, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
 | ⟨22, _⟩, Γ.one  => some ⟨⟨22, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
-| ⟨23, _⟩, Γ.zero => some ⟨⟨24, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
-| ⟨23, _⟩, Γ.one  => some ⟨⟨23, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
-| ⟨24, _⟩, Γ.zero => some ⟨⟨ 0, by omega⟩, ⟨Turing.Dir.right, Γ.zero⟩⟩
-| ⟨24, _⟩, Γ.one  => some ⟨⟨24, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
-| ⟨25, _⟩, Γ.zero => none
-| ⟨25, _⟩, Γ.one  => some ⟨⟨24, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
-| ⟨_+26, _⟩, _ => by omega -- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20on.20Fin.20isn't.20exhaustive.20for.20large.20matches/near/428048252
+| ⟨23, _⟩, Γ.zero => some ⟨⟨ 0, by omega⟩, ⟨Turing.Dir.right, Γ.zero⟩⟩
+| ⟨23, _⟩, Γ.one  => some ⟨⟨23, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
+| ⟨24, _⟩, Γ.zero => none
+| ⟨24, _⟩, Γ.one  => some ⟨⟨23, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
+| ⟨_+25, _⟩, _ => by omega -- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20on.20Fin.20isn't.20exhaustive.20for.20large.20matches/near/428048252
 
 def nth_cfg : (n : Nat) -> Option Cfg
 | 0 => init []
@@ -99,7 +97,7 @@ def nth_cfg : (n : Nat) -> Option Cfg
                 | some cfg =>  step machine cfg
 
 
--- https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/binderIdent.20vs.20Ident/near/402517388
+-- https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/binderIdent.20vs.20Ident/near/402516388
 def toBinderIdent (i : Ident) : TSyntax ``binderIdent := Unhygienic.run <|
   withRef i `(binderIdent| $i:ident)
 
@@ -125,7 +123,7 @@ elab "forward" g:ident : tactic => withSynthesize <| withMainContext do
   | _ => logInfo m!"please forward on nth_cfg i = some ⟨...⟩"
 
 
-theorem cfg45 : nth_cfg 45 = some ⟨22,
+theorem cfg45 : nth_cfg 45 = some ⟨21,
         { head := default, left := Turing.ListBlank.mk (List.replicate 4 Γ.one), right := Turing.ListBlank.mk [] } ⟩ := by
 have h : nth_cfg 0 = init [] := by simp!
 simp [init, Turing.Tape.mk₁, Turing.Tape.mk₂, Turing.Tape.mk'] at h
@@ -140,4 +138,4 @@ constructor
   tauto
 
 
-end Tm26
+end Tm25
diff --git a/README.md b/README.md
index c90fe4f..c2eceb0 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-# goldbach_tm26
+# goldbach_tm25
 
 https://gist.github.com/anonymous/a64213f391339236c2fe31f8749a0df6
 give a 27-state Turing machine which halts if, and only if, Goldbach's conjecture is false.
@@ -10,7 +10,7 @@ This repo verifies the 26-state and 31-state Turing machine formally in lean4
 ## Verify the proof
 
 ```
-# main results at `GoldbachTm/Tm26/Content.lean`
+# main results at `GoldbachTm/Tm25/Content.lean`
 lake build
 ```
 
@@ -18,7 +18,7 @@ lake build
 ## Run simulator
 
 ```
-lake exe sim26
+lake exe sim25
 lake exe sim31
 ```
 
diff --git a/lakefile.lean b/lakefile.lean
index 3881f24..22bfbc2 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -17,5 +17,5 @@ lean_lib «GoldbachTm» where
 lean_exe «sim31» where
   root := `GoldbachTm.Tm31.Sim31
 
-lean_exe «sim26» where
-  root := `GoldbachTm.Tm26.Sim26
+lean_exe «sim25» where
+  root := `GoldbachTm.Tm25.Sim25