Theory Pushdown_Automata

section ‹Pushdown Automata (PDA)›

theory Pushdown_Automata
imports Main
begin

subsection ‹Definitions›

text ‹In the following, we define \emph{pushdown automata} and show some basic properties of them.
The formalization is based on the Lean formalization by Leichtfried\cite{lean}.›

text ‹We represent the transition function $\delta$ by splitting it into two different functions
$\delta_1 : Q \times \Sigma \times \Gamma \rightarrow Q \times \Gamma^*$ and
$\delta_2 : Q \times \Gamma \rightarrow Q \times \Gamma^*$,
where $\delta_1(q, a, Z) := \delta(q, a, Z)$ and $\delta_2(q, Z) := \delta(q, \epsilon, Z)$.›

record ('q,'a,'s) pda = init_state    :: 'q
                        init_symbol   :: 's 
                        final_states  :: "'q set"
                        delta     :: "'q ⇒ 'a ⇒ 's ⇒ ('q × 's list) set"
                        delta_eps       :: "'q ⇒ 's ⇒ ('q × 's list) set"

locale pda =
  fixes M :: "('q :: finite, 'a :: finite, 's :: finite) pda"
  assumes finite_delta: "finite (delta M p a Z)"
      and finite_delta_eps: "finite (delta_eps M p Z)"
begin

notation delta ("δ")
notation delta_eps ("δε")

(*
TODO?
fun step1 :: "'q × 'a list × 's list ⇒ 'q × 'a list × 's list ⇒ bool" where
*)
fun step :: "'q × 'a list × 's list ⇒ ('q × 'a list × 's list) set" where
  "step (p, a#w, Z#α) = {(q, w, β@α) | q β. (q, β) ∈ δ M p a Z}
                        ∪ {(q, a#w, β@α) | q β. (q, β) ∈ δε M p Z}"
| "step (p, [], Z#α) = {(q, [], β@α) | q β. (q, β) ∈ δε M p Z}"
| "step (_, _, []) = {}"

fun step1 :: "'q × 'a list × 's list ⇒ 'q × 'a list × 's list ⇒ bool"
  ("(_ ↝ _)" [50, 50] 50) where
  "(p1, w1, α1) ↝ (p2, w2, α2) ⟷ (p2, w2, α2) ∈ step (p1, w1, α1)"

definition steps :: "'q × 'a list × 's list ⇒ 'q × 'a list × 's list ⇒ bool"
  ("(_ ↝* _)" [50, 50] 50) where
  "steps ≡ step1 ^**"

(* TODO:
definition stepn :: "nat ⇒ 'q × 'a list × 's list ⇒ 'q × 'a list × 's list ⇒ bool" where
"stepn n = step1^^n"
*)
inductive stepn :: "nat ⇒ 'q × 'a list × 's list ⇒ 'q × 'a list × 's list ⇒ bool" where
refln: "stepn 0 (p, w, α) (p, w, α)" |
stepn: "stepn n (p1, w1, α1) (p2, w2, α2) ⟹ step1 (p2, w2, α2) (p3, w3, α3) ⟹ stepn (Suc n) (p1, w1, α1) (p3, w3, α3)"

abbreviation stepsn ("(_ /↝'(_')/ _)" [50, 0, 50] 50) where
"c ↝(n) c' ≡ stepn n c c'"

text ‹The language accepted by empty stack:›

definition accept_stack :: "'a list set" where
  "accept_stack ≡ {w. ∃q. (init_state M, w, [init_symbol M]) ↝* (q, [], [])}"

text ‹The language accepted by final state:›

definition accept_final :: "'a list set" where 
  "accept_final ≡ {w. ∃q ∈ final_states M. ∃γ. (init_state M, w, [init_symbol M]) ↝* (q, [], γ)}"

subsection ‹Basic Lemmas›

subsubsection ‹const‹step› and const‹step1››

lemma card_trans_step: "card (δ M p a Z) = card {(q, w, β@α) | q β. (q, β) ∈ δ M p a Z}"
  by (rule bij_betw_same_card[where ?f = "λ(q,β). (q, w, β@α)"]) (auto simp: bij_betw_def inj_on_def)

lemma card_eps_step: "card (δε M p Z) = card {(q, w, β@α) | q β. (q, β) ∈ δε M p Z}"
  by (rule bij_betw_same_card[where ?f = "λ(q,β). (q, w, β@α)"]) (auto simp: bij_betw_def inj_on_def)

lemma card_empty_step: "card (step (p, [], Z#α)) = card (δε M p Z)"
  by (rule sym) (simp add: card_eps_step)

lemma finite_delta_step: "finite {(q, w, β @ α) |q β. (q, β) ∈ δ M p a Z}" (is "finite ?A")
  using bij_betw_finite[of "λ(q,β). (q, w, β@α)" "δ M p a Z" ?A] by (fastforce simp add: bij_betw_def inj_on_def finite_delta)

lemma finite_delta_eps_step: "finite {(q, w, β @ α) |q β. (q, β) ∈ δε M p Z}" (is "finite ?A")
  using bij_betw_finite[of "λ(q,β). (q, w, β@α)" "δε M p Z" ?A] by (fastforce simp add: bij_betw_def inj_on_def finite_delta_eps)

lemma card_nonempty_step: "card (step (p, a#w, Z#α)) = card (δ M p a Z) + card (δε M p Z)"
  apply (simp only: step.simps)
  apply (subst card_trans_step)
  apply (subst card_eps_step)
  apply (rule card_Un_disjoint)
    apply (auto simp: finite_delta_step finite_delta_eps_step)
  done

lemma finite_step: "finite (step (p, w, Z#α))"
  by (cases w) (auto simp: finite_delta_step finite_delta_eps_step)

lemma step1_nonempty_stack: "(p1, w1, α1) ↝ (p2, w2, α2) ⟹ ∃Z' α'. α1 = Z'#α'"
  by (cases α1) auto

lemma step1_empty_stack: "¬ (p1, w1, []) ↝ (p2, w2, α2)"
  by simp

lemma step1_rule: "(p1, w1, Z#α1) ↝ (p2, w2, α2) ⟷ (∃β. w2 = w1 ∧ α2 = β@α1 ∧ (p2, β) ∈ δε M p1 Z) 
                                                   ∨ (∃a β. w1 = a # w2 ∧ α2 = β@α1 ∧ (p2, β) ∈ δ M p1 a Z)"
  by (cases w1) auto

lemma step1_rule_ext: "(p1, w1, α1) ↝ (p2, w2, α2) ⟷ (∃Z' α'. α1 = Z'#α' ∧ ((∃β. w2 = w1 ∧ α2 = β@α' ∧ (p2, β) ∈ δε M p1 Z') 
                                                   ∨ (∃a β. w1 = a # w2 ∧ α2 = β@α' ∧ (p2, β) ∈ δ M p1 a Z')))" (is "?l ⟷ ?r")
  apply (rule iffI)
   apply (metis step1_nonempty_stack step1_rule)
  apply (use step1_rule in force)
  done

lemma step1_stack_app: "(p1, w1, α1) ↝ (p2, w2, α2) ⟹ (p1, w1, α1 @ γ) ↝ (p2, w2, α2 @ γ)"
  using step1_rule_ext by auto


subsubsection ‹const‹steps››

lemma steps_refl: "(p, w, α) ↝* (p, w, α)"
  by (simp add: steps_def)

lemma steps_trans: "⟦ (p1, w1, α1) ↝* (p2, w2, α2); (p2, w2, α2) ↝* (p3, w3, α3) ⟧
 ⟹ (p1, w1, α1) ↝* (p3, w3, α3)"
  unfolding steps_def using rtranclp_trans[where ?r = step1] by blast

lemma step1_steps: "(p1, w1, α1) ↝ (p2, w2, α2) ⟹ (p1, w1, α1) ↝* (p2, w2, α2)"
  by (simp add: steps_def r_into_rtranclp)

lemma steps_empty_stack: "(p1, w1, []) ↝* (p2, w2, α2) ⟹ p1 = p2 ∧ w1 = w2 ∧ α2 = []"
  unfolding steps_def using converse_rtranclpE2 by fastforce

lemma steps_induct2[consumes 1]:
  assumes "x1 ↝* x2"
      and "⋀p w α. P (p, w, α) (p, w, α)"
      and "⋀p1 w1 α1 p2 w2 α2 p3 w3 α3. (p1, w1, α1) ↝ (p2, w2, α2) ⟹ (p2, w2, α2) ↝* (p3, w3, α3) ⟹ 
                P (p2, w2, α2) (p3, w3, α3) ⟹ P (p1, w1, α1) (p3, w3, α3)"
    shows "P x1 x2"
using assms[unfolded steps_def]
proof(induction rule: converse_rtranclp_induct)
  case base thus ?case by (metis prod_cases3)
next
  case step thus ?case by simp (metis prod_cases3 step1.simps)
qed

lemma steps_induct2_bw[consumes 1, case_names base step]:
  assumes "steps x1 x2"
      and "⋀p w α. P (p, w, α) (p, w, α)"
      and "⋀p1 w1 α1 p2 w2 α2 p3 w3 α3. (p1, w1, α1) ↝* (p2, w2, α2) ⟹ (p2, w2, α2) ↝ (p3, w3, α3) ⟹ 
                P (p1, w1, α1) (p2, w2, α2) ⟹ P (p1, w1, α1) (p3, w3, α3)"
    shows "P x1 x2"
  using assms[unfolded steps_def]
proof(induction rule: rtranclp_induct)
  case base
  then show ?case by (metis prod_cases3)
next
  case (step)
  then show ?case by simp (metis prod_cases3 step1.simps)
qed

lemmas converse_rtranclp_induct3_aux =
  converse_rtranclp_induct [of step1 "(ax, ay, az)" "(bx, by, bz)", split_rule]
lemmas steps_induct =
  converse_rtranclp_induct3_aux [of M, folded steps_def,consumes 1, case_names refl step]

lemma step1_word_app: "step1 (p1, w1, α1) (p2, w2, α2) ⟷ step1 (p1, w1 @ w, α1) (p2, w2 @ w, α2)"
  using step1_rule_ext by simp

lemma decreasing_word: "(p1, w1, α1) ↝* (p2, w2, α2) ⟹ ∃w. w1 = w @ w2"
  by (induction rule: steps_induct) (use step1_rule_ext in auto)


subsubsection ‹const‹stepn››

inductive_cases stepn_zeroE[elim!]: "(p1, w1, α1) ↝(0) (p2, w2, α2)"
thm stepn_zeroE
inductive_cases stepn_sucE[elim!]: "(p1, w1, α1) ↝(Suc n) (p2, w2, α2)"
thm stepn_sucE

declare stepn.intros[simp, intro]

lemma step1_stepn_one: "(p1, w1, α1) ↝ (p2, w2, α2) ⟷ (p1, w1, α1) ↝(1) (p2, w2, α2)"
  by auto

lemma stepn_split_last: "(∃p' w' α'. (p1, w1, α1) ↝(n) (p', w', α') ∧ (p', w', α') ↝ (p2, w2, α2)) 
                                ⟷ (p1, w1, α1) ↝(Suc n) (p2, w2, α2)"
  by auto

lemma stepn_split_first: "(∃p' w' α'. (p1, w1, α1) ↝ (p', w', α') ∧ (p', w', α') ↝(n) (p2, w2, α2)) 
                                ⟷ (p1, w1, α1) ↝(Suc n) (p2, w2, α2)" (is "?l ⟷ ?r")
proof
  assume ?l
  then obtain p' w' α' where r1: "(p1, w1, α1) ↝ (p', w', α')" and rN: "(p', w', α') ↝(n) (p2, w2, α2)" by blast
  from rN r1 show ?r
    by (induction rule: stepn.induct) auto
next
  show "?r ⟹ ?l"
    by (induction "Suc n" "(p1, w1, α1)" "(p2, w2, α2)" arbitrary: n p2 w2 α2 rule: stepn.induct)
       (metis old.nat.exhaust refln stepn stepn_zeroE)
qed

lemma stepn_induct[consumes 1, case_names basen stepn]:
  assumes "x1 ↝(n) x2"
      and "⋀p w α. P 0 (p, w, α) (p, w, α)"
      and "⋀n p1 w1 α1 p2 w2 α2 p3 w3 α3. (p1, w1, α1) ↝ (p2, w2, α2) ⟹ (p2, w2, α2) ↝(n) (p3, w3, α3) ⟹ 
                P n (p2, w2, α2) (p3, w3, α3) ⟹ P (Suc n) (p1, w1, α1) (p3, w3, α3)"
    shows "P n x1 x2"
using assms proof (induction n arbitrary: x1)
  case 0
  obtain p1 w1 α1 p2 w2 α2 where [simp]: "x1 = (p1, w1, α1)" and [simp]: "x2 = (p2, w2, α2)"
    by (metis prod_cases3)
  from "0.prems"(1) have "x1 = x2" by auto
  with "0.prems"(2) show ?case by simp
next
  case (Suc n)
  obtain p1 w1 α1 p2 w2 α2 where [simp]: "x1 = (p1, w1, α1)" and x2_def[simp]: "x2 = (p2, w2, α2)"
    by (metis prod_cases3)
  from Suc.prems(1) obtain p' w' α' where 
      r1: "(p1, w1, α1) ↝ (p', w', α')" and rN: "(p', w', α') ↝(n) (p2, w2, α2)"
    using stepn_split_first[of p1 w1 α1 n p2 w2 α2] by auto
  have "P n (p', w', α') (p2, w2, α2)"
    using Suc.IH[unfolded x2_def, OF rN Suc.prems(2,3)] by simp
  then show ?case
    using Suc.prems(3)[OF r1 rN] by simp
qed

lemma stepn_trans:
  assumes "(p1, w1, α1) ↝(n) (p2, w2, α2)"
      and "(p2, w2, α2) ↝(m) (p3, w3, α3)"
    shows "(p1, w1, α1) ↝(n+m) (p3, w3, α3)"
using assms(2,1) by (induction rule: stepn.induct) auto

lemma stepn_steps: "(∃n. (p1, w1, α1) ↝(n) (p2, w2, α2)) ⟷ (p1, w1, α1) ↝* (p2, w2, α2)" (is "?l ⟷ ?r")
proof 
  assume ?l
  then obtain n where "(p1, w1, α1) ↝(n) (p2, w2, α2)" by blast
  thus "(p1, w1, α1) ↝* (p2, w2, α2)" 
    apply (induction rule: stepn.induct) 
     apply (rule steps_refl)
    apply (simp add: step1_steps steps_trans)
    done
next
  show "?r ⟹ ?l"
    by (induction rule: steps_induct) (use stepn_split_first in blast)+
qed

lemma stepn_word_app: "(p1, w1, α1) ↝(n) (p2, w2, α2) ⟷ (p1, w1 @ w, α1) ↝(n) (p2, w2 @ w, α2)" (is "?l ⟷ ?r")
proof
  show "?l ⟹ ?r"
    by (induction n "(p1, w1, α1)" "(p2, w2, α2)" arbitrary: p2 w2 α2 rule: stepn.induct) (use step1_word_app in auto)
next
  show "?r ⟹ ?l"
  proof (induction n "(p1, w1 @ w, α1)" "(p2, w2 @ w, α2)" arbitrary: p2 w2 α2 rule: stepn.induct)
    case (stepn n p2 w2 α2 p3 α3 w3)
    obtain w' where w2_def: "w2 = w' @ w3 @ w"
      using decreasing_word[OF step1_steps[OF stepn(3)]] by blast

    with stepn(2) have "(p1, w1, α1) ↝(n) (p2, w' @ w3, α2)" by simp

    moreover from stepn(3) w2_def have "(p2, w' @ w3, α2) ↝ (p3, w3, α3)"
      using step1_word_app by force

    ultimately show ?case by simp
  qed simp
qed

lemma steps_word_app: "(p1, w1, α1) ↝* (p2, w2, α2) ⟷ (p1, w1 @ w, α1) ↝* (p2, w2 @ w, α2)"
  using stepn_steps stepn_word_app by metis

lemma stepn_not_refl_split_first:
  assumes "(p1, w1, α1) ↝(n) (p2, w2, α2)"
      and "(p1, w1, α1) ≠ (p2, w2, α2)"
    shows "∃n' p' w' α'. n = Suc n' ∧ (p1, w1, α1) ↝ (p', w', α') ∧ (p', w', α') ↝(n') (p2, w2, α2)"
proof -
  from assms have "n > 0" by fast
  then obtain n' where "n = Suc n'"
    using not0_implies_Suc by blast
  with assms(1) show ?thesis
    using stepn_split_first by simp
qed

lemma stepn_not_refl_split_last:
  assumes "(p1, w1, α1) ↝(n) (p2, w2, α2)"
      and "(p1, w1, α1) ≠ (p2, w2, α2)"
    shows "∃n' p' w' α'. n = Suc n' ∧ (p1, w1, α1) ↝(n') (p', w', α') ∧ (p', w', α') ↝ (p2, w2, α2)"
proof -
  from assms have "n > 0" by fast
  then obtain n' where "n = Suc n'"
    using not0_implies_Suc by blast
  with assms(1) show ?thesis
    using stepn_split_last by simp
qed

lemma steps_not_refl_split_first:
  assumes "(p1, w1, α1) ↝* (p2, w2, α2)"
      and "(p1, w1, α1) ≠ (p2, w2, α2)"
    shows "∃p' w' α'. (p1, w1, α1) ↝ (p', w', α') ∧ (p', w', α') ↝* (p2, w2, α2)"
using assms stepn_steps stepn_not_refl_split_first by metis

lemma steps_not_refl_split_last:
  assumes "(p1, w1, α1) ↝* (p2, w2, α2)"
      and "(p1, w1, α1) ≠ (p2, w2, α2)"
    shows "∃p' w' α'. (p1, w1, α1) ↝* (p', w', α') ∧ (p', w', α') ↝ (p2, w2, α2)"
using assms stepn_steps stepn_not_refl_split_last by metis

lemma stepn_stack_app: "(p1, w1, α1) ↝(n) (p2, w2, α2) ⟹ (p1, w1, α1 @ β) ↝(n) (p2, w2, α2 @ β)"
  by (induction n "(p1, w1, α1)" "(p2, w2, α2)" arbitrary: p2 w2 α2 rule: stepn.induct) (fastforce intro: step1_stack_app)+

lemma steps_stack_app: "(p1, w1, α1) ↝* (p2, w2, α2) ⟹ (p1, w1, α1 @ β) ↝* (p2, w2, α2 @ β)"
  using stepn_steps stepn_stack_app by metis

lemma step1_stack_drop: 
  assumes "(p1, w1, α1 @ γ) ↝ (p2, w2, α2 @ γ)"
      and "α1 ≠ []"
    shows "(p1, w1, α1) ↝ (p2, w2, α2)"
proof -
  from assms(1) obtain Z' α' where α1_γ_def: "α1 @ γ = Z' # α'" and
           rule: "(∃β. w2 = w1 ∧ α2@γ = β@α' ∧ (p2, β) ∈ δε M p1 Z') 
                     ∨ (∃a β. w1 = a # w2 ∧ α2@γ = β@α' ∧ (p2,β) ∈ δ M p1 a Z')"
    using step1_rule_ext by auto
  from α1_γ_def assms(2) obtain α'' where α1_def: "α1 = Z' # α''" and α'_def: "α' = α'' @ γ"
    using Cons_eq_append_conv[of Z' α' α1 γ] by auto
  from rule α'_def have "(∃β. w2 = w1 ∧ α2 = β@α'' ∧ (p2, β) ∈ δε M p1 Z') 
           ∨ (∃a β. w1 = a # w2 ∧ α2 = β@α'' ∧ (p2,β) ∈ δ M p1 a Z')" by auto
  with α1_def show ?thesis
    using step1_rule by simp
qed

lemma stepn_reads_input:
  assumes "(p1, a # w, α1) ↝(n) (p2, [], α2)"
  shows "∃n' k q1 q2 γ1 γ2. n = Suc n' ∧ k ≤ n' ∧ (p1, a # w, α1) ↝(k) (q1, a # w, γ1) ∧ 
            (q1, a # w, γ1) ↝ (q2, w, γ2) ∧ (q2, w, γ2) ↝(n'-k) (p2, [], α2)"
using assms proof (induction n "(p1, a # w, α1)" "(p2, [] :: 'a list, α2)" arbitrary: p1 α1 rule: stepn_induct)
  case (stepn n p1 α1 p' w' α')
  from stepn(1) have case_dist: "w' = w ∨ w' = a#w" (is "?l ∨ ?r")
    using step1_rule_ext by auto
  show ?case proof (rule disjE[OF case_dist])
    assume l: ?l 

    from l stepn(1) have "step1 (p1, a # w, α1) (p', w, α')" by simp

    moreover from l stepn(2) have "(p', w, α') ↝(n) (p2, [], α2)" by simp

    ultimately show ?case by fastforce
  next 
    assume r: ?r
    obtain n' k q1 q2 γ1 γ2 where IH1: "n = Suc n'" and IH2: "k ≤ n'" and 
        IH3: "(p', a # w, α') ↝(k) (q1, a # w, γ1)" and IH4: "(q1, a # w, γ1) ↝ (q2, w, γ2)" and 
        IH5: "(q2, w, γ2) ↝(n'-k) (p2, [], α2)"
      using stepn(3)[OF r] by blast

    from IH1 IH2 have "Suc k ≤ n" by simp

    moreover from stepn(1) r IH3 have "(p1, a # w, α1) ↝(Suc k) (q1, a # w, γ1)"
      using stepn_split_first by blast

    moreover from IH1 IH5 have "stepn (n - Suc k) (q2, w, γ2) (p2, [], α2)" by simp

    ultimately show ?case
      using IH4 by metis
  qed
qed

lemma split_word:
"(p1, w @ w', α1) ↝(n) (p2, [], α2) ⟹ ∃k q γ. k ≤ n ∧ (p1, w, α1) ↝(k) (q, [], γ) ∧ (q, w', γ) ↝(n-k) (p2, [], α2)"
proof (induction w arbitrary: n p1 α1)
  case (Cons a w)
  from Cons(2) obtain n' k q1 q2 γ1 γ2 where n_def: "n = Suc n'" and k_lesseq_n': "k ≤ n'" and stepk: "(p1, a # (w @ w'), α1) ↝(k) (q1, a # (w @ w'), γ1)" and
                    step1: "(q1, a # (w @ w'), γ1) ↝ (q2, w @ w', γ2)" and stepnk: "(q2, w @ w', γ2) ↝(n'-k) (p2, [], α2)"
    using stepn_reads_input[of n p1 a "w @ w'" α1 p2 α2] by auto
  obtain k'' q γ where k''_lesseq_n'k: "k'' ≤ n'-k" and stepk'': "(q2, w, γ2) ↝(k'') (q, [], γ)" and stepn'kk'': "(q, w', γ) ↝(n'-k-k'') (p2, [], α2)"
    using Cons.IH[OF stepnk] by blast
  from stepk step1 have stepSuck: "stepn (Suc k) (p1, a # w, α1) (q2, w, γ2)"
    using stepn_word_app[of "Suc k" p1 "a # w" α1 q2 w γ2 w'] by simp

  have "(p1, a # w, α1) ↝(Suc k + k'') (q, [], γ)" 
    using stepn_trans[OF stepSuck stepk''] .

  moreover from n_def stepn'kk'' have "(q, w', γ) ↝(n - (Suc k + k'')) (p2, [], α2)" by simp

  moreover from n_def k_lesseq_n' k''_lesseq_n'k have "Suc k + k'' ≤ n" by simp

  ultimately show ?case by blast
qed fastforce

lemma split_stack: 
"stepn n (p1, w1, α1 @ β1) (p2, [], []) ⟹ ∃p' m1 m2 y y'. w1 = y @ y' ∧ m1 + m2 = n 
                                          ∧ (p1, y, α1) ↝(m1) (p', [], []) ∧ (p', y', β1) ↝(m2) (p2, [], [])"
proof (induction n arbitrary: p1 w1 α1)
  case (Suc n)
  show ?case proof (cases α1)
    case Nil

    from Nil have "stepn 0 (p1, [], α1) (p1, [], [])" by simp

    moreover from Suc.prems Nil have "stepn (Suc n) (p1, w1, β1) (p2, [], [])" by simp

    ultimately show ?thesis by force
  next
    case (Cons Z α)
    with Suc.prems obtain p' w' α' where r1: "step1 (p1, w1, Z # α @ β1) (p', w', α')" and rN: "stepn n (p', w', α') (p2, [], [])"
      using stepn_split_first[of p1 w1 "Z # α @ β1" n p2 "[]" "[]"] by auto 
    from r1 have rule: "(∃β. w' = w1 ∧ α' = β @ α @ β1 ∧ (p', β) ∈ δε M p1 Z) 
           ∨ (∃a β. w1 = a # w' ∧ α' = β @ α @ β1 ∧ (p',β) ∈ δ M p1 a Z)" (is "?l ∨ ?r")
      using step1_rule by blast
    show ?thesis proof (rule disjE[OF rule])
      assume ?l
      then obtain β where w1_def: "w1 = w'" and α'_def: "α' = β @ α @ β1" and e: "(p',β) ∈ δε M p1 Z" by blast
      from rN α'_def have rN2: "stepn n (p', w', (β @ α) @ β1) (p2, [], [])" by simp
      obtain p'' m1 m2 y y' where w'_def: "w' = y @ y'" and m1_m2_n: "m1 + m2 = n" 
          and rm1: "stepn m1 (p', y, β @ α) (p'', [], [])" and rm2: "stepn m2 (p'', y', β1) (p2, [], [])"
        using Suc.IH[OF rN2] by blast
      from e have s1: "step1 (p1, y, Z#α) (p', y, β@α)"
        using step1_rule by blast

      from w1_def w'_def have "w1 = y @ y'" by simp

      moreover from m1_m2_n have "Suc m1 + m2 = Suc n" by simp

      moreover from s1 rm1 Cons have "stepn (Suc m1) (p1, y, α1) (p'', [], [])"
        using stepn_split_first by blast

      ultimately show ?thesis
        using rm2 by metis
    next
      assume ?r
      then obtain a β where w1_def: "w1 = a # w'" and α'_def: "α' = β @ α @ β1" and tr: "(p',β) ∈ δ M p1 a Z" by blast
      from rN α'_def have rN2: "stepn n (p', w', (β @ α) @ β1) (p2, [], [])" by simp
      obtain p'' m1 m2 y y' where w'_def: "w' = y @ y'" and m1_m2_n: "m1 + m2 = n" 
          and rm1: "stepn m1 (p', y, β @ α) (p'', [], [])" and rm2: "stepn m2 (p'', y', β1) (p2, [], [])"
        using Suc.IH[OF rN2] by blast
      from tr have s1: "step1 (p1, a#y, Z#α) (p', y, β@α)" by simp

      from w1_def w'_def have "w1 = (a # y) @ y'" by simp

      moreover from m1_m2_n have "Suc m1 + m2 = Suc n" by simp

      moreover from s1 rm1 Cons have "stepn (Suc m1) (p1, a#y, α1) (p'', [], [])"
        using stepn_split_first by blast

      ultimately show ?thesis 
        using rm2 by metis
    qed
  qed
qed blast

end

end