Acc lang loop

theorem acc_lang_loop [Inhabited A] :    (M.Loop acc).AcceptedLang {inl ()} = (M.AcceptedLang acc)∗ := by  ext al ; constructor  · rintro ⟨n, as, ⟨ss, h_run, h_acc⟩, h_al⟩ ; simp [instIterStar, IterStar]    revert al    induction' n using Nat.strong_induction_on with n h_ind    intro al h_al    let loop k := 0 < k ∧ k < n ∧ ss k = inl ()    rcases Classical.em (∃ k, loop k) with h_loop | h_loop    · let m := Nat.findGreatest loop n      have h_m : loop m := by        obtain ⟨k, h_loop⟩ := h_loop        apply Nat.findGreatest_spec (m := k) (by omega) h_loop      obtain ⟨h_m_0, h_m_n, h_m_inl⟩ := h_m      let al' := as.extract 0 m      have h_run' := na_FinRun_imp_FinRun h_m_n h_run      obtain ⟨j, h_j⟩ := h_ind m h_m_n h_run' (by simp [h_m_inl]) (al') (by simp [al'])      have h_d : n - m > 0 := by omega      have h_run'' : (M.Loop acc).FinRun (n - m) (as.drop m) (ss.drop m) := by        constructor        · simp [NA.Loop, get_drop', h_m_inl]        intro k h_k        have h_next := h_run.2 (k + m) (by omega)        simp [h_next, get_drop', (show m + (k + 1) = k + m + 1 by omega), (show m + k = k + m by omega)]      have h_inl'' : (ss.drop m) (n - m) = inl () := by        simp at h_acc        simp [get_drop', (show m + (n - m) = n by omega), h_acc]      have h_inr'' : ∀ k < n - m, k > 0 → (ss.drop m) k ∈ range inr := by        intro k h_k_d h_k_0        have h_not_loop : ¬ loop (k + m) := by          exact Nat.findGreatest_is_greatest (show m < k + m by omega) (by omega)        simp [loop, -add_pos_iff] at h_not_loop        obtain ⟨s', h_s'⟩ := not_inl_unit.mp <| h_not_loop (by omega) (by omega)        simp [get_drop'] ; use s' ; rw [add_comm] ; simp [h_s']      obtain ⟨ss'', h_run'', h_acc'', _⟩ := (na_loop_fin_run h_d).mp ⟨h_run'', h_inl'', h_inr''⟩      let al'' := as.extract m n      use (j + 1) ; simp [instIterFin, IterFin]      use al', al'' ; constructorm* _ ∧ _      · exact h_j      · use (n - m), (as.drop m)        simp [al'', extract_drop, (show m + (n - m) = n by omega)]        use ss''      · simp (disch := omega) [← h_al, al', al'', append_extract_extract]    · rcases (show n = 0 ∨ n > 0 by omega) with ⟨rfl⟩ | h_n      · use 0 ; simp [← h_al, instIterFin, IterFin, extract_eq_nil]      simp [loop] at h_loop      have h_inr : ∀ k < n, k > 0 → ss k ∈ range inr := by        intro k h_k_n h_k_0        obtain ⟨s', h_s'⟩ := not_inl_unit.mp <| h_loop k h_k_0 h_k_n        use s' ; simp [h_s']      simp at h_acc      obtain ⟨ss', h_run', h_acc', _⟩ := (na_loop_fin_run h_n).mp ⟨h_run, h_acc, h_inr⟩      use 1 ; simp [instIterFin, IterFin, epsilon_ConcatFin]      use n, as ; simp [h_al]      use ss'  · rintro ⟨L, ⟨i, rfl⟩, h_al⟩ ; simp at h_al    revert al    induction' i with i h_ind    · intro al ; simp [instIterFin, IterFin] ; rintro ⟨rfl⟩      use 0 ; simp [extract_eq_nil]      use (fun k ↦ default), (fun k ↦ inl ()) ; simp [NA.FinRun, NA.Loop]    rintro al ⟨al1, al2, h_al1, h_al2, h_al⟩    specialize h_ind al1 h_al1    suffices _ : al2 ∈ (M.Loop acc).AcceptedLang {inl ()} by      apply acc_lang_loop_concat ; use al1, al2    obtain ⟨n2, as2, ⟨ss2', h_run2, h_acc2⟩, h_al2⟩ := h_al2    obtain ⟨ss2, h_run2, h_acc2, _⟩ := na_loop_fin_run_exists h_run2 h_acc2    use n2, as2 ; simp [h_al2]    use ss2 ; simp [h_run2, h_acc2]