G_to_J

Author: lengyijun

CollatzFunction/NonHalt/Main.lean

@@ -90,8 +90,7 @@ cases n with
       rw [← List.replicate_succ] at h
       apply copy_half at h
       rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
-      apply lemma_G_to_H at h
-      apply lemma_H_to_J at h
+      apply G_to_J at h
       forward h
       forward h
       use (11 + j + n / 2 * 13 + (n / 2) ^ 2 * 4)

CollatzFunction/NonHalt/Odd.lean

@@ -14,10 +14,9 @@ nth_cfg init_cfg (3 + i + b * 2) =  ⟨G, ⟨one,
   Turing.ListBlank.mk (List.replicate a one),
   Turing.ListBlank.mk (List.replicate (b+2) one)⟩⟩
 := by
-have g := lemma_G_to_H [] b
+have g := G_to_J [] b
 rw [ListBlank_empty_eq_single_zero] at g
 apply g at h
-apply lemma_H_to_J at h
 forward h
 simp [h]
 rw [← List.cons_append]

CollatzFunction/NonHalt/Transition.lean

@@ -5,7 +5,7 @@ namespace NonHalt
 
 open Lean Meta Elab Tactic Std Term TmState Γ
 
-theorem lemma_G_to_H (r: List Γ)(r1: ℕ)(i : ℕ)(l: List Γ)(init_cfg: Cfg)
+private lemma G_to_H (r: List Γ)(r1: ℕ)(i : ℕ)(l: List Γ)(init_cfg: Cfg)
 (h :
 nth_cfg init_cfg i =  ⟨G, ⟨Γ.one,
   Turing.ListBlank.mk l,
@@ -22,7 +22,7 @@ cases r1 with
              ring_nf at *
              simp [h]
 
-theorem lemma_H_to_J (r: List Γ)(r1: ℕ)(i : ℕ)(l: List Γ)(init_cfg: Cfg)
+private lemma H_to_J (r: List Γ)(r1: ℕ)(i : ℕ)(l: List Γ)(init_cfg: Cfg)
 (h :
 nth_cfg init_cfg i =  ⟨H, ⟨Γ.zero,
   Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r),
@@ -39,4 +39,18 @@ cases r1 with
              ring_nf at *
              simp [h]
 
+theorem G_to_J (r: List Γ)(r1: ℕ)(i : ℕ)(l: List Γ)(init_cfg: Cfg)
+(h :
+nth_cfg init_cfg i = ⟨G, ⟨Γ.one,
+  Turing.ListBlank.mk l,
+  Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩) :
+nth_cfg init_cfg (2+i+r1*2) = ⟨J, ⟨Γ.zero,
+  Turing.ListBlank.mk l,
+  Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.one r)⟩⟩
+:= by
+apply G_to_H at h
+apply H_to_J at h
+ring_nf at h
+simp [h]
+
 end NonHalt