16 stmt => 15 stmt

lengyijun · lengyijun · commit ceb699863634 · 2025-03-01T17:04:58.000+08:00
E.0 is only used in `collatz 0`
diff --git a/CollatzFunction/Tm8/Main.lean b/CollatzFunction/Tm8/Main.lean
@@ -17,23 +17,15 @@ theorem G_collatz (n i: ℕ) (init_cfg: Cfg)
 ∃ j>i, nth_cfg_is_n j (collatz n) init_cfg
 := by
 obtain ⟨l, h⟩ := h
--- somehow surprise, the proof of `inl h` and `inr h` are the same
-cases h with
-| inl h => cases n with
+cases n with
   | zero => forward h
             forward h
-            use (2+i)
-            constructor
-            any_goals omega
-            use l
-            left
+            forward h
+            use (3+i)
             unfold collatz
+            simp
+            use (zero :: l)
             simp [h]
-            simp! [Turing.ListBlank.mk]
-            rw [Quotient.eq'']
-            right
-            use 1
-            tauto
   | succ n => forward h
               cases n with
     | zero => simp at h
@@ -44,7 +36,6 @@ cases h with
               constructor
               any_goals omega
               use l
-              right
               unfold collatz
               simp [h]
     | succ n => forward h
@@ -61,7 +52,6 @@ cases h with
                   constructor
                   any_goals omega
                   use (List.replicate (n / 2) one ++ zero :: zero :: l)
-                  left
                   simp [h]
                   rw [← List.replicate_succ]
                   apply congr
@@ -96,104 +86,6 @@ cases h with
                     constructor
                     any_goals omega
                     use l
-                    right
-                    simp [h]
-                    apply congr
-                    any_goals rfl
-                    rw [← List.replicate_one]
-                    rw [List.replicate_append_replicate]
-                    rw [← List.replicate_succ]
-                    apply congr
-                    any_goals rfl
-                    apply congr
-                    any_goals rfl
-                    omega
-                  have g : (n+2) % 2 = 1 := by omega
-                  rw [← Nat.odd_iff] at g
-                  obtain ⟨a, g⟩ := g
-                  cases a with
-                  | zero => omega
-                  | succ a => use a; omega
-| inr h => cases n with
-  | zero => forward h
-            forward h
-            use (2+i)
-            constructor
-            any_goals omega
-            use l
-            left
-            unfold collatz
-            simp [h]
-            simp! [Turing.ListBlank.mk]
-            rw [Quotient.eq'']
-            right
-            use 1
-            tauto
-  | succ n => forward h
-              cases n with
-    | zero => simp at h
-              forward h
-              forward h
-              forward h
-              use (4+i)
-              constructor
-              any_goals omega
-              use l
-              right
-              unfold collatz
-              simp [h]
-    | succ n => forward h
-                unfold collatz
-                split_ifs <;> rename_i g
-                . rw [← (ListBlank_empty_eq_single_zero (List.replicate n one))] at h
-                  apply B_even at h
-                  obtain ⟨j, _, h⟩ := h
-                  forward h
-                  rw [add_comm 1 (n/2)] at h
-                  rw [List.replicate_succ] at h
-                  simp at h
-                  forward h
-                  use (2+j)
-                  constructor
-                  any_goals omega
-                  use (List.replicate (n / 2) one ++ zero :: zero :: l)
-                  left
-                  simp [h]
-                  rw [← List.replicate_succ]
-                  apply congr
-                  any_goals rfl
-                  apply congr
-                  any_goals rfl
-                  apply congr
-                  any_goals rfl
-                  omega
-                  rw [← Nat.even_iff] at g
-                  obtain ⟨a, g⟩ := g
-                  cases a with
-                  | zero => omega
-                  | succ a => use a; omega
-                . rw [← (ListBlank_empty_eq_single_zero (List.replicate n one))] at h
-                  apply B_odd at h
-                  obtain ⟨j, _, h⟩ := h
-                  forward h
-                  cases n with
-                  | zero => omega
-                  | succ n =>
-                    ring_nf at h
-                    have g : (2+n)/2 = n/2 + 1:= by omega
-                    rw [g] at h
-                    rw [List.replicate_succ] at h
-                    simp at h
-                    rw [← List.replicate_succ] at h
-                    apply copy_half at h
-                    rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
-                    apply G_to_J at h
-                    forward h
-                    use (10 + j + n / 2 * 13 + (n / 2) ^ 2 * 4)
-                    constructor
-                    any_goals omega
-                    use l
-                    right
                     simp [h]
                     apply congr
                     any_goals rfl
diff --git a/CollatzFunction/Tm8/Representation.lean b/CollatzFunction/Tm8/Representation.lean
@@ -13,7 +13,6 @@ open Lean Meta Elab Tactic Std Term TmState Γ
 -- `nth_cfg i cfg` represent `n`
 def nth_cfg_is_n (i n: Nat) (init_cfg : Cfg) :=
 ∃ l,
-nth_cfg init_cfg i = ⟨E, ⟨zero, Turing.ListBlank.mk (zero :: l), Turing.ListBlank.mk (List.replicate n one)⟩⟩ \/
 nth_cfg init_cfg i = ⟨G, ⟨zero, Turing.ListBlank.mk (zero :: l), Turing.ListBlank.mk (List.replicate n one)⟩⟩
 
 end Tm8
diff --git a/CollatzFunction/Tm8/TuringMachine8.lean b/CollatzFunction/Tm8/TuringMachine8.lean
@@ -52,7 +52,7 @@ instance : ToString Cfg where
     s!"{q}   {s}"
 
 /-- The initial configuration. -/
-def init (l : List Γ) : Cfg := ⟨TmState.E, Turing.Tape.mk₁ l⟩
+def init (l : List Γ) : Cfg := ⟨TmState.G, Turing.Tape.mk₁ l⟩
 
 /-- Execution semantics of the Turing machine. -/
 def step (M : Machine) : Cfg → Cfg :=
@@ -71,8 +71,8 @@ def machine : Machine
 | C, Γ.one =>  ⟨D, ⟨Turing.Dir.left, Γ.zero⟩⟩
 | D, Γ.zero => ⟨A, ⟨Turing.Dir.right, Γ.one⟩⟩
 | D, Γ.one =>  ⟨D, ⟨Turing.Dir.left, Γ.one⟩⟩
-| E, Γ.zero => ⟨A, ⟨Turing.Dir.right, Γ.zero⟩⟩
-| E, Γ.one =>  ⟨E, ⟨Turing.Dir.right, Γ.zero⟩⟩
+| E, Γ.zero => ⟨G, ⟨Turing.Dir.right, Γ.zero⟩⟩ -- only used in `collatz 0`
+| E, Γ.one =>  ⟨G, ⟨Turing.Dir.right, Γ.zero⟩⟩
 | G, Γ.zero => ⟨A, ⟨Turing.Dir.right, Γ.zero⟩⟩
 | G, Γ.one =>  ⟨H, ⟨Turing.Dir.right, Γ.zero⟩⟩
 | H, Γ.zero => ⟨J, ⟨Turing.Dir.left, Γ.one⟩⟩
diff --git a/README.md b/README.md
@@ -18,17 +18,13 @@ A B C D E G H J  are 8 states.
     - 1 states (E) for even cases
     - 3 states (G, H, J) for odd cases
 
-`000 (0F)    000` denotes 0
+`V 0(0G)  000` denotes 0, V is arbitrary list
 
-`000 (0G)    000` denotes 0
-
-`000 (0F)1^n 000` denotes n
-
-`000 (0G)1^n 000` denotes n
+`V 0(0G)1^n 000` denotes n, V is arbitrary list
 
 let b = collatz n
 
-`000 (0F)1^n 000` -> `000 (0F)1^b 000` or `000 (0G)1^b 000` 
+`V 0(0G)1^n 000` -> `W 0(0G)1^b 000` , V W are arbitrary list
 
 ## Comparsion to previous results
 
diff --git a/table.pdf b/table.pdf
diff --git a/table.tex b/table.tex
@@ -66,7 +66,7 @@
 \hline
 $D$ & 1R$A$ & 1L$D$ \\
 \hline
-$E$ & 0R$A$ & 0R$E$ \\
+$E$ & ---   & 0R$G$ \\
 \hline
 $G$ & 0R$A$ & 0R$H$ \\
 \hline
@@ -77,6 +77,8 @@
 \end{tabular}
 \end{center}
 
+--- means unreachable: any write, move and states is ok
+
 \begin{thebibliography}{99}
 \bibitem{Ba98} C.\ Baiocchi, 3N+1, UTM e Tag-systems (Italian),
 Dipartimento di Matematica dell'Universit\`a ``La Sapienza'' di Roma {\bf 98/38}, 1998.
