wip

GoldbachTm.lean

@@ -6,3 +6,6 @@ import GoldbachTm.ListBlank
 import GoldbachTm.Tm27.TuringMachine27
 import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.Hello
+import GoldbachTm.Tm31.Content
+import GoldbachTm.Tm31.Prime
+import GoldbachTm.Tm31.Clapboard

GoldbachTm/Tm31/Clapboard.lean

@@ -0,0 +1,11 @@
+import GoldbachTm.Tm31.TuringMachine31
+import Mathlib.Data.Nat.Prime.Defs
+
+-- TODO: maybe need double 0
+-- l1 : count of 1 on the left
+-- r1 : count of 1 on the right
+theorem lemma_26 : ∀ (i l1 r1: ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨26, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩ →
+(¬ Nat.Prime (l1+1)) \/ (¬ Nat.Prime r1) →
+∃ j, nth_cfg (i+j) = some ⟨⟨26, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate l1 Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one ++ List.cons Γ.zero r)⟩⟩ :=
+sorry

GoldbachTm/Tm31/Content.lean

@@ -0,0 +1,21 @@
+import GoldbachTm.Tm31.TuringMachine31
+import Mathlib.Data.Nat.Prime.Defs
+
+theorem lemma_25 (k : ℕ): ∀ (i : ℕ),
+nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate k Γ.one), Turing.ListBlank.mk []⟩⟩ →
+(¬ (∃ x y, x + y = k /\ Nat.Prime x /\ Nat.Prime y)) →
+∃ j, nth_cfg (i+j) = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+2) Γ.one), Turing.ListBlank.mk []⟩⟩
+:= by
+sorry
+
+theorem halt_lemma :
+(∃ (k x y: ℕ), k % 2 = 0 /\ x + y = k /\ Nat.Prime x /\ Nat.Prime y) →
+∃ i, nth_cfg i = none
+:= by
+sorry
+
+theorem halt_lemma_rev :
+∃ i, nth_cfg i = none →
+(∃ (k x y: ℕ), k % 2 = 0 /\ x + y = k /\ Nat.Prime x /\ Nat.Prime y)
+:= by
+sorry

GoldbachTm/Tm31/Prime.lean

@@ -0,0 +1 @@
+-- theorem of subroutine: judge prime