wip

we need a tactic

GoldbachTm/Tm31/Hello.lean

@@ -1,14 +1,16 @@
 import GoldbachTm.Tm31.TuringMachine31
 
 
-theorem t_5_to_6 (l r : List Γ) (i k : ℕ):
+theorem t_5_to_6 (k : ℕ): ∀ (l r : List Γ) (i: ℕ),
 nth_cfg i = some ⟨⟨5, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩  →
 nth_cfg (i + k + 1) = some ⟨⟨5, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
-intros h
 induction k with
-| zero => simp [nth_cfg]
+| zero => intros l r i h
+          simp [nth_cfg]
           rw [h]
           simp [step, machine, Turing.Tape.write, Turing.Tape.move]
 | succ k => rename_i induction_step
-            simp [nth_cfg]
+            intros l r i h
+            -- forward h
+            -- use induction_step
             sorry