wip

lengyijun · Oct 7, 2024 · 35ae32f · 35ae32f
1 parent 72a7a5a
commit 35ae32f
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/GoldbachTm.lean b/GoldbachTm.lean
@@ -6,3 +6,4 @@ import GoldbachTm.ListBlank
 import GoldbachTm.Tm27.TuringMachine27
 import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.Hello
+import GoldbachTm.Tm31.Content
diff --git a/GoldbachTm/Tm31/Content.lean b/GoldbachTm/Tm31/Content.lean
@@ -0,0 +1,9 @@
+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