[STATEMENT]
lemma subst_floatarith_Var_fold_const_fa[symmetric]:
  "fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) =
  subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa)
[PROOF STEP]
proof (induction fa)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Add fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Add fa1 fa2))
 2. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Minus fa))
 3. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Mult fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Mult fa1 fa2))
 4. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Inverse fa))
 5. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Cos fa))
 6. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Arctan fa))
 7. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Abs fa))
 8. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1 fa2))
 9. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Min fa1 fa2))
 10. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) Pi) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa Pi)
A total of 18 subgoals...
[PROOF STEP]
case (Add fa1 fa2)
[PROOF STATE]
proof (state)
this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1)
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)

goal (18 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Add fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Add fa1 fa2))
 2. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Minus fa))
 3. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Mult fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Mult fa1 fa2))
 4. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Inverse fa))
 5. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Cos fa))
 6. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Arctan fa))
 7. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Abs fa))
 8. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1 fa2))
 9. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Min fa1 fa2))
 10. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) Pi) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa Pi)
A total of 18 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1)
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1)
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)

goal (1 subgoal):
 1. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Add fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Add fa1 fa2))
[PROOF STEP]
apply (auto simp: fold_const_fa.simps
        split!: floatarith.splits option.splits if_splits
        elim!: dest_Num_fa_Some)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1)) = None; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2); subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)) = None; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 3. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 0\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 0
 5. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0\<rbrakk> \<Longrightarrow> False
 6. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 7. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 8. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 0\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 9. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0\<rbrakk> \<Longrightarrow> False
 10. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2); subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)) = None; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 0\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 0
 4. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0\<rbrakk> \<Longrightarrow> False
 5. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 6. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 7. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 0\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 8. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0\<rbrakk> \<Longrightarrow> False
 9. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 0\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 0
 3. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0\<rbrakk> \<Longrightarrow> False
 4. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 5. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 6. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 0\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 7. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0\<rbrakk> \<Longrightarrow> False
 8. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 0\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 0
 2. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0\<rbrakk> \<Longrightarrow> False
 3. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 4. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 5. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 0\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 6. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0\<rbrakk> \<Longrightarrow> False
 7. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 3. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 4. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 0\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 5. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0\<rbrakk> \<Longrightarrow> False
 6. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 2. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 3. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 0\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 4. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0\<rbrakk> \<Longrightarrow> False
 5. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 0\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 3. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0\<rbrakk> \<Longrightarrow> False
 4. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 0\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 2. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0\<rbrakk> \<Longrightarrow> False
 3. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Add fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Add fa1 fa2))

goal (17 subgoals):
 1. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Minus fa))
 2. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Mult fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Mult fa1 fa2))
 3. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Inverse fa))
 4. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Cos fa))
 5. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Arctan fa))
 6. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Abs fa))
 7. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1 fa2))
 8. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Min fa1 fa2))
 9. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) Pi) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa Pi)
 10. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Sqrt fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Sqrt fa))
A total of 17 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Minus fa))
 2. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Mult fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Mult fa1 fa2))
 3. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Inverse fa))
 4. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Cos fa))
 5. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Arctan fa))
 6. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Abs fa))
 7. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1 fa2))
 8. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Min fa1 fa2))
 9. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) Pi) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa Pi)
 10. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Sqrt fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Sqrt fa))
A total of 17 subgoals...
[PROOF STEP]
case (Mult fa1 fa2)
[PROOF STATE]
proof (state)
this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1)
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)

goal (17 subgoals):
 1. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Minus fa))
 2. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Mult fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Mult fa1 fa2))
 3. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Inverse fa))
 4. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Cos fa))
 5. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Arctan fa))
 6. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Abs fa))
 7. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1 fa2))
 8. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Min fa1 fa2))
 9. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) Pi) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa Pi)
 10. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Sqrt fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Sqrt fa))
A total of 17 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1)
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1)
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)

goal (1 subgoal):
 1. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Mult fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Mult fa1 fa2))
[PROOF STEP]
apply (auto simp: fold_const_fa.simps
        split!: floatarith.splits option.splits if_splits
        elim!: dest_Num_fa_Some)
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 0; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1)) = None; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1)) = None; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2); subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)) = None; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 4. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 0
 6. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 7. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2); subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)) = None; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 8. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 9. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 1
 10. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
A total of 15 subgoals...
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1)) = None; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2); subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)) = None; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 3. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 0
 5. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2); subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)) = None; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 7. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 8. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 1
 9. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 10. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
A total of 14 subgoals...
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2); subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)) = None; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 0
 4. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2); subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)) = None; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 6. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 7. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 1
 8. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 9. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 10. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
A total of 13 subgoals...
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 0
 3. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2); subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)) = None; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 5. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 1
 7. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 8. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 9. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 10. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
A total of 12 subgoals...
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 0
 2. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2); subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)) = None; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 4. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 1
 6. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 7. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 8. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 9. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 10. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0; x2a \<noteq> 1\<rbrakk> \<Longrightarrow> False
A total of 11 subgoals...
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 0; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 0; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2); subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)) = None; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 3. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 1
 5. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 6. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 7. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 8. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 9. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0; x2a \<noteq> 1\<rbrakk> \<Longrightarrow> False
 10. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2); subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)) = None; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 1
 4. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 5. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 6. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 7. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 8. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0; x2a \<noteq> 1\<rbrakk> \<Longrightarrow> False
 9. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 1
 3. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 4. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 5. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 6. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 7. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0; x2a \<noteq> 1\<rbrakk> \<Longrightarrow> False
 8. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num 1
 2. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 3. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 4. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 5. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 6. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0; x2a \<noteq> 1\<rbrakk> \<Longrightarrow> False
 7. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 3. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 4. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 5. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0; x2a \<noteq> 1\<rbrakk> \<Longrightarrow> False
 6. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num 1; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2; fold_const_fa fa1 = Num 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> fold_const_fa fa2 = Num x2
 2. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 3. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 4. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0; x2a \<noteq> 1\<rbrakk> \<Longrightarrow> False
 5. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; dest_Num_fa (fold_const_fa fa1) = None; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 3. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0; x2a \<noteq> 1\<rbrakk> \<Longrightarrow> False
 4. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num 1; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num 1\<rbrakk> \<Longrightarrow> fold_const_fa fa1 = Num x2
 2. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0; x2a \<noteq> 1\<rbrakk> \<Longrightarrow> False
 3. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1) = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa1) = None; fold_const_fa fa2 = Num x2a; x2a \<noteq> 0; x2a \<noteq> 1\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = Num x2; fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = Num x2a; subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2) = Num x2a; fold_const_fa fa1 = Num x2; x2 \<noteq> 0; x2 \<noteq> 1; dest_Num_fa (fold_const_fa fa2) = None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Num_eq_subst_Var dest_Num_fa.simps(1) option.simps(3))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Mult fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Mult fa1 fa2))

goal (16 subgoals):
 1. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Minus fa))
 2. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Inverse fa))
 3. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Cos fa))
 4. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Arctan fa))
 5. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Abs fa))
 6. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1 fa2))
 7. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Min fa1 fa2))
 8. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) Pi) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa Pi)
 9. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Sqrt fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Sqrt fa))
 10. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Exp fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Exp fa))
A total of 16 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (16 subgoals):
 1. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Minus fa))
 2. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Inverse fa))
 3. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Cos fa))
 4. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Arctan fa))
 5. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Abs fa))
 6. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1 fa2))
 7. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Min fa1 fa2))
 8. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) Pi) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa Pi)
 9. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Sqrt fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Sqrt fa))
 10. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Exp fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Exp fa))
A total of 16 subgoals...
[PROOF STEP]
case (Min)
[PROOF STATE]
proof (state)
this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1_) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1_)
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2_) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2_)

goal (16 subgoals):
 1. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Minus fa))
 2. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Inverse fa))
 3. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Cos fa))
 4. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Arctan fa))
 5. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Abs fa))
 6. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1 fa2))
 7. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Min fa1 fa2))
 8. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) Pi) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa Pi)
 9. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Sqrt fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Sqrt fa))
 10. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Exp fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Exp fa))
A total of 16 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1_) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1_)
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2_) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1_) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1_)
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2_) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2_)

goal (1 subgoal):
 1. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1_ fa2_)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Min fa1_ fa2_))
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (state)
this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1_ fa2_)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Min fa1_ fa2_))

goal (15 subgoals):
 1. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Minus fa))
 2. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Inverse fa))
 3. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Cos fa))
 4. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Arctan fa))
 5. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Abs fa))
 6. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1 fa2))
 7. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) Pi) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa Pi)
 8. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Sqrt fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Sqrt fa))
 9. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Exp fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Exp fa))
 10. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Powr fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Powr fa1 fa2))
A total of 15 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (15 subgoals):
 1. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Minus fa))
 2. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Inverse fa))
 3. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Cos fa))
 4. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Arctan fa))
 5. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Abs fa))
 6. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1 fa2))
 7. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) Pi) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa Pi)
 8. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Sqrt fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Sqrt fa))
 9. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Exp fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Exp fa))
 10. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Powr fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Powr fa1 fa2))
A total of 15 subgoals...
[PROOF STEP]
case (Max)
[PROOF STATE]
proof (state)
this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1_) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1_)
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2_) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2_)

goal (15 subgoals):
 1. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Minus fa))
 2. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Inverse fa))
 3. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Cos fa))
 4. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Arctan fa))
 5. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Abs fa))
 6. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1 fa2))
 7. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) Pi) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa Pi)
 8. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Sqrt fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Sqrt fa))
 9. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Exp fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Exp fa))
 10. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Powr fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Powr fa1 fa2))
A total of 15 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1_) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1_)
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2_) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1_) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1_)
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2_) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2_)

goal (1 subgoal):
 1. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1_ fa2_)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1_ fa2_))
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (state)
this:
fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1_ fa2_)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Max fa1_ fa2_))

goal (14 subgoals):
 1. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Minus fa))
 2. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Inverse fa))
 3. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Cos fa))
 4. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Arctan fa))
 5. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Abs fa))
 6. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) Pi) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa Pi)
 7. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Sqrt fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Sqrt fa))
 8. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Exp fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Exp fa))
 9. \<And>fa1 fa2. \<lbrakk>fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa1) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa1); fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa2) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa2)\<rbrakk> \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Powr fa1 fa2)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Powr fa1 fa2))
 10. \<And>fa. fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) \<Longrightarrow> fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) (Ln fa)) = subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa (Ln fa))
A total of 14 subgoals...
[PROOF STEP]
qed (auto simp: fold_const_fa.simps
        split!: floatarith.splits option.splits if_splits
        elim!: dest_Num_fa_Some)