[STATEMENT]
theorem (in endoNT) id_restrict_natural:
  "(\<lambda>A\<in>Ob. Id A) : (id_func AA) \<Rightarrow> (id_func AA) in Func(AA,AA)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict (category.id AA) (Ob) : id_func AA \<Rightarrow> id_func AA in Func (AA , AA )
[PROOF STEP]
proof (intro natural_transformation.intro natural_transformation_axioms.intro
    two_cats.intro ballI)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. category AA
 2. category AA
 3. Functor id_func AA : AA \<longrightarrow> AA
 4. Functor id_func AA : AA \<longrightarrow> AA
 5. restrict (category.id AA) (Ob) \<in> Ob \<rightarrow> Ar
 6. restrict (category.id AA) (Ob) \<in> extensional (Ob)
 7. \<And>A. A \<in> Ob \<Longrightarrow> restrict (category.id AA) (Ob) A \<in> Hom id_func AA \<^bsub>\<o>\<^esub> A id_func AA \<^bsub>\<o>\<^esub> A
 8. \<And>A B f. \<lbrakk>A \<in> Ob; B \<in> Ob; f \<in> Hom A B\<rbrakk> \<Longrightarrow> id_func AA \<^bsub>\<a>\<^esub> f \<bullet> restrict (category.id AA) (Ob) A = restrict (category.id AA) (Ob) B \<bullet> id_func AA \<^bsub>\<a>\<^esub> f
[PROOF STEP]
show "(\<lambda>A\<in>Ob. Id A) : Ob \<rightarrow> Ar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict (category.id AA) (Ob) \<in> Ob \<rightarrow> Ar
[PROOF STEP]
by (rule funcsetI) auto
[PROOF STATE]
proof (state)
this:
restrict (category.id AA) (Ob) \<in> Ob \<rightarrow> Ar

goal (7 subgoals):
 1. category AA
 2. category AA
 3. Functor id_func AA : AA \<longrightarrow> AA
 4. Functor id_func AA : AA \<longrightarrow> AA
 5. restrict (category.id AA) (Ob) \<in> extensional (Ob)
 6. \<And>A. A \<in> Ob \<Longrightarrow> restrict (category.id AA) (Ob) A \<in> Hom id_func AA \<^bsub>\<o>\<^esub> A id_func AA \<^bsub>\<o>\<^esub> A
 7. \<And>A B f. \<lbrakk>A \<in> Ob; B \<in> Ob; f \<in> Hom A B\<rbrakk> \<Longrightarrow> id_func AA \<^bsub>\<a>\<^esub> f \<bullet> restrict (category.id AA) (Ob) A = restrict (category.id AA) (Ob) B \<bullet> id_func AA \<^bsub>\<a>\<^esub> f
[PROOF STEP]
show "(\<lambda>A\<in>Ob. Id A) \<in> extensional (Ob)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict (category.id AA) (Ob) \<in> extensional (Ob)
[PROOF STEP]
by (rule restrict_extensional)
[PROOF STATE]
proof (state)
this:
restrict (category.id AA) (Ob) \<in> extensional (Ob)

goal (6 subgoals):
 1. category AA
 2. category AA
 3. Functor id_func AA : AA \<longrightarrow> AA
 4. Functor id_func AA : AA \<longrightarrow> AA
 5. \<And>A. A \<in> Ob \<Longrightarrow> restrict (category.id AA) (Ob) A \<in> Hom id_func AA \<^bsub>\<o>\<^esub> A id_func AA \<^bsub>\<o>\<^esub> A
 6. \<And>A B f. \<lbrakk>A \<in> Ob; B \<in> Ob; f \<in> Hom A B\<rbrakk> \<Longrightarrow> id_func AA \<^bsub>\<a>\<^esub> f \<bullet> restrict (category.id AA) (Ob) A = restrict (category.id AA) (Ob) B \<bullet> id_func AA \<^bsub>\<a>\<^esub> f
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. category AA
 2. category AA
 3. Functor id_func AA : AA \<longrightarrow> AA
 4. Functor id_func AA : AA \<longrightarrow> AA
 5. \<And>A. A \<in> Ob \<Longrightarrow> restrict (category.id AA) (Ob) A \<in> Hom id_func AA \<^bsub>\<o>\<^esub> A id_func AA \<^bsub>\<o>\<^esub> A
 6. \<And>A B f. \<lbrakk>A \<in> Ob; B \<in> Ob; f \<in> Hom A B\<rbrakk> \<Longrightarrow> id_func AA \<^bsub>\<a>\<^esub> f \<bullet> restrict (category.id AA) (Ob) A = restrict (category.id AA) (Ob) B \<bullet> id_func AA \<^bsub>\<a>\<^esub> f
[PROOF STEP]
assume A: "A \<in> Ob"
[PROOF STATE]
proof (state)
this:
A \<in> Ob

goal (6 subgoals):
 1. category AA
 2. category AA
 3. Functor id_func AA : AA \<longrightarrow> AA
 4. Functor id_func AA : AA \<longrightarrow> AA
 5. \<And>A. A \<in> Ob \<Longrightarrow> restrict (category.id AA) (Ob) A \<in> Hom id_func AA \<^bsub>\<o>\<^esub> A id_func AA \<^bsub>\<o>\<^esub> A
 6. \<And>A B f. \<lbrakk>A \<in> Ob; B \<in> Ob; f \<in> Hom A B\<rbrakk> \<Longrightarrow> id_func AA \<^bsub>\<a>\<^esub> f \<bullet> restrict (category.id AA) (Ob) A = restrict (category.id AA) (Ob) B \<bullet> id_func AA \<^bsub>\<a>\<^esub> f
[PROOF STEP]
hence "Id A \<in> Hom A A"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob

goal (1 subgoal):
 1. Id A \<in> Hom A A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Id A \<in> Hom A A

goal (6 subgoals):
 1. category AA
 2. category AA
 3. Functor id_func AA : AA \<longrightarrow> AA
 4. Functor id_func AA : AA \<longrightarrow> AA
 5. \<And>A. A \<in> Ob \<Longrightarrow> restrict (category.id AA) (Ob) A \<in> Hom id_func AA \<^bsub>\<o>\<^esub> A id_func AA \<^bsub>\<o>\<^esub> A
 6. \<And>A B f. \<lbrakk>A \<in> Ob; B \<in> Ob; f \<in> Hom A B\<rbrakk> \<Longrightarrow> id_func AA \<^bsub>\<a>\<^esub> f \<bullet> restrict (category.id AA) (Ob) A = restrict (category.id AA) (Ob) B \<bullet> id_func AA \<^bsub>\<a>\<^esub> f
[PROOF STEP]
thus "(\<lambda>X\<in>Ob. Id X) A \<in> Hom ((id_func AA)\<^bsub>\<o>\<^esub> A)  ((id_func AA)\<^bsub>\<o>\<^esub> A)"
[PROOF STATE]
proof (prove)
using this:
Id A \<in> Hom A A

goal (1 subgoal):
 1. restrict (category.id AA) (Ob) A \<in> Hom id_func AA \<^bsub>\<o>\<^esub> A id_func AA \<^bsub>\<o>\<^esub> A
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
Id A \<in> Hom A A
A \<in> Ob

goal (1 subgoal):
 1. restrict (category.id AA) (Ob) A \<in> Hom id_func AA \<^bsub>\<o>\<^esub> A id_func AA \<^bsub>\<o>\<^esub> A
[PROOF STEP]
by (simp add: id_func_def)
[PROOF STATE]
proof (state)
this:
restrict (category.id AA) (Ob) A \<in> Hom id_func AA \<^bsub>\<o>\<^esub> A id_func AA \<^bsub>\<o>\<^esub> A

goal (5 subgoals):
 1. category AA
 2. category AA
 3. Functor id_func AA : AA \<longrightarrow> AA
 4. Functor id_func AA : AA \<longrightarrow> AA
 5. \<And>A B f. \<lbrakk>A \<in> Ob; B \<in> Ob; f \<in> Hom A B\<rbrakk> \<Longrightarrow> id_func AA \<^bsub>\<a>\<^esub> f \<bullet> restrict (category.id AA) (Ob) A = restrict (category.id AA) (Ob) B \<bullet> id_func AA \<^bsub>\<a>\<^esub> f
[PROOF STEP]
fix B and f
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. category AA
 2. category AA
 3. Functor id_func AA : AA \<longrightarrow> AA
 4. Functor id_func AA : AA \<longrightarrow> AA
 5. \<And>A B f. \<lbrakk>A \<in> Ob; B \<in> Ob; f \<in> Hom A B\<rbrakk> \<Longrightarrow> id_func AA \<^bsub>\<a>\<^esub> f \<bullet> restrict (category.id AA) (Ob) A = restrict (category.id AA) (Ob) B \<bullet> id_func AA \<^bsub>\<a>\<^esub> f
[PROOF STEP]
assume B: "B \<in> Ob"
    and "f \<in> Hom A B"
[PROOF STATE]
proof (state)
this:
B \<in> Ob
f \<in> Hom A B

goal (5 subgoals):
 1. category AA
 2. category AA
 3. Functor id_func AA : AA \<longrightarrow> AA
 4. Functor id_func AA : AA \<longrightarrow> AA
 5. \<And>A B f. \<lbrakk>A \<in> Ob; B \<in> Ob; f \<in> Hom A B\<rbrakk> \<Longrightarrow> id_func AA \<^bsub>\<a>\<^esub> f \<bullet> restrict (category.id AA) (Ob) A = restrict (category.id AA) (Ob) B \<bullet> id_func AA \<^bsub>\<a>\<^esub> f
[PROOF STEP]
hence "f \<in> Ar" and "A = Dom f" and "B = Cod f" and "Dom f \<in> Ob" and "Cod f \<in> Ob"
[PROOF STATE]
proof (prove)
using this:
B \<in> Ob
f \<in> Hom A B

goal (1 subgoal):
 1. (f \<in> Ar &&& A = Dom f) &&& B = Cod f &&& Dom f \<in> Ob &&& Cod f \<in> Ob
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
B \<in> Ob
f \<in> Hom A B
A \<in> Ob

goal (1 subgoal):
 1. (f \<in> Ar &&& A = Dom f) &&& B = Cod f &&& Dom f \<in> Ob &&& Cod f \<in> Ob
[PROOF STEP]
by (simp_all add: hom_def)
[PROOF STATE]
proof (state)
this:
f \<in> Ar
A = Dom f
B = Cod f
Dom f \<in> Ob
Cod f \<in> Ob

goal (5 subgoals):
 1. category AA
 2. category AA
 3. Functor id_func AA : AA \<longrightarrow> AA
 4. Functor id_func AA : AA \<longrightarrow> AA
 5. \<And>A B f. \<lbrakk>A \<in> Ob; B \<in> Ob; f \<in> Hom A B\<rbrakk> \<Longrightarrow> id_func AA \<^bsub>\<a>\<^esub> f \<bullet> restrict (category.id AA) (Ob) A = restrict (category.id AA) (Ob) B \<bullet> id_func AA \<^bsub>\<a>\<^esub> f
[PROOF STEP]
thus "(id_func AA)\<^bsub>\<a>\<^esub> f \<bullet> (\<lambda>A\<in>Ob. Id A) A
      = (\<lambda>A\<in>Ob. Id A) B \<bullet> (id_func AA)\<^bsub>\<a>\<^esub> f"
[PROOF STATE]
proof (prove)
using this:
f \<in> Ar
A = Dom f
B = Cod f
Dom f \<in> Ob
Cod f \<in> Ob

goal (1 subgoal):
 1. id_func AA \<^bsub>\<a>\<^esub> f \<bullet> restrict (category.id AA) (Ob) A = restrict (category.id AA) (Ob) B \<bullet> id_func AA \<^bsub>\<a>\<^esub> f
[PROOF STEP]
by (simp add:  id_func_def)
[PROOF STATE]
proof (state)
this:
id_func AA \<^bsub>\<a>\<^esub> f \<bullet> restrict (category.id AA) (Ob) A = restrict (category.id AA) (Ob) B \<bullet> id_func AA \<^bsub>\<a>\<^esub> f

goal (4 subgoals):
 1. category AA
 2. category AA
 3. Functor id_func AA : AA \<longrightarrow> AA
 4. Functor id_func AA : AA \<longrightarrow> AA
[PROOF STEP]
qed (auto intro: id_func_functor, unfold_locales, unfold_locales)


[STATEMENT]
lemma is_distinguishing_formula_eqvt (*[eqvt]*):
    assumes "x distinguishes P from Q" shows "(p \<bullet> x) distinguishes (p \<bullet> P) from (p \<bullet> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<bullet> x) distinguishes (p \<bullet> P) from (p \<bullet> Q)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x distinguishes P from Q

goal (1 subgoal):
 1. (p \<bullet> x) distinguishes (p \<bullet> P) from (p \<bullet> Q)
[PROOF STEP]
unfolding is_distinguishing_formula_def
[PROOF STATE]
proof (prove)
using this:
P \<Turnstile> x \<and> \<not> Q \<Turnstile> x

goal (1 subgoal):
 1. p \<bullet> P \<Turnstile> p \<bullet> x \<and> \<not> p \<bullet> Q \<Turnstile> p \<bullet> x
[PROOF STEP]
by (metis permute_minus_cancel(2) FL_valid_eqvt)


[STATEMENT]
lemma FL_equivalent_iff_not_distinguished:
    "FL_logically_equivalent F P Q \<longleftrightarrow> \<not>(\<exists>x. x \<in> \<A>[F] \<and> x distinguishes P from Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FL_logically_equivalent F P Q = (\<nexists>x. x \<in> \<A>[F] \<and> x distinguishes P from Q)
[PROOF STEP]
by (meson FL_logically_equivalent_def Not is_distinguishing_formula_def FL_valid_Not)


[STATEMENT]
lemma FL_distinguished_bounded_support:
    assumes "x \<in> \<A>[F]" and "x distinguishes P from Q"
    obtains y where "y \<in> \<A>[F]" and "supp y \<subseteq> supp (F,P)" and "y distinguishes P from Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?B = "{p \<bullet> x|p. supp (F,P) \<sharp>* p}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "supp (F,P) supports ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (F, P) supports {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
unfolding supports_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. a \<notin> supp (F, P) \<and> b \<notin> supp (F, P) \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} = {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<notin> supp (F, P); b \<notin> supp (F, P)\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} = {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<notin> supp (F, P); b \<notin> supp (F, P)\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} = {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
assume a: "a \<notin> supp (F,P)" and b: "b \<notin> supp (F,P)"
[PROOF STATE]
proof (state)
this:
a \<notin> supp (F, P)
b \<notin> supp (F, P)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<notin> supp (F, P); b \<notin> supp (F, P)\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} = {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
have "(a \<rightleftharpoons> b) \<bullet> ?B \<subseteq> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
fix x'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
assume "x' \<in> (a \<rightleftharpoons> b) \<bullet> ?B"
[PROOF STATE]
proof (state)
this:
x' \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal (1 subgoal):
 1. \<And>xa. xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x' \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
obtain p where 1: "x' = (a \<rightleftharpoons> b) \<bullet> p \<bullet> x" and 2: "supp (F,P) \<sharp>* p"
[PROOF STATE]
proof (prove)
using this:
x' \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>x' = (a \<rightleftharpoons> b) \<bullet> p \<bullet> x; supp (F, P) \<sharp>* p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: permute_set_def)
[PROOF STATE]
proof (state)
this:
x' = (a \<rightleftharpoons> b) \<bullet> p \<bullet> x
supp (F, P) \<sharp>* p

goal (1 subgoal):
 1. \<And>xa. xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
let ?q = "(a \<rightleftharpoons> b) + p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
x' = (a \<rightleftharpoons> b) \<bullet> p \<bullet> x
[PROOF STEP]
have "x' = ?q \<bullet> x"
[PROOF STATE]
proof (prove)
using this:
x' = (a \<rightleftharpoons> b) \<bullet> p \<bullet> x

goal (1 subgoal):
 1. x' = ((a \<rightleftharpoons> b) + p) \<bullet> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x' = ((a \<rightleftharpoons> b) + p) \<bullet> x

goal (1 subgoal):
 1. \<And>xa. xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x' = ((a \<rightleftharpoons> b) + p) \<bullet> x

goal (1 subgoal):
 1. \<And>xa. xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
from a and b and 2
[PROOF STATE]
proof (chain)
picking this:
a \<notin> supp (F, P)
b \<notin> supp (F, P)
supp (F, P) \<sharp>* p
[PROOF STEP]
have "supp (F,P) \<sharp>* ?q"
[PROOF STATE]
proof (prove)
using this:
a \<notin> supp (F, P)
b \<notin> supp (F, P)
supp (F, P) \<sharp>* p

goal (1 subgoal):
 1. supp (F, P) \<sharp>* ((a \<rightleftharpoons> b) + p)
[PROOF STEP]
by (metis fresh_perm fresh_star_def fresh_star_plus swap_atom_simps(3))
[PROOF STATE]
proof (state)
this:
supp (F, P) \<sharp>* ((a \<rightleftharpoons> b) + p)

goal (1 subgoal):
 1. \<And>xa. xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x' = ((a \<rightleftharpoons> b) + p) \<bullet> x
supp (F, P) \<sharp>* ((a \<rightleftharpoons> b) + p)
[PROOF STEP]
show "x' \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
x' = ((a \<rightleftharpoons> b) + p) \<bullet> x
supp (F, P) \<sharp>* ((a \<rightleftharpoons> b) + p)

goal (1 subgoal):
 1. x' \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x' \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<notin> supp (F, P); b \<notin> supp (F, P)\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} = {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<notin> supp (F, P); b \<notin> supp (F, P)\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} = {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
have "?B \<subseteq> (a \<rightleftharpoons> b) \<bullet> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
fix x'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
assume "x' \<in> ?B"
[PROOF STATE]
proof (state)
this:
x' \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x' \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
obtain p where 1: "x' = p \<bullet> x" and 2: "supp (F,P) \<sharp>* p"
[PROOF STATE]
proof (prove)
using this:
x' \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>x' = p \<bullet> x; supp (F, P) \<sharp>* p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' = p \<bullet> x
supp (F, P) \<sharp>* p

goal (1 subgoal):
 1. \<And>xa. xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
let ?q = "(a \<rightleftharpoons> b) + p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
x' = p \<bullet> x
[PROOF STEP]
have "x' = (a \<rightleftharpoons> b) \<bullet> ?q \<bullet> x"
[PROOF STATE]
proof (prove)
using this:
x' = p \<bullet> x

goal (1 subgoal):
 1. x' = (a \<rightleftharpoons> b) \<bullet> ((a \<rightleftharpoons> b) + p) \<bullet> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x' = (a \<rightleftharpoons> b) \<bullet> ((a \<rightleftharpoons> b) + p) \<bullet> x

goal (1 subgoal):
 1. \<And>xa. xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x' = (a \<rightleftharpoons> b) \<bullet> ((a \<rightleftharpoons> b) + p) \<bullet> x

goal (1 subgoal):
 1. \<And>xa. xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
from a and b and 2
[PROOF STATE]
proof (chain)
picking this:
a \<notin> supp (F, P)
b \<notin> supp (F, P)
supp (F, P) \<sharp>* p
[PROOF STEP]
have "supp (F,P) \<sharp>* ?q"
[PROOF STATE]
proof (prove)
using this:
a \<notin> supp (F, P)
b \<notin> supp (F, P)
supp (F, P) \<sharp>* p

goal (1 subgoal):
 1. supp (F, P) \<sharp>* ((a \<rightleftharpoons> b) + p)
[PROOF STEP]
by (metis fresh_perm fresh_star_def fresh_star_plus swap_atom_simps(3))
[PROOF STATE]
proof (state)
this:
supp (F, P) \<sharp>* ((a \<rightleftharpoons> b) + p)

goal (1 subgoal):
 1. \<And>xa. xa \<in> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<Longrightarrow> xa \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x' = (a \<rightleftharpoons> b) \<bullet> ((a \<rightleftharpoons> b) + p) \<bullet> x
supp (F, P) \<sharp>* ((a \<rightleftharpoons> b) + p)
[PROOF STEP]
show "x' \<in> (a \<rightleftharpoons> b) \<bullet> ?B"
[PROOF STATE]
proof (prove)
using this:
x' = (a \<rightleftharpoons> b) \<bullet> ((a \<rightleftharpoons> b) + p) \<bullet> x
supp (F, P) \<sharp>* ((a \<rightleftharpoons> b) + p)

goal (1 subgoal):
 1. x' \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
using mem_permute_iff
[PROOF STATE]
proof (prove)
using this:
x' = (a \<rightleftharpoons> b) \<bullet> ((a \<rightleftharpoons> b) + p) \<bullet> x
supp (F, P) \<sharp>* ((a \<rightleftharpoons> b) + p)
(?p \<bullet> ?x \<in> ?p \<bullet> ?X) = (?x \<in> ?X)

goal (1 subgoal):
 1. x' \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x' \<in> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<notin> supp (F, P); b \<notin> supp (F, P)\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} = {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
{p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
show "(a \<rightleftharpoons> b) \<bullet> ?B = ?B"
[PROOF STATE]
proof (prove)
using this:
(a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> {p \<bullet> x |p. supp (F, P) \<sharp>* p}
{p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal (1 subgoal):
 1. (a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} = {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(a \<rightleftharpoons> b) \<bullet> {p \<bullet> x |p. supp (F, P) \<sharp>* p} = {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
supp (F, P) supports {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supp (F, P) supports {p \<bullet> x |p. supp (F, P) \<sharp>* p}
[PROOF STEP]
have supp_B_subset_supp_P: "supp ?B \<subseteq> supp (F,P)"
[PROOF STATE]
proof (prove)
using this:
supp (F, P) supports {p \<bullet> x |p. supp (F, P) \<sharp>* p}

goal (1 subgoal):
 1. supp {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> supp (F, P)
[PROOF STEP]
by (metis (erased, lifting) finite_supp supp_is_subset)
[PROOF STATE]
proof (state)
this:
supp {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> supp (F, P)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supp {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> supp (F, P)
[PROOF STEP]
have finite_supp_B: "finite (supp ?B)"
[PROOF STATE]
proof (prove)
using this:
supp {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> supp (F, P)

goal (1 subgoal):
 1. finite (supp {p \<bullet> x |p. supp (F, P) \<sharp>* p})
[PROOF STEP]
using finite_supp rev_finite_subset
[PROOF STATE]
proof (prove)
using this:
supp {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> supp (F, P)
finite (supp ?x)
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (supp {p \<bullet> x |p. supp (F, P) \<sharp>* p})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (supp {p \<bullet> x |p. supp (F, P) \<sharp>* p})

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "?B \<subseteq> (\<lambda>p. p \<bullet> x) ` UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> range (\<lambda>p. p \<bullet> x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> range (\<lambda>p. p \<bullet> x)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> range (\<lambda>p. p \<bullet> x)
[PROOF STEP]
have "|?B| \<le>o |UNIV :: perm set|"
[PROOF STATE]
proof (prove)
using this:
{p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> range (\<lambda>p. p \<bullet> x)

goal (1 subgoal):
 1. |{p \<bullet> x |p. supp (F, P) \<sharp>* p}| \<le>o |UNIV|
[PROOF STEP]
by (rule surj_imp_ordLeq)
[PROOF STATE]
proof (state)
this:
|{p \<bullet> x |p. supp (F, P) \<sharp>* p}| \<le>o |UNIV|

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
|{p \<bullet> x |p. supp (F, P) \<sharp>* p}| \<le>o |UNIV|

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "|UNIV :: perm set| <o |UNIV :: 'idx set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |UNIV| <o |UNIV|
[PROOF STEP]
by (metis card_idx_perm)
[PROOF STATE]
proof (state)
this:
|UNIV| <o |UNIV|

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
|UNIV| <o |UNIV|

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "|UNIV :: 'idx set| \<le>o natLeq +c |UNIV :: 'idx set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |UNIV| \<le>o natLeq +c |UNIV|
[PROOF STEP]
by (metis Cnotzero_UNIV ordLeq_csum2)
[PROOF STATE]
proof (state)
this:
|UNIV| \<le>o natLeq +c |UNIV|

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
|{p \<bullet> x |p. supp (F, P) \<sharp>* p}| <o natLeq +c |UNIV|
[PROOF STEP]
have card_B: "|?B| <o natLeq +c |UNIV :: 'idx set|"
[PROOF STATE]
proof (prove)
using this:
|{p \<bullet> x |p. supp (F, P) \<sharp>* p}| <o natLeq +c |UNIV|

goal (1 subgoal):
 1. |{p \<bullet> x |p. supp (F, P) \<sharp>* p}| <o natLeq +c |UNIV|
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
|{p \<bullet> x |p. supp (F, P) \<sharp>* p}| <o natLeq +c |UNIV|

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?y = "Conj (Abs_bset ?B) :: ('idx, 'pred, 'act, 'effect) formula"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from finite_supp_B and card_B and supp_B_subset_supp_P
[PROOF STATE]
proof (chain)
picking this:
finite (supp {p \<bullet> x |p. supp (F, P) \<sharp>* p})
|{p \<bullet> x |p. supp (F, P) \<sharp>* p}| <o natLeq +c |UNIV|
supp {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> supp (F, P)
[PROOF STEP]
have "supp ?y \<subseteq> supp (F,P)"
[PROOF STATE]
proof (prove)
using this:
finite (supp {p \<bullet> x |p. supp (F, P) \<sharp>* p})
|{p \<bullet> x |p. supp (F, P) \<sharp>* p}| <o natLeq +c |UNIV|
supp {p \<bullet> x |p. supp (F, P) \<sharp>* p} \<subseteq> supp (F, P)

goal (1 subgoal):
 1. supp (Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})) \<subseteq> supp (F, P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
supp (Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})) \<subseteq> supp (F, P)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
supp (Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})) \<subseteq> supp (F, P)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "?y \<in> \<A>[F]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<in> \<A>[F]
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (supp (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}))
 2. \<And>xa. xa \<in> set_bset (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<Longrightarrow> xa \<in> \<A>[F]
[PROOF STEP]
show "finite (supp (Abs_bset ?B :: (_,_,_,_) formula set['idx]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (supp (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}))
[PROOF STEP]
using finite_supp_B card_B
[PROOF STATE]
proof (prove)
using this:
finite (supp {p \<bullet> x |p. supp (F, P) \<sharp>* p})
|{p \<bullet> x |p. supp (F, P) \<sharp>* p}| <o natLeq +c |UNIV|

goal (1 subgoal):
 1. finite (supp (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (supp (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}))

goal (1 subgoal):
 1. \<And>xa. xa \<in> set_bset (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<Longrightarrow> xa \<in> \<A>[F]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set_bset (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<Longrightarrow> xa \<in> \<A>[F]
[PROOF STEP]
fix x'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set_bset (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<Longrightarrow> xa \<in> \<A>[F]
[PROOF STEP]
assume "x' \<in> set_bset (Abs_bset ?B :: (_,_,_,_) formula set['idx])"
[PROOF STATE]
proof (state)
this:
x' \<in> set_bset (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})

goal (1 subgoal):
 1. \<And>xa. xa \<in> set_bset (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<Longrightarrow> xa \<in> \<A>[F]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x' \<in> set_bset (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})
[PROOF STEP]
obtain p where p_x: "x' = p \<bullet> x" and fresh_p: "supp (F,P) \<sharp>* p"
[PROOF STATE]
proof (prove)
using this:
x' \<in> set_bset (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>x' = p \<bullet> x; supp (F, P) \<sharp>* p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using card_B
[PROOF STATE]
proof (prove)
using this:
x' \<in> set_bset (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})
|{p \<bullet> x |p. supp (F, P) \<sharp>* p}| <o natLeq +c |UNIV|

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>x' = p \<bullet> x; supp (F, P) \<sharp>* p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' = p \<bullet> x
supp (F, P) \<sharp>* p

goal (1 subgoal):
 1. \<And>xa. xa \<in> set_bset (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<Longrightarrow> xa \<in> \<A>[F]
[PROOF STEP]
from fresh_p
[PROOF STATE]
proof (chain)
picking this:
supp (F, P) \<sharp>* p
[PROOF STEP]
have "p \<bullet> F = F"
[PROOF STATE]
proof (prove)
using this:
supp (F, P) \<sharp>* p

goal (1 subgoal):
 1. p \<bullet> F = F
[PROOF STEP]
using fresh_star_Pair fresh_star_supp_conv perm_supp_eq
[PROOF STATE]
proof (prove)
using this:
supp (F, P) \<sharp>* p
?as \<sharp>* (?x, ?y) = (?as \<sharp>* ?x \<and> ?as \<sharp>* ?y)
supp ?x \<sharp>* ?y \<Longrightarrow> supp ?y \<sharp>* ?x
supp ?p \<sharp>* ?x \<Longrightarrow> ?p \<bullet> ?x = ?x

goal (1 subgoal):
 1. p \<bullet> F = F
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<bullet> F = F

goal (1 subgoal):
 1. \<And>xa. xa \<in> set_bset (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<Longrightarrow> xa \<in> \<A>[F]
[PROOF STEP]
with \<open>x \<in> \<A>[F]\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<A>[F]
p \<bullet> F = F
[PROOF STEP]
show "x' \<in> \<A>[F]"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<A>[F]
p \<bullet> F = F

goal (1 subgoal):
 1. x' \<in> \<A>[F]
[PROOF STEP]
using p_x
[PROOF STATE]
proof (prove)
using this:
x \<in> \<A>[F]
p \<bullet> F = F
x' = p \<bullet> x

goal (1 subgoal):
 1. x' \<in> \<A>[F]
[PROOF STEP]
by (metis is_FL_formula_eqvt)
[PROOF STATE]
proof (state)
this:
x' \<in> \<A>[F]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<in> \<A>[F]

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<in> \<A>[F]

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "?y distinguishes P from Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) distinguishes P from Q
[PROOF STEP]
unfolding is_distinguishing_formula_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Turnstile> Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<and> \<not> Q \<Turnstile> Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<Turnstile> Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})
 2. \<not> Q \<Turnstile> Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})
[PROOF STEP]
from \<open>x distinguishes P from Q\<close>
[PROOF STATE]
proof (chain)
picking this:
x distinguishes P from Q
[PROOF STEP]
show "P \<Turnstile> ?y"
[PROOF STATE]
proof (prove)
using this:
x distinguishes P from Q

goal (1 subgoal):
 1. P \<Turnstile> Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})
[PROOF STEP]
by (auto simp add: card_B finite_supp_B) (metis is_distinguishing_formula_def fresh_star_Un supp_Pair supp_perm_eq FL_valid_eqvt)
[PROOF STATE]
proof (state)
this:
P \<Turnstile> Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})

goal (1 subgoal):
 1. \<not> Q \<Turnstile> Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Q \<Turnstile> Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})
[PROOF STEP]
from \<open>x distinguishes P from Q\<close>
[PROOF STATE]
proof (chain)
picking this:
x distinguishes P from Q
[PROOF STEP]
show "\<not> Q \<Turnstile> ?y"
[PROOF STATE]
proof (prove)
using this:
x distinguishes P from Q

goal (1 subgoal):
 1. \<not> Q \<Turnstile> Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})
[PROOF STEP]
by (auto simp add: card_B finite_supp_B) (metis is_distinguishing_formula_def permute_zero fresh_star_zero)
[PROOF STATE]
proof (state)
this:
\<not> Q \<Turnstile> Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) distinguishes P from Q

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> \<A>[F]; supp y \<subseteq> supp (F, P); y distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
supp (Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})) \<subseteq> supp (F, P)
Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<in> \<A>[F]
Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) distinguishes P from Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
supp (Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})) \<subseteq> supp (F, P)
Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<in> \<A>[F]
Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) distinguishes P from Q

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
supp (Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p})) \<subseteq> supp (F, P)
Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) \<in> \<A>[F]
Conj (Abs_bset {p \<bullet> x |p. supp (F, P) \<sharp>* p}) distinguishes P from Q
\<lbrakk>?y9 \<in> \<A>[F]; supp ?y9 \<subseteq> supp (F, P); ?y9 distinguishes P from Q\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma FL_equivalence_is_L_bisimulation: "is_L_bisimulation FL_logically_equivalent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
fix F
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
have "symp (FL_logically_equivalent F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symp (FL_logically_equivalent F)
[PROOF STEP]
by (rule sympI) (metis FL_logically_equivalent_def)
[PROOF STATE]
proof (state)
this:
symp (FL_logically_equivalent F)

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
symp (FL_logically_equivalent ?F11)

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
symp (FL_logically_equivalent ?F11)

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
symp (FL_logically_equivalent ?F11)

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
fix F P Q f \<phi>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
assume "FL_logically_equivalent F P Q" and "f \<in>\<^sub>f\<^sub>s F" and "\<langle>f\<rangle>P \<turnstile> \<phi>"
[PROOF STATE]
proof (state)
this:
FL_logically_equivalent F P Q
f \<in>\<^sub>f\<^sub>s F
\<langle>f\<rangle>P \<turnstile> \<phi>

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FL_logically_equivalent F P Q
f \<in>\<^sub>f\<^sub>s F
\<langle>f\<rangle>P \<turnstile> \<phi>
[PROOF STEP]
have "\<langle>f\<rangle>Q \<turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
FL_logically_equivalent F P Q
f \<in>\<^sub>f\<^sub>s F
\<langle>f\<rangle>P \<turnstile> \<phi>

goal (1 subgoal):
 1. \<langle>f\<rangle>Q \<turnstile> \<phi>
[PROOF STEP]
by (metis FL_logically_equivalent_def Pred FL_valid_Pred)
[PROOF STATE]
proof (state)
this:
\<langle>f\<rangle>Q \<turnstile> \<phi>

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>FL_logically_equivalent ?F11 ?P11 ?Q11; ?f11 \<in>\<^sub>f\<^sub>s ?F11; \<langle>?f11\<rangle>?P11 \<turnstile> ?\<phi>11\<rbrakk> \<Longrightarrow> \<langle>?f11\<rangle>?Q11 \<turnstile> ?\<phi>11

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>FL_logically_equivalent ?F11 ?P11 ?Q11; ?f11 \<in>\<^sub>f\<^sub>s ?F11; \<langle>?f11\<rangle>?P11 \<turnstile> ?\<phi>11\<rbrakk> \<Longrightarrow> \<langle>?f11\<rangle>?Q11 \<turnstile> ?\<phi>11

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>FL_logically_equivalent ?F11 ?P11 ?Q11; ?f11 \<in>\<^sub>f\<^sub>s ?F11; \<langle>?f11\<rangle>?P11 \<turnstile> ?\<phi>11\<rbrakk> \<Longrightarrow> \<langle>?f11\<rangle>?Q11 \<turnstile> ?\<phi>11

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
fix F P Q f \<alpha> P'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
assume "FL_logically_equivalent F P Q" and "f \<in>\<^sub>f\<^sub>s F" and "bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f)" and "\<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>"
[PROOF STATE]
proof (state)
this:
FL_logically_equivalent F P Q
f \<in>\<^sub>f\<^sub>s F
bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f)
\<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FL_logically_equivalent F P Q
f \<in>\<^sub>f\<^sub>s F
bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f)
\<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>
[PROOF STEP]
have "\<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>,F,f)) P' Q'"
[PROOF STATE]
proof (prove)
using this:
FL_logically_equivalent F P Q
f \<in>\<^sub>f\<^sub>s F
bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f)
\<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>

goal (1 subgoal):
 1. \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
let ?Q' = "{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
assume "\<forall>Q'\<in>?Q'. \<not> FL_logically_equivalent (L (\<alpha>,F,f)) P' Q'"
[PROOF STATE]
proof (state)
this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<not> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<not> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
have "\<forall>Q'\<in>?Q'. \<exists>x :: ('idx, 'pred, 'act, 'effect) formula. x \<in> \<A>[L (\<alpha>,F,f)] \<and> x distinguishes P' from Q'"
[PROOF STATE]
proof (prove)
using this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<not> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'

goal (1 subgoal):
 1. \<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<exists>x. x \<in> \<A>[L (\<alpha>, F, f)] \<and> x distinguishes P' from Q'
[PROOF STEP]
by (metis FL_equivalent_iff_not_distinguished)
[PROOF STATE]
proof (state)
this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<exists>x. x \<in> \<A>[L (\<alpha>, F, f)] \<and> x distinguishes P' from Q'

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<exists>x. x \<in> \<A>[L (\<alpha>, F, f)] \<and> x distinguishes P' from Q'
[PROOF STEP]
have "\<forall>Q'\<in>?Q'. \<exists>x :: ('idx, 'pred, 'act, 'effect) formula. x \<in> \<A>[L (\<alpha>,F,f)] \<and> supp x \<subseteq> supp (L (\<alpha>,F,f), P') \<and> x distinguishes P' from Q'"
[PROOF STATE]
proof (prove)
using this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<exists>x. x \<in> \<A>[L (\<alpha>, F, f)] \<and> x distinguishes P' from Q'

goal (1 subgoal):
 1. \<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<exists>x. x \<in> \<A>[L (\<alpha>, F, f)] \<and> supp x \<subseteq> supp (L (\<alpha>, F, f), P') \<and> x distinguishes P' from Q'
[PROOF STEP]
by (metis FL_distinguished_bounded_support)
[PROOF STATE]
proof (state)
this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<exists>x. x \<in> \<A>[L (\<alpha>, F, f)] \<and> supp x \<subseteq> supp (L (\<alpha>, F, f), P') \<and> x distinguishes P' from Q'

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<exists>x. x \<in> \<A>[L (\<alpha>, F, f)] \<and> supp x \<subseteq> supp (L (\<alpha>, F, f), P') \<and> x distinguishes P' from Q'
[PROOF STEP]
obtain g :: "'state \<Rightarrow> ('idx, 'pred, 'act, 'effect) formula" where
              *: "\<forall>Q'\<in>?Q'. g Q' \<in> \<A>[L (\<alpha>,F,f)] \<and> supp (g Q') \<subseteq> supp (L (\<alpha>,F,f), P') \<and> (g Q') distinguishes P' from Q'"
[PROOF STATE]
proof (prove)
using this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<exists>x. x \<in> \<A>[L (\<alpha>, F, f)] \<and> supp x \<subseteq> supp (L (\<alpha>, F, f), P') \<and> x distinguishes P' from Q'

goal (1 subgoal):
 1. (\<And>g. \<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. g Q' \<in> \<A>[L (\<alpha>, F, f)] \<and> supp (g Q') \<subseteq> supp (L (\<alpha>, F, f), P') \<and> g Q' distinguishes P' from Q' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. g Q' \<in> \<A>[L (\<alpha>, F, f)] \<and> supp (g Q') \<subseteq> supp (L (\<alpha>, F, f), P') \<and> g Q' distinguishes P' from Q'

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
have "supp (g ` ?Q') \<subseteq> supp (L (\<alpha>,F,f), P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}) \<subseteq> supp (L (\<alpha>, F, f), P')
[PROOF STEP]
by (rule set_bounded_supp, fact finite_supp, cut_tac "*", blast)
[PROOF STATE]
proof (state)
this:
supp (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}) \<subseteq> supp (L (\<alpha>, F, f), P')

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supp (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}) \<subseteq> supp (L (\<alpha>, F, f), P')
[PROOF STEP]
have finite_supp_image: "finite (supp (g ` ?Q'))"
[PROOF STATE]
proof (prove)
using this:
supp (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}) \<subseteq> supp (L (\<alpha>, F, f), P')

goal (1 subgoal):
 1. finite (supp (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
using finite_supp rev_finite_subset
[PROOF STATE]
proof (prove)
using this:
supp (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}) \<subseteq> supp (L (\<alpha>, F, f), P')
finite (supp ?x)
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (supp (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (supp (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
have "|g ` ?Q'| \<le>o |UNIV :: 'state set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}| \<le>o |UNIV|
[PROOF STEP]
by (metis card_of_UNIV card_of_image ordLeq_transitive)
[PROOF STATE]
proof (state)
this:
|g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}| \<le>o |UNIV|

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
|g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}| \<le>o |UNIV|

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
have "|UNIV :: 'state set| <o |UNIV :: 'idx set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |UNIV| <o |UNIV|
[PROOF STEP]
by (metis card_idx_state)
[PROOF STATE]
proof (state)
this:
|UNIV| <o |UNIV|

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
|UNIV| <o |UNIV|

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
have "|UNIV :: 'idx set| \<le>o natLeq +c |UNIV :: 'idx set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |UNIV| \<le>o natLeq +c |UNIV|
[PROOF STEP]
by (metis Cnotzero_UNIV ordLeq_csum2)
[PROOF STATE]
proof (state)
this:
|UNIV| \<le>o natLeq +c |UNIV|

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
|g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}| <o natLeq +c |UNIV|
[PROOF STEP]
have card_image: "|g ` ?Q'| <o natLeq +c |UNIV :: 'idx set|"
[PROOF STATE]
proof (prove)
using this:
|g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}| <o natLeq +c |UNIV|

goal (1 subgoal):
 1. |g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}| <o natLeq +c |UNIV|
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
|g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}| <o natLeq +c |UNIV|

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
let ?y = "Conj (Abs_bset (g ` ?Q')) :: ('idx, 'pred, 'act, 'effect) formula"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
have "Act f \<alpha> ?y \<in> \<A>[F]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))) \<in> \<A>[F]
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f \<in>\<^sub>f\<^sub>s F
 2. bn \<alpha> \<sharp>* (F, f)
 3. Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
from \<open>f \<in>\<^sub>f\<^sub>s F\<close>
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>f\<^sub>s F
[PROOF STEP]
show "f \<in>\<^sub>f\<^sub>s F"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>f\<^sub>s F

goal (1 subgoal):
 1. f \<in>\<^sub>f\<^sub>s F
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>f\<^sub>s F

goal (2 subgoals):
 1. bn \<alpha> \<sharp>* (F, f)
 2. Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bn \<alpha> \<sharp>* (F, f)
 2. Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
from \<open>bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f)\<close>
[PROOF STATE]
proof (chain)
picking this:
bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f)
[PROOF STEP]
show "bn \<alpha> \<sharp>* (F, f)"
[PROOF STATE]
proof (prove)
using this:
bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f)

goal (1 subgoal):
 1. bn \<alpha> \<sharp>* (F, f)
[PROOF STEP]
using fresh_star_Pair
[PROOF STATE]
proof (prove)
using this:
bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f)
?as \<sharp>* (?x, ?y) = (?as \<sharp>* ?x \<and> ?as \<sharp>* ?y)

goal (1 subgoal):
 1. bn \<alpha> \<sharp>* (F, f)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bn \<alpha> \<sharp>* (F, f)

goal (1 subgoal):
 1. Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
show "Conj (Abs_bset (g ` ?Q')) \<in> \<A>[L (\<alpha>, F, f)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (supp (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))
 2. \<And>x. x \<in> set_bset (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<Longrightarrow> x \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
show "finite (supp (Abs_bset (g ` ?Q') :: (_,_,_,_) formula set['idx]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (supp (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))
[PROOF STEP]
using finite_supp_image card_image
[PROOF STATE]
proof (prove)
using this:
finite (supp (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
|g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}| <o natLeq +c |UNIV|

goal (1 subgoal):
 1. finite (supp (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (supp (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))

goal (1 subgoal):
 1. \<And>x. x \<in> set_bset (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<Longrightarrow> x \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set_bset (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<Longrightarrow> x \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
fix x'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set_bset (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<Longrightarrow> x \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
assume "x' \<in> set_bset (Abs_bset (g ` ?Q') :: (_,_,_,_) formula set['idx])"
[PROOF STATE]
proof (state)
this:
x' \<in> set_bset (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))

goal (1 subgoal):
 1. \<And>x. x \<in> set_bset (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<Longrightarrow> x \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x' \<in> set_bset (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
obtain Q' where "x' = g Q'" and "\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
x' \<in> set_bset (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>x' = g Q'; \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using card_image
[PROOF STATE]
proof (prove)
using this:
x' \<in> set_bset (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
|g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}| <o natLeq +c |UNIV|

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>x' = g Q'; \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' = g Q'
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>

goal (1 subgoal):
 1. \<And>x. x \<in> set_bset (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<Longrightarrow> x \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
with "*"
[PROOF STATE]
proof (chain)
picking this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. g Q' \<in> \<A>[L (\<alpha>, F, f)] \<and> supp (g Q') \<subseteq> supp (L (\<alpha>, F, f), P') \<and> g Q' distinguishes P' from Q'
x' = g Q'
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>
[PROOF STEP]
show "x' \<in> \<A>[L (\<alpha>, F, f)]"
[PROOF STATE]
proof (prove)
using this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. g Q' \<in> \<A>[L (\<alpha>, F, f)] \<and> supp (g Q') \<subseteq> supp (L (\<alpha>, F, f), P') \<and> g Q' distinguishes P' from Q'
x' = g Q'
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>

goal (1 subgoal):
 1. x' \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
using mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. g Q' \<in> \<A>[L (\<alpha>, F, f)] \<and> supp (g Q') \<subseteq> supp (L (\<alpha>, F, f), P') \<and> g Q' distinguishes P' from Q'
x' = g Q'
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. x' \<in> \<A>[L (\<alpha>, F, f)]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x' \<in> \<A>[L (\<alpha>, F, f)]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})) \<in> \<A>[L (\<alpha>, F, f)]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))) \<in> \<A>[F]

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))) \<in> \<A>[F]

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
have "P \<Turnstile> Act f \<alpha> ?y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))
[PROOF STEP]
unfolding FL_valid_Act
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<alpha>' x' P'. Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))) = Act f \<alpha>' x' \<and> \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>',P'\<rangle> \<and> P' \<Turnstile> x'
[PROOF STEP]
proof (standard+)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,?P'4\<rangle>
 2. ?P'4 \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
show "\<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>

goal (1 subgoal):
 1. P' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
fix Q'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
assume "\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>"
[PROOF STATE]
proof (state)
this:
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>

goal (1 subgoal):
 1. P' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
with "*"
[PROOF STATE]
proof (chain)
picking this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. g Q' \<in> \<A>[L (\<alpha>, F, f)] \<and> supp (g Q') \<subseteq> supp (L (\<alpha>, F, f), P') \<and> g Q' distinguishes P' from Q'
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>
[PROOF STEP]
have "P' \<Turnstile> g Q'"
[PROOF STATE]
proof (prove)
using this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. g Q' \<in> \<A>[L (\<alpha>, F, f)] \<and> supp (g Q') \<subseteq> supp (L (\<alpha>, F, f), P') \<and> g Q' distinguishes P' from Q'
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>

goal (1 subgoal):
 1. P' \<Turnstile> g Q'
[PROOF STEP]
by (metis is_distinguishing_formula_def mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
P' \<Turnstile> g Q'

goal (1 subgoal):
 1. P' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,?Q'11\<rangle> \<Longrightarrow> P' \<Turnstile> g ?Q'11

goal (1 subgoal):
 1. P' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,?Q'11\<rangle> \<Longrightarrow> P' \<Turnstile> g ?Q'11
[PROOF STEP]
show "P' \<Turnstile> ?y"
[PROOF STATE]
proof (prove)
using this:
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,?Q'11\<rangle> \<Longrightarrow> P' \<Turnstile> g ?Q'11

goal (1 subgoal):
 1. P' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
by (simp add: finite_supp_image card_image)
[PROOF STATE]
proof (state)
this:
P' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
have "\<not> Q \<Turnstile> Act f \<alpha> ?y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Q \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))) \<Longrightarrow> False
[PROOF STEP]
assume "Q \<Turnstile> Act f \<alpha> ?y"
[PROOF STATE]
proof (state)
this:
Q \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))

goal (1 subgoal):
 1. Q \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Q \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))
[PROOF STEP]
obtain Q' where 1: "\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>" and 2: "Q' \<Turnstile> ?y"
[PROOF STATE]
proof (prove)
using this:
Q \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>; Q' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f)\<close>
[PROOF STATE]
proof (prove)
using this:
Q \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))
bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f)

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>; Q' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis fresh_star_Pair FL_valid_Act_fresh)
[PROOF STATE]
proof (state)
this:
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>
Q' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))

goal (1 subgoal):
 1. Q \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))) \<Longrightarrow> False
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
Q' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))
[PROOF STEP]
have "\<And>Q''. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q''\<rangle> \<longrightarrow> Q' \<Turnstile> g Q''"
[PROOF STATE]
proof (prove)
using this:
Q' \<Turnstile> Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))

goal (1 subgoal):
 1. \<And>Q''. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q''\<rangle> \<longrightarrow> Q' \<Turnstile> g Q''
[PROOF STEP]
by (simp add: finite_supp_image card_image)
[PROOF STATE]
proof (state)
this:
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,?Q''9\<rangle> \<longrightarrow> Q' \<Turnstile> g ?Q''9

goal (1 subgoal):
 1. Q \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))) \<Longrightarrow> False
[PROOF STEP]
with 1 and "*"
[PROOF STATE]
proof (chain)
picking this:
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. g Q' \<in> \<A>[L (\<alpha>, F, f)] \<and> supp (g Q') \<subseteq> supp (L (\<alpha>, F, f), P') \<and> g Q' distinguishes P' from Q'
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,?Q''9\<rangle> \<longrightarrow> Q' \<Turnstile> g ?Q''9
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. g Q' \<in> \<A>[L (\<alpha>, F, f)] \<and> supp (g Q') \<subseteq> supp (L (\<alpha>, F, f), P') \<and> g Q' distinguishes P' from Q'
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,?Q''9\<rangle> \<longrightarrow> Q' \<Turnstile> g ?Q''9

goal (1 subgoal):
 1. False
[PROOF STEP]
using is_distinguishing_formula_def
[PROOF STATE]
proof (prove)
using this:
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. g Q' \<in> \<A>[L (\<alpha>, F, f)] \<and> supp (g Q') \<subseteq> supp (L (\<alpha>, F, f), P') \<and> g Q' distinguishes P' from Q'
\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,?Q''9\<rangle> \<longrightarrow> Q' \<Turnstile> g ?Q''9
?x distinguishes ?P from ?Q \<equiv> ?P \<Turnstile> ?x \<and> \<not> ?Q \<Turnstile> ?x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> Q \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))) \<in> \<A>[F]
P \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))
\<not> Q \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}))) \<in> \<A>[F]
P \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))
\<not> Q \<Turnstile> Act f \<alpha> (Conj (Abs_bset (g ` {Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>})))

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis \<open>FL_logically_equivalent F P Q\<close> FL_logically_equivalent_def)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<not> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q' \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>FL_logically_equivalent F P Q; f \<in>\<^sub>f\<^sub>s F; bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f); \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<not> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q' \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>Q'\<in>{Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>}. \<not> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q' \<Longrightarrow> False

goal (1 subgoal):
 1. \<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>FL_logically_equivalent ?F11 ?P11 ?Q11; ?f11 \<in>\<^sub>f\<^sub>s ?F11; bn ?\<alpha>11 \<sharp>* (\<langle>?f11\<rangle>?Q11, ?F11, ?f11); \<langle>?f11\<rangle>?P11 \<rightarrow> \<langle>?\<alpha>11,?P'11\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>?f11\<rangle>?Q11 \<rightarrow> \<langle>?\<alpha>11,Q'\<rangle> \<and> FL_logically_equivalent (L (?\<alpha>11, ?F11, ?f11)) ?P'11 Q'

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
symp (FL_logically_equivalent ?F11)
\<lbrakk>FL_logically_equivalent ?F11 ?P11 ?Q11; ?f11 \<in>\<^sub>f\<^sub>s ?F11; \<langle>?f11\<rangle>?P11 \<turnstile> ?\<phi>11\<rbrakk> \<Longrightarrow> \<langle>?f11\<rangle>?Q11 \<turnstile> ?\<phi>11
\<lbrakk>FL_logically_equivalent ?F11 ?P11 ?Q11; ?f11 \<in>\<^sub>f\<^sub>s ?F11; bn ?\<alpha>11 \<sharp>* (\<langle>?f11\<rangle>?Q11, ?F11, ?f11); \<langle>?f11\<rangle>?P11 \<rightarrow> \<langle>?\<alpha>11,?P'11\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>?f11\<rangle>?Q11 \<rightarrow> \<langle>?\<alpha>11,Q'\<rangle> \<and> FL_logically_equivalent (L (?\<alpha>11, ?F11, ?f11)) ?P'11 Q'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
symp (FL_logically_equivalent ?F11)
\<lbrakk>FL_logically_equivalent ?F11 ?P11 ?Q11; ?f11 \<in>\<^sub>f\<^sub>s ?F11; \<langle>?f11\<rangle>?P11 \<turnstile> ?\<phi>11\<rbrakk> \<Longrightarrow> \<langle>?f11\<rangle>?Q11 \<turnstile> ?\<phi>11
\<lbrakk>FL_logically_equivalent ?F11 ?P11 ?Q11; ?f11 \<in>\<^sub>f\<^sub>s ?F11; bn ?\<alpha>11 \<sharp>* (\<langle>?f11\<rangle>?Q11, ?F11, ?f11); \<langle>?f11\<rangle>?P11 \<rightarrow> \<langle>?\<alpha>11,?P'11\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>?f11\<rangle>?Q11 \<rightarrow> \<langle>?\<alpha>11,Q'\<rangle> \<and> FL_logically_equivalent (L (?\<alpha>11, ?F11, ?f11)) ?P'11 Q'

goal (1 subgoal):
 1. is_L_bisimulation FL_logically_equivalent
[PROOF STEP]
unfolding is_L_bisimulation_def
[PROOF STATE]
proof (prove)
using this:
symp (FL_logically_equivalent ?F11)
\<lbrakk>FL_logically_equivalent ?F11 ?P11 ?Q11; ?f11 \<in>\<^sub>f\<^sub>s ?F11; \<langle>?f11\<rangle>?P11 \<turnstile> ?\<phi>11\<rbrakk> \<Longrightarrow> \<langle>?f11\<rangle>?Q11 \<turnstile> ?\<phi>11
\<lbrakk>FL_logically_equivalent ?F11 ?P11 ?Q11; ?f11 \<in>\<^sub>f\<^sub>s ?F11; bn ?\<alpha>11 \<sharp>* (\<langle>?f11\<rangle>?Q11, ?F11, ?f11); \<langle>?f11\<rangle>?P11 \<rightarrow> \<langle>?\<alpha>11,?P'11\<rangle>\<rbrakk> \<Longrightarrow> \<exists>Q'. \<langle>?f11\<rangle>?Q11 \<rightarrow> \<langle>?\<alpha>11,Q'\<rangle> \<and> FL_logically_equivalent (L (?\<alpha>11, ?F11, ?f11)) ?P'11 Q'

goal (1 subgoal):
 1. \<forall>F. symp (FL_logically_equivalent F) \<and> (\<forall>P Q. FL_logically_equivalent F P Q \<longrightarrow> (\<forall>f. f \<in>\<^sub>f\<^sub>s F \<longrightarrow> (\<forall>\<phi>. \<langle>f\<rangle>P \<turnstile> \<phi> \<longrightarrow> \<langle>f\<rangle>Q \<turnstile> \<phi>))) \<and> (\<forall>P Q. FL_logically_equivalent F P Q \<longrightarrow> (\<forall>f. f \<in>\<^sub>f\<^sub>s F \<longrightarrow> (\<forall>\<alpha> P'. bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f) \<longrightarrow> \<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle> \<longrightarrow> (\<exists>Q'. \<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle> \<and> FL_logically_equivalent (L (\<alpha>, F, f)) P' Q'))))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_L_bisimulation FL_logically_equivalent

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem FL_equivalence_implies_bisimilarity: assumes "FL_logically_equivalent F P Q" shows "P \<sim>\<cdot>[F] Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<sim>\<cdot>[F] Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
FL_logically_equivalent F P Q

goal (1 subgoal):
 1. P \<sim>\<cdot>[F] Q
[PROOF STEP]
by (metis FL_bisimilar_def FL_equivalence_is_L_bisimulation)


[STATEMENT]
lemma denote_density_states:
  "\<rho> \<in> density_states \<Longrightarrow> well_com S \<Longrightarrow> denote S \<rho> \<in> density_states"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<rho> \<in> density_states; well_com S\<rbrakk> \<Longrightarrow> denote S \<rho> \<in> density_states
[PROOF STEP]
by (simp add: denote_dim_pdo density_states_def)


[STATEMENT]
lemma trace_measurement2:
  assumes m: "measurement n 2 M" and dA: "A \<in> carrier_mat n n"
  shows "trace ((M 0) * A * adjoint (M 0)) + trace ((M 1) * A * adjoint (M 1)) = trace A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (M 0 * A * adjoint (M 0)) + trace (M 1 * A * adjoint (M 1)) = trace A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace (M 0 * A * adjoint (M 0)) + trace (M 1 * A * adjoint (M 1)) = trace A
[PROOF STEP]
from m
[PROOF STATE]
proof (chain)
picking this:
measurement n 2 M
[PROOF STEP]
have dM0: "M 0 \<in> carrier_mat n n" and dM1: "M 1 \<in> carrier_mat n n" and id: "adjoint (M 0) * (M 0) + adjoint (M 1) * (M 1) = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
using this:
measurement n 2 M

goal (1 subgoal):
 1. M 0 \<in> carrier_mat n n &&& M 1 \<in> carrier_mat n n &&& adjoint (M 0) * M 0 + adjoint (M 1) * M 1 = 1\<^sub>m n
[PROOF STEP]
using measurement_def measurement_id2
[PROOF STATE]
proof (prove)
using this:
measurement n 2 M
measurement ?d ?n ?M = ((\<forall>j<?n. ?M j \<in> carrier_mat ?d ?d) \<and> matrix_sum ?d (\<lambda>j. adjoint (?M j) * ?M j) ?n = 1\<^sub>m ?d)
measurement ?d 2 ?M \<Longrightarrow> adjoint (?M 0) * ?M 0 + adjoint (?M 1) * ?M 1 = 1\<^sub>m ?d

goal (1 subgoal):
 1. M 0 \<in> carrier_mat n n &&& M 1 \<in> carrier_mat n n &&& adjoint (M 0) * M 0 + adjoint (M 1) * M 1 = 1\<^sub>m n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M 0 \<in> carrier_mat n n
M 1 \<in> carrier_mat n n
adjoint (M 0) * M 0 + adjoint (M 1) * M 1 = 1\<^sub>m n

goal (1 subgoal):
 1. trace (M 0 * A * adjoint (M 0)) + trace (M 1 * A * adjoint (M 1)) = trace A
[PROOF STEP]
have "trace (M 1 * A * adjoint (M 1)) + trace (M 0 * A * adjoint (M 0))
    = trace ((adjoint (M 0) * M 0 + adjoint (M 1) * M 1) * A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (M 1 * A * adjoint (M 1)) + trace (M 0 * A * adjoint (M 0)) = trace ((adjoint (M 0) * M 0 + adjoint (M 1) * M 1) * A)
[PROOF STEP]
using dM0 dM1 dA
[PROOF STATE]
proof (prove)
using this:
M 0 \<in> carrier_mat n n
M 1 \<in> carrier_mat n n
A \<in> carrier_mat n n

goal (1 subgoal):
 1. trace (M 1 * A * adjoint (M 1)) + trace (M 0 * A * adjoint (M 0)) = trace ((adjoint (M 0) * M 0 + adjoint (M 1) * M 1) * A)
[PROOF STEP]
by (mat_assoc n)
[PROOF STATE]
proof (state)
this:
trace (M 1 * A * adjoint (M 1)) + trace (M 0 * A * adjoint (M 0)) = trace ((adjoint (M 0) * M 0 + adjoint (M 1) * M 1) * A)

goal (1 subgoal):
 1. trace (M 0 * A * adjoint (M 0)) + trace (M 1 * A * adjoint (M 1)) = trace A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (M 1 * A * adjoint (M 1)) + trace (M 0 * A * adjoint (M 0)) = trace ((adjoint (M 0) * M 0 + adjoint (M 1) * M 1) * A)

goal (1 subgoal):
 1. trace (M 0 * A * adjoint (M 0)) + trace (M 1 * A * adjoint (M 1)) = trace A
[PROOF STEP]
have "\<dots> = trace (1\<^sub>m n * A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace ((adjoint (M 0) * M 0 + adjoint (M 1) * M 1) * A) = trace (1\<^sub>m n * A)
[PROOF STEP]
using id
[PROOF STATE]
proof (prove)
using this:
adjoint (M 0) * M 0 + adjoint (M 1) * M 1 = 1\<^sub>m n

goal (1 subgoal):
 1. trace ((adjoint (M 0) * M 0 + adjoint (M 1) * M 1) * A) = trace (1\<^sub>m n * A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace ((adjoint (M 0) * M 0 + adjoint (M 1) * M 1) * A) = trace (1\<^sub>m n * A)

goal (1 subgoal):
 1. trace (M 0 * A * adjoint (M 0)) + trace (M 1 * A * adjoint (M 1)) = trace A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace ((adjoint (M 0) * M 0 + adjoint (M 1) * M 1) * A) = trace (1\<^sub>m n * A)

goal (1 subgoal):
 1. trace (M 0 * A * adjoint (M 0)) + trace (M 1 * A * adjoint (M 1)) = trace A
[PROOF STEP]
have "\<dots> = trace A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (1\<^sub>m n * A) = trace A
[PROOF STEP]
using dA
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. trace (1\<^sub>m n * A) = trace A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (1\<^sub>m n * A) = trace A

goal (1 subgoal):
 1. trace (M 0 * A * adjoint (M 0)) + trace (M 1 * A * adjoint (M 1)) = trace A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trace (M 1 * A * adjoint (M 1)) + trace (M 0 * A * adjoint (M 0)) = trace A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace (M 1 * A * adjoint (M 1)) + trace (M 0 * A * adjoint (M 0)) = trace A

goal (1 subgoal):
 1. trace (M 0 * A * adjoint (M 0)) + trace (M 1 * A * adjoint (M 1)) = trace A
[PROOF STEP]
using dA dM0 dM1 local.id state_sig.trace_measure2_id
[PROOF STATE]
proof (prove)
using this:
trace (M 1 * A * adjoint (M 1)) + trace (M 0 * A * adjoint (M 0)) = trace A
A \<in> carrier_mat n n
M 0 \<in> carrier_mat n n
M 1 \<in> carrier_mat n n
adjoint (M 0) * M 0 + adjoint (M 1) * M 1 = 1\<^sub>m n
\<lbrakk>?M0.0 \<in> carrier_mat ?n ?n; ?M1.0 \<in> carrier_mat ?n ?n; adjoint ?M0.0 * ?M0.0 + adjoint ?M1.0 * ?M1.0 = 1\<^sub>m ?n; ?A \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> trace (?M0.0 * ?A * adjoint ?M0.0) + trace (?M1.0 * ?A * adjoint ?M1.0) = trace ?A

goal (1 subgoal):
 1. trace (M 0 * A * adjoint (M 0)) + trace (M 1 * A * adjoint (M 1)) = trace A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trace (M 0 * A * adjoint (M 0)) + trace (M 1 * A * adjoint (M 1)) = trace A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qp_close_under_unitary_operator:
  fixes U P :: "complex mat"
  assumes dU: "U \<in> carrier_mat d d"
    and u: "unitary U"
    and qp: "is_quantum_predicate P"
  shows "is_quantum_predicate (adjoint U * P * U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (adjoint U * P * U)
[PROOF STEP]
unfolding is_quantum_predicate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint U * P * U \<in> carrier_mat d d \<and> positive (adjoint U * P * U) \<and> adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. adjoint U * P * U \<in> carrier_mat d d
 2. positive (adjoint U * P * U)
 3. adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have dP: "P \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat d d
[PROOF STEP]
using qp is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate P
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

goal (1 subgoal):
 1. P \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat d d

goal (3 subgoals):
 1. adjoint U * P * U \<in> carrier_mat d d
 2. positive (adjoint U * P * U)
 3. adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
show "adjoint U * P * U \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint U * P * U \<in> carrier_mat d d
[PROOF STEP]
using dU dP
[PROOF STATE]
proof (prove)
using this:
U \<in> carrier_mat d d
P \<in> carrier_mat d d

goal (1 subgoal):
 1. adjoint U * P * U \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
adjoint U * P * U \<in> carrier_mat d d

goal (2 subgoals):
 1. positive (adjoint U * P * U)
 2. adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "positive P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive P
[PROOF STEP]
using qp is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate P
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

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

goal (2 subgoals):
 1. positive (adjoint U * P * U)
 2. adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive P
[PROOF STEP]
show "positive (adjoint U * P * U)"
[PROOF STATE]
proof (prove)
using this:
positive P

goal (1 subgoal):
 1. positive (adjoint U * P * U)
[PROOF STEP]
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dU] dP, simplified adjoint_adjoint]
[PROOF STATE]
proof (prove)
using this:
positive P
positive P \<Longrightarrow> positive (adjoint U * P * U)

goal (1 subgoal):
 1. positive (adjoint U * P * U)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
positive (adjoint U * P * U)

goal (1 subgoal):
 1. adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "adjoint U * U = 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint U * U = 1\<^sub>m d
[PROOF STEP]
apply (subgoal_tac "inverts_mat (adjoint U) U")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. inverts_mat (adjoint U) U \<Longrightarrow> adjoint U * U = 1\<^sub>m d
 2. inverts_mat (adjoint U) U
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverts_mat (adjoint U) U \<Longrightarrow> adjoint U * U = 1\<^sub>m d
[PROOF STEP]
unfolding inverts_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint U * U = 1\<^sub>m (dim_row (adjoint U)) \<Longrightarrow> adjoint U * U = 1\<^sub>m d
[PROOF STEP]
using dU
[PROOF STATE]
proof (prove)
using this:
U \<in> carrier_mat d d

goal (1 subgoal):
 1. adjoint U * U = 1\<^sub>m (dim_row (adjoint U)) \<Longrightarrow> adjoint U * U = 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverts_mat (adjoint U) U
[PROOF STEP]
using u
[PROOF STATE]
proof (prove)
using this:
unitary U

goal (1 subgoal):
 1. inverts_mat (adjoint U) U
[PROOF STEP]
unfolding unitary_def
[PROOF STATE]
proof (prove)
using this:
U \<in> carrier_mat (dim_row U) (dim_row U) \<and> inverts_mat U (adjoint U)

goal (1 subgoal):
 1. inverts_mat (adjoint U) U
[PROOF STEP]
using inverts_mat_symm[OF dU adjoint_dim[OF dU]]
[PROOF STATE]
proof (prove)
using this:
U \<in> carrier_mat (dim_row U) (dim_row U) \<and> inverts_mat U (adjoint U)
inverts_mat U (adjoint U) \<Longrightarrow> inverts_mat (adjoint U) U

goal (1 subgoal):
 1. inverts_mat (adjoint U) U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint U * U = 1\<^sub>m d

goal (1 subgoal):
 1. adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
adjoint U * U = 1\<^sub>m d
[PROOF STEP]
have u': "adjoint U * 1\<^sub>m d * U = 1\<^sub>m d"
[PROOF STATE]
proof (prove)
using this:
adjoint U * U = 1\<^sub>m d

goal (1 subgoal):
 1. adjoint U * 1\<^sub>m d * U = 1\<^sub>m d
[PROOF STEP]
using dU
[PROOF STATE]
proof (prove)
using this:
adjoint U * U = 1\<^sub>m d
U \<in> carrier_mat d d

goal (1 subgoal):
 1. adjoint U * 1\<^sub>m d * U = 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint U * 1\<^sub>m d * U = 1\<^sub>m d

goal (1 subgoal):
 1. adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have le: "P \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using qp is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate P
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

goal (1 subgoal):
 1. P \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
show "adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using lowner_le_keep_under_measurement[OF dU dP one_carrier_mat le] u'
[PROOF STATE]
proof (prove)
using this:
adjoint U * P * U \<le>\<^sub>L adjoint U * 1\<^sub>m d * U
adjoint U * 1\<^sub>m d * U = 1\<^sub>m d

goal (1 subgoal):
 1. adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint U * P * U \<le>\<^sub>L 1\<^sub>m d

goal:
No subgoals!
[PROOF STEP]
qed