[STATEMENT]
lemma nf_ACI_nFAND: 
  "\<lbrakk>sorted \<phi>s; distinct \<phi>s; list_all nf_ACI \<phi>s; list_all (\<lambda>x. \<not> is_FAnd x) \<phi>s\<rbrakk> \<Longrightarrow> nf_ACI (nFAND \<phi>s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted \<phi>s; distinct \<phi>s; list_all nf_ACI \<phi>s; list_all (\<lambda>x. \<not> is_FAnd x) \<phi>s\<rbrakk> \<Longrightarrow> nf_ACI (nFAND \<phi>s)
[PROOF STEP]
by (induct \<phi>s rule: nFAND.induct)
    (auto simp: juncts_list_singleton conjuncts_list_nFAND nf_ACI_D)