theory Deterministic_AI

lemma next_sib_set_in_next_slot_set:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>next \<in> next_sib_set slot (cdt_list s) (cdt s); valid_list s; valid_mdb s\<rbrakk>
    \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s)" apply(simp add: next_sib_set_def) apply(induct "next" slot rule: trancl.induct) apply(simp add: next_sib_in_next_slot_set) apply(simp add: next_slot_set_def) apply(rule trancl_trans) apply(simp) apply(drule(2) next_sib_in_next_slot_set) apply(simp add: next_slot_set_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next \<in> next_sib_set slot (cdt_list s) (cdt s); valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(next, slot) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> a \<in> next_slot_set b (cdt_list s) (cdt s)
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; \<lbrakk>valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> a \<in> next_slot_set b (cdt_list s) (cdt s); (b, c) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> a \<in> next_slot_set c (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; \<lbrakk>valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> a \<in> next_slot_set b (cdt_list s) (cdt s); (b, c) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> a \<in> next_slot_set c (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; (a, b) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; next_sib c (cdt_list s) (cdt s) = Some b; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> (a, c) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; (a, b) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; next_sib c (cdt_list s) (cdt s) = Some b; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> (a, ?y2 a b c) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+
 2. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; (a, b) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; next_sib c (cdt_list s) (cdt s) = Some b; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> (?y2 a b c, c) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; (a, b) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; next_sib c (cdt_list s) (cdt s) = Some b; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> (b, c) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; (a, b) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+; valid_list s; valid_mdb s; b \<in> next_slot_set c (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> (b, c) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}\<^sup>+ proof (prove)
goal:
No subgoals!