diff --git a/GoldbachTm/Tm27/Miscellaneous.lean b/GoldbachTm/Tm27/Miscellaneous.lean index c578de9..7706ed4 100644 --- a/GoldbachTm/Tm27/Miscellaneous.lean +++ b/GoldbachTm/Tm27/Miscellaneous.lean @@ -25,8 +25,7 @@ theorem lemma8 (k : ℕ): ∀ (i : ℕ) (l r : List Γ), nth_cfg i = some ⟨⟨8, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ → nth_cfg (i + k + 2) = some ⟨⟨9, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate k Γ.zero ++ r)⟩⟩ := by induction k with (intros i l r h; simp_all) -| zero => forward h - forward h +| zero => iterate 2 forward h rw [← h] ring_nf | succ k induction_step => @@ -42,8 +41,7 @@ theorem lemma5 (k : ℕ): ∀ (i : ℕ) (l r : List Γ), 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 + 2) = some ⟨⟨4, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate k Γ.zero ++ r)⟩⟩ := by induction k with (intros i l r h; simp_all) -| zero => forward h - forward h +| zero => iterate 2 forward h rw [← h] ring_nf | succ k induction_step => diff --git a/GoldbachTm/Tm27/PBP.lean b/GoldbachTm/Tm27/PBP.lean index a9412b4..789986e 100644 --- a/GoldbachTm/Tm27/PBP.lean +++ b/GoldbachTm/Tm27/PBP.lean @@ -35,9 +35,7 @@ by_cases hr1 : Nat.Prime (r1+1) repeat any_goals apply And.intro all_goals rfl obtain ⟨m, _, h⟩ := h - forward h - forward h - forward h + iterate 3 forward h apply rec26 at h forward h use (5+m+l1) @@ -264,19 +262,7 @@ induction l1 with use 1 tauto obtain ⟨j, _, h⟩ := hp - forward h - forward h - forward h - forward h - forward h - forward h - forward h - forward h - forward h - forward h - forward h - forward h - forward h + iterate 13 forward h use (13+j) . apply n_prime_17 at hp pick_goal 5 @@ -290,9 +276,7 @@ induction l1 with use 1 tauto obtain ⟨j, _, h⟩ := hp - forward h - forward h - forward h + iterate 3 forward h use (3+j) | succ l1 induction_step => intros i r1 h g hpp diff --git a/GoldbachTm/Tm27/TuringMachine27.lean b/GoldbachTm/Tm27/TuringMachine27.lean index 90c5f1f..dd010e9 100644 --- a/GoldbachTm/Tm27/TuringMachine27.lean +++ b/GoldbachTm/Tm27/TuringMachine27.lean @@ -131,51 +131,7 @@ theorem cfg45 : nth_cfg 45 = some ⟨26, { head := default, left := Turing.ListBlank.mk (List.replicate 4 Γ.one), right := Turing.ListBlank.mk [] } ⟩ := by have h : nth_cfg 0 = init [] := by simp! simp [init, Turing.Tape.mk₁, Turing.Tape.mk₂, Turing.Tape.mk'] at h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h -forward h +iterate 45 forward h simp [h] constructor . tauto