Theory Virtual_Substitution.DNF

section "QE Algorithm Proofs"
subsection "DNF"
theory DNF
  imports VSAlgos
begin


theorem dnf_eval : 
  "((al,fl)set (dnf φ). 
     (aset al. aEval a xs) 
    (fset fl. eval f xs))
   = eval φ xs"
proof(induction φ)
  case (And φ1 φ2)
  define f where "f = (λa. case a of
        (al, fl)  (aset al. aEval a xs)  (fset fl. eval f xs))"
  have h1:"(aset (dnf (And φ1 φ2)). f a) = (aset (dnf φ1). a'set(dnf φ2). f a  f a')"
    apply simp unfolding f_def apply auto
      apply blast
     apply blast
    subgoal for a b c d
      apply(rule bexI[where x="(a,b)"])
       apply(rule exI[where x="a@c"])
       apply(rule exI[where x="b@d"])
      by auto
    done
  also have h2 : "... = ((aset (dnf φ1). f a)(aset(dnf φ2). f a))"
    by auto
  show ?case unfolding f_def[symmetric] unfolding h1 h2 unfolding f_def using And by auto
qed auto


theorem dnf_modified_eval : 
  "((al,fl,n)set (dnf_modified φ).
      (L. (length L = n 
        (aset al. aEval a (L@xs))
        (fset fl. eval f (L@xs))))) = eval φ xs"
proof(induction φ arbitrary:xs)
  case (Atom x)
  then show ?case
    by (cases x, auto)
next
  case (And φ1 φ2)
  {fix d1 d2 A A' B B' L1 L2
    assume A : "(A,A',length (L1::real list))set (dnf_modified φ1)" and "(B,B',length (L2::real list))set (dnf_modified φ2)"
    have "(
      (aset ((map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B)). aEval a ((L1@L2) @ xs)) 
     (fset ( map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B'). eval f ((L1@L2) @ xs))) = 
      (
      (aset(map (liftAtom (length L1) (length L2)) A)  set( map (liftAtom 0 (length L1)) B). aEval a ((L1@L2) @ xs)) 
     (fset( map (liftFm (length L1) (length L2)) A')  set(map (liftFm 0 (length L1)) B'). eval f ((L1@L2) @ xs)))"
      by auto
    also have "... = (
      (aset(map (liftAtom (length L1) (length L2)) A).aEval a ((L1@L2) @ xs))
     (aset(map (liftAtom 0 (length L1)) B). aEval a ((L1@L2) @ xs)) 
     (fset(map (liftFm (length L1) (length L2)) A').eval f ((L1@L2) @ xs))
     (fset(map (liftFm 0 (length L1)) B'). eval f ((L1@L2) @ xs)))"
      by blast
    also have "... =  (
      (aset A. aEval (liftAtom (length L1) (length L2) a) ((L1@L2) @ xs))
     (aset B. aEval (liftAtom 0 (length L1) a) ((L1@L2) @ xs)) 
     (fset A'. eval (liftFm (length L1) (length L2) f) ((L1@L2) @ xs))
     (fset B'. eval (liftFm 0 (length L1) f) ((L1@L2) @ xs)))"
      by simp 
    also have "... =  (
      (aset A. aEval (liftAtom (length L1) (length L2) a) (insert_into (L1 @ xs) (length L1) L2))
     (aset B. aEval (liftAtom 0 (length L1) a) (insert_into (L2 @ xs) 0 L1)) 
     (fset A'. eval (liftFm (length L1) (length L2) f) (insert_into (L1 @ xs) (length L1) L2))
     (fset B'. eval (liftFm 0 (length L1) f) (insert_into (L2 @ xs) 0 L1)))"
      by auto
    also have "... = ( 
          ((aset A. aEval a (L1 @ xs))  (fset A'. eval f (L1 @ xs)))  
          ((aset B. aEval a (L2 @ xs))  (fset B'. eval f (L2 @ xs))) )"
    proof safe
      fix a
      show "aset A. aEval (liftAtom (length L1) (length L2) a) (insert_into (L1 @ xs) (length L1) L2) 
           a  set A  aEval a (L1 @ xs)"
        using eval_liftFm[of L2 "length L2" "length L1" "L1 @ xs" "Atom a", OF refl]
        by auto
    next
      fix f
      show "fset A'. eval (liftFm (length L1) (length L2) f) (insert_into (L1 @ xs) (length L1) L2) 
          f  set A'  eval f (L1 @ xs)"
        using eval_liftFm[of L2 "length L2" "length L1" "L1 @ xs" f, OF refl] by auto
    next 
      fix a
      show " aset B. aEval (liftAtom 0 (length L1) a) (insert_into (L2 @ xs) 0 L1) 
            a  set B  aEval a (L2 @ xs)"
        using eval_liftFm[of L1 "length L1" "0" "L2@xs" "Atom a", OF refl] by auto
    next
      fix f
      show " fset B'. eval (liftFm 0 (length L1) f) (insert_into (L2 @ xs) 0 L1)  f  set B'  eval f (L2 @ xs)"
        using eval_liftFm[of L1 "length L1" "0" "L2 @ xs" f, OF refl] by auto
    next
      fix a
      show " aset A. aEval a (L1 @ xs) 
         a  set A  aEval (liftAtom (length L1) (length L2) a) (insert_into (L1 @ xs) (length L1) L2)"
        using eval_liftFm[of L2 "length L2" "length L1" "L1 @ xs" "Atom a", OF refl] by auto
    next
      fix a
      show "aset B. aEval a (L2 @ xs)  a  set B  aEval (liftAtom 0 (length L1) a) (insert_into (L2 @ xs) 0 L1)"
        using eval_liftFm[of L1 "length L1" "0" "L2@xs" "Atom a", OF refl] by auto
    next
      fix f 
      show "fset A'. eval f (L1 @ xs) 
         f  set A'  eval (liftFm (length L1) (length L2) f) (insert_into (L1 @ xs) (length L1) L2)"
        using eval_liftFm[of L2 "length L2" "length L1" "L1 @ xs" f, OF refl] by auto
    next
      fix f
      show "fset B'. eval f (L2 @ xs)  f  set B'  eval (liftFm 0 (length L1) f) (insert_into (L2 @ xs) 0 L1)"
        using eval_liftFm[of L1 "length L1" "0" "L2 @ xs" f, OF refl] by auto
    qed
    finally have "(
      (aset ((map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B)). aEval a ((L1@L2) @ xs)) 
     (fset ( map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B'). eval f ((L1@L2) @ xs))) = ( 
          ((aset A. aEval a (L1 @ xs))  (fset A'. eval f (L1 @ xs)))  
          ((aset B. aEval a (L2 @ xs))  (fset B'. eval f (L2 @ xs))) )"
      by simp
  }
  then have h : "((A,A',d1)set (dnf_modified φ1). (B,B',d2)set (dnf_modified φ2).
      (L1.L2. length L1 = d1  length L2 = d2  
      (aset ((map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B)). aEval a ((L1@L2) @ xs)) 
     (fset ( map (liftFm d1 d2) A' @ map (liftFm 0 d1) B'). eval f ((L1@L2) @ xs)))) = (((A,A',d1)set (dnf_modified φ1). (B,B',d2)set(dnf_modified φ2). 
          (L1. length L1 = d1  (aset A. aEval a (L1 @ xs))  (fset A'. eval f (L1 @ xs)))  
          (L2. length L2 = d2  (aset B. aEval a (L2 @ xs))  (fset B'. eval f (L2 @ xs))) ))"
  proof safe
    fix A A' B B'  L1 L2
    assume prev : "(A A' L1 B B' L2.
           (A, A', length L1)  set (dnf_modified φ1) 
           (B, B', length L2)  set (dnf_modified φ2) 
           ((aset (map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B).
                aEval a ((L1 @ L2) @ xs)) 
            (fset (map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B').
                eval f ((L1 @ L2) @ xs))) =
           (((aset A. aEval a (L1 @ xs))  (fset A'. eval f (L1 @ xs))) 
            (aset B. aEval a (L2 @ xs))  (fset B'. eval f (L2 @ xs))))"
      and A: "(A,A',length L1)set (dnf_modified φ1)" and B: "(B,B',length L2)set (dnf_modified φ2)"
      and h1 : "aset (map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B).
          aEval a ((L1 @ L2) @ xs)"
      and h2 : "fset (map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B').
          eval f ((L1 @ L2) @ xs)"
    have h : "((aset (map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B).
         aEval a ((L1 @ L2) @ xs)) 
     (fset (map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B').
         eval f ((L1 @ L2) @ xs))) =
    (((aset A. aEval a (L1 @ xs))  (fset A'. eval f (L1 @ xs))) 
     (aset B. aEval a (L2 @ xs))  (fset B'. eval f (L2 @ xs)))"
      using prev[where A="A", where A'="A'", where B="B", where B'="B'"] A B by simp
    show "(A, A', d1)set (dnf_modified φ1).
          (B, B', d2)set (dnf_modified φ2).
             (L1. length L1 = d1  (aset A. aEval a (L1 @ xs))  (fset A'. eval f (L1 @ xs))) 
             (L2. length L2 = d2  (aset B. aEval a (L2 @ xs))  (fset B'. eval f (L2 @ xs)))"
      apply (rule bexI[where x="(A, A', length L1)", OF _ A])
      apply auto defer
      apply (rule bexI[where x="(B, B', length L2)", OF _ B])
      apply auto
      using h h1 h2
      by auto
  next
    fix A A' d1 B B' d2 L1 L2
    assume prev : "(A A' L1 B B' L2.
           (A, A', length L1)  set (dnf_modified φ1) 
           (B, B', length L2)  set (dnf_modified φ2) 
           ((aset (map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B).
                aEval a ((L1 @ L2) @ xs)) 
            (fset (map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B').
                eval f ((L1 @ L2) @ xs))) =
           (((aset A. aEval a (L1 @ xs))  (fset A'. eval f (L1 @ xs))) 
            (aset B. aEval a (L2 @ xs))  (fset B'. eval f (L2 @ xs))))"
      and A: "(A,A',length L1)set (dnf_modified φ1)" and B: "(B,B',length L2)set (dnf_modified φ2)"
      and h1 : "aset A. aEval a (L1 @ xs)" "fset A'. eval f (L1 @ xs)"
      "aset B. aEval a (L2 @ xs)" "fset B'. eval f (L2 @ xs)"
    have h : "((aset (map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B).
         aEval a ((L1 @ L2) @ xs)) 
     (fset (map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B').
         eval f ((L1 @ L2) @ xs))) =
    (((aset A. aEval a (L1 @ xs))  (fset A'. eval f (L1 @ xs))) 
     (aset B. aEval a (L2 @ xs))  (fset B'. eval f (L2 @ xs)))"
      using prev[where A="A", where A'="A'", where B="B", where B'="B'"] h1 A B by simp
    show "(A, A', d1)set (dnf_modified φ1).
          (B, B', d2)set (dnf_modified φ2).
             L1 L2.
                length L1 = d1 
                length L2 = d2 
                (aset (map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B). aEval a ((L1 @ L2) @ xs)) 
                (fset (map (liftFm d1 d2) A' @ map (liftFm 0 d1) B'). eval f ((L1 @ L2) @ xs))"
      apply (rule bexI[where x="(A, A', length L1)", OF _ A])
      apply auto defer
      apply (rule bexI[where x="(B, B', length L2)", OF _ B])
      apply auto
      apply (rule exI[where x="L1"])
      apply auto
      apply (rule exI[where x="L2"])
      apply auto
      using h h1 by auto
  qed

  define f where "f (x:: (atom list * atom fm list * nat)) = (case x of (al,fl,n)  (L. length L = n  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs))))" for x
  define g where "((g (uuaa::atom list) (uua::atom fm list) (uu::nat) x):: (atom list * atom fm list * nat)) = (
 case x of
                       (B, B', d2) 
                         (map (liftAtom uu d2) uuaa @ map (liftAtom 0 uu) B,
                          map (λx. map_fm_binders (λa x. liftAtom (uu + x) d2 a) x 0) uua @
                          map (λx. map_fm_binders (λa x. liftAtom (0 + x) uu a) x 0) B',
                          uu + d2))" for uuaa uua uu x

  define f' where "f' L A A' d1 B B' d2 = ((aset ((map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B)). aEval a (L @ xs)) 
     (fset ( map (liftFm d1 d2) A' @ map (liftFm 0 d1) B'). eval f (L @ xs)))" for L A A' d1 B B' d2
  have "((al, fl, n)set (dnf_modified (And φ1 φ2)).
               L. length L = n  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs)))
        = (yset (dnf_modified (And φ1 φ2)). f y)"
    unfolding f_def by simp
  also have "... = (yset (dnf_modified φ1).
        a aa b.
           (uu uua uuaa.
               (uuaa, uua, uu) = y 
               (a, aa, b)
                (g uuaa uua uu) `
                  set (dnf_modified φ2)) 
           f (a, aa, b))"
    using g_def by simp
  also have "... = ((A,A',d1)set (dnf_modified φ1).
        xset (dnf_modified φ2).
           f (g A A' d1 x))"
    by (smt case_prodE f_def imageE image_eqI prod.simps(2))
  also have "... = ((A,A',d1)set (dnf_modified φ1).
        xset (dnf_modified φ2).
           f (case x of (B,B',d2)  (map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B,
                          map (λx. liftFm d1 d2 x) A' @
                          map (λx. liftFm 0 d1 x) B',
                          d1 + d2)))"
    using g_def by simp 
  also have "... = ((A,A',d1)set (dnf_modified φ1). xset (dnf_modified φ2).
      (case (case x of (B,B',d2)  (map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B,
                          map (λx. liftFm d1 d2 x) A' @ map (λx. liftFm 0 d1 x) B',
                          d1 + d2)) of (al,fl,n)  (L. length L = n  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs))))
)"
    using f_def by simp
  also have "... = ((A,A',d1)set (dnf_modified φ1). (B,B',d2)set (dnf_modified φ2).
      (case ((map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B,
                          map (λx. liftFm d1 d2 x) A' @ map (λx. liftFm 0 d1 x) B',
                          d1 + d2)) of (al,fl,n)  (L. length L = n  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs))))
)"  
    by(smt case_prodE case_prodE2 old.prod.case)
  also have "... = ((A,A',d1)set (dnf_modified φ1). (B,B',d2)set (dnf_modified φ2).
      (L. length L = d1 + d2  
      (aset ((map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B)). aEval a (L @ xs)) 
     (fset ( map (liftFm d1 d2) A' @ map (liftFm 0 d1) B'). eval f (L @ xs))))"  
    by(smt case_prodE case_prodE2 old.prod.case)
  also have "... = ((A,A',d1)set (dnf_modified φ1). (B,B',d2)set (dnf_modified φ2).
      (L. length L = d1 + d2  (f' L A A' d1 B B' d2)))"  
    using f'_def by simp
  also have "... = ((A,A',d1)set (dnf_modified φ1). (B,B',d2)set (dnf_modified φ2).
      (L1.L2. length L1 = d1  length L2 = d2  (f' (L1@L2) A A' d1 B B' d2)))"
  proof safe
    fix A A' d1 B B' d2 L
    assume A: "(A,A',d1)set (dnf_modified φ1)" and B: "(B,B',d2)set (dnf_modified φ2)"
      and L: "length L = d1 + d2" "(f' L A A' d1 B B' d2)"
    show "(A, A', d1)set (dnf_modified φ1).
          (B, B', d2)set (dnf_modified φ2). L1 L2. length L1 = d1  length L2 = d2  f' (L1 @ L2) A A' d1 B B' d2"
      apply (rule bexI[where x="(A, A', d1)", OF _ A])
      apply auto
      apply (rule bexI[where x="(B, B', d2)", OF _ B])
      apply auto
      apply (rule exI[where x="take d1 L"])
      apply auto   defer
      apply (rule exI[where x="drop d1 L"])
      using L
      by auto
  next
    fix A A' d1 B B' d2 L1 L2
    assume A: "(A,A', length L1)set (dnf_modified φ1)" and B: "(B,B',length L2)set (dnf_modified φ2)"
      and L: "(f' (L1 @ L2) A A' (length L1) B B' (length L2))"
    thm exI
    thm bexI
    show "(A, A', d1)set (dnf_modified φ1). (B, B', d2)set (dnf_modified φ2). L. length L = d1 + d2  f' L A A' d1 B B' d2 "
      apply (rule bexI[where x="(A, A', length L1)", OF _ A])
      apply auto
      apply (rule bexI[where x="(B, B', length L2)", OF _ B])
      apply auto
      apply (rule exI[where x="L1 @ L2"])
      using L
      by auto
  qed

  also have "... = ((A,A',d1)set (dnf_modified φ1). (B,B',d2)set (dnf_modified φ2).
      (L1.L2. length L1 = d1  length L2 = d2  
      (aset ((map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B)). aEval a ((L1@L2) @ xs)) 
     (fset ( map (liftFm d1 d2) A' @ map (liftFm 0 d1) B'). eval f ((L1@L2) @ xs))))" 
    unfolding f'_def by simp
      (*also have "... = (∃(A,A',d1)∈set (dnf_modified φ1). ∃(B,B',d2)∈set (dnf_modified φ2).
      (∃L1.∃L2. length L1 = d1 ∧ length L2 = d2 ∧ 
      (∀a∈set (map (liftAtom d1 d2) A) ∪ set ( map (liftAtom 0 d1) B). aEval a ((L1@L2) @ xs)) 
    ∧ (∀f∈set ( map (liftFm d1 d2) A' @ map (liftFm 0 d1) B'). eval f ((L1@L2) @ xs))))"
    proof -
      have *: "(∀a∈set (map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B). aEval a ((L1 @ L2) @ xs))
        = (∀a∈set (map (liftAtom d1 d2) A) ∪ set ( map (liftAtom 0 d1) B). aEval a ((L1@L2) @ xs))"
        for d1 d2 A B L1 L2 by auto
      then show ?thesis apply (subst * ) ..
    qed (*
      apply (rule bex_cong[OF refl])
      unfolding split_beta
      apply (rule bex_cong[OF refl])
      apply (rule ex_cong1)+
      apply (rule conj_cong refl)+
      by auto *)
    *)
  also have "... = (((A,A',d1)set (dnf_modified φ1). (B,B',d2)set(dnf_modified φ2). 
          (L. length L = d1  (aset A. aEval a (L @ xs))  (fset A'. eval f (L @ xs)))  
          (L. length L = d2  (aset B. aEval a (L @ xs))  (fset B'. eval f (L @ xs))) ))"
    using h by simp
  also have "... = (((A,A',d1)set (dnf_modified φ1). (B,B',d2)set(dnf_modified φ2). 
          f (A,A',d1)  
          f (B,B',d2)))"
    using f_def by simp
  also have "... = ((aset (dnf_modified φ1). a1set(dnf_modified φ2). f a  f a1))"
    by (simp add: Bex_def_raw)
  also have "... = ((aset (dnf_modified φ1). f a)  (aset (dnf_modified φ2). f a))"
    by blast
  also have "... = eval (And φ1 φ2) xs"
    using And f_def by simp
  finally have "((al, fl, n)set (dnf_modified (And φ1 φ2)).
               L. length L = n  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs))) =
         eval (And φ1 φ2) xs"
    by simp
  then show ?case by simp
next
  case (Or φ1 φ2)
  have h1 : "eval (Or φ1 φ2) xs = eval φ1 xs  eval φ2 xs"
    using eval.simps(5) by blast
  have h2 : "set (dnf_modified (Or φ1 φ2)) = set(dnf_modified φ1)  set(dnf_modified φ2)"
    by simp 
  show ?case using Or h1 h2
    by (metis (no_types, lifting) Un_iff eval.simps(5)) 
next
  case (ExQ φ)
  have h1 : "((x. ((al, fl, n)set (dnf_modified φ).
               L. length L = n  (aset al. aEval a (L @ (x#xs)))  (fset fl. eval f (L @ (x#xs)))))
              =
              ((al, fl, n)set (dnf_modified φ).
               (x.L. length L = n  (aset al. aEval a ((L@[x]) @ xs))  (fset fl. eval f ((L@[x]) @ xs)))))"
    apply simp by blast
  { fix n al fl
    define f where "f L = (length (L:: real list) = ((n::nat)+1)  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs)))" for L
    have "(x.L. f (L@[x])) = (L. f L)"
      by (metis (full_types) One_nat_def add_Suc_right f_def list.size(3) nat.simps(3) rev_exhaust)
    then have "((x. L. length (L@[x]) = (n+1)  (aset al. aEval a ((L@[x]) @ xs))  (fset fl. eval f ((L@[x]) @ xs)))
              =
            (L. length L = (n+1)  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs))))"
      unfolding f_def by simp  
  }
  then have h2 : "n al fl. (
              (x. L. length (L@[x]) = (n+1)  (aset al. aEval a ((L@[x]) @ xs))  (fset fl. eval f ((L@[x]) @ xs)))
              =
              (L. length L = (n+1)  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs)))
            )"
    by simp
  { fix al fl n
    define f where "f al fl n = (L. length L = n  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs)))" for al fl n
    have "f al fl (n+1) = (case (case (al, fl, n) of (A, A', d)  (A, A',d+1)) of
             (al, fl, n)  f al fl n)"
      by simp
    then have "(L. length L = (n+1)  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs)))
              = (
             case (case (al, fl, n) of (A, A', d)  (A, A',d+1)) of
             (al, fl, n) 
               L. length L = n  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs)))"
      unfolding f_def by simp
  }
  then have h3 : "
              ((al, fl, n)set (dnf_modified φ).
               L. length L = (n+1)  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs)))
              = (aset (dnf_modified φ).
             case (case a of (A, A', d)  (A, A',d+1)) of
             (al, fl, n) 
               L. length L = n  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs)))"
    by (smt case_prodE case_prodI2) (* takes a second *)
  show ?case using ExQ h1 h2 h3 by simp
next
  case (ExN x1 φ)

  show ?case
    apply simp proof safe
    fix a aa b L
    have takedrop: "(take b L @ drop b L @ xs) = (L @ xs)" by auto
    assume h: "(a, aa, b)  set (dnf_modified φ)" "length L = b + x1" "aset a. aEval a (L @ xs)" "fset aa. eval f (L @ xs)"
    show "l. length l = x1  eval φ (l @ xs)"
      apply(rule exI[where x="drop b L"])
      apply auto
      using h(2) apply simp
      unfolding ExN[symmetric]
      apply(rule bexI[where x="(a,aa,b)"])
      apply simp
      apply(rule exI[where x="take b L"])
      apply auto
      using h apply simp
      unfolding takedrop
      using h by auto
  next
    fix l
    assume h: "eval φ (l @ xs)" "x1 = length l" 
    obtain al fl n where h1 : "(al, fl, n)set (dnf_modified φ)" "L. length L = n  (aset al. aEval a (L @ l @ xs))  (fset fl. eval f (L @ l @ xs))"
      using h(1) unfolding ExN[symmetric]
      by blast 
    obtain L where h2 : "length L = n" "(aset al. aEval a (L @ l @ xs))" "(fset fl. eval f (L @ l @ xs))" using h1(2) by metis 
    show "xset (dnf_modified φ).
            case case x of (A, A', d)  (A, A', d + length l) of
            (al, fl, n)  L. length L = n  (aset al. aEval a (L @ xs))  (fset fl. eval f (L @ xs))"
      apply(rule bexI[where x="(al,fl,n)"])
      apply simp
      apply(rule exI[where x="L@l"])
      apply auto
      using h2 h1 by auto
  qed
qed auto
end