theory Deterministic_AI

lemma next_slot_linear:
  "\<lbrakk>a \<in> next_slot_set c t m; b \<in> next_slot_set c t m; a \<noteq> b\<rbrakk>
    \<Longrightarrow> a \<in> next_slot_set b t m \<or> b \<in> next_slot_set a t m" apply(clarsimp) apply(simp add: next_slot_set_def) apply(induct a c rule: trancl.induct) apply(simp) apply(erule tranclE) apply(simp) apply(simp) apply(simp) apply(case_tac "ba=b") apply(simp) apply(subgoal_tac "(b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+") apply(simp) apply(erule_tac a=b and b=c in tranclE) apply(simp) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> next_slot_set c t m; b \<in> next_slot_set c t m; a \<noteq> b\<rbrakk> \<Longrightarrow> a \<in> next_slot_set b t m \<or> b \<in> next_slot_set a t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> next_slot_set c t m; b \<in> next_slot_set c t m; a \<noteq> b; b \<notin> next_slot_set a t m\<rbrakk> \<Longrightarrow> a \<in> next_slot_set b t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a ba. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+
 2. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>(b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (ba, c) \<in> {(next, p). next_slot p t m = Some next}; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a ba. \<lbrakk>next_slot ba t m = Some a; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+
 2. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>(b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (ba, c) \<in> {(next, p). next_slot p t m = Some next}; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>a ba. \<lbrakk>next_slot ba t m = Some a; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+
 2. \<And>a ba c. \<lbrakk>next_slot ba t m = Some a; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (c, ba) \<in> {(next, p). next_slot p t m = Some next}\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+
 3. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>(b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (ba, c) \<in> {(next, p). next_slot p t m = Some next}; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a ba c. \<lbrakk>next_slot ba t m = Some a; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (c, ba) \<in> {(next, p). next_slot p t m = Some next}\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+
 2. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>(b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (ba, c) \<in> {(next, p). next_slot p t m = Some next}; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; \<lbrakk>(b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (ba, c) \<in> {(next, p). next_slot p t m = Some next}; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some ba; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some ba; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+; ba = b\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+
 2. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some ba; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+; ba \<noteq> b\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some ba; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+; ba \<noteq> b\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some ba; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+; ba \<noteq> b; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+
 2. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some ba; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+; ba \<noteq> b\<rbrakk> \<Longrightarrow> (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some ba; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+; ba \<noteq> b\<rbrakk> \<Longrightarrow> (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a ba c. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some ba; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+; ba \<noteq> b; (b, c) \<in> {(next, p). next_slot p t m = Some next}\<rbrakk> \<Longrightarrow> (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+
 2. \<And>a ba c ca. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some ba; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+; ba \<noteq> b; (b, ca) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (ca, c) \<in> {(next, p). next_slot p t m = Some next}\<rbrakk> \<Longrightarrow> (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a ba c ca. \<lbrakk>(a, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ \<Longrightarrow> (a, b) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; next_slot c t m = Some ba; a \<noteq> b; (b, a) \<notin> {(next, p). next_slot p t m = Some next}\<^sup>+; ba \<noteq> b; (b, ca) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+; (ca, c) \<in> {(next, p). next_slot p t m = Some next}\<rbrakk> \<Longrightarrow> (b, ba) \<in> {(next, p). next_slot p t m = Some next}\<^sup>+ proof (prove)
goal:
No subgoals!