[STATEMENT]
theorem VSLuckyBlocks : "\<forall>xs. eval (VSLuckyBlocks \<phi>) xs = eval \<phi> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. eval (VSLuckyBlocks \<phi>) xs = eval \<phi> xs
[PROOF STEP]
unfolding VSLuckyBlocks_def Unpower_def opt_group_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. eval ((push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers \<circ> QE_dnf' (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers) (the_real_step_augment luckyFind') \<circ> VSLuckiestBlocks \<circ> (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers)) \<phi>) xs = eval \<phi> xs
[PROOF STEP]
using QE_dnf'_eval[OF the_real_step_augment[OF luckyFind'_eval, of "\<lambda>x _ _. x"] opt]
[PROOF STATE]
proof (prove)
using this:
(\<And>amount F \<Gamma> xs var L Fa \<Gamma>'. length xs = var \<Longrightarrow> length xs = var) \<Longrightarrow> eval (QE_dnf' (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers) (the_real_step_augment luckyFind') ?\<phi>) ?xs = eval ?\<phi> ?xs

goal (1 subgoal):
 1. \<forall>xs. eval ((push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers \<circ> QE_dnf' (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers) (the_real_step_augment luckyFind') \<circ> VSLuckiestBlocks \<circ> (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers)) \<phi>) xs = eval \<phi> xs
[PROOF STEP]
using opt VSLuckiestBlocks
[PROOF STATE]
proof (prove)
using this:
(\<And>amount F \<Gamma> xs var L Fa \<Gamma>'. length xs = var \<Longrightarrow> length xs = var) \<Longrightarrow> eval (QE_dnf' (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers) (the_real_step_augment luckyFind') ?\<phi>) ?xs = eval ?\<phi> ?xs
eval ((push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers) ?F) ?L = eval ?F ?L
\<forall>xs. eval (VSLuckiestBlocks ?\<phi>) xs = eval ?\<phi> xs

goal (1 subgoal):
 1. \<forall>xs. eval ((push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers \<circ> QE_dnf' (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers) (the_real_step_augment luckyFind') \<circ> VSLuckiestBlocks \<circ> (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers)) \<phi>) xs = eval \<phi> xs
[PROOF STEP]
by fastforce