[STATEMENT]
lemma distinguishing_weak_formula_is_weak:
    assumes "\<not> (P \<equiv>\<cdot> Q)"
    shows "weak_formula (distinguishing_weak_formula P Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
let ?some = "\<lambda>p. (\<some>x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
let ?B = "{- p \<bullet> ?some p|p. True}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> P \<equiv>\<cdot> Q
[PROOF STEP]
have "supp (Abs_bset ?B :: _ set['idx]) \<subseteq> supp P"
[PROOF STATE]
proof (prove)
using this:
\<not> P \<equiv>\<cdot> Q

goal (1 subgoal):
 1. supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) \<subseteq> supp P
[PROOF STEP]
by (rule distinguishing_weak_formula_supp_aux)
[PROOF STATE]
proof (state)
this:
supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) \<subseteq> supp P

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) \<subseteq> supp P
[PROOF STEP]
have "finite (supp (Abs_bset ?B :: _ set['idx]))"
[PROOF STATE]
proof (prove)
using this:
supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) \<subseteq> supp P

goal (1 subgoal):
 1. finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
[PROOF STEP]
using finite_supp rev_finite_subset
[PROOF STATE]
proof (prove)
using this:
supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) \<subseteq> supp P
finite (supp ?x)
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
have "set_bset (Abs_bset ?B :: _ set['idx]) = ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
[PROOF STEP]
using distinguishing_weak_formula_card_aux Abs_bset_inverse'
[PROOF STATE]
proof (prove)
using this:
|{- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> ?P) \<and> x distinguishes (p \<bullet> ?P) from (p \<bullet> ?Q)) |p. True}| <o natLeq +c |UNIV|
|?A| <o natLeq +c |UNIV| \<Longrightarrow> set_bset (Abs_bset ?A) = ?A

goal (1 subgoal):
 1. set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
assume "x \<in> ?B"
[PROOF STATE]
proof (state)
this:
x \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
[PROOF STEP]
obtain p where "x = -p \<bullet> ?some p"
[PROOF STATE]
proof (prove)
using this:
x \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}

goal (1 subgoal):
 1. (\<And>p. x = - p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = - p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = - p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> P \<equiv>\<cdot> Q
[PROOF STEP]
have "\<not> (p \<bullet> P) \<equiv>\<cdot> (p \<bullet> Q)"
[PROOF STATE]
proof (prove)
using this:
\<not> P \<equiv>\<cdot> Q

goal (1 subgoal):
 1. \<not> p \<bullet> P \<equiv>\<cdot> p \<bullet> Q
[PROOF STEP]
by (metis permute_minus_cancel(2) weakly_logically_equivalent_eqvt)
[PROOF STATE]
proof (state)
this:
\<not> p \<bullet> P \<equiv>\<cdot> p \<bullet> Q

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> p \<bullet> P \<equiv>\<cdot> p \<bullet> Q
[PROOF STEP]
have "weak_formula (?some p)"
[PROOF STATE]
proof (prove)
using this:
\<not> p \<bullet> P \<equiv>\<cdot> p \<bullet> Q

goal (1 subgoal):
 1. weak_formula (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))
[PROOF STEP]
by (metis (mono_tags, lifting) distinguished_bounded_support weakly_equivalent_iff_not_distinguished someI_ex)
[PROOF STATE]
proof (state)
this:
weak_formula (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = - p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))
weak_formula (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))
[PROOF STEP]
have "weak_formula x"
[PROOF STATE]
proof (prove)
using this:
x = - p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))
weak_formula (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))

goal (1 subgoal):
 1. weak_formula x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
weak_formula x

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x9 \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True} \<Longrightarrow> weak_formula ?x9

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
?x9 \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True} \<Longrightarrow> weak_formula ?x9
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
?x9 \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True} \<Longrightarrow> weak_formula ?x9

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
unfolding distinguishing_weak_formula_def
[PROOF STATE]
proof (prove)
using this:
finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
?x9 \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True} \<Longrightarrow> weak_formula ?x9

goal (1 subgoal):
 1. weak_formula (Conj (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
[PROOF STEP]
using wf_Conj
[PROOF STATE]
proof (prove)
using this:
finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
?x9 \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True} \<Longrightarrow> weak_formula ?x9
\<lbrakk>finite (supp ?xset); \<And>x. x \<in> set_bset ?xset \<Longrightarrow> weak_formula x\<rbrakk> \<Longrightarrow> weak_formula (Conj ?xset)

goal (1 subgoal):
 1. weak_formula (Conj (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
weak_formula (distinguishing_weak_formula P Q)

goal:
No subgoals!
[PROOF STEP]
qed