[STATEMENT]
theorem  convergence:
  assumes "set xs = set ys"
          "concurrent_ops_commute xs"
          "concurrent_ops_commute ys"
          "distinct xs"
          "distinct ys"
          "hb_consistent xs"
          "hb_consistent ys"
  shows   "apply_operations xs = apply_operations ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_operations xs = apply_operations ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set xs = set ys
concurrent_ops_commute xs
concurrent_ops_commute ys
distinct xs
distinct ys
hb_consistent xs
hb_consistent ys

goal (1 subgoal):
 1. apply_operations xs = apply_operations ys
[PROOF STEP]
proof(induction xs arbitrary: ys rule: rev_induct, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
case assms: (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>set xs = set ?ys1; concurrent_ops_commute xs; concurrent_ops_commute ?ys1; distinct xs; distinct ?ys1; hb_consistent xs; hb_consistent ?ys1\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ?ys1
set (xs @ [x]) = set ys
concurrent_ops_commute (xs @ [x])
concurrent_ops_commute ys
distinct (xs @ [x])
distinct ys
hb_consistent (xs @ [x])
hb_consistent ys

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>set xs = set ?ys1; concurrent_ops_commute xs; concurrent_ops_commute ?ys1; distinct xs; distinct ?ys1; hb_consistent xs; hb_consistent ?ys1\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ?ys1
set (xs @ [x]) = set ys
concurrent_ops_commute (xs @ [x])
concurrent_ops_commute ys
distinct (xs @ [x])
distinct ys
hb_consistent (xs @ [x])
hb_consistent ys
[PROOF STEP]
obtain prefix suffix where ys_split: "ys = prefix @ x # suffix \<and> concurrent_set x suffix"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set xs = set ?ys1; concurrent_ops_commute xs; concurrent_ops_commute ?ys1; distinct xs; distinct ?ys1; hb_consistent xs; hb_consistent ?ys1\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ?ys1
set (xs @ [x]) = set ys
concurrent_ops_commute (xs @ [x])
concurrent_ops_commute ys
distinct (xs @ [x])
distinct ys
hb_consistent (xs @ [x])
hb_consistent ys

goal (1 subgoal):
 1. (\<And>prefix suffix. ys = prefix @ x # suffix \<and> concurrent_set x suffix \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using hb_consistent_prefix_suffix_exists
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set xs = set ?ys1; concurrent_ops_commute xs; concurrent_ops_commute ?ys1; distinct xs; distinct ?ys1; hb_consistent xs; hb_consistent ?ys1\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ?ys1
set (xs @ [x]) = set ys
concurrent_ops_commute (xs @ [x])
concurrent_ops_commute ys
distinct (xs @ [x])
distinct ys
hb_consistent (xs @ [x])
hb_consistent ys
\<lbrakk>hb_consistent ?ys; hb_consistent (?xs @ [?x]); {?x} \<union> set ?xs = set ?ys; distinct (?x # ?xs); distinct ?ys\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. ?ys = prefix @ ?x # suffix \<and> concurrent_set ?x suffix

goal (1 subgoal):
 1. (\<And>prefix suffix. ys = prefix @ x # suffix \<and> concurrent_set x suffix \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
hence *: "distinct (prefix @ suffix)" "hb_consistent xs"
[PROOF STATE]
proof (prove)
using this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. distinct (prefix @ suffix) &&& hb_consistent xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix
\<lbrakk>set xs = set ?ys1; concurrent_ops_commute xs; concurrent_ops_commute ?ys1; distinct xs; distinct ?ys1; hb_consistent xs; hb_consistent ?ys1\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ?ys1
set (xs @ [x]) = set ys
concurrent_ops_commute (xs @ [x])
concurrent_ops_commute ys
distinct (xs @ [x])
distinct ys
hb_consistent (xs @ [x])
hb_consistent ys

goal (1 subgoal):
 1. distinct (prefix @ suffix) &&& hb_consistent xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (prefix @ suffix)
hb_consistent xs

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (prefix @ suffix)
hb_consistent xs

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
distinct (prefix @ suffix)
hb_consistent xs

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
have "hb_consistent prefix" "hb_consistent suffix"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hb_consistent prefix &&& hb_consistent suffix
[PROOF STEP]
using ys_split assms hb_consistent_append_D2 hb_consistent_append_elim_ConsD
[PROOF STATE]
proof (prove)
using this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix
\<lbrakk>set xs = set ?ys1; concurrent_ops_commute xs; concurrent_ops_commute ?ys1; distinct xs; distinct ?ys1; hb_consistent xs; hb_consistent ?ys1\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ?ys1
set (xs @ [x]) = set ys
concurrent_ops_commute (xs @ [x])
concurrent_ops_commute ys
distinct (xs @ [x])
distinct ys
hb_consistent (xs @ [x])
hb_consistent ys
hb_consistent (?xs @ ?ys) \<Longrightarrow> hb_consistent ?ys
hb_consistent (?y # ?ys) \<Longrightarrow> hb_consistent ?ys

goal (1 subgoal):
 1. hb_consistent prefix &&& hb_consistent suffix
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
hb_consistent prefix
hb_consistent suffix

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
hence "hb_consistent (prefix @ suffix)"
[PROOF STATE]
proof (prove)
using this:
hb_consistent prefix
hb_consistent suffix

goal (1 subgoal):
 1. hb_consistent (prefix @ suffix)
[PROOF STEP]
by (metis assms(8) hb_consistent_append hb_consistent_append_porder list.set_intros(2) ys_split)
[PROOF STATE]
proof (state)
this:
hb_consistent (prefix @ suffix)

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
hb_consistent (prefix @ suffix)

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hb_consistent (prefix @ suffix)

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
have **: "concurrent_ops_commute (prefix @ suffix @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concurrent_ops_commute (prefix @ suffix @ [x])
[PROOF STEP]
using assms ys_split
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set xs = set ?ys1; concurrent_ops_commute xs; concurrent_ops_commute ?ys1; distinct xs; distinct ?ys1; hb_consistent xs; hb_consistent ?ys1\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ?ys1
set (xs @ [x]) = set ys
concurrent_ops_commute (xs @ [x])
concurrent_ops_commute ys
distinct (xs @ [x])
distinct ys
hb_consistent (xs @ [x])
hb_consistent ys
ys = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. concurrent_ops_commute (prefix @ suffix @ [x])
[PROOF STEP]
by (clarsimp simp: concurrent_ops_commute_def)
[PROOF STATE]
proof (state)
this:
concurrent_ops_commute (prefix @ suffix @ [x])

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
concurrent_ops_commute (prefix @ suffix @ [x])

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
hence "concurrent_ops_commute (prefix @ suffix)"
[PROOF STATE]
proof (prove)
using this:
concurrent_ops_commute (prefix @ suffix @ [x])

goal (1 subgoal):
 1. concurrent_ops_commute (prefix @ suffix)
[PROOF STEP]
by (force simp del: append_assoc simp add: append_assoc[symmetric])
[PROOF STATE]
proof (state)
this:
concurrent_ops_commute (prefix @ suffix)

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix
distinct (prefix @ suffix)
hb_consistent xs
hb_consistent (prefix @ suffix)
concurrent_ops_commute (prefix @ suffix @ [x])
concurrent_ops_commute (prefix @ suffix)
[PROOF STEP]
have "apply_operations xs = apply_operations (prefix@suffix)"
[PROOF STATE]
proof (prove)
using this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix
distinct (prefix @ suffix)
hb_consistent xs
hb_consistent (prefix @ suffix)
concurrent_ops_commute (prefix @ suffix @ [x])
concurrent_ops_commute (prefix @ suffix)

goal (1 subgoal):
 1. apply_operations xs = apply_operations (prefix @ suffix)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix
distinct (prefix @ suffix)
hb_consistent xs
hb_consistent (prefix @ suffix)
concurrent_ops_commute (prefix @ suffix @ [x])
concurrent_ops_commute (prefix @ suffix)
\<lbrakk>set xs = set ?ys1; concurrent_ops_commute xs; concurrent_ops_commute ?ys1; distinct xs; distinct ?ys1; hb_consistent xs; hb_consistent ?ys1\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ?ys1
set (xs @ [x]) = set ys
concurrent_ops_commute (xs @ [x])
concurrent_ops_commute ys
distinct (xs @ [x])
distinct ys
hb_consistent (xs @ [x])
hb_consistent ys

goal (1 subgoal):
 1. apply_operations xs = apply_operations (prefix @ suffix)
[PROOF STEP]
by simp (metis Diff_insert_absorb Un_iff * concurrent_ops_commute_appendD set_append)
[PROOF STATE]
proof (state)
this:
apply_operations xs = apply_operations (prefix @ suffix)

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
apply_operations xs = apply_operations (prefix @ suffix)

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
have "apply_operations (prefix@suffix @ [x]) = apply_operations (prefix@x # suffix)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_operations (prefix @ suffix @ [x]) = apply_operations (prefix @ x # suffix)
[PROOF STEP]
using ys_split assms ** concurrent_ops_commute_concurrent_set
[PROOF STATE]
proof (prove)
using this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix
\<lbrakk>set xs = set ?ys1; concurrent_ops_commute xs; concurrent_ops_commute ?ys1; distinct xs; distinct ?ys1; hb_consistent xs; hb_consistent ?ys1\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ?ys1
set (xs @ [x]) = set ys
concurrent_ops_commute (xs @ [x])
concurrent_ops_commute ys
distinct (xs @ [x])
distinct ys
hb_consistent (xs @ [x])
hb_consistent ys
concurrent_ops_commute (prefix @ suffix @ [x])
\<lbrakk>concurrent_ops_commute (?prefix @ ?suffix @ [?x]); concurrent_set ?x ?suffix; distinct (?prefix @ ?x # ?suffix)\<rbrakk> \<Longrightarrow> apply_operations (?prefix @ ?suffix @ [?x]) = apply_operations (?prefix @ ?x # ?suffix)

goal (1 subgoal):
 1. apply_operations (prefix @ suffix @ [x]) = apply_operations (prefix @ x # suffix)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
apply_operations (prefix @ suffix @ [x]) = apply_operations (prefix @ x # suffix)

goal (1 subgoal):
 1. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>set xs = set ys; concurrent_ops_commute xs; concurrent_ops_commute ys; distinct xs; distinct ys; hb_consistent xs; hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations xs = apply_operations ys; set (xs @ [x]) = set ys; concurrent_ops_commute (xs @ [x]); concurrent_ops_commute ys; distinct (xs @ [x]); distinct ys; hb_consistent (xs @ [x]); hb_consistent ys\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
apply_operations xs = apply_operations (prefix @ suffix)
apply_operations (prefix @ suffix @ [x]) = apply_operations (prefix @ x # suffix)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
apply_operations xs = apply_operations (prefix @ suffix)
apply_operations (prefix @ suffix @ [x]) = apply_operations (prefix @ x # suffix)

goal (1 subgoal):
 1. apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
using ys_split
[PROOF STATE]
proof (prove)
using this:
apply_operations xs = apply_operations (prefix @ suffix)
apply_operations (prefix @ suffix @ [x]) = apply_operations (prefix @ x # suffix)
ys = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. apply_operations (xs @ [x]) = apply_operations ys
[PROOF STEP]
by (force simp: append_assoc[symmetric] simp del: append_assoc)
[PROOF STATE]
proof (state)
this:
apply_operations (xs @ [x]) = apply_operations ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem sec_convergence:
  assumes "set xs = set ys"
          "op_history xs"
          "op_history ys"
  shows   "apply_operations xs = apply_operations ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_operations xs = apply_operations ys
[PROOF STEP]
by (meson assms convergence causality commutativity distinctness)


[STATEMENT]
theorem sec_progress:
  assumes "op_history xs"
  shows   "apply_operations xs initial_state \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_operations xs initial_state \<noteq> None
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
op_history xs

goal (1 subgoal):
 1. apply_operations xs initial_state \<noteq> None
[PROOF STEP]
proof(induction xs rule: rev_induct, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>op_history xs \<Longrightarrow> apply_operations xs initial_state \<noteq> None; op_history (xs @ [x])\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) initial_state \<noteq> None
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
op_history xs \<Longrightarrow> apply_operations xs initial_state \<noteq> None
op_history (xs @ [x])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>op_history xs \<Longrightarrow> apply_operations xs initial_state \<noteq> None; op_history (xs @ [x])\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) initial_state \<noteq> None
[PROOF STEP]
have "apply_operations xs initial_state \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_operations xs initial_state \<noteq> None
[PROOF STEP]
using snoc.IH snoc.prems trunc_history kleisli_def bind_def
[PROOF STATE]
proof (prove)
using this:
op_history xs \<Longrightarrow> apply_operations xs initial_state \<noteq> None
op_history (xs @ [x])
op_history (?xs @ [?x]) \<Longrightarrow> op_history ?xs
?f \<rhd> ?g \<equiv> \<lambda>x. ?f x \<bind> ?g
?P \<bind> ?f = Sup (?f ` {x. pred.eval ?P x})

goal (1 subgoal):
 1. apply_operations xs initial_state \<noteq> None
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
apply_operations xs initial_state \<noteq> None

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>op_history xs \<Longrightarrow> apply_operations xs initial_state \<noteq> None; op_history (xs @ [x])\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) initial_state \<noteq> None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
apply_operations xs initial_state \<noteq> None

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>op_history xs \<Longrightarrow> apply_operations xs initial_state \<noteq> None; op_history (xs @ [x])\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) initial_state \<noteq> None
[PROOF STEP]
have "apply_operations (xs @ [x]) = apply_operations xs \<rhd> \<langle>x\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_operations (xs @ [x]) = apply_operations xs \<rhd> \<langle>x\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_operations (xs @ [x]) = apply_operations xs \<rhd> \<langle>x\<rangle>

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>op_history xs \<Longrightarrow> apply_operations xs initial_state \<noteq> None; op_history (xs @ [x])\<rbrakk> \<Longrightarrow> apply_operations (xs @ [x]) initial_state \<noteq> None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
apply_operations xs initial_state \<noteq> None
apply_operations (xs @ [x]) = apply_operations xs \<rhd> \<langle>x\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
apply_operations xs initial_state \<noteq> None
apply_operations (xs @ [x]) = apply_operations xs \<rhd> \<langle>x\<rangle>

goal (1 subgoal):
 1. apply_operations (xs @ [x]) initial_state \<noteq> None
[PROOF STEP]
using no_failure snoc.prems
[PROOF STATE]
proof (prove)
using this:
apply_operations xs initial_state \<noteq> None
apply_operations (xs @ [x]) = apply_operations xs \<rhd> \<langle>x\<rangle>
\<lbrakk>op_history (?xs @ [?x]); apply_operations ?xs initial_state = Some ?state\<rbrakk> \<Longrightarrow> \<langle>?x\<rangle> ?state \<noteq> None
op_history (xs @ [x])

goal (1 subgoal):
 1. apply_operations (xs @ [x]) initial_state \<noteq> None
[PROOF STEP]
by (clarsimp simp add: kleisli_def split: bind_splits)
[PROOF STATE]
proof (state)
this:
apply_operations (xs @ [x]) initial_state \<noteq> None

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interval_less_to_le_low [forward]:
  "(a::('a::linorder idx_interval)) < b \<Longrightarrow> low (int a) \<le> low (int b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < b \<Longrightarrow> low (idx_interval.int a) \<le> low (idx_interval.int b)
[PROOF STEP]
by (metis eq_iff iint_less int_less less_imp_le)


[STATEMENT]
lemma True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
nitpick[satisfy]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
oops \<comment> \<open>model found: axioms are consistent\<close>


[STATEMENT]
lemma "\<lfloor>D\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<box>x \<^bold>\<rightarrow> \<^bold>\<diamond>x) w)\<rfloor>
[PROOF STEP]
using A1a A1b A2
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<P> (\<rightharpoondown>x) \<^bold>\<rightarrow> \<^bold>\<not>\<P> x) w)\<rfloor>
\<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<P> (\<rightharpoondown>x)) w)\<rfloor>
\<lfloor>(\<lambda>w. universal (\<lambda>x xa. (\<P> x \<^bold>\<and> \<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb \<longrightarrow> xa xb) \<^bold>\<rightarrow> \<P> xa) w))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<box>x \<^bold>\<rightarrow> \<^bold>\<diamond>x) w)\<rfloor>
[PROOF STEP]
by blast \<comment> \<open>axioms already imply \emph{D} axiom\<close>


[STATEMENT]
lemma GodDefsAreEquivalent: "\<lfloor>\<^bold>\<forall>x. G x \<^bold>\<leftrightarrow> G* x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. \<P> xa w \<longrightarrow> xa x) = (\<forall>xa. \<P> xa w = xa x))\<rfloor>
[PROOF STEP]
using A1b
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<P> (\<rightharpoondown>x)) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. \<P> xa w \<longrightarrow> xa x) = (\<forall>xa. \<P> xa w = xa x))\<rfloor>
[PROOF STEP]
by fastforce


[STATEMENT]
theorem T1a: "\<lfloor>\<^bold>\<forall>X::\<langle>\<zero>\<rangle>. \<P> X \<^bold>\<rightarrow> \<^bold>\<diamond>(\<^bold>\<exists>\<^sup>Ez. \<lparr>X z\<rparr>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<diamond>(\<lambda>v. \<exists>xa. existsAt xa v \<and> x xa)) w)\<rfloor>
[PROOF STEP]
using A1a A2
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<P> (\<rightharpoondown>x) \<^bold>\<rightarrow> \<^bold>\<not>\<P> x) w)\<rfloor>
\<lfloor>(\<lambda>w. universal (\<lambda>x xa. (\<P> x \<^bold>\<and> \<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb \<longrightarrow> xa xb) \<^bold>\<rightarrow> \<P> xa) w))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<diamond>(\<lambda>v. \<exists>xa. existsAt xa v \<and> x xa)) w)\<rfloor>
[PROOF STEP]
by blast \<comment> \<open>this is the one used in the book\<close>


[STATEMENT]
theorem T1b: "\<lfloor>\<^bold>\<forall>X::\<up>\<langle>\<zero>\<rangle>. \<P> \<down>X \<^bold>\<rightarrow> \<^bold>\<diamond>(\<^bold>\<exists>\<^sup>Ez. X z)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<P> \<down> x \<^bold>\<rightarrow> \<^bold>\<diamond>mexistsActB x) w)\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<P> \<down> x \<^bold>\<rightarrow> \<^bold>\<diamond>mexistsActB x) w)\<rfloor>
[PROOF STEP]
oops \<comment> \<open>this one is also possible but not valid so we won't use it\<close>


[STATEMENT]
lemma "\<lfloor>\<^bold>\<box>\<^bold>\<exists>\<^sup>E (Q::\<up>\<langle>\<zero>\<rangle>) \<^bold>\<leftrightarrow> ((\<lambda>X. \<^bold>\<box>\<^bold>\<exists>\<^sup>E X) Q)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<^bold>\<box>mexistsActB Q) w = (\<^bold>\<box>mexistsActB Q) w)\<rfloor>
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<lfloor>\<^bold>\<box>\<^bold>\<exists>\<^sup>E (Q::\<up>\<langle>\<zero>\<rangle>) \<^bold>\<leftrightarrow> ((\<lambda>X. \<^bold>\<box>\<^bold>\<exists>\<^sup>E \<^bold>\<down>X) Q)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<^bold>\<box>mexistsActB Q) w = (\<^bold>\<box>mexistsActB Q) w)\<rfloor>
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<lfloor>\<^bold>\<box>\<^bold>\<exists>\<^sup>E (Q::\<up>\<langle>\<zero>\<rangle>) \<^bold>\<leftrightarrow> ((\<lambda>X. \<^bold>\<box>\<^bold>\<exists>\<^sup>E X) \<^bold>\<down>Q)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<^bold>\<box>mexistsActB Q) w = (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> Q x w)) w)\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<^bold>\<box>mexistsActB Q) w = (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> Q x w)) w)\<rfloor>
[PROOF STEP]
oops \<comment> \<open>not equivalent!\<close>


[STATEMENT]
theorem T3_deRe: "\<lfloor>(\<lambda>X. \<^bold>\<diamond>\<^bold>\<exists>\<^sup>E X) \<^bold>\<down>G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)))
[PROOF STEP]
using T1a T2
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<diamond>(\<lambda>v. \<exists>xa. existsAt xa v \<and> x xa)) w)\<rfloor>
\<lfloor>(\<lambda>w. \<P> (\<lambda>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) w)\<rfloor>

goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)))
[PROOF STEP]
by simp


[STATEMENT]
theorem T3_deDicto: "\<lfloor>\<^bold>\<diamond>\<^bold>\<exists>\<^sup>E \<^bold>\<down>G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x)))
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x)))
[PROOF STEP]
oops    \<comment> \<open>countersatisfiable\<close>


[STATEMENT]
lemma assumes T1b: "\<lfloor>\<^bold>\<forall>X. \<P> \<down>X \<^bold>\<rightarrow> \<^bold>\<diamond>(\<^bold>\<exists>\<^sup>Ez. X z)\<rfloor>"
   shows T3_deDicto: "\<lfloor>\<^bold>\<diamond>\<^bold>\<exists>\<^sup>E \<^bold>\<down>G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x)))
[PROOF STEP]
using assms T2
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<P> \<down> x \<^bold>\<rightarrow> \<^bold>\<diamond>mexistsActB x) w)\<rfloor>
\<lfloor>(\<lambda>w. \<P> (\<lambda>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) w)\<rfloor>

goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x)))
[PROOF STEP]
by simp


[STATEMENT]
lemma A4b: "\<lfloor>\<^bold>\<forall>X. \<^bold>\<not>(\<P> X) \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<not>(\<P> X)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<not>\<P> x) w)\<rfloor>
[PROOF STEP]
using A1a A1b A4a
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<P> (\<rightharpoondown>x) \<^bold>\<rightarrow> \<^bold>\<not>\<P> x) w)\<rfloor>
\<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<P> (\<rightharpoondown>x)) w)\<rfloor>
\<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<P> x) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<not>\<P> x) w)\<rfloor>
[PROOF STEP]
by blast


[STATEMENT]
lemma True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
nitpick[satisfy]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
oops \<comment> \<open>model found: so far all axioms consistent\<close>


[STATEMENT]
theorem GodIsEssential: "\<lfloor>\<^bold>\<forall>x. G x \<^bold>\<rightarrow> ((\<E> \<down>\<^sub>1G) x)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<and> (\<forall>xa. xa x \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> xa x)) w))\<rfloor>
[PROOF STEP]
using A1b
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<P> (\<rightharpoondown>x)) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<and> (\<forall>xa. xa x \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> xa x)) w))\<rfloor>
[PROOF STEP]
by metis


[STATEMENT]
theorem God_starIsEssential: "\<lfloor>\<^bold>\<forall>x. G* x \<^bold>\<rightarrow> ((\<E> \<down>\<^sub>1G*) x)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. \<P> xa w = xa x) \<longrightarrow> (\<forall>xa. \<P> xa w = xa x) \<and> (\<forall>xa. xa x \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. \<P> xa w = xa x) \<longrightarrow> xa x)) w))\<rfloor>
[PROOF STEP]
by meson


[STATEMENT]
lemma "\<lfloor>\<^bold>\<exists> G \<^bold>\<leftrightarrow> \<^bold>\<exists> \<^bold>\<down>G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) = (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x))\<rfloor>
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<lfloor>\<^bold>\<exists>\<^sup>E G \<^bold>\<leftrightarrow> \<^bold>\<exists>\<^sup>E \<^bold>\<down>G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. existsAt x w \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)) = (\<exists>x. existsAt x w \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)))\<rfloor>
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<lfloor>\<^bold>\<box>\<^bold>\<exists>\<^sup>E G \<^bold>\<leftrightarrow>  \<^bold>\<box>\<^bold>\<exists>\<^sup>E \<^bold>\<down>G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w = (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
by simp


[STATEMENT]
theorem GodExImpliesNecEx_v1: "\<lfloor>\<^bold>\<exists> \<^bold>\<down>G \<^bold>\<rightarrow>  \<^bold>\<box>\<^bold>\<exists>\<^sup>E \<^bold>\<down>G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
assume "\<exists>x. G x w"
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x
[PROOF STEP]
obtain g where 1: "G g w"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x

goal (1 subgoal):
 1. (\<And>g. \<forall>x. \<P> x w \<longrightarrow> x g \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<forall>x. \<P> x w \<longrightarrow> x g

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
hence "NE g w"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. \<P> x w \<longrightarrow> x g

goal (1 subgoal):
 1. \<forall>x. x g \<and> (\<forall>xa. xa g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb \<longrightarrow> xa xb)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>xa. existsAt xa v \<and> x xa)) w
[PROOF STEP]
using A5
[PROOF STATE]
proof (prove)
using this:
\<forall>x. \<P> x w \<longrightarrow> x g
\<lfloor>(\<lambda>w. \<P> (\<lambda>x. \<forall>xa. xa x \<and> (\<forall>xb. xb x \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> xa x \<longrightarrow> xb x)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> xa x)) w) w)\<rfloor>

goal (1 subgoal):
 1. \<forall>x. x g \<and> (\<forall>xa. xa g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb \<longrightarrow> xa xb)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>xa. existsAt xa v \<and> x xa)) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. x g \<and> (\<forall>xa. xa g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb \<longrightarrow> xa xb)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>xa. existsAt xa v \<and> x xa)) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
hence "\<forall>Y. (\<E> Y g w) \<longrightarrow> (\<^bold>\<box>(\<^bold>\<exists>\<^sup>Ez. \<lparr>Y z\<rparr>)) w"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x g \<and> (\<forall>xa. xa g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb \<longrightarrow> xa xb)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>xa. existsAt xa v \<and> x xa)) w

goal (1 subgoal):
 1. \<forall>Y. Y g \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> Y xa \<longrightarrow> x xa)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> Y x)) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>Y. Y g \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> Y xa \<longrightarrow> x xa)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> Y x)) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
hence "(\<E> (\<lambda>x. G x w) g w) \<longrightarrow> (\<^bold>\<box>(\<^bold>\<exists>\<^sup>Ez. \<lparr>(\<lambda>x. G x w) z\<rparr>)) w"
[PROOF STATE]
proof (prove)
using this:
\<forall>Y. Y g \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> Y xa \<longrightarrow> x xa)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> Y x)) w

goal (1 subgoal):
 1. (\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) w
[PROOF STEP]
by (rule allE)
[PROOF STATE]
proof (state)
this:
(\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
hence 2: "((\<E> \<down>\<^sub>1G) g w) \<longrightarrow> (\<^bold>\<box>(\<^bold>\<exists>\<^sup>E G)) w"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) w

goal (1 subgoal):
 1. (\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w
[PROOF STEP]
using A4b
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) w
\<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<not>\<P> x) w)\<rfloor>

goal (1 subgoal):
 1. (\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
(\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
have  "(\<^bold>\<forall>x. G x \<^bold>\<rightarrow> ((\<E> \<down>\<^sub>1G) x)) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<and> (\<forall>xa. xa x \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> xa x)) w)
[PROOF STEP]
using GodIsEssential
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<and> (\<forall>xa. xa x \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> xa x)) w))\<rfloor>

goal (1 subgoal):
 1. \<forall>x. (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<and> (\<forall>xa. xa x \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> xa x)) w)
[PROOF STEP]
by (rule allE)
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<and> (\<forall>xa. xa x \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> xa x)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
hence  "(G g \<^bold>\<rightarrow> ((\<E> \<down>\<^sub>1G) g)) w"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<and> (\<forall>xa. xa x \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> xa x)) w)

goal (1 subgoal):
 1. (\<forall>x. \<P> x w \<longrightarrow> x g) \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w)
[PROOF STEP]
by (rule allE)
[PROOF STATE]
proof (state)
this:
(\<forall>x. \<P> x w \<longrightarrow> x g) \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
hence  "G g w \<longrightarrow> (\<E> \<down>\<^sub>1G) g w"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. \<P> x w \<longrightarrow> x g) \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w)

goal (1 subgoal):
 1. (\<forall>x. \<P> x w \<longrightarrow> x g) \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>x. \<P> x w \<longrightarrow> x g) \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
from this 1
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x. \<P> x w \<longrightarrow> x g) \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w)
\<forall>x. \<P> x w \<longrightarrow> x g
[PROOF STEP]
have 3: "(\<E> \<down>\<^sub>1G) g w"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. \<P> x w \<longrightarrow> x g) \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w)
\<forall>x. \<P> x w \<longrightarrow> x g

goal (1 subgoal):
 1. (\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w)
[PROOF STEP]
by (rule mp)
[PROOF STATE]
proof (state)
this:
(\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
from 2 3
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w
(\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w)
[PROOF STEP]
have "(\<^bold>\<box>\<^bold>\<exists>\<^sup>E G) w"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w
(\<forall>x. \<P> x w \<longrightarrow> x g) \<and> (\<forall>x. x g \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. \<P> x w \<longrightarrow> x xa) \<longrightarrow> x xa)) w)

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w
[PROOF STEP]
by (rule mp)
[PROOF STATE]
proof (state)
this:
(\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x \<Longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
hence "(\<exists>x. G x w) \<longrightarrow> (\<^bold>\<box>\<^bold>\<exists>\<^sup>E G) w"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x \<Longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w

goal (1 subgoal):
 1. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w
[PROOF STEP]
by (rule impI)
[PROOF STATE]
proof (state)
this:
(\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
hence "((\<^bold>\<exists>x. G x) \<^bold>\<rightarrow>  \<^bold>\<box>\<^bold>\<exists>\<^sup>E G) w"
[PROOF STATE]
proof (prove)
using this:
(\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w

goal (1 subgoal):
 1. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(\<exists>x. \<forall>xa. \<P> xa ?w2 \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) ?w2

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>x. \<forall>xa. \<P> xa ?w2 \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) ?w2

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
by (rule allI)
[PROOF STATE]
proof (state)
this:
\<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem GodExImpliesNecEx_v2: "\<lfloor>\<^bold>\<exists> \<^bold>\<down>G \<^bold>\<rightarrow> ((\<lambda>X. \<^bold>\<box>\<^bold>\<exists>\<^sup>E X) \<^bold>\<down>G)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
using A4a GodExImpliesNecEx_v1
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<P> x) w)\<rfloor>
\<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
by metis


[STATEMENT]
theorem possExImpliesNecEx_v1: "\<lfloor>\<^bold>\<diamond>\<^bold>\<exists> \<^bold>\<down>G \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<exists>\<^sup>E \<^bold>\<down>G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. \<P> xa v \<longrightarrow> xa x) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))\<rfloor>
[PROOF STEP]
using GodExImpliesNecEx_v1 T3_deRe
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)))

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. \<P> xa v \<longrightarrow> xa x) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))\<rfloor>
[PROOF STEP]
by metis


[STATEMENT]
theorem possExImpliesNecEx_v2: "\<lfloor>(\<lambda>X. \<^bold>\<diamond>\<^bold>\<exists>\<^sup>E X) \<^bold>\<down>G \<^bold>\<rightarrow> ((\<lambda>X. \<^bold>\<box>\<^bold>\<exists>\<^sup>E X) \<^bold>\<down>G)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<^bold>\<diamond>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
using GodExImpliesNecEx_v2
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<^bold>\<diamond>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) w)\<rfloor>
[PROOF STEP]
by blast


[STATEMENT]
lemma T4_v1:  "\<lfloor>\<^bold>\<diamond>\<^bold>\<exists> \<^bold>\<down>G\<rfloor> \<longrightarrow> \<lfloor>\<^bold>\<box>\<^bold>\<exists>\<^sup>E \<^bold>\<down>G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. \<forall>xa. \<P> xa v \<longrightarrow> xa x)) \<longrightarrow> universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x)))
[PROOF STEP]
using possExImpliesNecEx_v1
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. \<P> xa v \<longrightarrow> xa x) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))\<rfloor>

goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. \<forall>xa. \<P> xa v \<longrightarrow> xa x)) \<longrightarrow> universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x)))
[PROOF STEP]
by simp


[STATEMENT]
lemma T4_v2:  "\<lfloor>(\<lambda>X. \<^bold>\<diamond>\<^bold>\<exists>\<^sup>E X) \<^bold>\<down>G\<rfloor> \<longrightarrow> \<lfloor>(\<lambda>X. \<^bold>\<box>\<^bold>\<exists>\<^sup>E X) \<^bold>\<down>G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) \<longrightarrow> universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)))
[PROOF STEP]
using possExImpliesNecEx_v2
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. (\<^bold>\<diamond>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) w)\<rfloor>

goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) \<longrightarrow> universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)))
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<lfloor>\<^bold>\<box>(\<lambda>X. \<^bold>\<exists>\<^sup>E X) \<^bold>\<down>G*\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v = xa x)))
[PROOF STEP]
using God_starNecExists_v1
[PROOF STATE]
proof (prove)
using this:
universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v = xa x)))

goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v = xa x)))
[PROOF STEP]
by simp \<comment> \<open>\emph{de dicto} shown here explicitly\<close>


[STATEMENT]
lemma GodNecExists_v2: "\<lfloor>(\<lambda>X. \<^bold>\<box>\<^bold>\<exists>\<^sup>E X) \<^bold>\<down>G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)))
[PROOF STEP]
using T3_deRe T4_v2
[PROOF STATE]
proof (prove)
using this:
serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)))
serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x))) \<longrightarrow> universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)))

goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)))
[PROOF STEP]
by blast


[STATEMENT]
lemma God_starNecExists_v2: "\<lfloor>(\<lambda>X. \<^bold>\<box>\<^bold>\<exists>\<^sup>E X) \<^bold>\<down>G*\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w = xa x)))
[PROOF STEP]
using GodNecExists_v2 GodDefsAreEquivalent
[PROOF STATE]
proof (prove)
using this:
universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)))
\<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. \<P> xa w \<longrightarrow> xa x) = (\<forall>xa. \<P> xa w = xa x))\<rfloor>

goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w = xa x)))
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<lfloor>\<^bold>\<forall>\<Phi>.(\<Phi> \<^bold>\<rightarrow> (\<^bold>\<box> \<Phi>))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
nitpick[card 't=1, card i=2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
oops \<comment> \<open>countermodel found in \emph{K}\<close>


[STATEMENT]
lemma "\<lfloor>\<^bold>\<forall>\<Phi>.(\<Phi> \<^bold>\<rightarrow> (\<^bold>\<box> \<Phi>))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
nitpick[card 't=1, card i=2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
oops \<comment> \<open>countermodel also found in \emph{S5}\<close>


[STATEMENT]
lemma Z_eq_Z': "Z = Z'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Z = Z'
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
have [simp]: "\<And>x. pmf_of_set {(True, undefined), (False, undefined)} \<noteq> return_pmf x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. pmf_of_set {(True, undefined), (False, undefined)} \<noteq> return_pmf x
[PROOF STEP]
by (auto simp: pmf_eq_iff split: split_indicator)
[PROOF STATE]
proof (state)
this:
pmf_of_set {(True, undefined), (False, undefined)} \<noteq> return_pmf ?x

goal (1 subgoal):
 1. False
[PROOF STEP]
have [simp]: "\<And>x. binsert (True, undefined) (binsert (False, undefined) bempty) \<noteq> bsingleton x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. binsert (True, undefined) (binsert (False, undefined) bempty) \<noteq> bsingleton x
[PROOF STEP]
unfolding bsingleton_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. binsert (True, undefined) (binsert (False, undefined) bempty) \<noteq> binsert x bempty
[PROOF STEP]
by transfer auto
[PROOF STATE]
proof (state)
this:
binsert (True, undefined) (binsert (False, undefined) bempty) \<noteq> bsingleton ?x1

goal (1 subgoal):
 1. False
[PROOF STEP]
define R where "R a b = b" for a b :: bool
[PROOF STATE]
proof (state)
this:
R ?a ?b = ?b

goal (1 subgoal):
 1. False
[PROOF STEP]
have "rel_var R (=) X Z'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_var R (=) X Z'
[PROOF STEP]
unfolding R_def var.in_rel mem_Collect_eq subset_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z. ((\<forall>(a, b)\<in>set1_var z. b) \<and> (\<forall>(x, y)\<in>set2_var z. x = y)) \<and> map_var fst fst z = X \<and> map_var snd snd z = Z'
[PROOF STEP]
apply (intro exI[of _ C])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>(a, b)\<in>set1_var C. b) \<and> (\<forall>(x, y)\<in>set2_var C. x = y)) \<and> map_var fst fst C = X \<and> map_var snd snd C = Z'
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>(a, b)\<in>set1_var0 (BPS (binsert ((True, True), undefined, undefined) (binsert ((False, True), undefined, undefined) bempty))). b) \<and> (\<forall>(x, y)\<in>set2_var0 (BPS (binsert ((True, True), undefined, undefined) (binsert ((False, True), undefined, undefined) bempty))). x = y)) \<and> map_var0 fst fst (BPS (binsert ((True, True), undefined, undefined) (binsert ((False, True), undefined, undefined) bempty))) \<sim> BPS (binsert (True, undefined) (binsert (False, undefined) bempty)) \<and> map_var0 snd snd (BPS (binsert ((True, True), undefined, undefined) (binsert ((False, True), undefined, undefined) bempty))) \<sim> BPS (bsingleton (True, undefined))
[PROOF STEP]
apply (auto simp: set_bset binsert.rep_eq fsts.simps snds.simps bempty.rep_eq bsingleton_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rel_var R (=) X Z'

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rel_var R (=) X Z'

goal (1 subgoal):
 1. False
[PROOF STEP]
define S where "S a b = a" for a b :: bool
[PROOF STATE]
proof (state)
this:
S ?a ?b = ?a

goal (1 subgoal):
 1. False
[PROOF STEP]
have "rel_var S (=) Z Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_var S (=) Z Y
[PROOF STEP]
unfolding S_def var.in_rel mem_Collect_eq subset_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z. ((\<forall>(a, b)\<in>set1_var z. a) \<and> (\<forall>(x, y)\<in>set2_var z. x = y)) \<and> map_var fst fst z = Z \<and> map_var snd snd z = Y
[PROOF STEP]
apply (intro exI[of _ C'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>(a, b)\<in>set1_var C'. a) \<and> (\<forall>(x, y)\<in>set2_var C'. x = y)) \<and> map_var fst fst C' = Z \<and> map_var snd snd C' = Y
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>(a, b)\<in>set1_var0 (PMF (map_pmf (\<lambda>((a, b), c, d). ((a, c), b, d)) (pair_pmf (return_pmf (True, undefined)) (pmf_of_set {(True, undefined), (False, undefined)})))). a) \<and> (\<forall>(x, y)\<in>set2_var0 (PMF (map_pmf (\<lambda>((a, b), c, d). ((a, c), b, d)) (pair_pmf (return_pmf (True, undefined)) (pmf_of_set {(True, undefined), (False, undefined)})))). x = y)) \<and> map_var0 fst fst (PMF (map_pmf (\<lambda>((a, b), c, d). ((a, c), b, d)) (pair_pmf (return_pmf (True, undefined)) (pmf_of_set {(True, undefined), (False, undefined)})))) \<sim> PMF (return_pmf (True, undefined)) \<and> map_var0 snd snd (PMF (map_pmf (\<lambda>((a, b), c, d). ((a, c), b, d)) (pair_pmf (return_pmf (True, undefined)) (pmf_of_set {(True, undefined), (False, undefined)})))) \<sim> PMF (pmf_of_set {(True, undefined), (False, undefined)})
[PROOF STEP]
apply (auto simp: fsts.simps snds.simps pmf.map_comp comp_def split_beta map_fst_pair_pmf map_snd_pair_pmf)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rel_var S (=) Z Y

goal (1 subgoal):
 1. False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rel_var R (=) X Z'
rel_var S (=) Z Y
[PROOF STEP]
have "rel_var (R OO S) ((=) OO (=)) X Y" (is "rel_var ?R ?S X Y")
[PROOF STATE]
proof (prove)
using this:
rel_var R (=) X Z'
rel_var S (=) Z Y

goal (1 subgoal):
 1. rel_var (R OO S) ((=) OO (=)) X Y
[PROOF STEP]
unfolding var.rel_compp
[PROOF STATE]
proof (prove)
using this:
rel_var R (=) X Z'
rel_var S (=) Z Y

goal (1 subgoal):
 1. (rel_var R (=) OO rel_var S (=)) X Y
[PROOF STEP]
unfolding Z_eq_Z'
[PROOF STATE]
proof (prove)
using this:
rel_var R (=) X Z'
rel_var S (=) Z' Y

goal (1 subgoal):
 1. (rel_var R (=) OO rel_var S (=)) X Y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_var (R OO S) ((=) OO (=)) X Y

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rel_var (R OO S) ((=) OO (=)) X Y

goal (1 subgoal):
 1. False
[PROOF STEP]
have "\<not> rel_var ?R ?S X Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> rel_var (R OO S) ((=) OO (=)) X Y
[PROOF STEP]
unfolding var.in_rel mem_Collect_eq subset_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>z. ((\<forall>(x, y)\<in>set1_var z. (R OO S) x y) \<and> (\<forall>(x, y)\<in>set2_var z. ((=) OO (=)) x y)) \<and> map_var fst fst z = X \<and> map_var snd snd z = Y
[PROOF STEP]
apply (auto simp: split_beta)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>map_var fst fst z = X; \<forall>x\<in>set1_var z. (R OO S) (fst x) (snd x); \<forall>x\<in>set2_var z. ((=) OO (=)) (fst x) (snd x); map_var snd snd z = Y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply transfer'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z R S. \<lbrakk>map_var0 fst fst z \<sim> BPS (binsert (True, undefined) (binsert (False, undefined) bempty)); \<forall>x\<in>set1_var0 z. (R OO S) (fst x) (snd x); \<forall>x\<in>set2_var0 z. ((=) OO (=)) (fst x) (snd x); map_var0 snd snd z \<sim> PMF (pmf_of_set {(True, undefined), (False, undefined)})\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto elim!: var_eq.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z R S. \<lbrakk>\<forall>x\<in>set1_var0 z. (R OO S) (fst x) (snd x); \<forall>x\<in>set2_var0 z. ((=) OO (=)) (fst x) (snd x); BPS (binsert (True, undefined) (binsert (False, undefined) bempty)) = map_var0 fst fst z; PMF (pmf_of_set {(True, undefined), (False, undefined)}) = map_var0 snd snd z\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (case_tac [!] z)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z R S x1. \<lbrakk>\<forall>x\<in>set1_var0 z. (R OO S) (fst x) (snd x); \<forall>x\<in>set2_var0 z. ((=) OO (=)) (fst x) (snd x); BPS (binsert (True, undefined) (binsert (False, undefined) bempty)) = map_var0 fst fst z; PMF (pmf_of_set {(True, undefined), (False, undefined)}) = map_var0 snd snd z; z = PMF x1\<rbrakk> \<Longrightarrow> False
 2. \<And>z R S x2. \<lbrakk>\<forall>x\<in>set1_var0 z. (R OO S) (fst x) (snd x); \<forall>x\<in>set2_var0 z. ((=) OO (=)) (fst x) (snd x); BPS (binsert (True, undefined) (binsert (False, undefined) bempty)) = map_var0 fst fst z; PMF (pmf_of_set {(True, undefined), (False, undefined)}) = map_var0 snd snd z; z = BPS x2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto simp add: snds.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<not> rel_var (R OO S) ((=) OO (=)) X Y

goal (1 subgoal):
 1. False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rel_var (R OO S) ((=) OO (=)) X Y
\<not> rel_var (R OO S) ((=) OO (=)) X Y
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
rel_var (R OO S) ((=) OO (=)) X Y
\<not> rel_var (R OO S) ((=) OO (=)) X Y

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_eqI':
  assumes "\<And>x. x \<in> A \<Longrightarrow> x \<in> B"
  assumes "\<And>x. x \<in> B \<Longrightarrow> x \<in> A"
  shows "A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> ?x \<in> B
?x \<in> B \<Longrightarrow> ?x \<in> A

goal (1 subgoal):
 1. A = B
[PROOF STEP]
by auto


[STATEMENT]
lemma comp_image:
  "((`) f \<circ> (`) g) = (`) (f o g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (`) f \<circ> (`) g = (`) (f \<circ> g)
[PROOF STEP]
by rule auto


[STATEMENT]
lemma partition_onI:
  assumes "\<And>p. p \<in> P \<Longrightarrow> p \<noteq> {}"
  assumes "\<Union>P = A"
  assumes "\<And>p p'. p \<in> P \<Longrightarrow> p' \<in> P \<Longrightarrow> p \<noteq> p' \<Longrightarrow> p \<inter> p' = {}"
  shows "partition_on A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on A P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?p \<in> P \<Longrightarrow> ?p \<noteq> {}
\<Union> P = A
\<lbrakk>?p \<in> P; ?p' \<in> P; ?p \<noteq> ?p'\<rbrakk> \<Longrightarrow> ?p \<inter> ?p' = {}

goal (1 subgoal):
 1. partition_on A P
[PROOF STEP]
unfolding partition_on_def disjoint_def
[PROOF STATE]
proof (prove)
using this:
?p \<in> P \<Longrightarrow> ?p \<noteq> {}
\<Union> P = A
\<lbrakk>?p \<in> P; ?p' \<in> P; ?p \<noteq> ?p'\<rbrakk> \<Longrightarrow> ?p \<inter> ?p' = {}

goal (1 subgoal):
 1. \<Union> P = A \<and> (\<forall>a\<in>P. \<forall>b\<in>P. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> {} \<notin> P
[PROOF STEP]
by blast


[STATEMENT]
lemma partition_onE:
  assumes "partition_on A P"
  obtains "\<And>p. p \<in> P \<Longrightarrow> p \<noteq> {}"
     "\<Union>P = A"
     "\<And>p p'. p \<in> P \<Longrightarrow> p' \<in> P \<Longrightarrow> p \<noteq> p' \<Longrightarrow> p \<inter> p' = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<And>p. p \<in> P \<Longrightarrow> p \<noteq> {}; \<Union> P = A; \<And>p p'. \<lbrakk>p \<in> P; p' \<in> P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
partition_on A P

goal (1 subgoal):
 1. (\<lbrakk>\<And>p. p \<in> P \<Longrightarrow> p \<noteq> {}; \<Union> P = A; \<And>p p'. \<lbrakk>p \<in> P; p' \<in> P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding partition_on_def disjoint_def
[PROOF STATE]
proof (prove)
using this:
\<Union> P = A \<and> (\<forall>a\<in>P. \<forall>b\<in>P. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> {} \<notin> P

goal (1 subgoal):
 1. (\<lbrakk>\<And>p. p \<in> P \<Longrightarrow> p \<noteq> {}; \<Union> P = A; \<And>p p'. \<lbrakk>p \<in> P; p' \<in> P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma partition_onD4: "partition_on A P \<Longrightarrow> p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> x \<in> p \<Longrightarrow> x \<in> q \<Longrightarrow> p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partition_on A P; p \<in> P; q \<in> P; x \<in> p; x \<in> q\<rbrakk> \<Longrightarrow> p = q
[PROOF STEP]
by (auto simp: partition_on_def disjoint_def)


[STATEMENT]
lemma partition_subset_imp_notin:
  assumes "partition_on A P" "X \<in> P"
  assumes "X' \<subset> X"
  shows "X' \<notin> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' \<notin> P
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X' \<in> P \<Longrightarrow> False
[PROOF STEP]
assume "X' \<in> P"
[PROOF STATE]
proof (state)
this:
X' \<in> P

goal (1 subgoal):
 1. X' \<in> P \<Longrightarrow> False
[PROOF STEP]
from \<open>X' \<in> P\<close> \<open>partition_on A P\<close>
[PROOF STATE]
proof (chain)
picking this:
X' \<in> P
partition_on A P
[PROOF STEP]
have "X' \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
X' \<in> P
partition_on A P

goal (1 subgoal):
 1. X' \<noteq> {}
[PROOF STEP]
using partition_onD3
[PROOF STATE]
proof (prove)
using this:
X' \<in> P
partition_on A P
partition_on ?A ?P \<Longrightarrow> {} \<notin> ?P

goal (1 subgoal):
 1. X' \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X' \<noteq> {}

goal (1 subgoal):
 1. X' \<in> P \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X' \<noteq> {}

goal (1 subgoal):
 1. X' \<in> P \<Longrightarrow> False
[PROOF STEP]
from \<open>X' \<in> P\<close> \<open>X \<in> P\<close> \<open>partition_on A P\<close> \<open>X' \<subset> X\<close>
[PROOF STATE]
proof (chain)
picking this:
X' \<in> P
X \<in> P
partition_on A P
X' \<subset> X
[PROOF STEP]
have "disjnt X X'"
[PROOF STATE]
proof (prove)
using this:
X' \<in> P
X \<in> P
partition_on A P
X' \<subset> X

goal (1 subgoal):
 1. disjnt X X'
[PROOF STEP]
by (metis disjnt_def disjointD inf.strict_order_iff partition_onD2)
[PROOF STATE]
proof (state)
this:
disjnt X X'

goal (1 subgoal):
 1. X' \<in> P \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
disjnt X X'

goal (1 subgoal):
 1. X' \<in> P \<Longrightarrow> False
[PROOF STEP]
note \<open>X' \<subset> X\<close>
[PROOF STATE]
proof (state)
this:
X' \<subset> X

goal (1 subgoal):
 1. X' \<in> P \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X' \<noteq> {}
disjnt X X'
X' \<subset> X
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
X' \<noteq> {}
disjnt X X'
X' \<subset> X

goal (1 subgoal):
 1. False
[PROOF STEP]
by (meson all_not_in_conv disjnt_iff psubsetD)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_Diff:
  assumes P: "partition_on A P" shows "Q \<subseteq> P \<Longrightarrow> partition_on (A - \<Union>Q) (P - Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<subseteq> P \<Longrightarrow> partition_on (A - \<Union> Q) (P - Q)
[PROOF STEP]
using P P[THEN partition_onD4]
[PROOF STATE]
proof (prove)
using this:
partition_on A P
\<lbrakk>?p \<in> P; ?q \<in> P; ?x \<in> ?p; ?x \<in> ?q\<rbrakk> \<Longrightarrow> ?p = ?q

goal (1 subgoal):
 1. Q \<subseteq> P \<Longrightarrow> partition_on (A - \<Union> Q) (P - Q)
[PROOF STEP]
by (auto simp: partition_on_def disjoint_def)


[STATEMENT]
lemma partition_on_UN:
  assumes A: "partition_on A B" and B: "\<And>b. b \<in> B \<Longrightarrow> partition_on b (P b)"
  shows "partition_on A (\<Union>b\<in>B. P b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on A (\<Union> (P ` B))
[PROOF STEP]
proof (rule partition_onI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p. p \<in> \<Union> (P ` B) \<Longrightarrow> p \<noteq> {}
 2. \<Union> (\<Union> (P ` B)) = A
 3. \<And>p p'. \<lbrakk>p \<in> \<Union> (P ` B); p' \<in> \<Union> (P ` B); p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
show "\<Union>(\<Union>b\<in>B. P b) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (\<Union> (P ` B)) = A
[PROOF STEP]
using B[THEN partition_onD1] A[THEN partition_onD1]
[PROOF STATE]
proof (prove)
using this:
?A \<in> B \<Longrightarrow> ?A = \<Union> (P ?A)
A = \<Union> B

goal (1 subgoal):
 1. \<Union> (\<Union> (P ` B)) = A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Union> (\<Union> (P ` B)) = A

goal (2 subgoals):
 1. \<And>p. p \<in> \<Union> (P ` B) \<Longrightarrow> p \<noteq> {}
 2. \<And>p p'. \<lbrakk>p \<in> \<Union> (P ` B); p' \<in> \<Union> (P ` B); p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. p \<in> \<Union> (P ` B) \<Longrightarrow> p \<noteq> {}
 2. \<And>p p'. \<lbrakk>p \<in> \<Union> (P ` B); p' \<in> \<Union> (P ` B); p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
show "p \<noteq> {}" if "p \<in> (\<Union>b\<in>B. P b)" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> {}
[PROOF STEP]
using B[THEN partition_onD3] that
[PROOF STATE]
proof (prove)
using this:
?A \<in> B \<Longrightarrow> {} \<notin> P ?A
p \<in> \<Union> (P ` B)

goal (1 subgoal):
 1. p \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?p \<in> \<Union> (P ` B) \<Longrightarrow> ?p \<noteq> {}

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> \<Union> (P ` B); p' \<in> \<Union> (P ` B); p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> \<Union> (P ` B); p' \<in> \<Union> (P ` B); p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
fix p q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> \<Union> (P ` B); p' \<in> \<Union> (P ` B); p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
assume "p \<in> (\<Union>i\<in>B. P i)" "q \<in> (\<Union>i\<in>B. P i)" and "p \<noteq> q"
[PROOF STATE]
proof (state)
this:
p \<in> \<Union> (P ` B)
q \<in> \<Union> (P ` B)
p \<noteq> q

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> \<Union> (P ` B); p' \<in> \<Union> (P ` B); p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<Union> (P ` B)
q \<in> \<Union> (P ` B)
p \<noteq> q
[PROOF STEP]
obtain i j where i: "p \<in> P i" "i \<in> B" and j: "q \<in> P j" "j \<in> B"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<Union> (P ` B)
q \<in> \<Union> (P ` B)
p \<noteq> q

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>p \<in> P i; i \<in> B; q \<in> P j; j \<in> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> P i
i \<in> B
q \<in> P j
j \<in> B

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> \<Union> (P ` B); p' \<in> \<Union> (P ` B); p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
show "p \<inter> q = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<inter> q = {}
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> p \<inter> q = {}
 2. \<not> ?P \<Longrightarrow> p \<inter> q = {}
[PROOF STEP]
assume "i = j"
[PROOF STATE]
proof (state)
this:
i = j

goal (2 subgoals):
 1. ?P \<Longrightarrow> p \<inter> q = {}
 2. \<not> ?P \<Longrightarrow> p \<inter> q = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = j

goal (1 subgoal):
 1. p \<inter> q = {}
[PROOF STEP]
using i j \<open>p \<noteq> q\<close> B[THEN partition_onD2, of i]
[PROOF STATE]
proof (prove)
using this:
i = j
p \<in> P i
i \<in> B
q \<in> P j
j \<in> B
p \<noteq> q
i \<in> B \<Longrightarrow> disjoint (P i)

goal (1 subgoal):
 1. p \<inter> q = {}
[PROOF STEP]
by (simp add: disjointD)
[PROOF STATE]
proof (state)
this:
p \<inter> q = {}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> p \<inter> q = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> p \<inter> q = {}
[PROOF STEP]
assume "i \<noteq> j"
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> p \<inter> q = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> j
[PROOF STEP]
have "disjnt i j"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j

goal (1 subgoal):
 1. disjnt i j
[PROOF STEP]
using i j A[THEN partition_onD2]
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j
p \<in> P i
i \<in> B
q \<in> P j
j \<in> B
disjoint B

goal (1 subgoal):
 1. disjnt i j
[PROOF STEP]
by (auto simp: pairwise_def)
[PROOF STATE]
proof (state)
this:
disjnt i j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> p \<inter> q = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
disjnt i j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> p \<inter> q = {}
[PROOF STEP]
have "p \<subseteq> i" "q \<subseteq> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<subseteq> i &&& q \<subseteq> j
[PROOF STEP]
using B[THEN partition_onD1, of i, symmetric] B[THEN partition_onD1, of j, symmetric] i j
[PROOF STATE]
proof (prove)
using this:
i \<in> B \<Longrightarrow> \<Union> (P i) = i
j \<in> B \<Longrightarrow> \<Union> (P j) = j
p \<in> P i
i \<in> B
q \<in> P j
j \<in> B

goal (1 subgoal):
 1. p \<subseteq> i &&& q \<subseteq> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<subseteq> i
q \<subseteq> j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> p \<inter> q = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
disjnt i j
p \<subseteq> i
q \<subseteq> j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
disjnt i j
p \<subseteq> i
q \<subseteq> j

goal (1 subgoal):
 1. p \<inter> q = {}
[PROOF STEP]
by (auto simp: disjnt_def)
[PROOF STATE]
proof (state)
this:
p \<inter> q = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p \<inter> q = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_notemptyI:
  assumes "partition_on A P"
  assumes "A \<noteq> {}"
  shows "P \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<noteq> {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
partition_on A P
A \<noteq> {}

goal (1 subgoal):
 1. P \<noteq> {}
[PROOF STEP]
by (auto elim: partition_onE)


[STATEMENT]
lemma partition_on_disjoint:
  assumes "partition_on A P"
  assumes "partition_on B Q"
  assumes "A \<inter> B = {}"
  shows "P \<inter> Q = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<inter> Q = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
partition_on A P
partition_on B Q
A \<inter> B = {}

goal (1 subgoal):
 1. P \<inter> Q = {}
[PROOF STEP]
by (fastforce elim: partition_onE)


[STATEMENT]
lemma partition_on_eq_implies_eq_carrier:
  assumes "partition_on A Q"
  assumes "partition_on B Q"
  shows "A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
partition_on A Q
partition_on B Q

goal (1 subgoal):
 1. A = B
[PROOF STEP]
by (fastforce elim: partition_onE)


[STATEMENT]
lemma partition_on_insert:
  assumes "partition_on A P"
  assumes "disjnt A X" "X \<noteq> {}"
  assumes "A \<union> X = A'"
  shows "partition_on A' (insert X P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on A' (insert X P)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
partition_on A P
disjnt A X
X \<noteq> {}
A \<union> X = A'

goal (1 subgoal):
 1. partition_on A' (insert X P)
[PROOF STEP]
by (auto simp: partition_on_def disjoint_def disjnt_def)


[STATEMENT]
lemma partition_on_insert':
  assumes "partition_on (A - X) P"
  assumes "X \<subseteq> A" "X \<noteq> {}"
  shows "partition_on A (insert X P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on A (insert X P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partition_on A (insert X P)
[PROOF STEP]
have "disjnt (A - X) X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjnt (A - X) X
[PROOF STEP]
by (simp add: disjnt_iff)
[PROOF STATE]
proof (state)
this:
disjnt (A - X) X

goal (1 subgoal):
 1. partition_on A (insert X P)
[PROOF STEP]
from assms(1) this assms(3)
[PROOF STATE]
proof (chain)
picking this:
partition_on (A - X) P
disjnt (A - X) X
X \<noteq> {}
[PROOF STEP]
have "partition_on ((A - X) \<union> X) (insert X P)"
[PROOF STATE]
proof (prove)
using this:
partition_on (A - X) P
disjnt (A - X) X
X \<noteq> {}

goal (1 subgoal):
 1. partition_on (A - X \<union> X) (insert X P)
[PROOF STEP]
by (auto intro: partition_on_insert)
[PROOF STATE]
proof (state)
this:
partition_on (A - X \<union> X) (insert X P)

goal (1 subgoal):
 1. partition_on A (insert X P)
[PROOF STEP]
from this \<open>X \<subseteq> A\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on (A - X \<union> X) (insert X P)
X \<subseteq> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
partition_on (A - X \<union> X) (insert X P)
X \<subseteq> A

goal (1 subgoal):
 1. partition_on A (insert X P)
[PROOF STEP]
by (metis Diff_partition sup_commute)
[PROOF STATE]
proof (state)
this:
partition_on A (insert X P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_insert_singleton:
  assumes "partition_on A P" "a \<notin> A" "insert a A = A'"
  shows "partition_on A' (insert {a} P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on A' (insert {a} P)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
partition_on A P
a \<notin> A
insert a A = A'

goal (1 subgoal):
 1. partition_on A' (insert {a} P)
[PROOF STEP]
by (auto simp: partition_on_def disjoint_def disjnt_def)


[STATEMENT]
lemma partition_on_remove_singleton:
  assumes "partition_on A P" "X \<in> P" "A - X = A'"
  shows "partition_on A' (P - {X})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on A' (P - {X})
[PROOF STEP]
using assms partition_on_Diff
[PROOF STATE]
proof (prove)
using this:
partition_on A P
X \<in> P
A - X = A'
\<lbrakk>partition_on ?A ?P; ?Q \<subseteq> ?P\<rbrakk> \<Longrightarrow> partition_on (?A - \<Union> ?Q) (?P - ?Q)

goal (1 subgoal):
 1. partition_on A' (P - {X})
[PROOF STEP]
by (metis Diff_cancel Diff_subset cSup_singleton insert_subset)


[STATEMENT]
lemma partition_on_partition_on_unique:
  assumes "partition_on A P"
  assumes "x \<in> A"
  shows "\<exists>!X. x \<in> X \<and> X \<in> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
from \<open>partition_on A P\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on A P
[PROOF STEP]
have "\<Union>P = A"
[PROOF STATE]
proof (prove)
using this:
partition_on A P

goal (1 subgoal):
 1. \<Union> P = A
[PROOF STEP]
by (auto elim: partition_onE)
[PROOF STATE]
proof (state)
this:
\<Union> P = A

goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
from this \<open>x \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Union> P = A
x \<in> A
[PROOF STEP]
obtain X where X: "x \<in> X \<and> X \<in> P"
[PROOF STATE]
proof (prove)
using this:
\<Union> P = A
x \<in> A

goal (1 subgoal):
 1. (\<And>X. x \<in> X \<and> X \<in> P \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> X \<and> X \<in> P

goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x \<in> X \<and> X \<in> P

goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
fix Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
assume "x \<in> Y \<and> Y \<in> P"
[PROOF STATE]
proof (state)
this:
x \<in> Y \<and> Y \<in> P

goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> Y \<and> Y \<in> P
[PROOF STEP]
have "X = Y"
[PROOF STATE]
proof (prove)
using this:
x \<in> Y \<and> Y \<in> P

goal (1 subgoal):
 1. X = Y
[PROOF STEP]
using X \<open>partition_on A P\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> Y \<and> Y \<in> P
x \<in> X \<and> X \<in> P
partition_on A P

goal (1 subgoal):
 1. X = Y
[PROOF STEP]
by (meson partition_onE disjoint_iff_not_equal)
[PROOF STATE]
proof (state)
this:
X = Y

goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x \<in> ?Y2 \<and> ?Y2 \<in> P \<Longrightarrow> X = ?Y2

goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
from this X
[PROOF STATE]
proof (chain)
picking this:
x \<in> ?Y2 \<and> ?Y2 \<in> P \<Longrightarrow> X = ?Y2
x \<in> X \<and> X \<in> P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> ?Y2 \<and> ?Y2 \<in> P \<Longrightarrow> X = ?Y2
x \<in> X \<and> X \<in> P

goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>!X. x \<in> X \<and> X \<in> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_the_part_mem:
  assumes "partition_on A P"
  assumes "x \<in> A"
  shows "(THE X. x \<in> X \<and> X \<in> P) \<in> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) \<in> P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) \<in> P
[PROOF STEP]
from \<open>x \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
[PROOF STEP]
have "\<exists>!X. x \<in> X \<and> X \<in> P"
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
using \<open>partition_on A P\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> A
partition_on A P

goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
by (simp add: partition_on_partition_on_unique)
[PROOF STATE]
proof (state)
this:
\<exists>!X. x \<in> X \<and> X \<in> P

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) \<in> P
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
show "(THE X. x \<in> X \<and> X \<in> P) \<in> P"
[PROOF STATE]
proof (prove)
using this:
\<exists>!X. x \<in> X \<and> X \<in> P

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) \<in> P
[PROOF STEP]
by (metis (no_types, lifting) theI)
[PROOF STATE]
proof (state)
this:
(THE X. x \<in> X \<and> X \<in> P) \<in> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_in_the_unique_part:
  assumes "partition_on A P"
  assumes "x \<in> A"
  shows "x \<in> (THE X. x \<in> X \<and> X \<in> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
partition_on A P
x \<in> A
[PROOF STEP]
have "\<exists>!X. x \<in> X \<and> X \<in> P"
[PROOF STATE]
proof (prove)
using this:
partition_on A P
x \<in> A

goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
by (simp add: partition_on_partition_on_unique)
[PROOF STATE]
proof (state)
this:
\<exists>!X. x \<in> X \<and> X \<in> P

goal (1 subgoal):
 1. x \<in> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>!X. x \<in> X \<and> X \<in> P

goal (1 subgoal):
 1. x \<in> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
by (metis (mono_tags, lifting) theI')
[PROOF STATE]
proof (state)
this:
x \<in> (THE X. x \<in> X \<and> X \<in> P)

goal:
No subgoals!
[PROOF STEP]
qed