wip

GoldbachTm.lean

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

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