theory GraphLang

lemma exec_graph_n_stack_extend:
  "continuing stack \<Longrightarrow>
    ((stack @ xs, stack') \<in> exec_graph_n Gamma n)
    = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma
                \<inter> {(st, _). continuing st}) ^^ n'
        \<and> ((n' < n \<and> \<not> continuing stack''
                \<and> (stack'' @ xs, stack') \<in> exec_graph_n Gamma (n - n'))
            \<or> (stack' = stack'' @ xs \<and> n' = n)))" unfolding exec_graph_n_def proof (induct n arbitrary: stack) case 0 show ?case by auto[1] next case (Suc n stack) show ?case apply (simp only: relpow_Suc_simp2) apply (rule iffI) apply (clarsimp simp: exec_graph_step_stack_extend Suc.prems) apply (case_tac "continuing stack''") apply (frule Suc.hyps, clarsimp) apply (rule_tac x="stack''a" in exI, rule_tac x="Suc n'" in exI) apply (simp only: relpow_Suc_simp2, clarsimp) apply (blast intro: Suc.prems) apply (rule_tac x="stack''" in exI, rule_tac x=1 in exI) apply (auto simp: Suc.prems)[1] apply (clarsimp) apply (case_tac n', simp_all only: minus_nat.diff_0 relpow_Suc_simp2) apply auto[1] apply clarsimp apply (rule_tac b="y @ xs" in relcompI) apply (simp add: exec_graph_step_stack_extend Suc.prems) apply (case_tac "nat = 0") apply auto[1] apply (subst Suc.hyps) apply (case_tac nat, simp_all only: relpow_Suc_simp2, auto)[1] apply auto[1] done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. continuing stack \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_n Gamma n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_n Gamma (n - n') \<or> stack' = stack'' @ xs \<and> n' = n)) proof (prove)
goal (1 subgoal):
 1. continuing stack \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - n') \<or> stack' = stack'' @ xs \<and> n' = n)) proof (state)
goal (2 subgoals):
 1. \<And>stack. continuing stack \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ 0) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < 0 \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (0 - n') \<or> stack' = stack'' @ xs \<and> n' = 0))
 2. \<And>n stack. \<lbrakk>\<And>stack. continuing stack \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - n') \<or> stack' = stack'' @ xs \<and> n' = n)); continuing stack\<rbrakk> \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ Suc n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)) proof (state)
this:
continuing stack

goal (2 subgoals):
 1. \<And>stack. continuing stack \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ 0) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < 0 \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (0 - n') \<or> stack' = stack'' @ xs \<and> n' = 0))
 2. \<And>n stack. \<lbrakk>\<And>stack. continuing stack \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - n') \<or> stack' = stack'' @ xs \<and> n' = n)); continuing stack\<rbrakk> \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ Suc n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)) proof (prove)
goal (1 subgoal):
 1. ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ 0) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < 0 \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (0 - n') \<or> stack' = stack'' @ xs \<and> n' = 0)) proof (state)
this:
((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ 0) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < 0 \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (0 - n') \<or> stack' = stack'' @ xs \<and> n' = 0))

goal (1 subgoal):
 1. \<And>n stack. \<lbrakk>\<And>stack. continuing stack \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - n') \<or> stack' = stack'' @ xs \<and> n' = n)); continuing stack\<rbrakk> \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ Suc n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)) proof (state)
goal (1 subgoal):
 1. \<And>n stack. \<lbrakk>\<And>stack. continuing stack \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - n') \<or> stack' = stack'' @ xs \<and> n' = n)); continuing stack\<rbrakk> \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ Suc n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)) proof (state)
this:
continuing ?stack \<Longrightarrow> ((?stack @ xs, stack') \<in> exec_graph_step Gamma ^^ n) = (\<exists>stack'' n'. (?stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - n') \<or> stack' = stack'' @ xs \<and> n' = n))
continuing stack

goal (1 subgoal):
 1. \<And>n stack. \<lbrakk>\<And>stack. continuing stack \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - n') \<or> stack' = stack'' @ xs \<and> n' = n)); continuing stack\<rbrakk> \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ Suc n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)) proof (prove)
goal (1 subgoal):
 1. ((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ Suc n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)) proof (prove)
goal (1 subgoal):
 1. ((stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)) proof (prove)
goal (2 subgoals):
 1. (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n \<Longrightarrow> \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)
 2. \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n) \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (2 subgoals):
 1. \<And>stack''. \<lbrakk>(stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ n; (stack, stack'') \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)
 2. \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n) \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (3 subgoals):
 1. \<And>stack''. \<lbrakk>(stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ n; (stack, stack'') \<in> exec_graph_step Gamma; continuing stack''\<rbrakk> \<Longrightarrow> \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)
 2. \<And>stack''. \<lbrakk>(stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ n; (stack, stack'') \<in> exec_graph_step Gamma; \<not> continuing stack''\<rbrakk> \<Longrightarrow> \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)
 3. \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n) \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (3 subgoals):
 1. \<And>stack'' stack''a n'. \<lbrakk>(stack, stack'') \<in> exec_graph_step Gamma; continuing stack''; (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ n; (stack'', stack''a) \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n'; n' < n \<and> \<not> continuing stack''a \<and> (stack''a @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - n') \<or> stack' = stack''a @ xs \<and> n' = n\<rbrakk> \<Longrightarrow> \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)
 2. \<And>stack''. \<lbrakk>(stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ n; (stack, stack'') \<in> exec_graph_step Gamma; \<not> continuing stack''\<rbrakk> \<Longrightarrow> \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)
 3. \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n) \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (3 subgoals):
 1. \<And>stack'' stack''a n'. \<lbrakk>(stack, stack'') \<in> exec_graph_step Gamma; continuing stack''; (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ n; (stack'', stack''a) \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n'; n' < n \<and> \<not> continuing stack''a \<and> (stack''a @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - n') \<or> stack' = stack''a @ xs \<and> n' = n\<rbrakk> \<Longrightarrow> (stack, stack''a) \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ Suc n' \<and> (Suc n' < Suc n \<and> \<not> continuing stack''a \<and> (stack''a @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - Suc n') \<or> stack' = stack''a @ xs \<and> Suc n' = Suc n)
 2. \<And>stack''. \<lbrakk>(stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ n; (stack, stack'') \<in> exec_graph_step Gamma; \<not> continuing stack''\<rbrakk> \<Longrightarrow> \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)
 3. \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n) \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (3 subgoals):
 1. \<And>stack'' stack''a n'. \<lbrakk>(stack, stack'') \<in> exec_graph_step Gamma; continuing stack''; (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ n; (stack'', stack''a) \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n'; n' < n \<and> \<not> continuing stack''a \<and> (stack''a @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - n') \<or> stack' = stack''a @ xs \<and> n' = n\<rbrakk> \<Longrightarrow> (stack, stack''a) \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) O (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n'
 2. \<And>stack''. \<lbrakk>(stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ n; (stack, stack'') \<in> exec_graph_step Gamma; \<not> continuing stack''\<rbrakk> \<Longrightarrow> \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)
 3. \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n) \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (2 subgoals):
 1. \<And>stack''. \<lbrakk>(stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ n; (stack, stack'') \<in> exec_graph_step Gamma; \<not> continuing stack''\<rbrakk> \<Longrightarrow> \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n)
 2. \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n) \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (2 subgoals):
 1. \<And>stack''. \<lbrakk>(stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ n; (stack, stack'') \<in> exec_graph_step Gamma; \<not> continuing stack''\<rbrakk> \<Longrightarrow> (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ 1 \<and> (1 < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - 1) \<or> stack' = stack'' @ xs \<and> 1 = Suc n)
 2. \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n) \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (1 subgoal):
 1. \<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n) \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (1 subgoal):
 1. \<And>stack'' n'. \<lbrakk>(stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n'; n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n\<rbrakk> \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (2 subgoals):
 1. \<And>stack'' n'. \<lbrakk>(stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ 0; 0 < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n \<or> stack' = stack'' @ xs \<and> 0 = Suc n; n' = 0\<rbrakk> \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n
 2. \<And>stack'' n' nat. \<lbrakk>(stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) O (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ nat; Suc nat < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - Suc nat) \<or> stack' = stack'' @ xs \<and> Suc nat = Suc n; n' = Suc nat\<rbrakk> \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (1 subgoal):
 1. \<And>stack'' n' nat. \<lbrakk>(stack, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) O (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ nat; Suc nat < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - Suc nat) \<or> stack' = stack'' @ xs \<and> Suc nat = Suc n; n' = Suc nat\<rbrakk> \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (1 subgoal):
 1. \<And>nat y z. \<lbrakk>nat < n \<and> \<not> continuing z \<and> (z @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - nat) \<or> stack' = z @ xs \<and> nat = n; (y, z) \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ nat; (stack, y) \<in> exec_graph_step Gamma; continuing stack\<rbrakk> \<Longrightarrow> (stack @ xs, stack') \<in> exec_graph_step Gamma O exec_graph_step Gamma ^^ n proof (prove)
goal (2 subgoals):
 1. \<And>nat y z. \<lbrakk>nat < n \<and> \<not> continuing z \<and> (z @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - nat) \<or> stack' = z @ xs \<and> nat = n; (y, z) \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ nat; (stack, y) \<in> exec_graph_step Gamma; continuing stack\<rbrakk> \<Longrightarrow> (stack @ xs, y @ xs) \<in> exec_graph_step Gamma
 2. \<And>nat y z. \<lbrakk>nat < n \<and> \<not> continuing z \<and> (z @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - nat) \<or> stack' = z @ xs \<and> nat = n; (y, z) \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ nat; (stack, y) \<in> exec_graph_step Gamma; continuing stack\<rbrakk> \<Longrightarrow> (y @ xs, stack') \<in> exec_graph_step Gamma ^^ n proof (prove)
goal (1 subgoal):
 1. \<And>nat y z. \<lbrakk>nat < n \<and> \<not> continuing z \<and> (z @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - nat) \<or> stack' = z @ xs \<and> nat = n; (y, z) \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ nat; (stack, y) \<in> exec_graph_step Gamma; continuing stack\<rbrakk> \<Longrightarrow> (y @ xs, stack') \<in> exec_graph_step Gamma ^^ n proof (prove)
goal (2 subgoals):
 1. \<And>nat y z. \<lbrakk>nat < n \<and> \<not> continuing z \<and> (z @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - nat) \<or> stack' = z @ xs \<and> nat = n; (y, z) \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ nat; (stack, y) \<in> exec_graph_step Gamma; continuing stack; nat = 0\<rbrakk> \<Longrightarrow> (y @ xs, stack') \<in> exec_graph_step Gamma ^^ n
 2. \<And>nat y z. \<lbrakk>nat < n \<and> \<not> continuing z \<and> (z @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - nat) \<or> stack' = z @ xs \<and> nat = n; (y, z) \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ nat; (stack, y) \<in> exec_graph_step Gamma; continuing stack; nat \<noteq> 0\<rbrakk> \<Longrightarrow> (y @ xs, stack') \<in> exec_graph_step Gamma ^^ n proof (prove)
goal (1 subgoal):
 1. \<And>nat y z. \<lbrakk>nat < n \<and> \<not> continuing z \<and> (z @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - nat) \<or> stack' = z @ xs \<and> nat = n; (y, z) \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ nat; (stack, y) \<in> exec_graph_step Gamma; continuing stack; nat \<noteq> 0\<rbrakk> \<Longrightarrow> (y @ xs, stack') \<in> exec_graph_step Gamma ^^ n proof (prove)
goal (2 subgoals):
 1. \<And>nat y z. \<lbrakk>nat < n \<and> \<not> continuing z \<and> (z @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - nat) \<or> stack' = z @ xs \<and> nat = n; (y, z) \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ nat; (stack, y) \<in> exec_graph_step Gamma; continuing stack; nat \<noteq> 0\<rbrakk> \<Longrightarrow> continuing y
 2. \<And>nat y z. \<lbrakk>nat < n \<and> \<not> continuing z \<and> (z @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - nat) \<or> stack' = z @ xs \<and> nat = n; (y, z) \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ nat; (stack, y) \<in> exec_graph_step Gamma; continuing stack; nat \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>stack'' n'. (y, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - n') \<or> stack' = stack'' @ xs \<and> n' = n) proof (prove)
goal (1 subgoal):
 1. \<And>nat y z. \<lbrakk>nat < n \<and> \<not> continuing z \<and> (z @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - nat) \<or> stack' = z @ xs \<and> nat = n; (y, z) \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ nat; (stack, y) \<in> exec_graph_step Gamma; continuing stack; nat \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>stack'' n'. (y, stack'') \<in> (exec_graph_step Gamma \<inter> {(st, uu_). continuing st}) ^^ n' \<and> (n' < n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (n - n') \<or> stack' = stack'' @ xs \<and> n' = n) proof (prove)
goal:
No subgoals! proof (state)
this:
((stack @ xs, stack') \<in> exec_graph_step Gamma ^^ Suc n) = (\<exists>stack'' n'. (stack, stack'') \<in> (exec_graph_step Gamma \<inter> {a. case a of (st, uu_) \<Rightarrow> continuing st}) ^^ n' \<and> (n' < Suc n \<and> \<not> continuing stack'' \<and> (stack'' @ xs, stack') \<in> exec_graph_step Gamma ^^ (Suc n - n') \<or> stack' = stack'' @ xs \<and> n' = Suc n))

goal:
No subgoals!