theory Deterministic_AI

lemma last_last_child_next_not_child:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  assumes "last_last_child slot (cdt_list s) = Some child" "valid_mdb s" "valid_list s"
  shows "next_not_child child (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s)" apply(insert assms) apply(frule(2) last_last_child_empty_desc) apply(frule(2) last_last_child_next_sib) apply(frule(2) last_last_child_in_desc) apply(induct slot rule: last_child_induct[where s=s]) apply(simp add: last_last_child_termination) apply(case_tac "y=child") apply(subst next_not_child.psimps) apply(simp add: next_not_child_termination finite_depth) apply(drule last_childD, simp,simp) apply(simp, atomize) apply(elim impE) apply(subst(asm) last_last_child.psimps) apply(simp add: last_last_child_termination) apply(simp split: option.splits if_split_asm) apply(subst(asm) last_last_child.psimps) apply(simp add: last_last_child_termination) apply(simp split: if_split_asm) apply(rule last_last_child_in_desc, simp+) apply(drule last_childD, simp) apply(simp add: next_not_child_termination finite_depth) using assms apply(simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_not_child child (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>last_last_child slot (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>last_last_child slot (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>last_last_child slot (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>last_last_child slot (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child slot (cdt_list s) (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>last_child x (cdt_list s) = None; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y = child\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y = child\<rbrakk> \<Longrightarrow> next_not_child_dom (child, cdt_list s, cdt s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y = child\<rbrakk> \<Longrightarrow> (if next_sib child (cdt_list s) (cdt s) = None then case cdt s child of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s) else next_sib child (cdt_list s) (cdt s)) = next_not_child x (cdt_list s) (cdt s)
 3. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y = child\<rbrakk> \<Longrightarrow> (if next_sib child (cdt_list s) (cdt s) = None then case cdt s child of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s) else next_sib child (cdt_list s) (cdt s)) = next_not_child x (cdt_list s) (cdt s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child y (cdt_list s) = Some child \<longrightarrow> child \<in> descendants_of y (cdt s) \<longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> last_last_child y (cdt_list s) = Some child
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s)
 3. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child; next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (6 subgoals):
 1. \<And>x y. \<lbrakk>valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child; last_child x (cdt_list s) = Some y\<rbrakk> \<Longrightarrow> last_last_child_dom (x, cdt_list s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; (case last_child x (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else last_last_child child (cdt_list s)) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> last_last_child y (cdt_list s) = Some child
 3. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s)
 4. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child; next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 5. valid_mdb s
 6. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; (case last_child x (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else last_last_child child (cdt_list s)) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> last_last_child y (cdt_list s) = Some child
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s)
 3. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child; next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child; next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child; last_child x (cdt_list s) = Some y\<rbrakk> \<Longrightarrow> last_last_child_dom (x, cdt_list s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; (case last_child x (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else last_last_child child (cdt_list s)) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s)
 3. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child; next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; (case last_child x (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else last_last_child child (cdt_list s)) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child; next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child; last_child x (cdt_list s) = Some y; \<exists>ya. last_child y (cdt_list s) = Some ya; last_last_child y (cdt_list s) = Some child\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child; next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_not_child child (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child; next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_not_child y (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; descendants_of child (cdt s) = {}; next_sib child (cdt_list s) (cdt s) = None; child \<in> descendants_of x (cdt s); y \<noteq> child; next_not_child child (cdt_list s) (cdt s) = next_not_child y (cdt_list s) (cdt s); cdt s y = Some x \<and> next_sib y (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> next_not_child y (cdt_list s) (cdt s) = next_not_child x (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (2 subgoals):
 1. valid_mdb s
 2. valid_list s proof (prove)
using this:
last_last_child slot (cdt_list s) = Some child
valid_mdb s
valid_list s

goal (2 subgoals):
 1. valid_mdb s
 2. valid_list s proof (prove)
goal:
No subgoals!