diff --git a/GoldbachTm.lean b/GoldbachTm.lean
index c732ab9..5e80542 100644
--- a/GoldbachTm.lean
+++ b/GoldbachTm.lean
@@ -3,10 +3,18 @@
 import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank
+
 import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm27.Search0
+import GoldbachTm.Tm27.Transition
+import GoldbachTm.Tm27.Miscellaneous
+import GoldbachTm.Tm27.Prime
+import GoldbachTm.Tm27.PBP
+import GoldbachTm.Tm27.Content
+
 import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.Search0
-import GoldbachTm.Tm31.Content
+import GoldbachTm.Tm31.Transition
 import GoldbachTm.Tm31.Prime
 import GoldbachTm.Tm31.PBP
-import GoldbachTm.Tm31.Transition
+import GoldbachTm.Tm31.Content
diff --git a/GoldbachTm/Tm27/Content.lean b/GoldbachTm/Tm27/Content.lean
new file mode 100644
index 0000000..329e125
--- /dev/null
+++ b/GoldbachTm/Tm27/Content.lean
@@ -0,0 +1,126 @@
+import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm27.Search0
+import GoldbachTm.Tm27.PBP
+import Mathlib.Data.Nat.Prime.Defs
+
+namespace Tm27
+
+theorem lemma_26 (n : ℕ) (i : ℕ)
+(even_n : Even (n+2))
+(g :
+nth_cfg i = some ⟨⟨26, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4) Γ.one), Turing.ListBlank.mk []⟩⟩ )
+( hpp : goldbach (n+4)) :
+∃ j>i, nth_cfg j = some ⟨⟨26, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4+2) Γ.one), Turing.ListBlank.mk []⟩⟩
+:= by
+forward g g i
+repeat rw [← List.replicate_succ] at g
+apply (leap_18 _ _ 0) at g
+any_goals omega
+any_goals assumption
+refine (?_ ∘ g) ?_
+. intros g
+  obtain ⟨k, _, h⟩ := g
+  use k
+  constructor
+  . omega
+  . simp [h]
+. obtain ⟨x, y, _, hx, hy⟩ := hpp
+  by_cases x ≤ y
+  . use! x, y
+    repeat any_goals apply And.intro
+    any_goals assumption
+    apply Nat.Prime.two_le at hx
+    omega
+  . use! y, x
+    repeat any_goals apply And.intro
+    any_goals assumption
+    any_goals omega
+    apply Nat.Prime.two_le at hy
+    omega
+
+lemma never_halt_step (n : ℕ) :
+(∀ i < n, goldbach (2*i+4)) ->
+∃ j, nth_cfg j = some ⟨⟨26, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
+ := by
+induction n with
+| zero =>
+intros _
+use 45
+simp [cfg45]
+tauto
+| succ n =>
+rename_i induction_step
+intros h
+refine (?_ ∘ induction_step) ?_
+. intros g
+  obtain ⟨j, g⟩ := g
+  specialize h n (by omega)
+  apply lemma_26 at g
+  . specialize g h
+    obtain ⟨k, g⟩ := g
+    use k
+    simp [g]
+    ring_nf
+  . use (n+1)
+    ring_nf
+. intros i hi
+  apply h i (by omega)
+
+theorem never_halt (never_none : ∀ i, nth_cfg i ≠ none) (n : ℕ):
+goldbach (2*n + 4)
+:= by
+induction' n using Nat.strongRecOn with n IH
+apply never_halt_step at IH
+obtain ⟨j, g⟩ := IH
+by_contra! h
+forward g g j
+repeat rw [← List.replicate_succ] at g
+apply (leap_18_halt _ _ 0) at g
+any_goals omega
+refine (?_ ∘ g) ?_
+. intros h
+  obtain ⟨k, h⟩ := h
+  apply never_none _ h
+. intros x y _
+  apply h ⟨x, y, ?_⟩
+  ring_nf at *
+  tauto
+
+
+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 ⟨⟨26, 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_26 (2*n)) at g
+  . specialize g (h _)
+    obtain ⟨j, g⟩ := g
+    use j
+    simp! [g]
+  . use (n+1)
+    ring_nf
+. intros i n g j hij _
+  have h₂ : ∀ k, nth_cfg (j+k) = none := by
+    intro k
+    induction k with
+    | zero => tauto
+    | succ k => rename_i h₁
+                forward h₁ h₁ (j+k)
+                rw [← h₁]
+                ring_nf
+  specialize h₂ (i-j)
+  have h₃ : j + (i-j) = i := by omega
+  rw [h₃] at h₂
+  rw [h₂] at g
+  tauto
+
+theorem halt_lemma_rev :
+(∃ i, nth_cfg i = none) → (∃ n, ¬ goldbach (2*n+4))
+:= by
+intros h
+by_contra! g
+apply halt_lemma_rev' at g
+tauto
+
+
+end Tm27
diff --git a/GoldbachTm/Tm27/Miscellaneous.lean b/GoldbachTm/Tm27/Miscellaneous.lean
new file mode 100644
index 0000000..c32bc5e
--- /dev/null
+++ b/GoldbachTm/Tm27/Miscellaneous.lean
@@ -0,0 +1,116 @@
+-- some lemmas tm31 doesn't contain
+
+import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm27.Transition
+
+namespace Tm27
+
+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⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨7, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.zero ++ r)⟩⟩ := by
+induction k with (intros i l r h; simp_all)
+| zero => forward h h i
+          rw [← h]
+          ring_nf
+| succ k => forward h h i
+            rename_i induction_step
+            apply induction_step at h
+            ring_nf at *
+            simp! [h]
+            rw [List.append_cons]
+            rw [← List.replicate_succ']
+            ring_nf
+
+theorem lemma8 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨8, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 2) = some ⟨⟨9, 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 => forward h h i
+          forward h h (1+i)
+          rw [← h]
+          ring_nf
+| succ k => forward h h i
+            rename_i induction_step
+            apply induction_step at h
+            ring_nf at *
+            simp! [h]
+            rw [List.append_cons]
+            rw [← List.replicate_succ']
+            ring_nf
+
+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
+induction k with (intros i l r h; simp_all)
+| zero => forward h h i
+          forward h h (1+i)
+          rw [← h]
+          ring_nf
+| succ k => forward h h i
+            rename_i induction_step
+            apply induction_step at h
+            ring_nf at *
+            simp! [h]
+            rw [List.append_cons]
+            rw [← List.replicate_succ']
+            ring_nf
+
+theorem lemma10 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨10, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.zero ++ List.cons Γ.one r) ⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨10, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ l), Turing.ListBlank.mk r⟩⟩ := by
+induction k with (intros i l r h; simp_all)
+| zero => forward h h i
+          rw [← h]
+          ring_nf
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) (List.cons Γ.one l) r
+            have g : i + (k+1) +1 = i + 1 + k + 1 := by omega
+            rw [g, induction_step]
+            . simp [List.replicate_succ' (k+1)]
+            . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+
+theorem lemma_6_to_7 (i : ℕ) (l1: ℕ) (l r : List Γ)
+(h :
+nth_cfg i = some ⟨⟨6, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk (List.replicate l1 Γ.one ++ List.cons Γ.zero l),
+  Turing.ListBlank.mk r,
+  ⟩⟩) :
+∃ j>i, nth_cfg j = some ⟨⟨7, by omega⟩, ⟨Γ.zero,
+    Turing.ListBlank.mk l,
+    Turing.ListBlank.mk (List.replicate (l1+1) Γ.zero ++ r),
+    ⟩⟩
+:= by
+forward h h i
+cases l1 with
+| zero => use (1+i)
+          simp [h]
+| succ l1 => simp! at h
+             apply lemma7 at h
+             use (1+i+l1 + 1)
+             simp [h]
+             constructor
+             . omega
+             . rw [List.append_cons, ← List.replicate_succ']
+
+theorem lemma_9_to_10 (i : ℕ) (r1: ℕ) (l r : List Γ)
+(h :
+nth_cfg i = some ⟨⟨9, by omega⟩, ⟨Γ.zero,
+  Turing.ListBlank.mk l,
+  Turing.ListBlank.mk (List.replicate r1 Γ.zero ++ List.cons Γ.one r),
+  ⟩⟩) :
+∃ j>i, nth_cfg j = some ⟨⟨10, by omega⟩, ⟨Γ.one,
+    Turing.ListBlank.mk (List.replicate r1 Γ.one ++ Γ.zero :: l),
+    Turing.ListBlank.mk r,
+    ⟩⟩
+:= by
+forward h h i
+cases r1 with simp_all
+| zero => use (1+i)
+          simp [h]
+| succ l1 => simp! at h
+             apply lemma10 at h
+             use (1+i+l1 + 1)
+             simp [h]
+             omega
+
+end Tm27
diff --git a/GoldbachTm/Tm27/PBP.lean b/GoldbachTm/Tm27/PBP.lean
new file mode 100644
index 0000000..5fabbbe
--- /dev/null
+++ b/GoldbachTm/Tm27/PBP.lean
@@ -0,0 +1,315 @@
+-- PDP is short for "prime board prime"
+import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm27.Search0
+import GoldbachTm.Tm27.Prime
+import Mathlib.Data.Nat.Prime.Defs
+
+namespace Tm27
+
+-- l1 : count of 1 on the left
+-- r1 : count of 1 on the right
+theorem lemma_18 (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)⟩⟩
+):
+∃ 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
+forward g g i
+forward g g (1+i)
+forward g g (2+i)
+by_cases hr1 : Nat.Prime (r1+1)
+. refine (?_ ∘ (prime_21 (3+i) r1 (Γ.one :: List.replicate l1 Γ.one) [])) ?_
+  . intros g
+    specialize g hr1
+    obtain ⟨j, _, g⟩ := g
+    forward g g j
+    refine (?_ ∘ (lemma_22_to_24 (1+j) l1 [] (Γ.zero :: Γ.one :: (List.replicate r1 Γ.one ++ [Γ.zero])))) ?_
+    . intros g
+      obtain ⟨k, g⟩ := g
+      forward g g (k+(1+j))
+      have h : ¬ Nat.Prime (l1+1) := by tauto
+      apply n_prime_17 at h
+      pick_goal 5
+      . rw [g]
+        simp
+        repeat any_goals apply And.intro
+        all_goals rfl
+      obtain ⟨m, _, h⟩ := h
+      forward h h m
+      forward h h (1+m)
+      forward h h (2+m)
+      apply rec26 at h
+      forward h h (3+m+l1+1)
+      use (5+m+l1)
+      constructor
+      . omega
+      . simp [h]
+        repeat any_goals apply And.intro
+        all_goals simp! [Turing.ListBlank.mk]
+        all_goals rw [Quotient.eq'']
+        all_goals right
+        . use 2
+          tauto
+        . use 1
+          simp
+          tauto
+    . simp! [g, Turing.ListBlank.mk]
+      rw [Quotient.eq'']
+      left
+      use 1
+      tauto
+  . simp! [g, Turing.ListBlank.mk]
+    rw [Quotient.eq'']
+    left
+    use 1
+    tauto
+. apply n_prime_17 at hr1
+  pick_goal 5
+  . rw [g]
+    simp
+    repeat any_goals apply And.intro
+    . rfl
+    . simp! [Turing.ListBlank.mk]
+      rw [Quotient.eq'']
+      left
+      use 1
+      tauto
+  obtain ⟨j, _, g⟩ := hr1
+  forward g g j
+  use (1+j)
+  constructor
+  . omega
+  . simp! [g]
+    simp! [Turing.ListBlank.mk]
+    rw [Quotient.eq'']
+    right
+    use 1
+    rw [← List.cons_append]
+    rw [← List.replicate_succ]
+    rw [← List.cons_append]
+    rw [← List.replicate_succ]
+    ring_nf
+    tauto
+
+-- +2
+theorem both_prime (i l1 r1: ℕ)
+(hpl : Nat.Prime (l1+1))
+(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)⟩⟩
+) :
+∃ j>i, nth_cfg j = some ⟨⟨26, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (l1+r1+4) Γ.one), Turing.ListBlank.mk []⟩⟩ := by
+forward g g i
+forward g g (1+i)
+forward g g (2+i)
+apply prime_21 at hpr
+pick_goal 5
+. rw [g]
+  simp
+  constructor
+  . rfl
+  . simp! [Turing.ListBlank.mk]
+    rw [Quotient.eq'']
+    left
+    use 1
+    tauto
+clear g
+obtain ⟨j, _, g⟩ := hpr
+forward g g j
+refine (?_ ∘ (lemma_22_to_24 (1+j) l1 []  (Γ.zero :: Γ.one :: (List.replicate r1 Γ.one ++ [Γ.zero])))) ?_
+. intros h
+  obtain ⟨k, h⟩ := h
+  forward h h (k+(1+j))
+  apply prime_21 at hpl
+  pick_goal 5
+  . rw [h]
+    simp
+    constructor <;> rfl
+  obtain ⟨m, _, g⟩ := hpl
+  forward g g m
+  forward g g (1+m)
+  forward g g (2+m)
+  apply rec23 at g
+  forward g g (3+m+l1+1)
+  rw [← List.cons_append] at g
+  rw [← List.replicate_succ] at g
+  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
+  forward g g (5+m+l1+(l1+1)+1)
+  rw [← List.cons_append] at g
+  rw [← List.replicate_succ] at g
+  rw [← List.cons_append] at g
+  rw [← List.replicate_succ] at g
+  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
+  refine (?_ ∘ g) ?_
+  . clear g
+    intros g
+    obtain ⟨n, _, g⟩ := g
+    forward g g n
+    forward g g (1+n)
+    forward g g (2+n)
+    rw [← List.cons_append] at g
+    rw [← List.replicate_succ] at g
+    apply rec26 at g
+    use (3 + n + (2 + l1 + r1 + 1) + 1)
+    constructor
+    . omega
+    . rw [g]
+      simp [Turing.ListBlank.mk]
+      rw [Quotient.eq'']
+      right
+      use 2
+      ring_nf
+      tauto
+  . apply (@Nat.not_prime_of_dvd_of_lt 2)
+    any_goals omega
+    ring_nf
+    rw [add_assoc]
+    apply Nat.dvd_add
+    . omega
+    . apply Even.two_dvd
+      assumption
+. rw [g]
+  simp! [Turing.ListBlank.mk]
+  rw [Quotient.eq'']
+  left
+  use 1
+  tauto
+
+
+theorem leap_18 (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)⟩⟩ →
+(∃ x y, x + y = l1 + r1 + 2 /\ Nat.Prime x /\ Nat.Prime y /\ (r1+1) ≤ x /\ x ≤ y) →
+∃ j>i, nth_cfg j = some ⟨⟨26, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (l1+r1+4) Γ.one), Turing.ListBlank.mk []⟩⟩
+:= by
+induction l1 with
+| zero => omega
+| succ l1 =>
+  rename_i induction_step
+  intros i r1 h _ g hpp
+  by_cases hp : ¬ Nat.Prime (l1+2) \/ ¬ Nat.Prime (r1+1)
+  . -- induction step
+    apply lemma_18 at g
+    any_goals tauto
+    obtain ⟨j, _, g⟩ := g
+    apply induction_step at g
+    all_goals ring_nf at *
+    any_goals assumption
+    refine (?_ ∘ g) ?_
+    . intros g
+      obtain ⟨m, g₂⟩ := g
+      use m
+      ring_nf at *
+      simp [g₂]
+      omega
+    . obtain ⟨x, y, _, _, _, _⟩ := hpp
+      use! x, y
+      repeat any_goals apply And.intro
+      any_goals assumption
+      any_goals omega
+      by_cases x = r1+1
+      any_goals omega
+      subst x
+      exfalso
+      cases hp with
+      | inl hp => apply hp
+                  have : y = l1+2 := by omega
+                  subst y
+                  ring_nf at *
+                  assumption
+      | inr hp => apply hp
+                  ring_nf at *
+                  assumption
+  . -- both prime
+    apply both_prime at g
+    all_goals tauto
+
+
+theorem leap_18_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)⟩⟩ →
+(∀ x y, x + y = l1 + r1 + 2 /\ Nat.Prime x /\ Nat.Prime y → False) →
+∃ j, nth_cfg j = none
+:= by
+induction l1 with
+| zero =>
+  intros i r1 h g hpp
+  have hr1 : ∃ r2, r2 + 2 = r1 := by use (r1-2); omega
+  obtain ⟨r2, _⟩ := hr1
+  subst r1
+  forward g g i
+  forward g g (1+i)
+  forward g g (2+i)
+  rw [← List.replicate_succ] at g
+  rw [← List.replicate_succ] at g
+  by_cases hp : Nat.Prime (r2+3)
+  . apply prime_21 at hp
+    pick_goal 5
+    . rw [g]
+      simp
+      constructor
+      . rfl
+      . simp! [Turing.ListBlank.mk]
+        rw [Quotient.eq'']
+        left
+        use 1
+        tauto
+    obtain ⟨j, _, h⟩ := hp
+    forward h h j
+    forward h h (1+j)
+    forward h h (2+j)
+    forward h h (3+j)
+    forward h h (4+j)
+    forward h h (5+j)
+    forward h h (6+j)
+    forward h h (7+j)
+    forward h h (8+j)
+    forward h h (9+j)
+    forward h h (10+j)
+    forward h h (11+j)
+    forward h h (12+j)
+    use (13+j)
+  . apply n_prime_17 at hp
+    pick_goal 5
+    . rw [g]
+      simp
+      constructor
+      . rfl
+      . simp! [Turing.ListBlank.mk]
+        rw [Quotient.eq'']
+        left
+        use 1
+        tauto
+    obtain ⟨j, _, h⟩ := hp
+    forward h h j
+    forward h h (1+j)
+    forward h h (2+j)
+    use (3+j)
+| succ l1 =>
+    intros i r1 h g hpp
+    apply lemma_18 at g
+    . rename_i induction_step
+      obtain ⟨j, _, g⟩ := g
+      apply induction_step at g
+      any_goals omega
+      apply g
+      ring_nf at hpp
+      ring_nf
+      assumption
+    . specialize hpp (l1+2) (r1+1)
+      ring_nf at hpp
+      simp at hpp
+      ring_nf
+      tauto
+
+end Tm27
diff --git a/GoldbachTm/Tm27/Prime.lean b/GoldbachTm/Tm27/Prime.lean
new file mode 100644
index 0000000..b4281df
--- /dev/null
+++ b/GoldbachTm/Tm27/Prime.lean
@@ -0,0 +1,465 @@
+import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm27.Transition
+import GoldbachTm.Tm27.Miscellaneous
+
+namespace Tm27
+
+-- c1++, c2++
+--    l 0 [la 11] 0  [lb 11] 0 [ra 11111] 0  [(rb+1) 1] 0 r
+--                c1         ^            c2
+--
+--    l 0 [la' 1] 0  [lb' 1] 0 [(ra+1) 1] 0  [rb 11111] 0 r
+--                c1         ^            c2
+private lemma step_10_pointer (i la lb ra rb: ℕ) (l r : List Γ) :
+nth_cfg i = some ⟨⟨10, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk (List.replicate lb Γ.one ++ List.cons Γ.zero (List.replicate la Γ.one ++ List.cons Γ.zero l)),
+  Turing.ListBlank.mk (List.replicate ra Γ.one ++ List.cons Γ.zero (List.replicate (rb+1) Γ.one ++ List.cons Γ.zero r))⟩⟩ →
+  (ra + 2) ≡ (la + 1) [MOD (la + lb + 1)] →
+∃ j>i, ∃ la' lb', nth_cfg j = some ⟨⟨10, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk (List.replicate lb' Γ.one ++ List.cons Γ.zero (List.replicate la' Γ.one ++ List.cons Γ.zero l)),
+  Turing.ListBlank.mk (List.replicate (ra+1) Γ.one ++ List.cons Γ.zero (List.replicate rb Γ.one ++ List.cons Γ.zero r))⟩⟩
+  /\ (ra + 3) ≡ (la' + 1) [MOD (la + lb + 1)]
+  /\ la + lb = la' + lb'
+:= by
+intros g hm
+apply lemma_10_to_11 at g
+obtain ⟨j, g⟩ := g
+forward g g (j+i)
+forward g g (1+j+i)
+apply rec13 at g
+forward g g (2+j+i+ra+1)
+cases lb with simp_all
+| zero => forward g g (4+j+i+ra)
+          cases la with simp_all
+          | zero => forward g g (5+j+i+ra)
+                    forward g g (6+j+i+ra)
+                    use (7+j+i+ra)
+                    constructor
+                    . omega
+                    . simp [g]
+                      use! 0, 0
+                      simp!
+                      apply Nat.modEq_one
+          | succ la => simp! at g
+                       apply lemma8 at g
+                       forward g g (5+j+i+ra+la+2)
+                       rw [List.append_cons] at g
+                       rw [← List.replicate_succ'] at g
+                       simp! at g
+                       apply lemma10 at g
+                       use (8+j+i+ra+la+la+1)
+                       constructor
+                       . omega
+                       . use! 0, (la+1)
+                         rw [g]
+                         simp!
+                         apply Nat.ModEq.add_right 1
+                         apply Nat.ModEq.trans hm
+                         rw [Nat.modEq_zero_iff_dvd]
+| succ lb =>  simp! at g
+              apply lemma_6_to_7 at g
+              obtain ⟨k, _,  g⟩ := g
+              forward g g k
+              apply lemma_9_to_10 at g
+              obtain ⟨n, _,  g⟩ := g
+              use n
+              constructor
+              . omega
+              . use! (la+1), lb
+                simp! [g]
+                constructor
+                . apply Nat.ModEq.add_right 1 hm
+                . omega
+
+-- c1++, c2++
+--    l 0 [la 11] 0  [lb 11] 0 [ra 11111111] 0  [rb 1] 0 r
+--                c1         ^               c2
+--
+--    l 0 [la' 1] 0  [lb' 1] 0 [(ra+rb) 111] 0         0 r
+--                c1         ^               c2
+theorem end_10  (rb : ℕ): ∀ (i la lb ra : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨10, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk (List.replicate lb Γ.one ++ List.cons Γ.zero (List.replicate la Γ.one ++ List.cons Γ.zero l)),
+  Turing.ListBlank.mk (List.replicate ra Γ.one ++ List.cons Γ.zero (List.replicate rb Γ.one ++ List.cons Γ.zero r))⟩⟩ →
+  (ra + 2) ≡ (la + 1) [MOD (la + lb + 1)] →
+∃ j≥i, ∃ la' lb', nth_cfg j = some ⟨⟨10, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk (List.replicate lb' Γ.one ++ List.cons Γ.zero (List.replicate la' Γ.one ++ List.cons Γ.zero l)),
+  Turing.ListBlank.mk (List.replicate (ra+rb) Γ.one ++ List.cons Γ.zero (List.cons Γ.zero r))⟩⟩
+  /\ (ra + rb + 2) ≡ (la' + 1) [MOD (la + lb + 1)]
+  /\ la + lb = la' + lb'
+:= by
+induction rb with intros i la lb ra l r g hm
+| zero => use! i
+          constructor
+          . omega
+          . use! la, lb
+            simp [g, hm]
+| succ rb =>  rename_i induction_step
+              apply step_10_pointer at g
+              specialize g hm
+              obtain ⟨j, _, la', lb', g, h₁, h₂⟩ := g
+              apply induction_step at g
+              rw [← h₂] at g
+              ring_nf at *
+              specialize g h₁
+              obtain ⟨k, _, la'', lb'', g, h₃, h₄⟩ := g
+              use! k
+              constructor
+              . omega
+              . use! la'', lb''
+                ring_nf at *
+                repeat any_goals constructor
+                all_goals tauto
+
+
+--    l 0 1 0  [lb 11]    0  0  [(rb+1) 1] 0 r
+--          c1            ^  c2
+--
+--    l 0 1 0  [(lb+1) 1] 0  0  [rb 11111] 0 r
+--          c1            ^  c2
+theorem step_10_n_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+1) Γ.one ++ List.cons Γ.zero r))⟩⟩ →
+  ¬ (lb + 2) ∣ (rb + 3) →
+∃ j>i, nth_cfg j = some ⟨⟨10, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk (List.replicate (lb+1) Γ.one ++ Γ.zero :: Γ.one :: Γ.zero :: l),
+  Turing.ListBlank.mk (List.cons Γ.zero (List.replicate rb Γ.one ++ List.cons Γ.zero r))⟩⟩
+:= by
+intros g ne_dvd
+have h := end_10 (rb+1) i 1 lb 0 l r
+simp at h
+specialize h g rfl
+clear g
+obtain ⟨j, _, la', lb', g, h₁, h₂⟩ := h
+apply lemma_10_to_11 at g
+obtain ⟨k, g⟩ := g
+forward g g (k+j)
+forward g g (1+k+j)
+rw [← List.cons_append, ← List.replicate.eq_2] at g
+apply rec14 at g
+forward g g (2+k+j+rb.succ+1)
+cases lb' with (simp! [*, -nth_cfg] at g; simp_all)
+| zero => subst la'
+          exfalso
+          apply ne_dvd
+          rw [← Nat.modEq_zero_iff_dvd]
+          ring_nf at *
+          apply Nat.ModEq.trans h₁
+          rw [Nat.modEq_zero_iff_dvd]
+| succ lb' => apply lemma_15_to_19 at g
+              obtain ⟨m, g⟩ := g
+              forward g g (m + (5 + k + j + rb))
+              apply rec20 at g
+              forward g g (6 + m + k + j + rb + lb' + 1)
+              forward g g (8 + m + k + j + rb + lb')
+              forward g g (9 + m + k + j + rb + lb')
+              forward g g (10 + m + k + j + rb + lb')
+              rw [← List.cons_append] at g
+              rw [← List.replicate.eq_2] at g
+              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 lemma5 at g
+              forward g g (11 + m + k + j + rb + lb' + (lb'.succ + 1 + la') + 2)
+              rw [List.replicate_add] at g
+              rw [List.replicate_add] at g
+              simp! [*, -nth_cfg] at g
+              forward g g  (16 + m + k + j + rb + lb' * 2 + la')
+              rw [List.replicate_add] at g
+              rw [List.replicate_add] at g
+              simp! [*, -nth_cfg] at g
+              apply lemma10 at g
+              use (17 + m + k + j + rb + lb' * 2 + la' + (1 + lb' + la' - 1) + 1)
+              constructor
+              . omega
+              . rw [g]
+                simp!
+                repeat any_goals first | omega | rfl | apply congr
+
+--    l 0 1 0  [lb 11]    0  0  [rb 1] 0 r
+--          c1            ^  c2
+--                        10
+--
+--    l 0 1 1  [lb 11]    1  1  [rb 1] 0 r
+--      ^
+--      17
+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,
+  Turing.ListBlank.mk l,
+  Turing.ListBlank.mk (List.replicate (lb+rb+4) Γ.one ++ List.cons Γ.zero r)⟩⟩
+:= by
+intros g dvd
+have h := end_10 rb i 1 lb 0 l r
+simp at h
+specialize h g rfl
+clear g
+obtain ⟨j, _, la', lb', g, h₁, h₂⟩ := h
+apply lemma_10_to_11 at g
+obtain ⟨k, g⟩ := g
+forward g g (k+j)
+forward g g (1+k+j)
+apply rec14 at g
+forward g g (2+k+j+rb+1)
+rw [← List.cons_append] at g
+cases lb' with (simp! [*, -nth_cfg] at g; simp_all)
+| zero => subst la'
+          forward g g (4+k+j+rb)
+          forward g g (5+k+j+rb)
+          apply rec17 at g
+          use (6 + k + j + rb + (1+lb)+1)
+          constructor
+          . omega
+          . simp [g]
+            rw [List.append_cons, ← List.replicate_succ']
+            rw [List.append_cons, ← List.replicate_succ']
+            rw [← List.append_assoc, ← List.replicate_add]
+            ring_nf
+| succ lb' => have : lb = la'+ lb' := by omega
+              subst lb
+              clear h₂
+              ring_nf at *
+              rw [Nat.ModEq.comm] at h₁
+              rw [← Nat.modEq_zero_iff_dvd] at dvd
+              have h := Nat.ModEq.trans h₁ dvd
+              rw [Nat.modEq_zero_iff_dvd] at h
+              apply Nat.le_of_dvd at h <;> omega
+
+--    l 0 1 0  [lb 11]     0  0  [rb 1] 0 r
+--          c1             ^  c2
+--
+--    l 0 1 0  [(lb+rb) 1] 0  0         0 r
+--          c1             ^  c2
+theorem leap_10_prime (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))⟩⟩ →
+Nat.Prime (lb+rb+4) →
+∃ j≥i, nth_cfg j = some ⟨⟨10, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk (List.replicate (lb+rb) Γ.one ++ Γ.zero :: Γ.one :: Γ.zero :: l),
+  Turing.ListBlank.mk (Γ.zero :: Γ.zero :: r)⟩⟩
+:= by
+induction rb with intros i lb l r g p
+| zero => use i
+          constructor
+          . omega
+          . simp! [g]
+| succ rb => apply step_10_n_dvd at g
+             by_cases h : (lb + 2 ∣ rb + 3)
+             . have g : (lb + 2 ∣ lb + 2) := Nat.dvd_refl _
+               have g := Nat.dvd_add g h
+               ring_nf at p g
+               rw [Nat.Prime.dvd_iff_eq] at g
+               any_goals omega
+               all_goals assumption
+             . specialize g h
+               rename_i induction_step
+               obtain ⟨j, _, g⟩ := g
+               apply induction_step at g
+               ring_nf at g p
+               specialize g p
+               obtain ⟨k, _, g⟩ := g
+               use k
+               constructor
+               . omega
+               . simp! [g]
+                 rw [← List.cons_append]
+                 rw [← List.replicate_succ]
+                 ring_nf
+
+theorem prime_21 (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)⟩⟩ :=
+match h : r1 with
+| Nat.zero => by subst r1
+                 exfalso
+                 apply Nat.not_prime_one p
+| Nat.succ Nat.zero => by
+  subst r1
+  forward g g i
+  forward g g (1+i)
+  forward g g (2+i)
+  forward g g (3+i)
+  forward g g (4+i)
+  use (5+i)
+  simp [g]
+| Nat.succ (Nat.succ Nat.zero) => by
+  subst r1
+  forward g g i
+  forward g g (1+i)
+  forward g g (2+i)
+  forward g g (3+i)
+  forward g g (4+i)
+  forward g g (5+i)
+  forward g g (6+i)
+  use (7+i)
+  simp [g]
+| Nat.succ (Nat.succ (Nat.succ r1)) => by
+  clear h
+  forward g g i
+  forward g g (1+i)
+  forward g g (2+i)
+  forward g g (3+i)
+  forward g g (4+i)
+  forward g g (5+i)
+  forward g g (6+i)
+  forward g g (7+i)
+  forward g g (8+i)
+  forward g g (9+i)
+  apply (leap_10_prime _ _ 0) at g
+  have h : r1.succ.succ.succ + 1 = 0 + r1 +4 := by omega
+  rw [h] at p
+  specialize g p
+  obtain ⟨j, _, g⟩ := g
+  forward g g j
+  forward g g (1+j)
+  forward g g (2+j)
+  forward g g (3+j)
+  forward g g (4+j)
+  cases r1 with
+  | zero => exfalso
+            have g : ¬ Nat.Prime 4 := by decide
+            apply g p
+  | succ r1 => apply lemma_15_to_19 at g
+               obtain ⟨k, g⟩ := g
+               forward g g (k+(5+j))
+               apply rec20 at g
+               forward g g (6 + k + j + r1 + 1)
+               forward g g (8 + k + j + r1)
+               forward g g (9 + k + j + r1)
+               forward g g (10 + k + j + r1)
+               rw [List.append_cons, ← List.replicate_succ'] at g
+               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
+               use (11 + k + j + r1 + (r1 + 1 + 1 + 1) + 1)
+               constructor
+               . omega
+               . rw [g]
+                 simp
+                 rw [List.append_cons, ← List.replicate_succ']
+
+
+--    l 0 1 0  [lb 11]    0  0  [rb 1] 0 r
+--          c1            ^  c2
+--                        10
+--
+--    l 0 1 1  [lb 11]    1  1  [rb 1] 0 r
+--      ^
+--      17
+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,
+  Turing.ListBlank.mk l,
+  Turing.ListBlank.mk (List.replicate (lb+rb+4) Γ.one ++ List.cons Γ.zero r)⟩⟩
+:= by
+induction rb with intros i lb l r g hd
+| zero => by_cases h : (lb+2) ∣ 2
+          . apply step_10_dvd at g
+            ring_nf at *
+            apply g h
+          . obtain ⟨divisor, _, _, h₃⟩ := hd
+            have g : divisor = lb + 2 \/ divisor = lb + 3 := by omega
+            have h₁ : divisor ∣ divisor := Nat.dvd_refl _
+            ring_nf at *
+            cases g <;> subst divisor
+            . have g := Nat.dvd_sub (by omega) h₃ h₁
+              have h₁ : 4+lb-(2+lb) = 2 := by omega
+              rw [h₁] at g
+              specialize h g
+              tauto
+            . have g := Nat.dvd_sub (by omega) h₃ h₁
+              have h : 4+lb-(3+lb) = 1 := by omega
+              rw [h] at g
+              apply Nat.eq_one_of_dvd_one at g
+              omega
+| succ rb =>  by_cases h : (lb+2) ∣ rb+3
+              . apply step_10_dvd at g
+                apply g h
+              . apply step_10_n_dvd at g
+                specialize g h
+                rename_i induction_step
+                obtain ⟨j, _, g⟩ := g
+                apply induction_step at g
+                refine (?_ ∘ g) ?_
+                . intros g
+                  obtain ⟨k, _, g⟩ := g
+                  use k
+                  constructor
+                  . omega
+                  . simp [g]
+                    ring_nf
+                . obtain ⟨divisor, h₁, h₂, h₃⟩ := hd
+                  use divisor
+                  ring_nf at *
+                  repeat any_goals apply And.intro
+                  any_goals omega
+                  by_cases h : divisor = 2 + lb
+                  . subst divisor
+                    exfalso
+                    apply h
+                    have h := Nat.dvd_sub (by omega) h₃ (Nat.dvd_refl _)
+                    have g : (5 + lb + rb - (2+lb)) = 3 + rb := by omega
+                    rw [g] at h
+                    assumption
+                  . omega
+
+theorem n_prime_17 (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)⟩⟩ :=
+match r1 with
+| Nat.zero => by simp_all
+                 forward g g i
+                 forward g g (1+i)
+                 forward g g (2+i)
+                 use (3+i)
+                 rw [← g]
+                 simp
+| Nat.succ Nat.zero => by exfalso
+                          apply hp
+                          decide
+| Nat.succ (Nat.succ Nat.zero) => by exfalso
+                                     apply hp
+                                     decide
+| Nat.succ (Nat.succ (Nat.succ r1)) => by
+  forward g g i
+  forward g g (1+i)
+  forward g g (2+i)
+  forward g g (3+i)
+  forward g g (4+i)
+  forward g g (5+i)
+  forward g g (6+i)
+  forward g g (7+i)
+  forward g g (8+i)
+  forward g g (9+i)
+  apply (leap_10_dvd _ _ 0) at g
+  refine (?_ ∘ g) ?_
+  . intros h
+    obtain ⟨j, _, h⟩ := h
+    use j
+    constructor
+    . omega
+    . simp [h]
+  . rw [Nat.not_prime_iff_exists_dvd_lt] at hp <;> try omega
+    obtain ⟨p, h, g, hp⟩ := hp
+    use p
+    repeat any_goals apply And.intro
+    any_goals omega
+    have g : r1.succ.succ.succ +1 = 0+r1+4 := by omega
+    rw [g] at h
+    exact h
+
+end Tm27
diff --git a/GoldbachTm/Tm27/Search0.lean b/GoldbachTm/Tm27/Search0.lean
new file mode 100644
index 0000000..4184c80
--- /dev/null
+++ b/GoldbachTm/Tm27/Search0.lean
@@ -0,0 +1,129 @@
+-- theorem of recursive states
+-- all these states' usage is to search 0
+import GoldbachTm.Tm27.TuringMachine27
+
+namespace Tm27
+
+-- left
+theorem rec13 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨13, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨13, 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 => rename_i induction_step
+            specialize induction_step (i+1) l (List.cons Γ.one r)
+            have g : i + (k+1) +1 = i + 1 + k + 1 := by omega
+            rw [g, induction_step]
+            . simp [List.replicate_succ' (k+1)]
+            . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+
+theorem rec14 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨14, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨14, 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 => rename_i induction_step
+            specialize induction_step (i+1) l (List.cons Γ.one r)
+            have g : i + (k+1) +1 = i + 1 + k + 1 := by omega
+            rw [g, induction_step]
+            . 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
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) l (List.cons Γ.one r)
+            have g : i + (k+1) +1 = i + 1 + k + 1 := by omega
+            rw [g, induction_step]
+            . 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
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) l (List.cons Γ.one r)
+            have g : i + (k+1) +1 = i + 1 + k + 1 := by omega
+            rw [g, induction_step]
+            . 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
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) l (List.cons Γ.one r)
+            have g : i + (k+1) +1 = i + 1 + k + 1 := by omega
+            rw [g, induction_step]
+            . 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
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) l (List.cons Γ.one r)
+            have g : i + (k+1) +1 = i + 1 + k + 1 := by omega
+            rw [g, induction_step]
+            . simp [List.replicate_succ' (k+1)]
+            . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+
+--right
+theorem rec11 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨11, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨11, 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 => rename_i induction_step
+            specialize induction_step (i+1) (List.cons Γ.one l) r
+            have g : i + (k+1) +1 = i + 1 + k + 1 := by omega
+            rw [g, induction_step]
+            . 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
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) (List.cons Γ.one l) r
+            have g : i + (k+1) +1 = i + 1 + k + 1 := by omega
+            rw [g, induction_step]
+            . 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
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) (List.cons Γ.one l) r
+            have g : i + (k+1) +1 = i + 1 + k + 1 := by omega
+            rw [g, induction_step]
+            . simp [List.replicate_succ' (k+1)]
+            . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+
+theorem rec26 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨26, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨26, 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 => rename_i induction_step
+            specialize induction_step (i+1) (List.cons Γ.one l) r
+            have g : i + (k+1) +1 = i + 1 + k + 1 := by omega
+            rw [g, induction_step]
+            . simp [List.replicate_succ' (k+1)]
+            . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+
+end Tm27
diff --git a/GoldbachTm/Tm27/Transition.lean b/GoldbachTm/Tm27/Transition.lean
new file mode 100644
index 0000000..cb80cfd
--- /dev/null
+++ b/GoldbachTm/Tm27/Transition.lean
@@ -0,0 +1,68 @@
+import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm27.Search0
+
+namespace Tm27
+
+theorem lemma_10_to_11 (i : ℕ) (r1: ℕ) (l r : List Γ)
+(h :
+nth_cfg i = some ⟨⟨10, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk l,
+  Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩) :
+
+∃ j, nth_cfg (j + i) = some ⟨⟨11, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩
+:= by
+forward h h i
+cases r1 with
+| zero => use 1
+          simp [h]
+| succ r1 => apply rec11 at h
+             use (r1 + 2)
+             rw [← h]
+             ring_nf
+
+theorem lemma_15_to_19 (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,
+    Turing.ListBlank.mk l,
+    Turing.ListBlank.mk (List.replicate (l1+1) Γ.one ++ r),
+    ⟩⟩
+:= by
+forward h h i
+cases l1 with simp! [*, -nth_cfg] at h
+| zero => use 1
+          simp [h]
+| succ r1 =>  apply rec19 at h
+              use (r1+2)
+              ring_nf at *
+              simp [h]
+              rw [List.append_cons, ← List.replicate_succ']
+              ring_nf
+
+theorem lemma_22_to_24 (i : ℕ) (l1: ℕ) (l r : List Γ)
+(h :
+nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk (List.replicate l1 Γ.one ++ List.cons Γ.zero l),
+  Turing.ListBlank.mk r,
+  ⟩⟩) :
+
+∃ j, nth_cfg (j + i) = some ⟨⟨24, by omega⟩, ⟨Γ.zero,
+    Turing.ListBlank.mk l,
+    Turing.ListBlank.mk (List.replicate (l1+1) Γ.one ++ r),
+    ⟩⟩
+:= by
+forward h h i
+cases l1 with
+| zero => use 1
+          simp [h]
+| succ l1 => apply rec24 at h
+             use (l1 + 2)
+             ring_nf at *
+             simp [h]
+             rw [List.append_cons, ← List.replicate_succ']
+             ring_nf
+
+end Tm27
diff --git a/GoldbachTm/Tm27/TuringMachine27.lean b/GoldbachTm/Tm27/TuringMachine27.lean
index f7f8015..73d9112 100644
--- a/GoldbachTm/Tm27/TuringMachine27.lean
+++ b/GoldbachTm/Tm27/TuringMachine27.lean
@@ -1,5 +1,6 @@
 -- inspired by https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Computability/TuringMachine.lean
 import Mathlib.Computability.TuringMachine
+import Mathlib.Data.Real.Sqrt
 import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank
@@ -91,4 +92,81 @@ def machine : Machine
 | ⟨26, _⟩, Γ.one  => some ⟨⟨26, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
 | ⟨_+27, _⟩, _ => 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 []
+| Nat.succ n => match (nth_cfg n) with
+                | none => none
+                | some cfg =>  step machine cfg
+
+
+-- g1 = g2
+macro "forward" g1:ident g2:Lean.binderIdent i:term: tactic => `(tactic| (
+have h : nth_cfg ($i + 1) = nth_cfg ($i + 1) := rfl
+nth_rewrite 2 [nth_cfg] at h
+simp [*, step, Option.map, machine, Turing.Tape.write, Turing.Tape.move] at h
+try simp! [*, -nth_cfg] at h
+try ring_nf at h
+clear $g1
+rename_i $g2
+))
+
+theorem cfg45 : nth_cfg 45 = some ⟨26,
+        { 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
+forward h h 0
+forward h h 1
+forward h h 2
+forward h h 3
+forward h h 4
+forward h h 5
+forward h h 6
+forward h h 7
+forward h h 8
+forward h h 9
+forward h h 10
+forward h h 11
+forward h h 12
+forward h h 13
+forward h h 14
+forward h h 15
+forward h h 16
+forward h h 17
+forward h h 18
+forward h h 19
+forward h h 20
+forward h h 21
+forward h h 22
+forward h h 23
+forward h h 24
+forward h h 25
+forward h h 26
+forward h h 27
+forward h h 28
+forward h h 29
+forward h h 30
+forward h h 31
+forward h h 32
+forward h h 33
+forward h h 34
+forward h h 35
+forward h h 36
+forward h h 37
+forward h h 38
+forward h h 39
+forward h h 40
+forward h h 41
+forward h h 42
+forward h h 43
+forward h h 44
+simp [h]
+constructor
+. tauto
+. simp! [Turing.ListBlank.mk]
+  rw [Quotient.eq'']
+  right
+  use 2
+  tauto
+
+
 end Tm27
diff --git a/archieve/Busy beaver - Wikipedia_2024-10-17T08:56:05UTC.pdf b/archieve/Busy beaver - Wikipedia_2024-10-17T08:56:05UTC.pdf
new file mode 100644
index 0000000..aba9300
Binary files /dev/null and b/archieve/Busy beaver - Wikipedia_2024-10-17T08:56:05UTC.pdf differ