theory Deterministic_AI

lemma finite_depth:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "finite_depth m \<Longrightarrow> finite_depth n" apply(simp add: finite_depth_def descendants) apply(simp add: n_def) apply(rule allI) apply(case_tac "slot=dest") apply(erule_tac x=src in allE) apply(elim exE conjE) apply(erule disjE) apply(rule_tac x=p in exI) apply(simp) apply(rule impI, simp add: desc) apply(rule_tac x=dest in exI) apply(simp) apply(erule_tac x=slot in allE) apply(elim exE conjE) apply(rule_tac x=p in exI) apply(simp) apply(rule impI) apply(simp add: desc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite_depth m \<Longrightarrow> finite_depth n proof (prove)
goal (1 subgoal):
 1. \<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None \<Longrightarrow> \<forall>slot. \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> n p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> n p = None) proof (prove)
goal (1 subgoal):
 1. \<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None \<Longrightarrow> \<forall>slot. \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot = dest\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None))
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>slot = dest; \<exists>p. (src \<in> descendants_of p m \<or> p = src) \<and> m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None))
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None))
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; src \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None))
 2. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None))
 3. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; src \<in> descendants_of p m\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None))
 2. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None))
 3. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; src \<in> descendants_of p m\<rbrakk> \<Longrightarrow> p = dest \<longrightarrow> m src = None
 2. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None))
 3. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None))
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> (dest = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (dest \<noteq> dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m dest = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m dest = None))
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>slot \<noteq> dest; \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> slot = dest \<or> dest = slot) \<and> m src = None) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (slot \<in> descendants_of dest m \<or> dest = slot) \<and> m src = None)) \<and> (p \<noteq> dest \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> slot = dest \<or> p = slot) \<and> m p = None) \<and> (src \<notin> descendants_of p m \<longrightarrow> (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None)) proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None\<rbrakk> \<Longrightarrow> p = dest \<longrightarrow> slot \<in> descendants_of dest m \<and> m src = None proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p = dest\<rbrakk> \<Longrightarrow> slot \<in> descendants_of dest m \<and> m src = None proof (prove)
goal:
No subgoals!