theory ListLibLemmas

lemma indexed_trancl_as_set: "distinct list \<Longrightarrow> {(i, j). \<exists> p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j }
      = {(i, j). \<exists> p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j }\<^sup>+" apply (rule equalityI) apply (rule subsetI) apply (case_tac x, simp) apply (elim exE conjE) apply (frule less_imp_Suc_add) apply (erule exE) apply (rule_tac cap = "length list" and m = q and n = p and k = k in range_nat_relation_induct) apply (simp) apply (simp) apply (rule allI, rule impI) apply (rule_tac p = p and q = q and k = k and n = n in indexed_trancl_as_set_helper) apply (simp)+ apply (rule subsetI) apply (case_tac x, simp) apply (erule trancl_induct) apply (simp, elim exE conjE) apply (rule_tac x = p in exI, rule_tac x = "Suc p" in exI, simp) apply (simp) apply (rotate_tac 4, erule exE, rule_tac x = p in exI) apply (erule exE, rule_tac x = "Suc pa" in exI) apply (intro conjI) defer apply (simp) apply (erule exE, simp) apply (simp) apply (erule exE) apply (subgoal_tac "pa = q") apply (simp) apply (frule_tac xs = list and i = pa and j = q in nth_eq_iff_index_eq) apply (simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct list \<Longrightarrow> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} = {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. distinct list \<Longrightarrow> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} \<subseteq> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 2. distinct list \<Longrightarrow> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<subseteq> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct list; x \<in> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j}\<rbrakk> \<Longrightarrow> x \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 2. distinct list \<Longrightarrow> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<subseteq> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>distinct list; \<exists>p q. p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = b; x = (a, b)\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 2. distinct list \<Longrightarrow> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<subseteq> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (2 subgoals):
 1. \<And>x a b p q. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 2. distinct list \<Longrightarrow> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<subseteq> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (2 subgoals):
 1. \<And>x a b p q. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; \<exists>k. q = Suc (p + k)\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 2. distinct list \<Longrightarrow> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<subseteq> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (2 subgoals):
 1. \<And>x a b p q k. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k)\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 2. distinct list \<Longrightarrow> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<subseteq> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (5 subgoals):
 1. \<And>x a b p q k. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k)\<rbrakk> \<Longrightarrow> q = Suc (p + k)
 2. \<And>x a b p q k. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k)\<rbrakk> \<Longrightarrow> q < length list
 3. \<And>x a b p q k. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k)\<rbrakk> \<Longrightarrow> \<forall>n. Suc n < length list \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 4. \<And>x a b p q k. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k)\<rbrakk> \<Longrightarrow> \<forall>i j k. i < length list \<and> j < length list \<and> k < length list \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 5. distinct list \<Longrightarrow> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<subseteq> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (4 subgoals):
 1. \<And>x a b p q k. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k)\<rbrakk> \<Longrightarrow> q < length list
 2. \<And>x a b p q k. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k)\<rbrakk> \<Longrightarrow> \<forall>n. Suc n < length list \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 3. \<And>x a b p q k. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k)\<rbrakk> \<Longrightarrow> \<forall>i j k. i < length list \<and> j < length list \<and> k < length list \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 4. distinct list \<Longrightarrow> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<subseteq> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (3 subgoals):
 1. \<And>x a b p q k. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k)\<rbrakk> \<Longrightarrow> \<forall>n. Suc n < length list \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 2. \<And>x a b p q k. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k)\<rbrakk> \<Longrightarrow> \<forall>i j k. i < length list \<and> j < length list \<and> k < length list \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 3. distinct list \<Longrightarrow> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<subseteq> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (3 subgoals):
 1. \<And>x a b p q k n. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k); Suc n < length list\<rbrakk> \<Longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 2. \<And>x a b p q k. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k)\<rbrakk> \<Longrightarrow> \<forall>i j k. i < length list \<and> j < length list \<and> k < length list \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 3. distinct list \<Longrightarrow> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<subseteq> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (8 subgoals):
 1. \<And>x a b p q k n. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k); Suc n < length list\<rbrakk> \<Longrightarrow> p < q
 2. \<And>x a b p q k n. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k); Suc n < length list\<rbrakk> \<Longrightarrow> q < length list
 3. \<And>x a b p q k n. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k); Suc n < length list\<rbrakk> \<Longrightarrow> list ! p = a
 4. \<And>x a b p q k n. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k); Suc n < length list\<rbrakk> \<Longrightarrow> list ! q = b
 5. \<And>x a b p q k n. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k); Suc n < length list\<rbrakk> \<Longrightarrow> q = Suc (p + k)
 6. \<And>x a b p q k n. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k); Suc n < length list\<rbrakk> \<Longrightarrow> Suc n < length list
 7. \<And>x a b p q k. \<lbrakk>distinct list; x = (a, b); p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k)\<rbrakk> \<Longrightarrow> \<forall>i j k. i < length list \<and> j < length list \<and> k < length list \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<longrightarrow> (a, b) \<in> {a. case a of (i, j) \<Rightarrow> \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 8. distinct list \<Longrightarrow> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<subseteq> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (1 subgoal):
 1. distinct list \<Longrightarrow> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ \<subseteq> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>distinct list; x \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> {(i, j). \<exists>p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j} proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>distinct list; (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; x = (a, b)\<rbrakk> \<Longrightarrow> \<exists>p q. p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = b proof (prove)
goal (2 subgoals):
 1. \<And>x a b y. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<rbrakk> \<Longrightarrow> \<exists>p q. p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y
 2. \<And>x a b y z. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; (y, z) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}; \<exists>p q. p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y\<rbrakk> \<Longrightarrow> \<exists>p q. p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = z proof (prove)
goal (2 subgoals):
 1. \<And>x a b y p. \<lbrakk>distinct list; x = (a, b); Suc p < length list; list ! p = a; list ! Suc p = y\<rbrakk> \<Longrightarrow> \<exists>p q. p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y
 2. \<And>x a b y z. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; (y, z) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}; \<exists>p q. p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y\<rbrakk> \<Longrightarrow> \<exists>p q. p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = z proof (prove)
goal (1 subgoal):
 1. \<And>x a b y z. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; (y, z) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}; \<exists>p q. p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y\<rbrakk> \<Longrightarrow> \<exists>p q. p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = z proof (prove)
goal (1 subgoal):
 1. \<And>x a b y z. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>p. Suc p < length list \<and> list ! p = y \<and> list ! Suc p = z; \<exists>p q. p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y\<rbrakk> \<Longrightarrow> \<exists>p q. p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = z proof (prove)
goal (1 subgoal):
 1. \<And>x a b y z p. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>p. Suc p < length list \<and> list ! p = y \<and> list ! Suc p = z; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y\<rbrakk> \<Longrightarrow> \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = z proof (prove)
goal (1 subgoal):
 1. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> p < Suc pa \<and> Suc pa < length list \<and> list ! p = a \<and> list ! Suc pa = z proof (prove)
goal (4 subgoals):
 1. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> p < Suc pa
 2. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> Suc pa < length list
 3. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> list ! p = a
 4. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> list ! Suc pa = z proof (prove)
goal (4 subgoals):
 1. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> Suc pa < length list
 2. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> list ! p = a
 3. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> list ! Suc pa = z
 4. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> p < Suc pa proof (prove)
goal (3 subgoals):
 1. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> list ! p = a
 2. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> list ! Suc pa = z
 3. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> p < Suc pa proof (prove)
goal (2 subgoals):
 1. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> list ! Suc pa = z
 2. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> p < Suc pa proof (prove)
goal (1 subgoal):
 1. \<And>x a b y z p pa. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; \<exists>q>p. q < length list \<and> list ! p = a \<and> list ! q = y; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z\<rbrakk> \<Longrightarrow> p < Suc pa proof (prove)
goal (1 subgoal):
 1. \<And>x a b y z p pa q. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z; p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y\<rbrakk> \<Longrightarrow> p < Suc pa proof (prove)
goal (2 subgoals):
 1. \<And>x a b y z p pa q. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z; p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y; pa = q\<rbrakk> \<Longrightarrow> p < Suc pa
 2. \<And>x a b y z p pa q. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z; p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y\<rbrakk> \<Longrightarrow> pa = q proof (prove)
goal (1 subgoal):
 1. \<And>x a b y z p pa q. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z; p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y\<rbrakk> \<Longrightarrow> pa = q proof (prove)
goal (3 subgoals):
 1. \<And>x a b y z p pa q. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z; p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y\<rbrakk> \<Longrightarrow> pa < length list
 2. \<And>x a b y z p pa q. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z; p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y\<rbrakk> \<Longrightarrow> q < length list
 3. \<And>x a b y z p pa q. \<lbrakk>distinct list; x = (a, b); (a, y) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; Suc pa < length list \<and> list ! pa = y \<and> list ! Suc pa = z; p < q \<and> q < length list \<and> list ! p = a \<and> list ! q = y; (list ! pa = list ! q) = (pa = q)\<rbrakk> \<Longrightarrow> pa = q proof (prove)
goal:
No subgoals!