wip

Author: lengyijun

GoldbachTm/Tm31/Content.lean

@@ -90,14 +90,16 @@ 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
+theorem halt_lemma_rev :
+(∃ i, nth_cfg i = none) → (∃ n, ¬ goldbach (2*n+4))
 := by
+intros h
 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)
+/-
+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
+-/