[STATEMENT]
lemma mirror_ex:
  assumes "iszlfm p"
  shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) \<longleftrightarrow> (\<exists>x. Ifm bbs (x#bs) p)"
  (is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. Ifm bbs (x # bs) (mirror p)) = (\<exists>x. Ifm bbs (x # bs) p)
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. Ifm bbs (x # bs) (mirror p) \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) p
 2. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. Ifm bbs (x # bs) (mirror p) \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) p
 2. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
assume "?I x ?mp"
[PROOF STATE]
proof (state)
this:
Ifm bbs (x # bs) (mirror p)

goal (2 subgoals):
 1. \<And>x. Ifm bbs (x # bs) (mirror p) \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) p
 2. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
have "?I (- x) p"
[PROOF STATE]
proof (prove)
using this:
Ifm bbs (x # bs) (mirror p)

goal (1 subgoal):
 1. Ifm bbs (- x # bs) p
[PROOF STEP]
using mirror[OF assms]
[PROOF STATE]
proof (prove)
using this:
Ifm bbs (x # bs) (mirror p)
Ifm ?bbs (?x # ?bs) (mirror p) = Ifm ?bbs (- ?x # ?bs) p

goal (1 subgoal):
 1. Ifm bbs (- x # bs) p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ifm bbs (- x # bs) p

goal (2 subgoals):
 1. \<And>x. Ifm bbs (x # bs) (mirror p) \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) p
 2. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ifm bbs (- x # bs) p
[PROOF STEP]
show "\<exists>x. ?I x p"
[PROOF STATE]
proof (prove)
using this:
Ifm bbs (- x # bs) p

goal (1 subgoal):
 1. \<exists>x. Ifm bbs (x # bs) p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. Ifm bbs (x # bs) p

goal (1 subgoal):
 1. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
assume "?I x p"
[PROOF STATE]
proof (state)
this:
Ifm bbs (x # bs) p

goal (1 subgoal):
 1. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ifm bbs (x # bs) p
[PROOF STEP]
have "?I (- x) ?mp"
[PROOF STATE]
proof (prove)
using this:
Ifm bbs (x # bs) p

goal (1 subgoal):
 1. Ifm bbs (- x # bs) (mirror p)
[PROOF STEP]
using mirror[OF assms, where x="- x", symmetric]
[PROOF STATE]
proof (prove)
using this:
Ifm bbs (x # bs) p
Ifm ?bbs (- (- x) # ?bs) p = Ifm ?bbs (- x # ?bs) (mirror p)

goal (1 subgoal):
 1. Ifm bbs (- x # bs) (mirror p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ifm bbs (- x # bs) (mirror p)

goal (1 subgoal):
 1. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ifm bbs (- x # bs) (mirror p)
[PROOF STEP]
show "\<exists>x. ?I x ?mp"
[PROOF STATE]
proof (prove)
using this:
Ifm bbs (- x # bs) (mirror p)

goal (1 subgoal):
 1. \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. Ifm bbs (x # bs) (mirror p)

goal:
No subgoals!
[PROOF STEP]
qed