# Bash-term-to-dnf

`Bash-term-to-dnf` is a tool that simplifies a term, producing
a list of clauses such that if all output clauses are theorems, then so is the
input term.

This utility is defined in community book
`"misc/bash.lisp"`. We assume here familiarity with the bash
tool defined in that book, focusing below on how the present tool differs from
that one.

If you submit `(bash-term-to-dnf term)` then the result is a list of
goals produced by ACL2's simplification process, much as for the result of
`(bash term)`; see bash. However, unlike `bash`,
`bash-term-to-dnf` returns a list of *clauses*, where each clause
is a list of terms that represents the disjunction of those terms, and the list
of clauses is implicitly conjoined.

Again: For related utilities, see simp and bash.

### Example

First we execute:

(include-book "misc/bash" :dir :system)

Then:

ACL2 !>(bash-term-to-dnf
'(implies (true-listp x) (equal (append x y) zzz))
'(("Goal" :expand ((true-listp x)
(true-listp (cdr x))
(append x y))))
nil t state)
(((EQUAL Y ZZZ))
((NOT (CONSP X))
(NOT (CONSP (CDR X)))
(NOT (TRUE-LISTP (CDDR X)))
(EQUAL (LIST* (CAR X)
(CADR X)
(APPEND (CDDR X) Y))
ZZZ))
((NOT (CONSP X))
(CDR X)
(EQUAL (CONS (CAR X) Y) ZZZ)))
ACL2 !>

### General Form:

(bash-term-to-dnf form hints verbose untranslate-flg state)

returns a list of clauses, each of which is a list of terms, where:

`form` is a user-level (untranslated) term;
`hints`, if supplied, is a hints structure (as for
defthm);
`verbose` is `nil` by default, in which case output is
inhibited; on the other extreme, if `verbose` is `:all` then a
warning is printed when no simplification takes place; and
`untranslate-flg` is `nil` by default, in which case each
term in each returned clause is a term in internal (translated) form and
otherwise, each such term is in user-level (untranslated) form;

If each returned clause (viewed as a disjunction) is a theorem, then the input

`form` is a theorem.