wip

lengyijun · Oct 14, 2024 · a20b725 · a20b725
1 parent 7200144
commit a20b725
Showing 1 changed file with 12 additions and 6 deletions.
diff --git a/GoldbachTm/Tm31/Content.lean b/GoldbachTm/Tm31/Content.lean
@@ -87,14 +87,20 @@ refine (?_ ∘ g) ?_
   tauto
 
 
-theorem halt_lemma :
-(∃ (n x y: ℕ), Even n /\ n > 2 /\ x + y = n /\ Nat.Prime x /\ Nat.Prime y) →
-∃ i, nth_cfg i = none
-:= by
+theorem halt_lemma_rev' (h : ∀ n, goldbach (2*n+4)) :
+∀ i, nth_cfg i ≠ none := by
 sorry
 
 theorem halt_lemma_rev :
-∃ i, nth_cfg i = none →
-(∃ (n x y: ℕ), Even n /\ n > 2 /\ x + y = n /\ Nat.Prime x /\ Nat.Prime y)
+(∃ i, nth_cfg i = none) → (∃ n, ¬ goldbach (2*n+4))
+:= by
+intros h
+sorry
+
+/-
+theorem halt_lemma_useless :
+(∃ (n x y: ℕ), Even n /\ n > 2 /\ x + y = n /\ Nat.Prime x /\ Nat.Prime y) →
+∃ i, nth_cfg i = none
 := by
 sorry
+-/