theory Deterministic_AI

lemma next_slot:
  "next_slot p t' n
    = (if p = src then
        (if next_slot dest t m = Some src then Some dest
         else next_slot dest t m)
      else if p = dest then
        (if next_slot src t m = Some dest then Some src
         else next_slot src t m)
      else if next_slot p t m = Some src then Some dest
      else if next_slot p t m = Some dest then Some src
      else next_slot p t m)" apply(case_tac "p=src") apply(simp add: next_slot_def next_child next_not_child valid_list t'_empty) apply(case_tac "p=dest") apply(simp add: next_slot_def next_child next_not_child valid_list t'_empty
         split: if_split_asm) apply(case_tac "next_slot p t m = Some src") apply(simp add: next_slot_def next_child next_not_child s_d_swap_def t'_empty
         split: if_split_asm) apply(case_tac "next_slot p t m = Some dest") apply(simp add: next_slot_def next_child next_not_child s_d_swap_def  t'_empty
         split: if_split_asm) apply(simp add: next_slot_def next_child next_not_child s_d_swap_def t'_empty
        split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. p = src \<Longrightarrow> next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m)
 2. p \<noteq> src \<Longrightarrow> next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m) proof (prove)
goal (1 subgoal):
 1. p \<noteq> src \<Longrightarrow> next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m)
 2. \<lbrakk>p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<noteq> src; p \<noteq> dest; next_slot p t m = Some src\<rbrakk> \<Longrightarrow> next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m)
 2. \<lbrakk>p \<noteq> src; p \<noteq> dest; next_slot p t m \<noteq> Some src\<rbrakk> \<Longrightarrow> next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> src; p \<noteq> dest; next_slot p t m \<noteq> Some src\<rbrakk> \<Longrightarrow> next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<noteq> src; p \<noteq> dest; next_slot p t m \<noteq> Some src; next_slot p t m = Some dest\<rbrakk> \<Longrightarrow> next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m)
 2. \<lbrakk>p \<noteq> src; p \<noteq> dest; next_slot p t m \<noteq> Some src; next_slot p t m \<noteq> Some dest\<rbrakk> \<Longrightarrow> next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> src; p \<noteq> dest; next_slot p t m \<noteq> Some src; next_slot p t m \<noteq> Some dest\<rbrakk> \<Longrightarrow> next_slot p t' n = (if p = src then if next_slot dest t m = Some src then Some dest else next_slot dest t m else if p = dest then if next_slot src t m = Some dest then Some src else next_slot src t m else if next_slot p t m = Some src then Some dest else if next_slot p t m = Some dest then Some src else next_slot p t m) proof (prove)
goal:
No subgoals!