wip

lengyijun · Oct 14, 2024 · 9f7812f · 9f7812f
1 parent 49f07bf
commit 9f7812f
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/GoldbachTm/Tm31/Content.lean b/GoldbachTm/Tm31/Content.lean
@@ -1,10 +1,10 @@
 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 []⟩⟩
+theorem lemma_25 (n : ℕ): ∀ (i : ℕ),
+nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate n Γ.one), Turing.ListBlank.mk []⟩⟩ →
+(∃ x y, x + y = n /\ Nat.Prime x /\ Nat.Prime y) →
+∃ j, nth_cfg (i+j) = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+2) Γ.one), Turing.ListBlank.mk []⟩⟩
 := by
 sorry