theory ListLibLemmas

lemma prepend_after_in_list_distinct : "distinct (a # list) \<Longrightarrow> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ =
       {(next, p). after_in_list (list) p = Some next}\<^sup>+ \<union>
       set list \<times> {a} " apply (rule equalityI) 
   (* \<subseteq> direction *)
    apply (rule subsetI, case_tac x) apply (simp) apply (erule trancl_induct) 
     (* base case *)
     apply (drule CollectD, simp) apply (case_tac list, simp) apply (simp split:if_split_asm) apply (rule r_into_trancl) apply (rule CollectI, simp) 
    (* Inductive case *)
    apply (drule CollectD, simp) apply (erule disjE) apply (case_tac "a \<noteq> z") apply (rule disjI1) apply (rule_tac b =y in trancl_into_trancl) apply (simp, case_tac list, simp, simp) apply (simp) apply (rule disjI2) apply (erule conjE) apply (frule_tac x = aa and y = y in distinct_after_in_list_in_list_trancl) apply (simp) apply (simp) apply (subgoal_tac "after_in_list (a # list) z \<noteq> Some a", simp) apply (rule_tac hd_not_after_in_list, simp, simp) 
(* \<supseteq> direction *)
   apply (rule subsetI) apply (case_tac x) apply (simp) apply (erule disjE) 
    (* transitive case *)
    apply (erule tranclE2) apply (drule CollectD, simp) apply (subgoal_tac "b \<noteq> a") apply (rule r_into_trancl) apply (rule CollectI, simp) apply (case_tac list, simp, simp) apply (frule after_in_list_in_list') apply (erule conjE) apply (blast) apply (rule_tac y = c in trancl_trans) apply (subgoal_tac "c \<noteq> a") apply (case_tac list, simp, simp) apply (case_tac "aaa = aa") apply (rule r_into_trancl) apply (rule CollectI, simp) apply (rule r_into_trancl) apply (rule CollectI, simp) apply (erule CollectE, simp) apply (frule after_in_list_in_list') apply (erule conjE, blast) apply (erule trancl_induct) apply (simp) apply (rule r_into_trancl, simp) apply (subgoal_tac "y \<noteq> a") apply (case_tac list, simp, simp) apply (rotate_tac 3) apply (frule after_in_list_in_list') apply (erule conjE, blast) apply (rule_tac b = y in trancl_into_trancl, simp) apply (rule CollectI, simp) apply (subgoal_tac "a \<noteq> z") apply (case_tac list, simp, simp) apply (rotate_tac 3) apply (frule after_in_list_in_list') apply (blast) 
(* not so transitive case *)
   apply (subgoal_tac "distinct (a # list)") apply (frule_tac x = aa in after_in_list_trancl_prepend, simp, simp) apply (rule trancl_Collect_rev, simp) apply (simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ = {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} proof (prove)
goal (2 subgoals):
 1. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ \<subseteq> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a}
 2. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ \<subseteq> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a}
 2. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b. \<lbrakk>distinct (a # list); x \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; x = (aa, b)\<rbrakk> \<Longrightarrow> x \<in> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a}
 2. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; x = (aa, b)\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> b = a
 2. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b y. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<rbrakk> \<Longrightarrow> (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list (a # list) p = Some next}; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b y. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<rbrakk> \<Longrightarrow> (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list (a # list) p = Some next}; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b y. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list (a # list) y = Some aa\<rbrakk> \<Longrightarrow> (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list (a # list) p = Some next}; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b y aaa lista. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list (a # list) y = Some aa; list = aaa # lista\<rbrakk> \<Longrightarrow> (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list (a # list) p = Some next}; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b y aaa lista. \<lbrakk>list = aaa # lista; x = (aa, b); y \<noteq> a; a \<noteq> aaa; a \<notin> set lista; aaa \<notin> set lista; distinct lista; after_in_list (aaa # lista) y = Some aa\<rbrakk> \<Longrightarrow> (aa, y) \<in> {(next, p). after_in_list (aaa # lista) p = Some next}\<^sup>+
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list (a # list) p = Some next}; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b y aaa lista. \<lbrakk>list = aaa # lista; x = (aa, b); y \<noteq> a; a \<noteq> aaa; a \<notin> set lista; aaa \<notin> set lista; distinct lista; after_in_list (aaa # lista) y = Some aa\<rbrakk> \<Longrightarrow> (aa, y) \<in> {(next, p). after_in_list (aaa # lista) p = Some next}
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list (a # list) p = Some next}; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list (a # list) p = Some next}; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 2. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list (a # list) p = Some next}; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 2. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> y = a; after_in_list (a # list) z = Some y\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 2. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (4 subgoals):
 1. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; a \<noteq> z\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; \<not> a \<noteq> z\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 4. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (4 subgoals):
 1. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; a \<noteq> z\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; \<not> a \<noteq> z\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 4. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (5 subgoals):
 1. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; a \<noteq> z\<rbrakk> \<Longrightarrow> (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; a \<noteq> z\<rbrakk> \<Longrightarrow> (y, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}
 3. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; \<not> a \<noteq> z\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 4. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 5. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; \<not> a \<noteq> z\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b y z. \<lbrakk>z \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (z # list) p = Some next}\<^sup>+; after_in_list (z # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; a = z\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b y z. \<lbrakk>z \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (z # list) p = Some next}\<^sup>+; after_in_list (z # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; a = z\<rbrakk> \<Longrightarrow> aa \<in> set list
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b y z. \<lbrakk>x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (z # list) p = Some next}\<^sup>+; after_in_list (z # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; a = z; z \<notin> set list; distinct list\<rbrakk> \<Longrightarrow> aa \<in> set list
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (4 subgoals):
 1. \<And>x aa b y z. \<lbrakk>x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (z # list) p = Some next}\<^sup>+; after_in_list (z # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; a = z; z \<notin> set list; distinct list\<rbrakk> \<Longrightarrow> (aa, y) \<in> {(p, q). after_in_list list q = Some p}\<^sup>+
 2. \<And>x aa b y z. \<lbrakk>x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (z # list) p = Some next}\<^sup>+; after_in_list (z # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; a = z; z \<notin> set list; distinct list; aa \<in> set list\<rbrakk> \<Longrightarrow> aa \<in> set list
 3. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 4. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b y z. \<lbrakk>x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (z # list) p = Some next}\<^sup>+; after_in_list (z # list) z = Some y; (aa, y) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+; a = z; z \<notin> set list; distinct list; aa \<in> set list\<rbrakk> \<Longrightarrow> aa \<in> set list
 2. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 3. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> (aa, z) \<in> {a. case a of (next, p) \<Rightarrow> after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> z = a
 2. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, y) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+; after_in_list (a # list) z = Some y; aa \<in> set list \<and> y = a\<rbrakk> \<Longrightarrow> after_in_list (a # list) z \<noteq> Some a
 2. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. distinct (a # list) \<Longrightarrow> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a} \<subseteq> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>distinct (a # list); x \<in> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a}\<rbrakk> \<Longrightarrow> x \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>x aa b. \<lbrakk>distinct (a # list); x \<in> {(next, p). after_in_list list p = Some next}\<^sup>+ \<union> set list \<times> {a}; x = (aa, b)\<rbrakk> \<Longrightarrow> x \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; (aa, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+ \<or> aa \<in> set list \<and> b = a; x = (aa, b)\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, b) \<in> {(next, p). after_in_list list p = Some next}\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list b = Some aa\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (4 subgoals):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list b = Some aa; b \<noteq> a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list b = Some aa\<rbrakk> \<Longrightarrow> b \<noteq> a
 3. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 4. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (4 subgoals):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list b = Some aa; b \<noteq> a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list b = Some aa\<rbrakk> \<Longrightarrow> b \<noteq> a
 3. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 4. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (4 subgoals):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list b = Some aa; b \<noteq> a\<rbrakk> \<Longrightarrow> after_in_list (a # list) b = Some aa
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list b = Some aa\<rbrakk> \<Longrightarrow> b \<noteq> a
 3. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 4. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list b = Some aa\<rbrakk> \<Longrightarrow> b \<noteq> a
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list b = Some aa; b \<in> set list\<rbrakk> \<Longrightarrow> b \<noteq> a
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b. \<lbrakk>x = (aa, b); after_in_list list b = Some aa; b \<in> set list; a \<notin> set list; distinct list\<rbrakk> \<Longrightarrow> b \<noteq> a
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, c) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (4 subgoals):
 1. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; c \<noteq> a\<rbrakk> \<Longrightarrow> (aa, c) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> c \<noteq> a
 3. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 4. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (4 subgoals):
 1. \<And>x aa b c aaa lista. \<lbrakk>a \<noteq> aaa \<and> a \<notin> set lista \<and> aaa \<notin> set lista \<and> distinct lista; x = (aa, b); after_in_list (aaa # lista) c = Some aa; (c, b) \<in> {(next, p). after_in_list (aaa # lista) p = Some next}\<^sup>+; c \<noteq> a; list = aaa # lista\<rbrakk> \<Longrightarrow> (aa, c) \<in> {(next, p). (p = a \<longrightarrow> aaa = next) \<and> (p \<noteq> a \<longrightarrow> after_in_list (aaa # lista) p = Some next)}\<^sup>+
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> c \<noteq> a
 3. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 4. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (5 subgoals):
 1. \<And>x aa b c aaa lista. \<lbrakk>a \<noteq> aaa \<and> a \<notin> set lista \<and> aaa \<notin> set lista \<and> distinct lista; x = (aa, b); after_in_list (aaa # lista) c = Some aa; (c, b) \<in> {(next, p). after_in_list (aaa # lista) p = Some next}\<^sup>+; c \<noteq> a; list = aaa # lista; aaa = aa\<rbrakk> \<Longrightarrow> (aa, c) \<in> {(next, p). (p = a \<longrightarrow> aaa = next) \<and> (p \<noteq> a \<longrightarrow> after_in_list (aaa # lista) p = Some next)}\<^sup>+
 2. \<And>x aa b c aaa lista. \<lbrakk>a \<noteq> aaa \<and> a \<notin> set lista \<and> aaa \<notin> set lista \<and> distinct lista; x = (aa, b); after_in_list (aaa # lista) c = Some aa; (c, b) \<in> {(next, p). after_in_list (aaa # lista) p = Some next}\<^sup>+; c \<noteq> a; list = aaa # lista; aaa \<noteq> aa\<rbrakk> \<Longrightarrow> (aa, c) \<in> {(next, p). (p = a \<longrightarrow> aaa = next) \<and> (p \<noteq> a \<longrightarrow> after_in_list (aaa # lista) p = Some next)}\<^sup>+
 3. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> c \<noteq> a
 4. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 5. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (5 subgoals):
 1. \<And>x aa b c aaa lista. \<lbrakk>a \<noteq> aaa \<and> a \<notin> set lista \<and> aaa \<notin> set lista \<and> distinct lista; x = (aa, b); after_in_list (aaa # lista) c = Some aa; (c, b) \<in> {(next, p). after_in_list (aaa # lista) p = Some next}\<^sup>+; c \<noteq> a; list = aaa # lista; aaa = aa\<rbrakk> \<Longrightarrow> (aa, c) \<in> {(next, p). (p = a \<longrightarrow> aaa = next) \<and> (p \<noteq> a \<longrightarrow> after_in_list (aaa # lista) p = Some next)}
 2. \<And>x aa b c aaa lista. \<lbrakk>a \<noteq> aaa \<and> a \<notin> set lista \<and> aaa \<notin> set lista \<and> distinct lista; x = (aa, b); after_in_list (aaa # lista) c = Some aa; (c, b) \<in> {(next, p). after_in_list (aaa # lista) p = Some next}\<^sup>+; c \<noteq> a; list = aaa # lista; aaa \<noteq> aa\<rbrakk> \<Longrightarrow> (aa, c) \<in> {(next, p). (p = a \<longrightarrow> aaa = next) \<and> (p \<noteq> a \<longrightarrow> after_in_list (aaa # lista) p = Some next)}\<^sup>+
 3. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> c \<noteq> a
 4. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 5. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (4 subgoals):
 1. \<And>x aa b c aaa lista. \<lbrakk>a \<noteq> aaa \<and> a \<notin> set lista \<and> aaa \<notin> set lista \<and> distinct lista; x = (aa, b); after_in_list (aaa # lista) c = Some aa; (c, b) \<in> {(next, p). after_in_list (aaa # lista) p = Some next}\<^sup>+; c \<noteq> a; list = aaa # lista; aaa \<noteq> aa\<rbrakk> \<Longrightarrow> (aa, c) \<in> {(next, p). (p = a \<longrightarrow> aaa = next) \<and> (p \<noteq> a \<longrightarrow> after_in_list (aaa # lista) p = Some next)}\<^sup>+
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> c \<noteq> a
 3. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 4. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (4 subgoals):
 1. \<And>x aa b c aaa lista. \<lbrakk>a \<noteq> aaa \<and> a \<notin> set lista \<and> aaa \<notin> set lista \<and> distinct lista; x = (aa, b); after_in_list (aaa # lista) c = Some aa; (c, b) \<in> {(next, p). after_in_list (aaa # lista) p = Some next}\<^sup>+; c \<noteq> a; list = aaa # lista; aaa \<noteq> aa\<rbrakk> \<Longrightarrow> (aa, c) \<in> {(next, p). (p = a \<longrightarrow> aaa = next) \<and> (p \<noteq> a \<longrightarrow> after_in_list (aaa # lista) p = Some next)}
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> c \<noteq> a
 3. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 4. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> c \<noteq> a
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; after_in_list list c = Some aa\<rbrakk> \<Longrightarrow> c \<noteq> a
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; after_in_list list c = Some aa; c \<in> set list\<rbrakk> \<Longrightarrow> c \<noteq> a
 2. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b c. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, b) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b c y. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<rbrakk> \<Longrightarrow> (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, z) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b c y. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa; after_in_list list y = Some c\<rbrakk> \<Longrightarrow> (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, z) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b c y. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa; after_in_list list y = Some c\<rbrakk> \<Longrightarrow> after_in_list (a # list) y = Some c
 2. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, z) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (4 subgoals):
 1. \<And>x aa b c y. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa; after_in_list list y = Some c; y \<noteq> a\<rbrakk> \<Longrightarrow> after_in_list (a # list) y = Some c
 2. \<And>x aa b c y. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa; after_in_list list y = Some c\<rbrakk> \<Longrightarrow> y \<noteq> a
 3. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, z) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+
 4. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b c y. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa; after_in_list list y = Some c\<rbrakk> \<Longrightarrow> y \<noteq> a
 2. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, z) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b c y. \<lbrakk>after_in_list list y = Some c; a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa\<rbrakk> \<Longrightarrow> y \<noteq> a
 2. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, z) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b c y. \<lbrakk>after_in_list list y = Some c; a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa; y \<in> set list\<rbrakk> \<Longrightarrow> y \<noteq> a
 2. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, z) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (c, z) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); (aa, c) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; (y, z) \<in> {(next, p). after_in_list list p = Some next}; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; after_in_list list z = Some y; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> after_in_list (a # list) z = Some y
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; after_in_list list z = Some y; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+; a \<noteq> z\<rbrakk> \<Longrightarrow> after_in_list (a # list) z = Some y
 2. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; after_in_list list z = Some y; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> a \<noteq> z
 3. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b c y z. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa; (c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; after_in_list list z = Some y; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> a \<noteq> z
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b c y z. \<lbrakk>(c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; after_in_list list z = Some y; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+; a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa\<rbrakk> \<Longrightarrow> a \<noteq> z
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b c y z. \<lbrakk>(c, y) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+; after_in_list list z = Some y; (c, y) \<in> {b. case b of (next, p) \<Rightarrow> after_in_list (a # list) p = Some next}\<^sup>+; a \<notin> set list \<and> distinct list; x = (aa, b); after_in_list list c = Some aa; z \<in> set list\<rbrakk> \<Longrightarrow> a \<noteq> z
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a; distinct (a # list)\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> distinct (a # list) proof (prove)
goal (2 subgoals):
 1. \<And>x aa. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, a); aa \<in> set list; (a, aa) \<in> {(n, p). after_in_list (a # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, a) \<in> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+
 2. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> distinct (a # list) proof (prove)
goal (1 subgoal):
 1. \<And>x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); aa \<in> set list \<and> b = a\<rbrakk> \<Longrightarrow> distinct (a # list) proof (prove)
goal:
No subgoals!