theory CSpace1_R

lemma descendants:
  "descendants_of' p n =
  (let swap = \<lambda>S. S - {src,dest} \<union>
                (if src \<in> S then {dest} else {}) \<union>
                (if dest \<in> S then {src} else {}) in
  swap (descendants_of' (s_d_swp p) m))" apply (simp add: Let_def parency descendants_of'_def s_d_swap_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p n = (let swap = \<lambda>S. S - {src, dest} \<union> (if src \<in> S then {dest} else {}) \<union> (if dest \<in> S then {src} else {}) in swap (descendants_of' (s_d_swp p) m)) proof (prove)
goal (1 subgoal):
 1. (m \<turnstile> p \<rightarrow> src \<longrightarrow> (p = dest \<longrightarrow> (m \<turnstile> src \<rightarrow> dest \<longrightarrow> {c'. c' \<noteq> dest \<and> (c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<longrightarrow> m \<turnstile> src \<rightarrow> c')} = insert src (Collect (subtree m src) - {dest})) \<and> (\<not> m \<turnstile> src \<rightarrow> dest \<longrightarrow> {c'. c' \<noteq> dest \<and> (c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<and> (c' \<noteq> src \<longrightarrow> m \<turnstile> src \<rightarrow> c'))} = Collect (subtree m src))) \<and> (p \<noteq> dest \<longrightarrow> (m \<turnstile> dest \<rightarrow> src \<longrightarrow> (p = src \<longrightarrow> {c'. c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<and> (c' \<noteq> src \<longrightarrow> m \<turnstile> dest \<rightarrow> c')} = insert dest (Collect (subtree m dest) - {src, dest})) \<and> (p \<noteq> src \<longrightarrow> (m \<turnstile> p \<rightarrow> dest \<longrightarrow> {c'. c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> c'} = insert src (insert dest (Collect (subtree m p) - {src, dest}))) \<and> (\<not> m \<turnstile> p \<rightarrow> dest \<longrightarrow> {c'. c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<and> (c' \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> c')} = insert dest (Collect (subtree m p) - {src, dest})))) \<and> (\<not> m \<turnstile> dest \<rightarrow> src \<longrightarrow> (p = src \<longrightarrow> {c'. c' \<noteq> dest \<and> (c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<and> (c' \<noteq> src \<longrightarrow> m \<turnstile> dest \<rightarrow> c'))} = Collect (subtree m dest)) \<and> (p \<noteq> src \<longrightarrow> (m \<turnstile> p \<rightarrow> dest \<longrightarrow> {c'. c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> c'} = insert src (insert dest (Collect (subtree m p) - {src, dest}))) \<and> (\<not> m \<turnstile> p \<rightarrow> dest \<longrightarrow> {c'. c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<and> (c' \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> c')} = insert dest (Collect (subtree m p) - {src, dest})))))) \<and> (\<not> m \<turnstile> p \<rightarrow> src \<longrightarrow> (p = dest \<longrightarrow> (m \<turnstile> src \<rightarrow> dest \<longrightarrow> {c'. c' \<noteq> dest \<and> (c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<longrightarrow> m \<turnstile> src \<rightarrow> c')} = insert src (Collect (subtree m src) - {dest})) \<and> (\<not> m \<turnstile> src \<rightarrow> dest \<longrightarrow> {c'. c' \<noteq> dest \<and> (c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<and> (c' \<noteq> src \<longrightarrow> m \<turnstile> src \<rightarrow> c'))} = Collect (subtree m src))) \<and> (p \<noteq> dest \<longrightarrow> (m \<turnstile> dest \<rightarrow> src \<longrightarrow> (p = src \<longrightarrow> {c'. c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<and> (c' \<noteq> src \<longrightarrow> m \<turnstile> dest \<rightarrow> c')} = insert dest (Collect (subtree m dest) - {src, dest})) \<and> (p \<noteq> src \<longrightarrow> (m \<turnstile> p \<rightarrow> dest \<longrightarrow> {c'. c' \<noteq> dest \<and> (c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> c')} = insert src (Collect (subtree m p) - {dest})) \<and> (\<not> m \<turnstile> p \<rightarrow> dest \<longrightarrow> {c'. c' \<noteq> dest \<and> (c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<and> (c' \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> c'))} = Collect (subtree m p)))) \<and> (\<not> m \<turnstile> dest \<rightarrow> src \<longrightarrow> (p = src \<longrightarrow> {c'. c' \<noteq> dest \<and> (c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<and> (c' \<noteq> src \<longrightarrow> m \<turnstile> dest \<rightarrow> c'))} = Collect (subtree m dest)) \<and> (p \<noteq> src \<longrightarrow> (m \<turnstile> p \<rightarrow> dest \<longrightarrow> {c'. c' \<noteq> dest \<and> (c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> c')} = insert src (Collect (subtree m p) - {dest})) \<and> (\<not> m \<turnstile> p \<rightarrow> dest \<longrightarrow> {c'. c' \<noteq> dest \<and> (c' \<noteq> dest \<longrightarrow> c' \<noteq> src \<and> (c' \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> c'))} = Collect (subtree m p)))))) proof (prove)
goal:
No subgoals!