[STATEMENT]
lemma min_inf:
  "nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs)"
  (is "_ \<Longrightarrow> \<exists>x. ?P f x")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs)
[PROOF STEP]
proof(induct f)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>x. nqfree (Atom x) \<Longrightarrow> \<exists>xa. \<forall>y\<le>xa. R.I (inf\<^sub>- (Atom x)) xs = R.I (Atom x) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 5. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 7. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
case (Atom a)
[PROOF STATE]
proof (state)
this:
nqfree (Atom a)

goal (7 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>x. nqfree (Atom x) \<Longrightarrow> \<exists>xa. \<forall>y\<le>xa. R.I (inf\<^sub>- (Atom x)) xs = R.I (Atom x) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 5. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 7. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. a = Less x11 x12 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
 2. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
case (Less r cs)
[PROOF STATE]
proof (state)
this:
a = Less r cs

goal (2 subgoals):
 1. \<And>x11 x12. a = Less x11 x12 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
 2. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
proof(cases cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs = [] \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
 2. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
cs = []

goal (2 subgoals):
 1. cs = [] \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
 2. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cs = []

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Less
[PROOF STATE]
proof (prove)
using this:
cs = []
a = Less r cs

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
cs__ = c # cs

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
cs__ = c # cs

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
assume "c=0"
[PROOF STATE]
proof (state)
this:
c = 0

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Less Cons
[PROOF STATE]
proof (prove)
using this:
c = 0
a = Less r cs__
cs__ = c # cs

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
assume "c<0"
[PROOF STATE]
proof (state)
this:
c < 0

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence "?P (Atom a) ((r - \<langle>cs,xs\<rangle> + 1)/c)"
[PROOF STATE]
proof (prove)
using this:
c < 0

goal (1 subgoal):
 1. \<forall>y\<le>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Less Cons
[PROOF STATE]
proof (prove)
using this:
c < 0
a = Less r cs__
cs__ = c # cs

goal (1 subgoal):
 1. \<forall>y\<le>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by(auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<forall>y\<le>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<le>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
assume "c>0"
[PROOF STATE]
proof (state)
this:
0 < c

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence "?P (Atom a) ((r - \<langle>cs,xs\<rangle> - 1)/c)"
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. \<forall>y\<le>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Less Cons
[PROOF STATE]
proof (prove)
using this:
0 < c
a = Less r cs__
cs__ = c # cs

goal (1 subgoal):
 1. \<forall>y\<le>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by(auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<forall>y\<le>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<le>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 < c \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
0 < c \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
0 < c \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
case (Eq r cs)
[PROOF STATE]
proof (state)
this:
a = Eq r cs

goal (1 subgoal):
 1. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
proof(cases cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs = [] \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
 2. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
cs = []

goal (2 subgoals):
 1. cs = [] \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
 2. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cs = []

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Eq
[PROOF STATE]
proof (prove)
using this:
cs = []
a = Eq r cs

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
cs__ = c # cs

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
cs__ = c # cs

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
assume "c=0"
[PROOF STATE]
proof (state)
this:
c = 0

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Eq Cons
[PROOF STATE]
proof (prove)
using this:
c = 0
a = Eq r cs__
cs__ = c # cs

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
assume "c<0"
[PROOF STATE]
proof (state)
this:
c < 0

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence "?P (Atom a) ((r - \<langle>cs,xs\<rangle> + 1)/c)"
[PROOF STATE]
proof (prove)
using this:
c < 0

goal (1 subgoal):
 1. \<forall>y\<le>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Eq Cons
[PROOF STATE]
proof (prove)
using this:
c < 0
a = Eq r cs__
cs__ = c # cs

goal (1 subgoal):
 1. \<forall>y\<le>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by(auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<forall>y\<le>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<le>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
assume "c>0"
[PROOF STATE]
proof (state)
this:
0 < c

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence "?P (Atom a) ((r - \<langle>cs,xs\<rangle> - 1)/c)"
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. \<forall>y\<le>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Eq Cons
[PROOF STATE]
proof (prove)
using this:
0 < c
a = Eq r cs__
cs__ = c # cs

goal (1 subgoal):
 1. \<forall>y\<le>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by(auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<forall>y\<le>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<le>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 < c \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
0 < c \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
0 < c \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Atom a)) xs = R.I (Atom a) (y # xs)

goal (6 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
case (And f1 f2)
[PROOF STATE]
proof (state)
this:
nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs)
nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs)
nqfree (And f1 f2)

goal (6 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs)
nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs)
nqfree (And f1 f2)
[PROOF STEP]
obtain x1 x2 where "?P f1 x1" "?P f2 x2"
[PROOF STATE]
proof (prove)
using this:
nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs)
nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs)
nqfree (And f1 f2)

goal (1 subgoal):
 1. (\<And>x1 x2. \<lbrakk>\<forall>y\<le>x1. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); \<forall>y\<le>x2. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
\<forall>y\<le>x1. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs)
\<forall>y\<le>x2. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs)

goal (6 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
hence "?P (And f1 f2) (min x1 x2)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<le>x1. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs)
\<forall>y\<le>x2. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs)

goal (1 subgoal):
 1. \<forall>y\<le>min x1 x2. R.I (inf\<^sub>- (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
[PROOF STEP]
by(force simp:and_def)
[PROOF STATE]
proof (state)
this:
\<forall>y\<le>min x1 x2. R.I (inf\<^sub>- (And f1 f2)) xs = R.I (And f1 f2) (y # xs)

goal (6 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<le>min x1 x2. R.I (inf\<^sub>- (And f1 f2)) xs = R.I (And f1 f2) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (And f1 f2)) xs = R.I (And f1 f2) (y # xs)

goal (5 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 4. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 4. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
case (Or f1 f2)
[PROOF STATE]
proof (state)
this:
nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs)
nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs)
nqfree (Or f1 f2)

goal (5 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 4. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs)
nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs)
nqfree (Or f1 f2)
[PROOF STEP]
obtain x1 x2 where "?P f1 x1" "?P f2 x2"
[PROOF STATE]
proof (prove)
using this:
nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs)
nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs)
nqfree (Or f1 f2)

goal (1 subgoal):
 1. (\<And>x1 x2. \<lbrakk>\<forall>y\<le>x1. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); \<forall>y\<le>x2. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
\<forall>y\<le>x1. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs)
\<forall>y\<le>x2. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs)

goal (5 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 4. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
hence "?P (Or f1 f2) (min x1 x2)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<le>x1. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs)
\<forall>y\<le>x2. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs)

goal (1 subgoal):
 1. \<forall>y\<le>min x1 x2. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
[PROOF STEP]
by(force simp:or_def)
[PROOF STATE]
proof (state)
this:
\<forall>y\<le>min x1 x2. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)

goal (5 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 4. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<le>min x1 x2. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)

goal (4 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (Neg f)) xs = R.I (Neg f) (y # xs)
 4. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<le>x. R.I (inf\<^sub>- (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma plus_inf:
  "nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs)"
  (is "_ \<Longrightarrow> \<exists>x. ?P f x")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs)
[PROOF STEP]
proof(induct f)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>x. nqfree (Atom x) \<Longrightarrow> \<exists>xa. \<forall>y\<ge>xa. R.I (inf\<^sub>+ (Atom x)) xs = R.I (Atom x) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 5. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 7. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
case (Atom a)
[PROOF STATE]
proof (state)
this:
nqfree (Atom a)

goal (7 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>x. nqfree (Atom x) \<Longrightarrow> \<exists>xa. \<forall>y\<ge>xa. R.I (inf\<^sub>+ (Atom x)) xs = R.I (Atom x) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 5. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 7. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. a = Less x11 x12 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
 2. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
case (Less r cs)
[PROOF STATE]
proof (state)
this:
a = Less r cs

goal (2 subgoals):
 1. \<And>x11 x12. a = Less x11 x12 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
 2. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
proof(cases cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs = [] \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
 2. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
cs = []

goal (2 subgoals):
 1. cs = [] \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
 2. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cs = []

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Less
[PROOF STATE]
proof (prove)
using this:
cs = []
a = Less r cs

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
cs__ = c # cs

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
cs__ = c # cs

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
assume "c=0"
[PROOF STATE]
proof (state)
this:
c = 0

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Less Cons
[PROOF STATE]
proof (prove)
using this:
c = 0
a = Less r cs__
cs__ = c # cs

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
assume "c<0"
[PROOF STATE]
proof (state)
this:
c < 0

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence "?P (Atom a) ((r - \<langle>cs,xs\<rangle> - 1)/c)"
[PROOF STATE]
proof (prove)
using this:
c < 0

goal (1 subgoal):
 1. \<forall>y\<ge>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Less Cons
[PROOF STATE]
proof (prove)
using this:
c < 0
a = Less r cs__
cs__ = c # cs

goal (1 subgoal):
 1. \<forall>y\<ge>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by(auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<forall>y\<ge>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<ge>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
assume "c>0"
[PROOF STATE]
proof (state)
this:
0 < c

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence "?P (Atom a) ((r - \<langle>cs,xs\<rangle> + 1)/c)"
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. \<forall>y\<ge>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Less Cons
[PROOF STATE]
proof (prove)
using this:
0 < c
a = Less r cs__
cs__ = c # cs

goal (1 subgoal):
 1. \<forall>y\<ge>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by(auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<forall>y\<ge>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<ge>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 < c \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
0 < c \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
0 < c \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
case (Eq r cs)
[PROOF STATE]
proof (state)
this:
a = Eq r cs

goal (1 subgoal):
 1. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
proof(cases cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs = [] \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
 2. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
cs = []

goal (2 subgoals):
 1. cs = [] \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
 2. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cs = []

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Eq
[PROOF STATE]
proof (prove)
using this:
cs = []
a = Eq r cs

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. cs = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
cs__ = c # cs

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
cs__ = c # cs

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
assume "c=0"
[PROOF STATE]
proof (state)
this:
c = 0

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Eq Cons
[PROOF STATE]
proof (prove)
using this:
c = 0
a = Eq r cs__
cs__ = c # cs

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
assume "c<0"
[PROOF STATE]
proof (state)
this:
c < 0

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence "?P (Atom a) ((r - \<langle>cs,xs\<rangle> - 1)/c)"
[PROOF STATE]
proof (prove)
using this:
c < 0

goal (1 subgoal):
 1. \<forall>y\<ge>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Eq Cons
[PROOF STATE]
proof (prove)
using this:
c < 0
a = Eq r cs__
cs__ = c # cs

goal (1 subgoal):
 1. \<forall>y\<ge>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by(auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<forall>y\<ge>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<ge>(r - \<langle>cs,xs\<rangle> - 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
assume "c>0"
[PROOF STATE]
proof (state)
this:
0 < c

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence "?P (Atom a) ((r - \<langle>cs,xs\<rangle> + 1)/c)"
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. \<forall>y\<ge>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
using Eq Cons
[PROOF STATE]
proof (prove)
using this:
0 < c
a = Eq r cs__
cs__ = c # cs

goal (1 subgoal):
 1. \<forall>y\<ge>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by(auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<forall>y\<ge>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<ge>(r - \<langle>cs,xs\<rangle> + 1) / c. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 < c \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<And>aa list. cs__ = aa # list \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
0 < c \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
c < 0 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
0 < c \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Atom a)) xs = R.I (Atom a) (y # xs)

goal (6 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
case (And f1 f2)
[PROOF STATE]
proof (state)
this:
nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs)
nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs)
nqfree (And f1 f2)

goal (6 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs)
nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs)
nqfree (And f1 f2)
[PROOF STEP]
obtain x1 x2 where "?P f1 x1" "?P f2 x2"
[PROOF STATE]
proof (prove)
using this:
nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs)
nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs)
nqfree (And f1 f2)

goal (1 subgoal):
 1. (\<And>x1 x2. \<lbrakk>\<forall>y\<ge>x1. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); \<forall>y\<ge>x2. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
\<forall>y\<ge>x1. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs)
\<forall>y\<ge>x2. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs)

goal (6 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
hence "?P (And f1 f2) (max x1 x2)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<ge>x1. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs)
\<forall>y\<ge>x2. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs)

goal (1 subgoal):
 1. \<forall>y\<ge>max x1 x2. R.I (inf\<^sub>+ (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
[PROOF STEP]
by(force simp:and_def)
[PROOF STATE]
proof (state)
this:
\<forall>y\<ge>max x1 x2. R.I (inf\<^sub>+ (And f1 f2)) xs = R.I (And f1 f2) (y # xs)

goal (6 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (And f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
 4. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 6. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<ge>max x1 x2. R.I (inf\<^sub>+ (And f1 f2)) xs = R.I (And f1 f2) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (And f1 f2)) xs = R.I (And f1 f2) (y # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (And f1 f2)) xs = R.I (And f1 f2) (y # xs)

goal (5 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 4. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 4. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
case (Or f1 f2)
[PROOF STATE]
proof (state)
this:
nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs)
nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs)
nqfree (Or f1 f2)

goal (5 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 4. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs)
nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs)
nqfree (Or f1 f2)
[PROOF STEP]
obtain x1 x2 where "?P f1 x1" "?P f2 x2"
[PROOF STATE]
proof (prove)
using this:
nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs)
nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs)
nqfree (Or f1 f2)

goal (1 subgoal):
 1. (\<And>x1 x2. \<lbrakk>\<forall>y\<ge>x1. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); \<forall>y\<ge>x2. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
\<forall>y\<ge>x1. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs)
\<forall>y\<ge>x2. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs)

goal (5 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 4. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
hence "?P (Or f1 f2) (max x1 x2)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<ge>x1. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs)
\<forall>y\<ge>x2. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs)

goal (1 subgoal):
 1. \<forall>y\<ge>max x1 x2. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
[PROOF STEP]
by(force simp:or_def)
[PROOF STATE]
proof (state)
this:
\<forall>y\<ge>max x1 x2. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)

goal (5 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f1 f2. \<lbrakk>nqfree f1 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f1) xs = R.I f1 (y # xs); nqfree f2 \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f2) xs = R.I f2 (y # xs); nqfree (Or f1 f2)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
 4. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 5. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<ge>max x1 x2. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Or f1 f2)) xs = R.I (Or f1 f2) (y # xs)

goal (4 subgoals):
 1. nqfree TrueF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ TrueF) xs = R.I TrueF (y # xs)
 2. nqfree FalseF \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ FalseF) xs = R.I FalseF (y # xs)
 3. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (Neg f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (Neg f)) xs = R.I (Neg f) (y # xs)
 4. \<And>f. \<lbrakk>nqfree f \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ f) xs = R.I f (y # xs); nqfree (ExQ f)\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>y\<ge>x. R.I (inf\<^sub>+ (ExQ f)) xs = R.I (ExQ f) (y # xs)
[PROOF STEP]
qed simp_all