theory ListLibLemmas

lemma after_in_list_trancl_prepend:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+" apply(induct list arbitrary:x y) apply(simp) apply(case_tac "x=a") apply(rule r_into_trancl) apply(simp) apply(drule set_ConsD) apply(elim disjE) apply(simp) apply(atomize) apply(drule_tac x=x in spec) apply(drule_tac x=y in spec) apply(drule_tac mp) apply(simp) apply(drule_tac mp) apply(simp) apply(erule trancl_induct) apply(drule CollectD, simp) apply(rule_tac b = a in trancl_into_trancl2) apply(simp) apply(rule r_into_trancl) apply(rule_tac a = "(a,ya)" in CollectI) apply(clarsimp) apply(case_tac list) apply(simp) apply(simp) apply(case_tac "ya=a") apply(drule CollectD) apply(simp del:after_in_list.simps) apply(drule after_in_list_in_list') apply(simp) apply(rule_tac b=ya in trancl_into_trancl) apply(simp) apply(drule CollectD) apply(rule CollectI) apply(case_tac "ya=y") apply(frule_tac x=y in distinct_after_in_list_not_self_trancl) apply(simp) apply(case_tac list) apply(simp) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>distinct [y]; x \<in> set []\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list [y] n = Some p}\<^sup>+
 2. \<And>a list x y. \<lbrakk>\<And>x y. \<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; distinct (y # a # list); x \<in> set (a # list)\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a list x y. \<lbrakk>\<And>x y. \<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; distinct (y # a # list); x \<in> set (a # list)\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y. \<lbrakk>\<And>x y. \<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; distinct (y # a # list); x \<in> set (a # list); x = a\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+
 2. \<And>a list x y. \<lbrakk>\<And>x y. \<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; distinct (y # a # list); x \<in> set (a # list); x \<noteq> a\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y. \<lbrakk>\<And>x y. \<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; distinct (y # a # list); x \<in> set (a # list); x = a\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}
 2. \<And>a list x y. \<lbrakk>\<And>x y. \<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; distinct (y # a # list); x \<in> set (a # list); x \<noteq> a\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a list x y. \<lbrakk>\<And>x y. \<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; distinct (y # a # list); x \<in> set (a # list); x \<noteq> a\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a list x y. \<lbrakk>\<And>x y. \<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; distinct (y # a # list); x \<noteq> a; x = a \<or> x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y. \<lbrakk>\<And>x y. \<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; distinct (y # a # list); x \<noteq> a; x = a\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+
 2. \<And>a list x y. \<lbrakk>\<And>x y. \<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; distinct (y # a # list); x \<noteq> a; x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a list x y. \<lbrakk>\<And>x y. \<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; distinct (y # a # list); x \<noteq> a; x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a list x y. \<lbrakk>\<forall>x y. distinct (y # list) \<longrightarrow> x \<in> set list \<longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; distinct (y # a # list); x \<noteq> a; x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a list x y. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; \<forall>y. distinct (y # list) \<longrightarrow> x \<in> set list \<longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a list x y. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; distinct (y # list) \<longrightarrow> x \<in> set list \<longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list\<rbrakk> \<Longrightarrow> distinct (y # list)
 2. \<And>a list x y. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; x \<in> set list \<longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a list x y. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; x \<in> set list \<longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list\<rbrakk> \<Longrightarrow> x \<in> set list
 2. \<And>a list x y. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a list x y. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<rbrakk> \<Longrightarrow> (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya. \<lbrakk>y \<noteq> a \<and> y \<notin> set list \<and> a \<notin> set list \<and> distinct list; x \<noteq> a; x \<in> set list; after_in_list (y # list) y = Some ya\<rbrakk> \<Longrightarrow> (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> (if n = y then Some a else after_in_list (a # list) n) = Some p}\<^sup>+
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>a list x y ya. \<lbrakk>y \<noteq> a \<and> y \<notin> set list \<and> a \<notin> set list \<and> distinct list; x \<noteq> a; x \<in> set list; after_in_list (y # list) y = Some ya\<rbrakk> \<Longrightarrow> (y, a) \<in> {b. case b of (n, p) \<Rightarrow> (if n = y then Some a else after_in_list (a # list) n) = Some p}
 2. \<And>a list x y ya. \<lbrakk>y \<noteq> a \<and> y \<notin> set list \<and> a \<notin> set list \<and> distinct list; x \<noteq> a; x \<in> set list; after_in_list (y # list) y = Some ya\<rbrakk> \<Longrightarrow> (a, ya) \<in> {b. case b of (n, p) \<Rightarrow> (if n = y then Some a else after_in_list (a # list) n) = Some p}\<^sup>+
 3. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya. \<lbrakk>y \<noteq> a \<and> y \<notin> set list \<and> a \<notin> set list \<and> distinct list; x \<noteq> a; x \<in> set list; after_in_list (y # list) y = Some ya\<rbrakk> \<Longrightarrow> (a, ya) \<in> {b. case b of (n, p) \<Rightarrow> (if n = y then Some a else after_in_list (a # list) n) = Some p}\<^sup>+
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya. \<lbrakk>y \<noteq> a \<and> y \<notin> set list \<and> a \<notin> set list \<and> distinct list; x \<noteq> a; x \<in> set list; after_in_list (y # list) y = Some ya\<rbrakk> \<Longrightarrow> (a, ya) \<in> {b. case b of (n, p) \<Rightarrow> (if n = y then Some a else after_in_list (a # list) n) = Some p}
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya. \<lbrakk>y \<noteq> a \<and> y \<notin> set list \<and> a \<notin> set list \<and> distinct list; x \<noteq> a; x \<in> set list; after_in_list (y # list) y = Some ya\<rbrakk> \<Longrightarrow> case (a, ya) of (n, p) \<Rightarrow> (if n = y then Some a else after_in_list (a # list) n) = Some p
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya. \<lbrakk>x \<noteq> a; x \<in> set list; after_in_list (y # list) y = Some ya; y \<noteq> a; y \<notin> set list; a \<notin> set list; distinct list\<rbrakk> \<Longrightarrow> after_in_list (a # list) a = Some ya
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>a list x y ya. \<lbrakk>x \<noteq> a; x \<in> set list; after_in_list (y # list) y = Some ya; y \<noteq> a; y \<notin> set list; a \<notin> set list; distinct list; list = []\<rbrakk> \<Longrightarrow> after_in_list (a # list) a = Some ya
 2. \<And>a list x y ya aa lista. \<lbrakk>x \<noteq> a; x \<in> set list; after_in_list (y # list) y = Some ya; y \<noteq> a; y \<notin> set list; a \<notin> set list; distinct list; list = aa # lista\<rbrakk> \<Longrightarrow> after_in_list (a # list) a = Some ya
 3. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya aa lista. \<lbrakk>x \<noteq> a; x \<in> set list; after_in_list (y # list) y = Some ya; y \<noteq> a; y \<notin> set list; a \<notin> set list; distinct list; list = aa # lista\<rbrakk> \<Longrightarrow> after_in_list (a # list) a = Some ya
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya = a\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya = a; case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # list) n = Some p\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya z. \<lbrakk>y \<noteq> a \<and> y \<notin> set list \<and> a \<notin> set list \<and> distinct list; x \<noteq> a; x \<in> set list; (y, a) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, a) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya = a; after_in_list (y # list) a = Some z\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya z. \<lbrakk>y \<noteq> a \<and> y \<notin> set list \<and> a \<notin> set list \<and> distinct list; x \<noteq> a; x \<in> set list; (y, a) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, a) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya = a; a \<in> set (y # list)\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a\<rbrakk> \<Longrightarrow> (y, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a\<rbrakk> \<Longrightarrow> (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a\<rbrakk> \<Longrightarrow> (ya, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p} proof (prove)
goal (1 subgoal):
 1. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (ya, z) \<in> {(n, p). after_in_list (y # list) n = Some p}; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a\<rbrakk> \<Longrightarrow> (ya, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p} proof (prove)
goal (1 subgoal):
 1. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a; case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # list) n = Some p\<rbrakk> \<Longrightarrow> (ya, z) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p} proof (prove)
goal (1 subgoal):
 1. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a; case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # list) n = Some p\<rbrakk> \<Longrightarrow> case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a; case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # list) n = Some p; ya = y\<rbrakk> \<Longrightarrow> case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a; case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # list) n = Some p; ya \<noteq> y\<rbrakk> \<Longrightarrow> case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a; case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # list) n = Some p; ya = y; (y, y) \<notin> {(p, q). after_in_list (y # a # list) p = Some q}\<^sup>+\<rbrakk> \<Longrightarrow> case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p
 2. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a; case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # list) n = Some p; ya \<noteq> y\<rbrakk> \<Longrightarrow> case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p proof (prove)
goal (1 subgoal):
 1. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a; case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # list) n = Some p; ya \<noteq> y\<rbrakk> \<Longrightarrow> case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p proof (prove)
goal (2 subgoals):
 1. \<And>a list x y ya z. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a; case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # list) n = Some p; ya \<noteq> y; list = []\<rbrakk> \<Longrightarrow> case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p
 2. \<And>a list x y ya z aa lista. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a; case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # list) n = Some p; ya \<noteq> y; list = aa # lista\<rbrakk> \<Longrightarrow> case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p proof (prove)
goal (1 subgoal):
 1. \<And>a list x y ya z aa lista. \<lbrakk>distinct (y # a # list); x \<noteq> a; x \<in> set list; (y, ya) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+; (y, ya) \<in> {b. case b of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p}\<^sup>+; ya \<noteq> a; case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # list) n = Some p; ya \<noteq> y; list = aa # lista\<rbrakk> \<Longrightarrow> case (ya, z) of (n, p) \<Rightarrow> after_in_list (y # a # list) n = Some p proof (prove)
goal:
No subgoals!