[STATEMENT]
lemma freeIn_substInfinitesimalQuadratic_fm : assumes "var \<notin> vars a"
  "var \<notin> vars b"
  "var \<notin> vars c"
  "var \<notin> vars d"
shows"freeIn var (substInfinitesimalQuadratic_fm var a b c d F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalQuadratic_fm var a b c d F)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalQuadratic_fm var a b c d F)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalQuadratic_fm var a b c d F)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalQuadratic_fm var a b c d F)
[PROOF STEP]
have "freeIn (var+z)
     (liftmap
       (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b)
              (liftPoly 0 x c) (liftPoly 0 x d))
       F z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)
[PROOF STEP]
apply(induction F arbitrary:z)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) TrueF z)
 2. \<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) FalseF z)
 3. \<And>x z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) (fm.Atom x) z)
 4. \<And>F1 F2 z. \<lbrakk>\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F1 z); \<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F2 z)\<rbrakk> \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) (And F1 F2) z)
 5. \<And>F1 F2 z. \<lbrakk>\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F1 z); \<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F2 z)\<rbrakk> \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) (Or F1 F2) z)
 6. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) (Neg F) z)
 7. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) (ExQ F) z)
 8. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) (AllQ F) z)
 9. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) (ExN x1 F) z)
 10. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) (AllN x1 F) z)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x z. freeIn (var + z) (substInfinitesimalQuadratic (var + z) (liftPoly 0 z a) (liftPoly 0 z b) (liftPoly 0 z c) (liftPoly 0 z d) x)
 2. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (Suc z))
 3. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (Suc z))
 4. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (z + x1))
 5. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (z + x1))
[PROOF STEP]
apply(rule freeIn_substInfinitesimalQuadratic)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x z. var + z \<notin> vars (liftPoly 0 z a)
 2. \<And>x z. var + z \<notin> vars (liftPoly 0 z b)
 3. \<And>x z. var + z \<notin> vars (liftPoly 0 z c)
 4. \<And>x z. var + z \<notin> vars (liftPoly 0 z d)
 5. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (Suc z))
 6. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (Suc z))
 7. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (z + x1))
 8. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (z + x1))
[PROOF STEP]
apply (simp_all add: assms not_in_lift)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (Suc z))
 2. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (Suc z))
 3. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (z + x1))
 4. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (z + x1))
[PROOF STEP]
apply (metis (no_types, lifting) add_Suc_right)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (Suc z))
 2. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (z + x1))
 3. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (z + x1))
[PROOF STEP]
apply (metis (mono_tags, lifting) add_Suc_right)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (z + x1))
 2. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (z + x1))
[PROOF STEP]
apply (simp add: ab_semigroup_add_class.add_ac(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F (z + x1))
[PROOF STEP]
by (simp add: add.assoc)
[PROOF STATE]
proof (state)
this:
freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F z)

goal (1 subgoal):
 1. freeIn var (substInfinitesimalQuadratic_fm var a b c d F)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
freeIn (var + ?z2) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F ?z2)

goal (1 subgoal):
 1. freeIn var (substInfinitesimalQuadratic_fm var a b c d F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
freeIn (var + ?z2) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F ?z2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
freeIn (var + ?z2) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F ?z2)

goal (1 subgoal):
 1. freeIn var (substInfinitesimalQuadratic_fm var a b c d F)
[PROOF STEP]
unfolding substInfinitesimalQuadratic_fm.simps
[PROOF STATE]
proof (prove)
using this:
freeIn (var + ?z2) (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F ?z2)

goal (1 subgoal):
 1. freeIn var (liftmap (\<lambda>x. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) F 0)
[PROOF STEP]
by (metis (no_types, lifting) add.right_neutral)
[PROOF STATE]
proof (state)
this:
freeIn var (substInfinitesimalQuadratic_fm var a b c d F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma freeIn_substInfinitesimalLinear:
  assumes "var \<notin> vars a" "var \<notin> vars b"
  shows "freeIn var (substInfinitesimalLinear var a b At)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
proof(cases At)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1. At = Less x1 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 2. \<And>x2. At = Eq x2 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 3. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 4. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
case (Less p)
[PROOF STATE]
proof (state)
this:
At = Less p

goal (4 subgoals):
 1. \<And>x1. At = Less x1 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 2. \<And>x2. At = Eq x2 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 3. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 4. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
unfolding Less substInfinitesimalLinear.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (convertDerivative var p) 0)
[PROOF STEP]
using var_not_in_linear_fm[of var a b "(convertDerivative var p)", OF assms]
[PROOF STATE]
proof (prove)
using this:
freeIn var (linear_substitution_fm var a b (convertDerivative var p))

goal (1 subgoal):
 1. freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (convertDerivative var p) 0)
[PROOF STEP]
unfolding linear_substitution_fm.simps linear_substitution_fm_helper.simps
[PROOF STATE]
proof (prove)
using this:
freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (convertDerivative var p) 0)

goal (1 subgoal):
 1. freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (convertDerivative var p) 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
freeIn var (substInfinitesimalLinear var a b At)

goal (3 subgoals):
 1. \<And>x2. At = Eq x2 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 2. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 3. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x2. At = Eq x2 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 2. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 3. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
case (Eq p)
[PROOF STATE]
proof (state)
this:
At = Eq p

goal (3 subgoals):
 1. \<And>x2. At = Eq x2 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 2. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 3. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
At = Eq p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
At = Eq p

goal (1 subgoal):
 1. freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. At = Eq p \<Longrightarrow> freeIn var (list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]))
[PROOF STEP]
apply(rule freeIn_list_conj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. At = Eq p \<Longrightarrow> \<forall>f\<in>set (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]). freeIn var f
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>At = Eq p; var \<in> vars (isolate_variable_sparse p var (MPoly_Type.degree p var))\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>At = Eq p; x < MPoly_Type.degree p var; var \<in> vars (isolate_variable_sparse p var x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using not_in_isovarspar
[PROOF STATE]
proof (prove)
using this:
isolate_variable_sparse ?p ?var ?x = ?q \<Longrightarrow> ?var \<notin> vars ?q

goal (2 subgoals):
 1. \<lbrakk>At = Eq p; var \<in> vars (isolate_variable_sparse p var (MPoly_Type.degree p var))\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>At = Eq p; x < MPoly_Type.degree p var; var \<in> vars (isolate_variable_sparse p var x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
freeIn var (substInfinitesimalLinear var a b At)

goal (2 subgoals):
 1. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 2. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 2. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
case (Leq p)
[PROOF STATE]
proof (state)
this:
At = Leq p

goal (2 subgoals):
 1. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
 2. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
unfolding Leq substInfinitesimalLinear.simps freeIn.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (allZero p var) \<and> freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (convertDerivative var p) 0)
[PROOF STEP]
using var_not_in_linear_fm[of var a b "(convertDerivative var p)", OF assms]
[PROOF STATE]
proof (prove)
using this:
freeIn var (linear_substitution_fm var a b (convertDerivative var p))

goal (1 subgoal):
 1. freeIn var (allZero p var) \<and> freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (convertDerivative var p) 0)
[PROOF STEP]
unfolding linear_substitution_fm.simps linear_substitution_fm_helper.simps
[PROOF STATE]
proof (prove)
using this:
freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (convertDerivative var p) 0)

goal (1 subgoal):
 1. freeIn var (allZero p var) \<and> freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (convertDerivative var p) 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (if MPoly_Type.degree p var = 0 then fm.Atom (Less p) else Or (fm.Atom (Less p)) (And (fm.Atom (Eq p)) (convertDerivative var (derivative var p)))) 0) \<Longrightarrow> freeIn var (list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]))
[PROOF STEP]
apply(rule freeIn_list_conj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (if MPoly_Type.degree p var = 0 then fm.Atom (Less p) else Or (fm.Atom (Less p)) (And (fm.Atom (Eq p)) (convertDerivative var (derivative var p)))) 0) \<Longrightarrow> \<forall>f\<in>set (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]). freeIn var f
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (if MPoly_Type.degree p var = 0 then fm.Atom (Less p) else Or (fm.Atom (Less p)) (And (fm.Atom (Eq p)) (convertDerivative var (derivative var p)))) 0); var \<in> vars (isolate_variable_sparse p var (MPoly_Type.degree p var))\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>x < MPoly_Type.degree p var; var \<in> vars (isolate_variable_sparse p var x); freeIn var (fm.Atom (let d = MPoly_Type.degree p var in Less (((\<Sum>i = 0..<d. isolate_variable_sparse p var i * liftPoly 0 0 a ^ i * liftPoly 0 0 b ^ (d - i)) + isolate_variable_sparse p var d * liftPoly 0 0 a ^ d) * liftPoly 0 0 b ^ (d mod 2)))); freeIn var (fm.Atom (let d = MPoly_Type.degree p var in Eq ((\<Sum>i = 0..<d. isolate_variable_sparse p var i * liftPoly 0 0 a ^ i * liftPoly 0 0 b ^ (d - i)) + isolate_variable_sparse p var d * liftPoly 0 0 a ^ d))); freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (if MPoly_Type.degree (derivative var p) var = 0 then fm.Atom (Less (derivative var p)) else Or (fm.Atom (Less (derivative var p))) (And (fm.Atom (Eq (derivative var p))) (convertDerivative var (derivative var (derivative var p))))) 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using not_in_isovarspar
[PROOF STATE]
proof (prove)
using this:
isolate_variable_sparse ?p ?var ?x = ?q \<Longrightarrow> ?var \<notin> vars ?q

goal (2 subgoals):
 1. \<lbrakk>freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (if MPoly_Type.degree p var = 0 then fm.Atom (Less p) else Or (fm.Atom (Less p)) (And (fm.Atom (Eq p)) (convertDerivative var (derivative var p)))) 0); var \<in> vars (isolate_variable_sparse p var (MPoly_Type.degree p var))\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>x < MPoly_Type.degree p var; var \<in> vars (isolate_variable_sparse p var x); freeIn var (fm.Atom (let d = MPoly_Type.degree p var in Less (((\<Sum>i = 0..<d. isolate_variable_sparse p var i * liftPoly 0 0 a ^ i * liftPoly 0 0 b ^ (d - i)) + isolate_variable_sparse p var d * liftPoly 0 0 a ^ d) * liftPoly 0 0 b ^ (d mod 2)))); freeIn var (fm.Atom (let d = MPoly_Type.degree p var in Eq ((\<Sum>i = 0..<d. isolate_variable_sparse p var i * liftPoly 0 0 a ^ i * liftPoly 0 0 b ^ (d - i)) + isolate_variable_sparse p var d * liftPoly 0 0 a ^ d))); freeIn var (liftmap (\<lambda>x A. fm.Atom (linear_substitution (var + x) (liftPoly 0 x a) (liftPoly 0 x b) A)) (if MPoly_Type.degree (derivative var p) var = 0 then fm.Atom (Less (derivative var p)) else Or (fm.Atom (Less (derivative var p))) (And (fm.Atom (Eq (derivative var p))) (convertDerivative var (derivative var (derivative var p))))) 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
freeIn var (substInfinitesimalLinear var a b At)

goal (1 subgoal):
 1. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
case (Neq p)
[PROOF STATE]
proof (state)
this:
At = Neq p

goal (1 subgoal):
 1. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
At = Neq p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
At = Neq p

goal (1 subgoal):
 1. freeIn var (substInfinitesimalLinear var a b At)
[PROOF STEP]
apply (auto simp add:neg_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>At = Neq p; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> FalseF; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> TrueF\<rbrakk> \<Longrightarrow> freeIn var (list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]))
[PROOF STEP]
apply(rule freeIn_list_conj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>At = Neq p; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> FalseF; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> TrueF\<rbrakk> \<Longrightarrow> \<forall>f\<in>set (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]). freeIn var f
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>At = Neq p; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> FalseF; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> TrueF; var \<in> vars (isolate_variable_sparse p var (MPoly_Type.degree p var))\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>At = Neq p; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> FalseF; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> TrueF; x < MPoly_Type.degree p var; var \<in> vars (isolate_variable_sparse p var x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using not_in_isovarspar
[PROOF STATE]
proof (prove)
using this:
isolate_variable_sparse ?p ?var ?x = ?q \<Longrightarrow> ?var \<notin> vars ?q

goal (2 subgoals):
 1. \<lbrakk>At = Neq p; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> FalseF; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> TrueF; var \<in> vars (isolate_variable_sparse p var (MPoly_Type.degree p var))\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>At = Neq p; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> FalseF; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> TrueF; x < MPoly_Type.degree p var; var \<in> vars (isolate_variable_sparse p var x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
freeIn var (substInfinitesimalLinear var a b At)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma freeIn_substInfinitesimalLinear_fm:
  assumes "var \<notin> vars a" "var \<notin> vars b"
  shows "freeIn var (substInfinitesimalLinear_fm var a b F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalLinear_fm var a b F)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalLinear_fm var a b F)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalLinear_fm var a b F)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalLinear_fm var a b F)
[PROOF STEP]
have "freeIn (var+z)
     (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)
[PROOF STEP]
apply(induction F arbitrary:z)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) TrueF z)
 2. \<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) FalseF z)
 3. \<And>x z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) (fm.Atom x) z)
 4. \<And>F1 F2 z. \<lbrakk>\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F1 z); \<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F2 z)\<rbrakk> \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) (And F1 F2) z)
 5. \<And>F1 F2 z. \<lbrakk>\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F1 z); \<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F2 z)\<rbrakk> \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) (Or F1 F2) z)
 6. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) (Neg F) z)
 7. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) (ExQ F) z)
 8. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) (AllQ F) z)
 9. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) (ExN x1 F) z)
 10. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) (AllN x1 F) z)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x z. freeIn (var + z) (substInfinitesimalLinear (var + z) (liftPoly 0 z a) (liftPoly 0 z b) x)
 2. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (Suc z))
 3. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (Suc z))
 4. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (z + x1))
 5. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (z + x1))
[PROOF STEP]
apply(rule freeIn_substInfinitesimalLinear)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x z. var + z \<notin> vars (liftPoly 0 z a)
 2. \<And>x z. var + z \<notin> vars (liftPoly 0 z b)
 3. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (Suc z))
 4. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (Suc z))
 5. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (z + x1))
 6. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (z + x1))
[PROOF STEP]
apply (simp_all add: assms not_in_lift)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (Suc z))
 2. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (Suc z))
 3. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (z + x1))
 4. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (z + x1))
[PROOF STEP]
apply (metis (full_types) Suc_eq_plus1 ab_semigroup_add_class.add_ac(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (Suc (var + z)) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (Suc z))
 2. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (z + x1))
 3. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (z + x1))
[PROOF STEP]
apply (metis (full_types) Suc_eq_plus1 ab_semigroup_add_class.add_ac(1))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (z + x1))
 2. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (z + x1))
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 F z. (\<And>z. freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)) \<Longrightarrow> freeIn (var + z + x1) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F (z + x1))
[PROOF STEP]
by (simp add: add.assoc)
[PROOF STATE]
proof (state)
this:
freeIn (var + z) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)

goal (1 subgoal):
 1. freeIn var (substInfinitesimalLinear_fm var a b F)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
freeIn (var + ?z2) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F ?z2)

goal (1 subgoal):
 1. freeIn var (substInfinitesimalLinear_fm var a b F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
freeIn (var + ?z2) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F ?z2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
freeIn (var + ?z2) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F ?z2)

goal (1 subgoal):
 1. freeIn var (substInfinitesimalLinear_fm var a b F)
[PROOF STEP]
unfolding substInfinitesimalLinear_fm.simps
[PROOF STATE]
proof (prove)
using this:
freeIn (var + ?z2) (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F ?z2)

goal (1 subgoal):
 1. freeIn var (liftmap (\<lambda>x. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F 0)
[PROOF STEP]
by (metis (no_types, lifting) add.right_neutral)
[PROOF STATE]
proof (state)
this:
freeIn var (substInfinitesimalLinear_fm var a b F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compute_bound_fa_correct:
  "interpret_floatarith f i \<in>\<^sub>r ivl"
  if "compute_bound_fa prec f I = Some ivl"
    "i all_in I"
  for i::"real list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith f i \<in>\<^sub>r ivl
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith f i \<in>\<^sub>r ivl
[PROOF STEP]
have bounded: "bounded_by i (map Some I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by i (map Some I)
[PROOF STEP]
using that(2)
[PROOF STATE]
proof (prove)
using this:
i all_in I

goal (1 subgoal):
 1. bounded_by i (map Some I)
[PROOF STEP]
unfolding bounded_by_def
[PROOF STATE]
proof (prove)
using this:
i all_in I

goal (1 subgoal):
 1. \<forall>ia<length (map Some I). case map Some I ! ia of None \<Rightarrow> True | Some ivl \<Rightarrow> i ! ia \<in>\<^sub>r ivl
[PROOF STEP]
by (auto simp: bounds_of_interval_eq_lower_upper set_of_eq)
[PROOF STATE]
proof (state)
this:
bounded_by i (map Some I)

goal (1 subgoal):
 1. interpret_floatarith f i \<in>\<^sub>r ivl
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
compute_bound_fa prec f I = Some ivl
i all_in I
[PROOF STEP]
have Some: "approx prec f (map Some I) = Some ivl"
[PROOF STATE]
proof (prove)
using this:
compute_bound_fa prec f I = Some ivl
i all_in I

goal (1 subgoal):
 1. approx prec f (map Some I) = Some ivl
[PROOF STEP]
by (auto simp: lower_Interval upper_Interval min_def split: option.splits if_splits)
[PROOF STATE]
proof (state)
this:
approx prec f (map Some I) = Some ivl

goal (1 subgoal):
 1. interpret_floatarith f i \<in>\<^sub>r ivl
[PROOF STEP]
from approx[OF bounded Some]
[PROOF STATE]
proof (chain)
picking this:
interpret_floatarith f i \<in>\<^sub>r ivl
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interpret_floatarith f i \<in>\<^sub>r ivl

goal (1 subgoal):
 1. interpret_floatarith f i \<in>\<^sub>r ivl
[PROOF STEP]
by (auto simp: set_of_eq)
[PROOF STATE]
proof (state)
this:
interpret_floatarith f i \<in>\<^sub>r ivl

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Ipoly_num_params_cong: "Ipoly xs p = Ipoly ys p"
  if "\<And>i. i < num_params p \<Longrightarrow> xs ! i = ys ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ipoly xs p = Ipoly ys p
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?i < num_params p \<Longrightarrow> xs ! ?i = ys ! ?i

goal (1 subgoal):
 1. Ipoly xs p = Ipoly ys p
[PROOF STEP]
by (induction p; auto)


[STATEMENT]
lemma insertion_num_params_cong: "insertion e p = insertion f p"
  if "\<And>i. i < num_params p \<Longrightarrow> e i = f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e p = insertion f p
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?i < num_params p \<Longrightarrow> e ?i = f ?i

goal (1 subgoal):
 1. insertion e p = insertion f p
[PROOF STEP]
by (induction p; auto)


[STATEMENT]
lemma insertion_eq_IpolyI: "insertion xs p = Ipoly ys p"
  if "\<And>i. i < num_params p \<Longrightarrow> xs i = ys ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion xs p = Ipoly ys p
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?i < num_params p \<Longrightarrow> xs ?i = ys ! ?i

goal (1 subgoal):
 1. insertion xs p = Ipoly ys p
[PROOF STEP]
by (induction p; auto)


[STATEMENT]
lemma Ipoly_eq_insertionI: "Ipoly ys p = insertion xs p"
  if "\<And>i. i < num_params p \<Longrightarrow> xs i = ys ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ipoly ys p = insertion xs p
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?i < num_params p \<Longrightarrow> xs ?i = ys ! ?i

goal (1 subgoal):
 1. Ipoly ys p = insertion xs p
[PROOF STEP]
by (induction p; auto)


[STATEMENT]
lemma range_tmI:
  "x \<in>\<^sub>i range_tm e tm"
  if x: "x \<in>\<^sub>i interval_of (insertion e ((tm_poly tm))) + real_interval (tm_bound tm)"
  for e::"nat\<Rightarrow>real"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e tm
[PROOF STEP]
by (auto simp: range_tm_def x)


[STATEMENT]
lemma range_tmD:
  "x \<in>\<^sub>i interval_of (insertion e (tm_poly tm)) + real_interval (tm_bound tm)"
  if "x \<in>\<^sub>i range_tm e tm"
  for e::"nat\<Rightarrow>real"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly tm))) + real_interval (tm_bound tm)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>i range_tm e tm

goal (1 subgoal):
 1. x \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly tm))) + real_interval (tm_bound tm)
[PROOF STEP]
by (auto simp: range_tm_def)


[STATEMENT]
lemma compute_bound_tm_def:
  "compute_bound_tm prec I a tm = compute_bound_poly prec (tm_poly tm) I a + (tm_bound tm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compute_bound_tm prec I a tm = compute_bound_poly prec (map_poly interval_of (tm_poly tm)) I a + tm_bound tm
[PROOF STEP]
by (cases tm) auto


[STATEMENT]
lemma real_of_float_in_real_interval_of[intro, simp]: "real_of_float x \<in>\<^sub>r X" if "x \<in>\<^sub>i X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_float x \<in>\<^sub>r X
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>i X

goal (1 subgoal):
 1. real_of_float x \<in>\<^sub>r X
[PROOF STEP]
by (auto simp: set_of_eq)


[STATEMENT]
lemma in_set_of_round_interval[intro, simp]:
  "x \<in>\<^sub>r round_interval prec X" if "x \<in>\<^sub>r X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>r round_interval prec X
[PROOF STEP]
using round_ivl_correct[of X prec] that
[PROOF STATE]
proof (prove)
using this:
set_of X \<subseteq> set_of (round_interval prec X)
x \<in>\<^sub>r X

goal (1 subgoal):
 1. x \<in>\<^sub>r round_interval prec X
[PROOF STEP]
by (auto simp: set_of_eq)


[STATEMENT]
lemma in_set_real_minus_interval[intro, simp]:
  "x - y \<in>\<^sub>r X - Y" if "x \<in>\<^sub>r X" "y \<in>\<^sub>r Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - y \<in>\<^sub>r X - Y
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>r X
y \<in>\<^sub>r Y

goal (1 subgoal):
 1. x - y \<in>\<^sub>r X - Y
[PROOF STEP]
by (auto simp: set_of_eq)


[STATEMENT]
lemma real_interval_plus: "real_interval (a + b) = real_interval a + real_interval b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_interval (a + b) = real_interval a + real_interval b
[PROOF STEP]
by (simp add: interval_eqI)


[STATEMENT]
lemma real_interval_uminus: "real_interval (- b) = - real_interval b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_interval (- b) = - real_interval b
[PROOF STEP]
by (simp add: interval_eqI)


[STATEMENT]
lemma real_interval_of: "real_interval (interval_of b) = interval_of b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_interval (interval_of b) = interval_of (real_of_float b)
[PROOF STEP]
by (simp add: interval_eqI)


[STATEMENT]
lemma real_interval_minus: "real_interval (a - b) = real_interval a - real_interval b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_interval (a - b) = real_interval a - real_interval b
[PROOF STEP]
using real_interval_plus[of a "-b"] real_interval_uminus[of b]
[PROOF STATE]
proof (prove)
using this:
real_interval (a + - b) = real_interval a + real_interval (- b)
real_interval (- b) = - real_interval b

goal (1 subgoal):
 1. real_interval (a - b) = real_interval a - real_interval b
[PROOF STEP]
by (auto simp: interval_eq_iff)


[STATEMENT]
lemma in_set_neg_plus_interval[intro, simp]:
  "- y \<in>\<^sub>r - Y" if "y \<in>\<^sub>r Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - y \<in>\<^sub>r - Y
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
y \<in>\<^sub>r Y

goal (1 subgoal):
 1. - y \<in>\<^sub>r - Y
[PROOF STEP]
by (auto simp: set_of_eq)


[STATEMENT]
lemma in_set_real_times_interval[intro, simp]:
  "x * y \<in>\<^sub>r X * Y" if "x \<in>\<^sub>r X" "y \<in>\<^sub>r Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<in>\<^sub>r X * Y
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>r X
y \<in>\<^sub>r Y

goal (1 subgoal):
 1. x * y \<in>\<^sub>r X * Y
[PROOF STEP]
by (auto simp: real_interval_times intro!: times_in_intervalI)


[STATEMENT]
lemma real_interval_zero: "real_interval 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_interval 0 = 0
[PROOF STEP]
by (simp add: interval_eqI)


[STATEMENT]
lemma real_interval_power: "real_interval (a ^ b) = real_interval a ^ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_interval (a ^ b) = real_interval a ^ b
[PROOF STEP]
by (induction b arbitrary: a)
    (auto simp: real_interval_times real_interval_one)


[STATEMENT]
lemma in_set_real_power_interval[intro, simp]:
  "x ^ n \<in>\<^sub>r X ^ n" if "x \<in>\<^sub>r X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ^ n \<in>\<^sub>r X ^ n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>r X

goal (1 subgoal):
 1. x ^ n \<in>\<^sub>r X ^ n
[PROOF STEP]
by (auto simp: real_interval_power intro!: set_of_power_mono)


[STATEMENT]
lemma power_float_interval_real_interval[intro, simp]:
  "x ^ n \<in>\<^sub>r power_float_interval prec n X" if "x \<in>\<^sub>r X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ^ n \<in>\<^sub>r power_float_interval prec n X
[PROOF STEP]
by (auto simp: real_interval_power that intro!: power_float_intervalI)


[STATEMENT]
lemma in_set_mult_float_interval[intro, simp]:
  "x * y \<in>\<^sub>r mult_float_interval prec X Y" if "x \<in>\<^sub>r X" "y \<in>\<^sub>r Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<in>\<^sub>r mult_float_interval prec X Y
[PROOF STEP]
using mult_float_interval[of X Y] in_set_real_times_interval[OF that] that(1) that(2)
[PROOF STATE]
proof (prove)
using this:
set_of (real_interval X) * set_of (real_interval Y) \<subseteq> set_of (real_interval (mult_float_interval ?prec X Y))
x * y \<in>\<^sub>r X * Y
x \<in>\<^sub>r X
y \<in>\<^sub>r Y

goal (1 subgoal):
 1. x * y \<in>\<^sub>r mult_float_interval prec X Y
[PROOF STEP]
by blast


[STATEMENT]
lemma in_set_real_minus_swapI: "e i \<in>\<^sub>r I ! i - a ! i"
  if "x - e i \<in>\<^sub>r a ! i" "x \<in>\<^sub>r I ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e i \<in>\<^sub>r I ! i - a ! i
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x - e i \<in>\<^sub>r a ! i
x \<in>\<^sub>r I ! i

goal (1 subgoal):
 1. e i \<in>\<^sub>r I ! i - a ! i
[PROOF STEP]
by (auto simp: set_of_eq)


[STATEMENT]
lemma develops_at_withinI:
  assumes all_in: "a all_subset I"
  assumes e: "\<And>i. i < length I \<Longrightarrow> e i \<in>\<^sub>r I ! i - a ! i"
  shows "develops_at_within e a I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. develops_at_within e a I
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a all_subset I
?i < length I \<Longrightarrow> e ?i \<in>\<^sub>r I ! ?i - a ! ?i

goal (1 subgoal):
 1. develops_at_within e a I
[PROOF STEP]
by (auto simp: develops_at_within_def)


[STATEMENT]
lemma develops_at_withinD:
  assumes "develops_at_within e a I"
  shows "a all_subset I"
    "\<And>i. i < length I \<Longrightarrow> e i \<in>\<^sub>r I ! i - a ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a all_subset I &&& (\<And>i. i < length I \<Longrightarrow> e i \<in>\<^sub>r I ! i - a ! i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
develops_at_within e a I

goal (1 subgoal):
 1. a all_subset I &&& (\<And>i. i < length I \<Longrightarrow> e i \<in>\<^sub>r I ! i - a ! i)
[PROOF STEP]
by (auto simp: develops_at_within_def)