theory Finalise_AI

lemma (in mdb_empty_abs) parency:
  "n \<Turnstile> p \<rightarrow> p' = (p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p')" proof assume n: "n \<Turnstile> p \<rightarrow> p'" from n have "p \<noteq> slot" by (clarsimp dest!: tranclD simp: n_def cdt_parent_of_def
                 split: if_split_asm) moreover from n have "p' \<noteq> slot" by (clarsimp dest!: tranclD2 simp: n_def cdt_parent_of_def ) moreover from n have "m \<Turnstile> p \<rightarrow> p'" proof induct case (base x) thus ?case apply (clarsimp simp: cdt_parent_of_def n_def split: if_split_asm) apply (rule trancl_trans) apply (fastforce simp: cdt_parent_of_def)+ done next case (step y z) thus ?case apply (clarsimp simp: cdt_parent_of_def n_def split: if_split_asm) apply (erule trancl_trans) apply (rule trancl_trans) apply (fastforce simp: cdt_parent_of_def) apply (fastforce simp: cdt_parent_of_def) apply (erule trancl_trans) apply (fastforce simp: cdt_parent_of_def) done qed ultimately show "p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'" by simp next assume asm: "p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'" from asm have p: "p \<noteq> slot" .. from asm have p': "p' \<noteq> slot" by simp from asm have m: "m \<Turnstile> p \<rightarrow> p'" by simp hence neq: "p \<noteq> p'" by clarsimp from m have "if p' = slot then
          \<exists>p''. (p, p'') \<in> (cdt_parent_rel m)^* \<and> m \<Turnstile> p'' \<leadsto> p' \<and> (p, p'') \<in> (cdt_parent_rel n)^*
        else
          n \<Turnstile> p \<rightarrow> p'" proof induct case (base y) thus ?case apply (clarsimp simp: cdt_parent_of_def simp del: split_paired_Ex) apply (fastforce simp: cdt_parent_of_def n_def p) done next case (step y z) thus ?case apply (clarsimp simp: cdt_parent_of_def simp del: split_paired_Ex) apply (rule conjI) apply (clarsimp simp del: split_paired_Ex) apply (cases "y = slot", simp) apply fastforce apply (clarsimp simp del: split_paired_Ex) apply (cases "y = slot") apply (simp del: split_paired_Ex) apply (elim exE conjE) apply (drule rtranclD [where R="cdt_parent_rel n"]) apply (erule disjE) apply simp apply (rule r_into_trancl) apply (clarsimp simp: cdt_parent_of_def n_def) apply clarsimp apply (erule trancl_trans) apply (fastforce simp: cdt_parent_of_def n_def) apply simp apply (erule trancl_trans) apply (fastforce simp: cdt_parent_of_def n_def) done qed with p' show "n \<Turnstile> p \<rightarrow> p'" by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<Turnstile> p \<rightarrow> p' = (p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p') proof (state)
goal (2 subgoals):
 1. n \<Turnstile> p \<rightarrow> p' \<Longrightarrow> p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'
 2. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (state)
this:
n \<Turnstile> p \<rightarrow> p'

goal (2 subgoals):
 1. n \<Turnstile> p \<rightarrow> p' \<Longrightarrow> p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'
 2. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (chain)
picking this:
n \<Turnstile> p \<rightarrow> p' proof (prove)
using this:
n \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. p \<noteq> slot proof (state)
this:
p \<noteq> slot

goal (2 subgoals):
 1. n \<Turnstile> p \<rightarrow> p' \<Longrightarrow> p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'
 2. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (state)
this:
p \<noteq> slot

goal (2 subgoals):
 1. n \<Turnstile> p \<rightarrow> p' \<Longrightarrow> p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'
 2. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (chain)
picking this:
n \<Turnstile> p \<rightarrow> p' proof (prove)
using this:
n \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. p' \<noteq> slot proof (state)
this:
p' \<noteq> slot

goal (2 subgoals):
 1. n \<Turnstile> p \<rightarrow> p' \<Longrightarrow> p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'
 2. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (state)
this:
p' \<noteq> slot

goal (2 subgoals):
 1. n \<Turnstile> p \<rightarrow> p' \<Longrightarrow> p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'
 2. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (chain)
picking this:
n \<Turnstile> p \<rightarrow> p' proof (prove)
using this:
n \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. m \<Turnstile> p \<rightarrow> p' proof (state)
goal (2 subgoals):
 1. \<And>y. n \<Turnstile> p \<leadsto> y \<Longrightarrow> m \<Turnstile> p \<rightarrow> y
 2. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z proof (state)
this:
n \<Turnstile> p \<leadsto> x

goal (2 subgoals):
 1. \<And>y. n \<Turnstile> p \<leadsto> y \<Longrightarrow> m \<Turnstile> p \<rightarrow> y
 2. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
using this:
n \<Turnstile> p \<leadsto> x

goal (1 subgoal):
 1. m \<Turnstile> p \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> slot; m x = Some slot; m slot = Some p\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> x
 2. \<lbrakk>x \<noteq> slot; p \<noteq> slot; m x = Some p\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<noteq> slot; m x = Some slot; m slot = Some p\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> ?y28
 2. \<lbrakk>x \<noteq> slot; m x = Some slot; m slot = Some p\<rbrakk> \<Longrightarrow> m \<Turnstile> ?y28 \<rightarrow> x
 3. \<lbrakk>x \<noteq> slot; p \<noteq> slot; m x = Some p\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> x proof (prove)
goal:
No subgoals! proof (state)
this:
m \<Turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z proof (state)
this:
n \<Turnstile> p \<rightarrow> y
n \<Turnstile> y \<leadsto> z
m \<Turnstile> p \<rightarrow> y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
using this:
n \<Turnstile> p \<rightarrow> y
n \<Turnstile> y \<leadsto> z
m \<Turnstile> p \<rightarrow> y

goal (1 subgoal):
 1. m \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<lambda>p. if m p = Some slot then m slot else m p)(slot := None) \<Turnstile> p \<rightarrow> y; m \<Turnstile> p \<rightarrow> y; z \<noteq> slot; m z = Some slot; m slot = Some y\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z
 2. \<lbrakk>(\<lambda>p. if m p = Some slot then m slot else m p)(slot := None) \<Turnstile> p \<rightarrow> y; m \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot; m z = Some y\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<lambda>p. if m p = Some slot then m slot else m p)(slot := None) \<Turnstile> p \<rightarrow> y; z \<noteq> slot; m z = Some slot; m slot = Some y\<rbrakk> \<Longrightarrow> m \<Turnstile> y \<rightarrow> z
 2. \<lbrakk>(\<lambda>p. if m p = Some slot then m slot else m p)(slot := None) \<Turnstile> p \<rightarrow> y; m \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot; m z = Some y\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<lambda>p. if m p = Some slot then m slot else m p)(slot := None) \<Turnstile> p \<rightarrow> y; z \<noteq> slot; m z = Some slot; m slot = Some y\<rbrakk> \<Longrightarrow> m \<Turnstile> y \<rightarrow> ?y31
 2. \<lbrakk>(\<lambda>p. if m p = Some slot then m slot else m p)(slot := None) \<Turnstile> p \<rightarrow> y; z \<noteq> slot; m z = Some slot; m slot = Some y\<rbrakk> \<Longrightarrow> m \<Turnstile> ?y31 \<rightarrow> z
 3. \<lbrakk>(\<lambda>p. if m p = Some slot then m slot else m p)(slot := None) \<Turnstile> p \<rightarrow> y; m \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot; m z = Some y\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<lambda>p. if m p = Some slot then m slot else m p)(slot := None) \<Turnstile> p \<rightarrow> y; z \<noteq> slot; m z = Some slot; m slot = Some y\<rbrakk> \<Longrightarrow> m \<Turnstile> slot \<rightarrow> z
 2. \<lbrakk>(\<lambda>p. if m p = Some slot then m slot else m p)(slot := None) \<Turnstile> p \<rightarrow> y; m \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot; m z = Some y\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>p. if m p = Some slot then m slot else m p)(slot := None) \<Turnstile> p \<rightarrow> y; m \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot; m z = Some y\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>p. if m p = Some slot then m slot else m p)(slot := None) \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot; m z = Some y\<rbrakk> \<Longrightarrow> m \<Turnstile> y \<rightarrow> z proof (prove)
goal:
No subgoals! proof (state)
this:
m \<Turnstile> p \<rightarrow> z

goal:
No subgoals! proof (state)
this:
m \<Turnstile> p \<rightarrow> p'

goal (2 subgoals):
 1. n \<Turnstile> p \<rightarrow> p' \<Longrightarrow> p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'
 2. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (chain)
picking this:
p \<noteq> slot
p' \<noteq> slot
m \<Turnstile> p \<rightarrow> p' proof (prove)
using this:
p \<noteq> slot
p' \<noteq> slot
m \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' proof (state)
this:
p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (state)
goal (1 subgoal):
 1. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (state)
this:
p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (chain)
picking this:
p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' proof (prove)
using this:
p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. p \<noteq> slot proof (state)
this:
p \<noteq> slot

goal (1 subgoal):
 1. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (chain)
picking this:
p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' proof (prove)
using this:
p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. p' \<noteq> slot proof (state)
this:
p' \<noteq> slot

goal (1 subgoal):
 1. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (chain)
picking this:
p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' proof (prove)
using this:
p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. m \<Turnstile> p \<rightarrow> p' proof (state)
this:
m \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (prove)
using this:
m \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. p \<noteq> p' proof (state)
this:
p \<noteq> p'

goal (1 subgoal):
 1. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (chain)
picking this:
m \<Turnstile> p \<rightarrow> p' proof (prove)
using this:
m \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. if p' = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> p' \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> p' proof (state)
goal (2 subgoals):
 1. \<And>y. m \<Turnstile> p \<leadsto> y \<Longrightarrow> if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y
 2. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> if z = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> z \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> z proof (state)
this:
m \<Turnstile> p \<leadsto> y

goal (2 subgoals):
 1. \<And>y. m \<Turnstile> p \<leadsto> y \<Longrightarrow> if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y
 2. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> if z = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> z \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> z proof (prove)
using this:
m \<Turnstile> p \<leadsto> y

goal (1 subgoal):
 1. if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y proof (prove)
goal (1 subgoal):
 1. m y = Some p \<Longrightarrow> (y = slot \<longrightarrow> (\<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m slot = Some p'' \<and> n \<Turnstile> p \<rightarrow>* p'')) \<and> (y \<noteq> slot \<longrightarrow> n \<Turnstile> p \<rightarrow> y) proof (prove)
goal:
No subgoals! proof (state)
this:
if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> if z = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> z \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> z proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> if z = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> z \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> z proof (state)
this:
m \<Turnstile> p \<rightarrow> y
m \<Turnstile> y \<leadsto> z
if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> if z = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> z \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> z proof (prove)
using this:
m \<Turnstile> p \<rightarrow> y
m \<Turnstile> y \<leadsto> z
if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y

goal (1 subgoal):
 1. if z = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> z \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> (z = slot \<longrightarrow> (\<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m slot = Some p'' \<and> n \<Turnstile> p \<rightarrow>* p'')) \<and> (z \<noteq> slot \<longrightarrow> n \<Turnstile> p \<rightarrow> z) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z = slot \<longrightarrow> (\<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m slot = Some p'' \<and> n \<Turnstile> p \<rightarrow>* p'')
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m slot = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z = slot\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow>* y \<and> n \<Turnstile> p \<rightarrow>* y
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m slot = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z = slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow>* y \<and> n \<Turnstile> p \<rightarrow>* y
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y = slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> slot; m z = Some slot; \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> slot \<and> n \<Turnstile> p \<rightarrow>* p''; z \<noteq> slot; y = slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<And>p''. \<lbrakk>m \<Turnstile> p \<rightarrow> slot; m z = Some slot; z \<noteq> slot; y = slot; m \<Turnstile> p \<rightarrow>* p''; m \<Turnstile> p'' \<leadsto> slot; n \<Turnstile> p \<rightarrow>* p''\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<And>p''. \<lbrakk>m \<Turnstile> p \<rightarrow> slot; m z = Some slot; z \<noteq> slot; y = slot; m \<Turnstile> p \<rightarrow>* p''; m \<Turnstile> p'' \<leadsto> slot; p = p'' \<or> p \<noteq> p'' \<and> n \<Turnstile> p \<rightarrow> p''\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (3 subgoals):
 1. \<And>p''. \<lbrakk>m \<Turnstile> p \<rightarrow> slot; m z = Some slot; z \<noteq> slot; y = slot; m \<Turnstile> p \<rightarrow>* p''; m \<Turnstile> p'' \<leadsto> slot; p = p''\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z
 2. \<And>p''. \<lbrakk>m \<Turnstile> p \<rightarrow> slot; m z = Some slot; z \<noteq> slot; y = slot; m \<Turnstile> p \<rightarrow>* p''; m \<Turnstile> p'' \<leadsto> slot; p \<noteq> p'' \<and> n \<Turnstile> p \<rightarrow> p''\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z
 3. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (3 subgoals):
 1. \<And>p''. \<lbrakk>m \<Turnstile> p'' \<rightarrow> slot; m z = Some slot; z \<noteq> slot; y = slot; m \<Turnstile> p'' \<leadsto> slot; p = p''\<rbrakk> \<Longrightarrow> n \<Turnstile> p'' \<rightarrow> z
 2. \<And>p''. \<lbrakk>m \<Turnstile> p \<rightarrow> slot; m z = Some slot; z \<noteq> slot; y = slot; m \<Turnstile> p \<rightarrow>* p''; m \<Turnstile> p'' \<leadsto> slot; p \<noteq> p'' \<and> n \<Turnstile> p \<rightarrow> p''\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z
 3. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (3 subgoals):
 1. \<And>p''. \<lbrakk>m \<Turnstile> p'' \<rightarrow> slot; m z = Some slot; z \<noteq> slot; y = slot; m \<Turnstile> p'' \<leadsto> slot; p = p''\<rbrakk> \<Longrightarrow> n \<Turnstile> p'' \<leadsto> z
 2. \<And>p''. \<lbrakk>m \<Turnstile> p \<rightarrow> slot; m z = Some slot; z \<noteq> slot; y = slot; m \<Turnstile> p \<rightarrow>* p''; m \<Turnstile> p'' \<leadsto> slot; p \<noteq> p'' \<and> n \<Turnstile> p \<rightarrow> p''\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z
 3. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<And>p''. \<lbrakk>m \<Turnstile> p \<rightarrow> slot; m z = Some slot; z \<noteq> slot; y = slot; m \<Turnstile> p \<rightarrow>* p''; m \<Turnstile> p'' \<leadsto> slot; p \<noteq> p'' \<and> n \<Turnstile> p \<rightarrow> p''\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>m \<Turnstile> p \<rightarrow> slot; m z = Some slot; z \<noteq> slot; y = slot; m \<Turnstile> p \<rightarrow>* (a, b); m \<Turnstile> (a, b) \<leadsto> slot; p \<noteq> (a, b); n \<Turnstile> p \<rightarrow> (a, b)\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>m \<Turnstile> p \<rightarrow> slot; m z = Some slot; z \<noteq> slot; y = slot; m \<Turnstile> p \<rightarrow>* (a, b); m \<Turnstile> (a, b) \<leadsto> slot; p \<noteq> (a, b)\<rbrakk> \<Longrightarrow> n \<Turnstile> (a, b) \<rightarrow> z
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; if y = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> y \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; n \<Turnstile> p \<rightarrow> y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m z = Some y; z \<noteq> slot; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<Turnstile> y \<rightarrow> z proof (prove)
goal:
No subgoals! proof (state)
this:
if z = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> z \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> z

goal:
No subgoals! proof (state)
this:
if p' = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> p' \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (chain)
picking this:
p' \<noteq> slot
if p' = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> p' \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> p' proof (prove)
using this:
p' \<noteq> slot
if p' = slot then \<exists>p''. m \<Turnstile> p \<rightarrow>* p'' \<and> m \<Turnstile> p'' \<leadsto> p' \<and> n \<Turnstile> p \<rightarrow>* p'' else n \<Turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. n \<Turnstile> p \<rightarrow> p' proof (state)
this:
n \<Turnstile> p \<rightarrow> p'

goal:
No subgoals!