theory CSpace_AI

lemma descendants_of_insert_child:
  assumes d: "descendants_of dest m = {}"
  assumes s: "src \<noteq> dest"
  shows
  "descendants_of x (m (dest \<mapsto> src)) =
   (if src \<in> descendants_of x m \<or> x = src
    then descendants_of x m \<union> {dest} else descendants_of x m - {dest})" using assms apply (simp add: descendants_of_def cdt_parent_defs del: fun_upd_apply) apply (rule conjI) apply clarify apply (rule set_eqI) apply (simp del: fun_upd_apply) apply (rule iffI) apply (simp only: disj_imp) apply (erule_tac b="xa" in trancl_induct) apply fastforce apply clarsimp apply (erule impE) apply fastforce apply (rule trancl_into_trancl) prefer 2 apply simp apply assumption apply (erule disjE) apply (drule descendants_insert_evil_trancl_induct [OF _ d]) apply (simp add: descendants_of_def cdt_parent_defs) apply (simp add: descendants_of_def cdt_parent_defs del: fun_upd_apply) apply (erule trancl_into_trancl) apply fastforce apply (case_tac "xa = dest") apply (simp del: fun_upd_apply) apply (drule descendants_insert_evil_trancl_induct [OF _ d]) apply (simp add: descendants_of_def cdt_parent_defs) apply (simp add: descendants_of_def cdt_parent_defs del: fun_upd_apply) apply (erule trancl_into_trancl) apply fastforce apply (rule_tac P="xa \<noteq> dest" in mp) prefer 2 apply assumption apply (erule_tac b=xa in trancl_induct) apply fastforce apply (clarsimp simp del: fun_upd_apply) apply (erule impE) apply fastforce apply (fastforce elim: trancl_into_trancl) apply (rule conjI) apply (clarsimp simp del: fun_upd_apply) apply (rule set_eqI) apply (simp del: fun_upd_apply) apply (rule iffI) apply (simp only: disj_imp) apply (erule_tac b="xa" in trancl_induct) apply fastforce apply clarsimp apply (erule impE) apply fastforce apply (rule trancl_into_trancl) prefer 2 apply simp apply assumption apply (erule disjE) apply fastforce apply (case_tac "xa = dest") apply fastforce apply (rule_tac P="xa \<noteq> dest" in mp) prefer 2 apply assumption apply (erule_tac b=xa in trancl_induct) apply fastforce apply (clarsimp simp del: fun_upd_apply) apply (erule impE) apply fastforce apply (fastforce elim: trancl_into_trancl) apply clarify apply (rule set_eqI) apply (simp del: fun_upd_apply) apply (rule iffI) apply (erule trancl_induct) apply (fastforce split: if_split_asm) apply (clarsimp split: if_split_asm) apply (fastforce elim: trancl_into_trancl) apply (elim conjE) apply (rule_tac P="xa \<noteq> dest" in mp) prefer 2 apply assumption apply (erule_tac b=xa in trancl_induct) apply fastforce apply (clarsimp simp del: fun_upd_apply) apply (erule impE) apply fastforce apply (erule trancl_into_trancl) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of x (m(dest \<mapsto> src)) = (if src \<in> descendants_of x m \<or> x = src then descendants_of x m \<union> {dest} else descendants_of x m - {dest}) proof (prove)
using this:
descendants_of dest m = {}
src \<noteq> dest

goal (1 subgoal):
 1. descendants_of x (m(dest \<mapsto> src)) = (if src \<in> descendants_of x m \<or> x = src then descendants_of x m \<union> {dest} else descendants_of x m - {dest}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> ((x, src) \<in> {(p, c). m c = Some p}\<^sup>+ \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<in> {(p, c). m c = Some p}\<^sup>+ \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+}
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+}
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (xa \<in> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+}) = (xa \<in> insert dest {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+})
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> ((x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+) = (xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+)
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> xa \<noteq> dest \<longrightarrow> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (4 subgoals):
 1. \<And>xa y. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, y) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<rbrakk> \<Longrightarrow> y \<noteq> dest \<longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+
 2. \<And>xa y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, y) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+; (y, z) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}; y \<noteq> dest \<longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+
 3. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 4. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, y) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+; (y, z) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}; y \<noteq> dest \<longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (a, b) \<noteq> dest \<longrightarrow> (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (aa, ba) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest\<rbrakk> \<Longrightarrow> (a, b) \<noteq> dest
 2. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 4. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, ?b49 a b aa ba) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (?b49 a b aa ba, aa, ba) \<in> {(p, c). m c = Some p}
 3. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 4. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (?b49 a b aa ba, aa, ba) \<in> {(p, c). m c = Some p}
 2. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, ?b49 a b aa ba) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 4. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest \<or> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest\<rbrakk> \<Longrightarrow> src \<in> descendants_of (?x56 xa) m
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest; src \<in> descendants_of (?x56 xa) (m(dest \<mapsto> src))\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 4. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest; src \<in> descendants_of x (m(dest \<mapsto> src))\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest; (x, src) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, dest) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest\<rbrakk> \<Longrightarrow> (src, dest) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, dest) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest\<rbrakk> \<Longrightarrow> (x, dest) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, dest) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest\<rbrakk> \<Longrightarrow> src \<in> descendants_of (?x68 xa) m
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, dest) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest; src \<in> descendants_of (?x68 xa) (m(dest \<mapsto> src))\<rbrakk> \<Longrightarrow> (x, dest) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 4. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, dest) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest; src \<in> descendants_of x (m(dest \<mapsto> src))\<rbrakk> \<Longrightarrow> (x, dest) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, dest) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest; (x, src) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, dest) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, dest) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest\<rbrakk> \<Longrightarrow> (src, dest) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest \<longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest \<longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest \<longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>xa y. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest; (x, y) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> y \<noteq> dest \<longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; y \<noteq> dest \<longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<And>xa y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; y \<noteq> dest \<longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<noteq> dest; (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (aa, ba) \<noteq> dest \<longrightarrow> (x, aa, ba) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+; (ab, bb) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, ab, bb) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<noteq> dest; (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (ab, bb) \<noteq> dest\<rbrakk> \<Longrightarrow> (aa, ba) \<noteq> dest
 2. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<noteq> dest; (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (ab, bb) \<noteq> dest; (x, aa, ba) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, ab, bb) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<noteq> dest; (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (ab, bb) \<noteq> dest; (x, aa, ba) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, ab, bb) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}) \<and> ((x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> x = src \<longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src\<rbrakk> \<Longrightarrow> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+}
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src\<rbrakk> \<Longrightarrow> (xa \<in> {q. (src, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+}) = (xa \<in> insert dest {q. (src, q) \<in> {(p, c). m c = Some p}\<^sup>+})
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src\<rbrakk> \<Longrightarrow> ((src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+) = (xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+)
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> xa \<noteq> dest \<longrightarrow> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (4 subgoals):
 1. \<And>xa y. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, y) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<rbrakk> \<Longrightarrow> y \<noteq> dest \<longrightarrow> (src, y) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+
 2. \<And>xa y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, y) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+; (y, z) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}; y \<noteq> dest \<longrightarrow> (src, y) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (src, z) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+
 3. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 4. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (3 subgoals):
 1. \<And>xa y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, y) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+; (y, z) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}; y \<noteq> dest \<longrightarrow> (src, y) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (src, z) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (a, b) \<noteq> dest \<longrightarrow> (src, a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (aa, ba) \<noteq> dest\<rbrakk> \<Longrightarrow> (src, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest\<rbrakk> \<Longrightarrow> (a, b) \<noteq> dest
 2. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (src, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 4. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (src, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (src, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, ?b190 a b aa ba) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (src, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (?b190 a b aa ba, aa, ba) \<in> {(p, c). m c = Some p}
 3. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 4. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (src, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (?b190 a b aa ba, aa, ba) \<in> {(p, c). m c = Some p}
 2. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (src, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, ?b190 a b aa ba) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 4. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, a, b) \<in> {(p, c). (if c = dest then Some src else m c) = Some p}\<^sup>+; m (aa, ba) = Some (a, b); (aa, ba) \<noteq> dest; (src, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, a, b) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa = dest \<or> (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa = dest\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa = dest\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest \<longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest \<longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (src, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest \<longrightarrow> (src, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (3 subgoals):
 1. \<And>xa y. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa \<noteq> dest; (src, y) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> y \<noteq> dest \<longrightarrow> (src, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa \<noteq> dest; (src, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; y \<noteq> dest \<longrightarrow> (src, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (src, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (2 subgoals):
 1. \<And>xa y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; xa \<noteq> dest; (src, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; y \<noteq> dest \<longrightarrow> (src, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (src, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (a, b) \<noteq> dest; (src, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (aa, ba) \<noteq> dest \<longrightarrow> (src, aa, ba) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+; (ab, bb) \<noteq> dest\<rbrakk> \<Longrightarrow> (src, ab, bb) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (a, b) \<noteq> dest; (src, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (ab, bb) \<noteq> dest\<rbrakk> \<Longrightarrow> (aa, ba) \<noteq> dest
 2. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (a, b) \<noteq> dest; (src, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (ab, bb) \<noteq> dest; (src, aa, ba) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, ab, bb) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 3. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; x = src; (a, b) \<noteq> dest; (src, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (ab, bb) \<noteq> dest; (src, aa, ba) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (src, ab, bb) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest\<rbrakk> \<Longrightarrow> (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+ \<and> x \<noteq> src \<longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src\<rbrakk> \<Longrightarrow> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src\<rbrakk> \<Longrightarrow> (xa \<in> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+}) = (xa \<in> {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src\<rbrakk> \<Longrightarrow> ((x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+) = ((x, xa) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> xa \<noteq> dest) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> xa \<noteq> dest
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>xa y. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, y) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<rbrakk> \<Longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+ \<and> y \<noteq> dest
 2. \<And>xa y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, y) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+; (y, z) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}; (x, y) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+ \<and> y \<noteq> dest\<rbrakk> \<Longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+ \<and> z \<noteq> dest
 3. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>xa y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, y) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+; (y, z) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}; (x, y) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+ \<and> y \<noteq> dest\<rbrakk> \<Longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+ \<and> z \<noteq> dest
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<noteq> dest; (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> src = p) \<and> (c = dest \<or> m c = Some p)}\<^sup>+; (aa, ba) \<noteq> dest; m (aa, ba) = Some (a, b)\<rbrakk> \<Longrightarrow> (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest \<longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest
 2. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest \<longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (x, xa) \<in> {(p, c). m c = Some p}\<^sup>+; xa \<noteq> dest\<rbrakk> \<Longrightarrow> xa \<noteq> dest \<longrightarrow> (x, xa) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; xa \<noteq> dest; (x, y) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> y \<noteq> dest \<longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+
 2. \<And>xa y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; xa \<noteq> dest; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; y \<noteq> dest \<longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>xa y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; xa \<noteq> dest; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; y \<noteq> dest \<longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (a, b) \<noteq> dest; (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (aa, ba) \<noteq> dest \<longrightarrow> (x, aa, ba) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+; (ab, bb) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, ab, bb) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (a, b) \<noteq> dest; (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (ab, bb) \<noteq> dest\<rbrakk> \<Longrightarrow> (aa, ba) \<noteq> dest
 2. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (a, b) \<noteq> dest; (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (ab, bb) \<noteq> dest; (x, aa, ba) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, ab, bb) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (a, b) \<noteq> dest; (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (ab, bb) \<noteq> dest; (x, aa, ba) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, ab, bb) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src \<noteq> dest; (x, src) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> src; (a, b) \<noteq> dest; (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); (ab, bb) \<noteq> dest\<rbrakk> \<Longrightarrow> ((aa, ba), ab, bb) \<in> {(p, c). (m(dest \<mapsto> src)) c = Some p} proof (prove)
goal:
No subgoals!