theory ListLibLemmas

lemma after_in_list_list_set:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "distinct list \<Longrightarrow>
         set (after_in_list_list list x)
         = {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}" apply(intro equalityI) 
  (* \<subseteq> *)
    apply(induct list arbitrary:x) apply(simp) apply(atomize) apply(simp) apply(rule conjI, rule impI, rule subsetI) apply(rule_tac a = xa in CollectI) apply(rule trancl_Collect_rev) apply(rule after_in_list_trancl_prepend) apply(simp) apply(simp) apply(clarify) apply(drule_tac x=x in spec) apply(drule_tac B="{a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}" in set_rev_mp) apply(simp) apply(drule CollectD) apply(simp add:prepend_after_in_list_distinct) 
 (* \<supseteq> *)
   apply(clarsimp) apply(drule trancl_Collect_rev) apply(erule trancl_induct) 
    (* base *)
    apply(simp) apply(induct list arbitrary:x) apply(simp) apply(case_tac "a=x") apply(frule_tac src=x in distinct_after_in_list_not_self) apply(simp) apply(drule after_in_list_in_list) apply(simp)+ apply(drule_tac list=list in after_in_list_append_not_hd) apply(simp) 
   (* inductive *)
   apply(simp) apply(drule trancl_Collect_rev) apply(induct list arbitrary: x) apply(simp) apply(case_tac "a\<noteq>x") 
  (* a\<noteq>x *)
    apply(atomize, drule_tac x=y in spec, drule_tac x=z in spec, drule_tac x=x in spec) apply(simp add:prepend_after_in_list_distinct) apply(case_tac "a=y") apply(simp add:after_in_list_list_in_list) apply(simp add:after_in_list_append_not_hd) 
   (* a=x *)
   apply(frule after_in_list_in_cons, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct list \<Longrightarrow> set (after_in_list_list list x) = {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} proof (prove)
goal (2 subgoals):
 1. distinct list \<Longrightarrow> set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}
 2. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. distinct list \<Longrightarrow> set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}
 2. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (3 subgoals):
 1. \<And>x. distinct [] \<Longrightarrow> set (after_in_list_list [] x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list [] p = Some next}\<^sup>+}
 2. \<And>a list x. \<lbrakk>\<And>x. distinct list \<Longrightarrow> set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; distinct (a # list)\<rbrakk> \<Longrightarrow> set (after_in_list_list (a # list) x) \<subseteq> {aa. (aa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+}
 3. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>a list x. \<lbrakk>\<And>x. distinct list \<Longrightarrow> set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; distinct (a # list)\<rbrakk> \<Longrightarrow> set (after_in_list_list (a # list) x) \<subseteq> {aa. (aa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+}
 2. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>a list x. \<lbrakk>\<forall>x. distinct list \<longrightarrow> set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; distinct (a # list)\<rbrakk> \<Longrightarrow> set (after_in_list_list (a # list) x) \<subseteq> {aa. (aa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+}
 2. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>a list x. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list\<rbrakk> \<Longrightarrow> (x = a \<longrightarrow> set list \<subseteq> {aa. (aa, a) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+}) \<and> (x \<noteq> a \<longrightarrow> set (after_in_list_list list x) \<subseteq> {aa. (aa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+})
 2. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (3 subgoals):
 1. \<And>a list x xa. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list; x = a; xa \<in> set list\<rbrakk> \<Longrightarrow> xa \<in> {aa. (aa, a) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+}
 2. \<And>a list x. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> set (after_in_list_list list x) \<subseteq> {aa. (aa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+}
 3. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (3 subgoals):
 1. \<And>a list x xa. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list; x = a; xa \<in> set list\<rbrakk> \<Longrightarrow> (xa, a) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>a list x. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> set (after_in_list_list list x) \<subseteq> {aa. (aa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+}
 3. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (3 subgoals):
 1. \<And>a list x xa. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list; x = a; xa \<in> set list\<rbrakk> \<Longrightarrow> (a, xa) \<in> {(next, p). after_in_list (a # list) next = Some p}\<^sup>+
 2. \<And>a list x. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> set (after_in_list_list list x) \<subseteq> {aa. (aa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+}
 3. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (4 subgoals):
 1. \<And>a list x xa. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list; x = a; xa \<in> set list\<rbrakk> \<Longrightarrow> distinct (a # list)
 2. \<And>a list x xa. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list; x = a; xa \<in> set list\<rbrakk> \<Longrightarrow> xa \<in> set list
 3. \<And>a list x. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> set (after_in_list_list list x) \<subseteq> {aa. (aa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+}
 4. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (3 subgoals):
 1. \<And>a list x xa. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list; x = a; xa \<in> set list\<rbrakk> \<Longrightarrow> xa \<in> set list
 2. \<And>a list x. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> set (after_in_list_list list x) \<subseteq> {aa. (aa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+}
 3. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>a list x. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list \<and> distinct list\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> set (after_in_list_list list x) \<subseteq> {aa. (aa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+}
 2. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>a list x xa. \<lbrakk>\<forall>x. set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; a \<notin> set list; distinct list; x \<noteq> a; xa \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> (xa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>a list x xa. \<lbrakk>a \<notin> set list; distinct list; x \<noteq> a; xa \<in> set (after_in_list_list list x); set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> (xa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (3 subgoals):
 1. \<And>a list x xa. \<lbrakk>a \<notin> set list; distinct list; x \<noteq> a; set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}
 2. \<And>a list x xa. \<lbrakk>a \<notin> set list; distinct list; x \<noteq> a; set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; xa \<in> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> (xa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 3. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>a list x xa. \<lbrakk>a \<notin> set list; distinct list; x \<noteq> a; set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; xa \<in> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> (xa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>a list x xa. \<lbrakk>a \<notin> set list; distinct list; x \<noteq> a; set (after_in_list_list list x) \<subseteq> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}; (xa, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (xa, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (1 subgoal):
 1. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (1 subgoal):
 1. distinct list \<Longrightarrow> {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+} \<subseteq> set (after_in_list_list list x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>distinct list; (xa, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> xa \<in> set (after_in_list_list list x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>distinct list; (x, xa) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> xa \<in> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x)
 2. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x)
 2. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>distinct list; after_in_list list x = Some y\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x)
 2. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (3 subgoals):
 1. \<And>y x. \<lbrakk>distinct []; after_in_list [] x = Some y\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list [] x)
 2. \<And>a list y x. \<lbrakk>\<And>y x. \<lbrakk>distinct list; after_in_list list x = Some y\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) x = Some y\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list (a # list) x)
 3. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>a list y x. \<lbrakk>\<And>y x. \<lbrakk>distinct list; after_in_list list x = Some y\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) x = Some y\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list (a # list) x)
 2. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (3 subgoals):
 1. \<And>a list y x. \<lbrakk>\<And>y x. \<lbrakk>distinct list; after_in_list list x = Some y\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) x = Some y; a = x\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list (a # list) x)
 2. \<And>a list y x. \<lbrakk>\<And>y x. \<lbrakk>distinct list; after_in_list list x = Some y\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) x = Some y; a \<noteq> x\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list (a # list) x)
 3. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (3 subgoals):
 1. \<And>a list y x. \<lbrakk>\<And>y x. \<lbrakk>distinct list; after_in_list list x = Some y\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) x = Some y; a = x; after_in_list (a # list) x \<noteq> Some x\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list (a # list) x)
 2. \<And>a list y x. \<lbrakk>\<And>y x. \<lbrakk>distinct list; after_in_list list x = Some y\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) x = Some y; a \<noteq> x\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list (a # list) x)
 3. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (3 subgoals):
 1. \<And>a list y x. \<lbrakk>\<And>y x. after_in_list list x = Some y \<Longrightarrow> y \<in> set (after_in_list_list list x); x \<notin> set list \<and> distinct list; after_in_list (x # list) x = Some y; a = x; y \<noteq> x\<rbrakk> \<Longrightarrow> y \<in> set list
 2. \<And>a list y x. \<lbrakk>\<And>y x. \<lbrakk>distinct list; after_in_list list x = Some y\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) x = Some y; a \<noteq> x\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list (a # list) x)
 3. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (3 subgoals):
 1. \<And>a list y x. \<lbrakk>\<And>y x. after_in_list list x = Some y \<Longrightarrow> y \<in> set (after_in_list_list list x); x \<notin> set list \<and> distinct list; a = x; y \<noteq> x; y \<in> set (x # list)\<rbrakk> \<Longrightarrow> y \<in> set list
 2. \<And>a list y x. \<lbrakk>\<And>y x. \<lbrakk>distinct list; after_in_list list x = Some y\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) x = Some y; a \<noteq> x\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list (a # list) x)
 3. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>a list y x. \<lbrakk>\<And>y x. after_in_list list x = Some y \<Longrightarrow> y \<in> set (after_in_list_list list x); a \<notin> set list \<and> distinct list; after_in_list (a # list) x = Some y; a \<noteq> x\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x)
 2. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>a list y x. \<lbrakk>\<And>y x. after_in_list list x = Some y \<Longrightarrow> y \<in> set (after_in_list_list list x); a \<notin> set list \<and> distinct list; after_in_list (a # list) x = Some y; after_in_list (a # list) x = after_in_list list x\<rbrakk> \<Longrightarrow> y \<in> set (after_in_list_list list x)
 2. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (1 subgoal):
 1. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (1 subgoal):
 1. \<And>xa y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list next = Some p}; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>distinct list; (x, y) \<in> {(next, p). after_in_list list next = Some p}\<^sup>+; after_in_list list y = Some z; y \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x) proof (prove)
goal (2 subgoals):
 1. \<And>y z x. \<lbrakk>distinct []; after_in_list [] y = Some z; y \<in> set (after_in_list_list [] x); (y, x) \<in> {(next, p). after_in_list [] p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list [] x)
 2. \<And>a list y z x. \<lbrakk>\<And>y z x. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x) proof (prove)
goal (1 subgoal):
 1. \<And>a list y z x. \<lbrakk>\<And>y z x. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x) proof (prove)
goal (2 subgoals):
 1. \<And>a list y z x. \<lbrakk>\<And>y z x. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; a \<noteq> x\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x)
 2. \<And>a list y z x. \<lbrakk>\<And>y z x. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; \<not> a \<noteq> x\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x) proof (prove)
goal (2 subgoals):
 1. \<And>a list y z x. \<lbrakk>\<And>y z x. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; a \<noteq> x\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x)
 2. \<And>a list y z x. \<lbrakk>\<And>y z x. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; \<not> a \<noteq> x\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x) proof (prove)
goal (2 subgoals):
 1. \<And>a list y z x. \<lbrakk>distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; a \<noteq> x; distinct list \<longrightarrow> after_in_list list y = Some z \<longrightarrow> y \<in> set (after_in_list_list list x) \<longrightarrow> (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+ \<longrightarrow> z \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x)
 2. \<And>a list y z x. \<lbrakk>\<And>y z x. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; \<not> a \<noteq> x\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x) proof (prove)
goal (2 subgoals):
 1. \<And>a list y z x. \<lbrakk>a \<notin> set list \<and> distinct list; after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; a \<noteq> x; after_in_list list y = Some z \<longrightarrow> z \<in> set (after_in_list_list list x)\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x)
 2. \<And>a list y z x. \<lbrakk>\<And>y z x. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; \<not> a \<noteq> x\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x) proof (prove)
goal (3 subgoals):
 1. \<And>a list y z x. \<lbrakk>a \<notin> set list \<and> distinct list; after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; a \<noteq> x; after_in_list list y = Some z \<longrightarrow> z \<in> set (after_in_list_list list x); a = y\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x)
 2. \<And>a list y z x. \<lbrakk>a \<notin> set list \<and> distinct list; after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; a \<noteq> x; after_in_list list y = Some z \<longrightarrow> z \<in> set (after_in_list_list list x); a \<noteq> y\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x)
 3. \<And>a list y z x. \<lbrakk>\<And>y z x. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; \<not> a \<noteq> x\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x) proof (prove)
goal (2 subgoals):
 1. \<And>a list y z x. \<lbrakk>a \<notin> set list \<and> distinct list; after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; a \<noteq> x; after_in_list list y = Some z \<longrightarrow> z \<in> set (after_in_list_list list x); a \<noteq> y\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x)
 2. \<And>a list y z x. \<lbrakk>\<And>y z x. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; \<not> a \<noteq> x\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x) proof (prove)
goal (1 subgoal):
 1. \<And>a list y z x. \<lbrakk>\<And>y z x. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; \<not> a \<noteq> x\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x) proof (prove)
goal (1 subgoal):
 1. \<And>a list y z x. \<lbrakk>\<And>y z x. \<lbrakk>distinct list; after_in_list list y = Some z; y \<in> set (after_in_list_list list x); (y, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list list x); distinct (a # list); after_in_list (a # list) y = Some z; y \<in> set (after_in_list_list (a # list) x); (y, x) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; \<not> a \<noteq> x\<rbrakk> \<Longrightarrow> z \<in> set (after_in_list_list (a # list) x) proof (prove)
goal:
No subgoals!