;; Proof of the equivalence of nondeterministic and deterministic automaton
;;
;; Debora Weber-Wulff, Berlin, February 1997

(boot-strap nqthm)

;; -------------------------------------------------------------------------
;;      Library functions
;; -------------------------------------------------------------------------
;; These functions were copied from the basis.events, bags-and-sets.events,
;; and lists.events for nqthm-1992 that I obtained in Austin 1993.
;; Only these were needed for the proof, and it speeds up the proof 
;; considerably to keep unnecessary stuff out - they do not need to be
;; considered at every step.

(defn setp (l)
  (if (not (listp l))
      t
      (and (not (member (car l) (cdr l)))
           (setp (cdr l)))))

(prove-lemma setp-cons (rewrite)
  (equal (setp (cons x l))
         (and (not (member x l))
              (setp l)))
  ((enable setp)))

(defn consl (x l)
   (if (listp l)
       (cons (cons x (car l))
             (consl x (cdr l)))
       nil))

(prove-lemma member-consl (rewrite)
  (equal (member x (consl v lst))
         (and (listp x)
              (equal (car x) v)
              (member (cdr x) lst))))

(prove-lemma member-non-list (rewrite)
  (implies (not (listp l))
           (not (member x l))))

(prove-lemma member-union (rewrite)
  (equal (member x (union a b))
         (or (member x a)
             (member x b))))

(defn length (l) 
  (if (not (listp l))
      0 
      (add1 (length (cdr l)))))

(prove-lemma length-cons (rewrite)
  (equal (length (cons a x))
         (add1 (length x)))
  ((enable length)))

(defn plistp (l)
  (if (not (listp l))
      (equal l nil)
      (plistp (cdr l))))

(prove-lemma plistp-cons (rewrite)
  (equal (plistp (cons a l))
         (plistp l))
  ((enable plistp)))

(defn all-subbags (l)
   (if (listp l)
       (let ((x (all-subbags (cdr l))))
         (union x (consl (car l) x)))
       (list nil)))

;; -------------------------------------------------------------------------
;;      Basic functions
;; -------------------------------------------------------------------------

;; some-member
;; This is a witness for the existence of an element in the intersection

(defn some-member (l1 l2)
 (if (nlistp l1)
     F
     (if (member (car l1) l2)
         T
         (some-member (cdr l1) l2))))

(prove-lemma some-member-member (rewrite)
  (implies (and (member n y)
                (member n x))
           (some-member x y)))

;; -------------------------------------------------------------------------
;;      subsetp
;; -------------------------------------------------------------------------
;; I will use a weak definition of subset: all elements of a are in b
;; (some may be double).
 
(defn subsetp (a b)
  (if (nlistp a)
      T
      (and (member (car a) b)
           (subsetp (cdr a) b))))

(prove-lemma subsetp-union (rewrite)
 (equal (subsetp (union a b) c)
        (and (subsetp a c)
             (subsetp b c))))

(prove-lemma subsetp-union2 (rewrite)
 (subsetp y (union y x)))

(prove-lemma subsetp-cons (rewrite)
 (implies (subsetp x y)
          (subsetp x (cons z y))))

(prove-lemma subsetp-reflexive (rewrite)
 (subsetp x x))

(prove-lemma member-subsetp (Rewrite)
 (implies (and (member x a)
               (subsetp a b))
          (member x b)))

(prove-lemma some-member-and-subsetp (rewrite)
 (implies (and (some-member a b)
               (subsetp b c))
          (some-member a c)))

;; -------------------------------------------------------------------------
;; --- theorems about setp -----

;; consl preserves setp
(prove-lemma setp-consl (Rewrite)
 (implies (setp x)
          (setp (consl y x))))

(prove-lemma setp-union (rewrite)
 (implies (and (setp x)
               (setp y))
          (setp (union x y))))

;; -------------------------------------------------------------------------
;; --- theorems about consl -----

(prove-lemma setp-union-consl (REWRITE)
   (IMPLIES (SETP Y)
            (SETP (UNION Y (CONSL V Y)))))

;; --- theorems about all-subbags -----

(prove-lemma listp-all-subbags (rewrite)
 (listp (all-subbags d)))

;; nil is a member of all power sets.

(prove-lemma nil-member-all-subbags (rewrite)
 (member nil (all-subbags x)))

;; Singleton lists of members of a list are members of the power set.

(prove-lemma member-list-all-subbags (rewrite)
  (implies (member x y)
           (member (list x) (all-subbags y))))

;; If x is a set, the 'power-set' is a set

(prove-lemma setp-all-subbags (rewrite)
 (implies (setp x)
          (setp (all-subbags x))))
             
(defn all-subbags-hint1 (x y)
  (if (nlistp y)
      T
      (and (all-subbags-hint1 (cdr x) (cdr y))
           (all-subbags-hint1 x (cdr y)))))

(prove-lemma member-all-subbags (rewrite)
 (implies (member x (all-subbags y))
          (subsetp x y))
 ((induct (all-subbags-hint1 x y))))

;; --- Theorems about union

(prove-lemma nothing-member-nil (rewrite)
             (not (member x nil)))

;; -------------------------------------------------------------------------
;;      order
;; -------------------------------------------------------------------------
;; To simulate set equality we order the list representation of
;; a set (x) along a basis (lst).

;; Order the elements of x according to lst, a finite total order for x.

(defn order (x lst)
  (if (nlistp lst)
      nil
      (if (member (car lst) x)
          (cons (car lst) (order x (cdr lst)))
          (order x (cdr lst)))))

(prove-lemma order-preserves-member (rewrite)
 (implies (member x (order y z))
          (and (member x y)
               (member x z))))

(prove-lemma member-both-member-order (rewrite)
 (implies (and (member z x)
               (member z v))
          (member z (order x v))))

; ---- order and all-subbags

(prove-lemma helper1 (rewrite)
 (implies (equal (order x z) y)
          (member y (all-subbags z))))

(prove-lemma ordered-member-all-subbags (rewrite)
 (implies (equal (order x z) x)
          (member x (all-subbags z))))

(disable helper1)
(disable ordered-member-all-subbags)

(prove-lemma member-order-all-subbags (rewrite)
 (member (order w d) (all-subbags d)))

(prove-lemma some-member-order1 (rewrite)
 (implies (some-member (order a b) c)
          (some-member (order (cons x a) b) c))
 ((disable member-subsetp)))

(prove-lemma subsetp-order-2 (rewrite)
 (subsetp (order a b) (order (cons c a) b)))

(prove-lemma some-member-order (rewrite)
 (implies (some-member (order w d) z)
          (some-member w z)))

(prove-lemma some-member-order-2 (rewrite)
 (implies (and (subsetp b c)
               (some-member a b))
          (some-member (order a c) b))
 ((induct (length a))))

;; -------------------------------------------------------------------------
;;      all-member
;; -------------------------------------------------------------------------

;; This is a key definition for the proof - it turns out to be the same 
;; as my definition of subsetp.

(defn all-member
      (a b)
      (if (nlistp a)
          t
          (and (member (car a) b)
               (all-member (cdr a) b))))

;; -------------------------------------------------------------------------
;;       Definedp
;; -------------------------------------------------------------------------
;; needed to explain the workings of next-state

(defn definedp (x table)
  (if (nlistp table)
      F
      (or (equal x (caar table))
          (definedp x (cdr table)))))

;; -------------------------------------------------------------------------
;; This is the basic automaton recognizer for NQTHM.

(add-shell fsa* nil fsap*
  ((alphabet (none-of) zero)
   (states   (none-of) zero)
   (starts   (none-of) zero)
   (table    (none-of) zero)
   (finals   (none-of) zero)))

;; A "real" finite state automaton is an NQTHM-automaton with the following
;; properties:

(defn fsap (auto)
  (let ((al (alphabet auto))
        (st (states auto))
        (s0 (starts auto))
        (tr (table auto))
        (fi (finals auto)))
    (and (fsap* auto)
         (listp al)
         (listp st)
         (listp s0)
         (subsetp s0 st)
         (setp st)
         (setp fi)
         (subsetp fi st))))

;; A transition is a list ((state . input) nexts) where nexts is a list
;; of following states, for example (mk-transition 'q 'a '(q r s)).

(defn mk-transition (state input nexts)
  (cons (cons state input) nexts))

;; Selector functions, will open up immediately

(defn state (trans) (caar trans))
(defn input (trans) (cdar trans))
(defn nexts (trans) (cdr trans))
  
;; A good transition is one where the input is a member of the alphabet,
;; and the states and all the elements of nexts are members of states.
;; nexts must also be a proper list. 

(defn transitionp (trans alphabet states)
 (and (member (input trans) alphabet)
      (member (state trans) states)
      (subsetp (nexts trans) states)
      (plistp (nexts trans))))

;; A table is well-formed if all the entries are transitions
;; with respect to an alphabet and a table.

(defn wf-table (table alphabet states)
  (if (nlistp table)
      (equal table nil)
      (and (transitionp (car table) alphabet states)
           (wf-table (cdr table) alphabet states))))

;; A nice nondeterministic automaton is a well-formed one

(defn ndfsap (a)
  (and (fsap a)
       (wf-table (table a) (alphabet a) (states a))))

;; ----- Construct the new automaton

;; Looking up the next states is done like this. nil is returned if
;; there is no next state.

(defn next-states (table st a)
  (if (nlistp table)
      nil
      (if (equal (cons st a) (caar table))
          (nexts (car table))
          (next-states (cdr table) st a))))

;; If M is a well-formed table, then the result of next-states
;; is a subset of nstates.

(prove-lemma subsetp-next-states (rewrite)
 (implies (wf-table M alphabet nstates)
          (subsetp (next-states M state symbol)
                   nstates)))

;; If (cons st a) is not defined, the next-state is nil.

(prove-lemma non-definedp-next-state (rewrite)
 (implies (not (definedp (cons st a) table))
          (equal (next-states table st a) nil)))

;; If the next state is not in the first part, look in the second

(prove-lemma next-states-append (rewrite)
 (equal (next-states (append a b) s x)
        (if (definedp (cons s x) a)
            (next-states a s x)
            (next-states b s x))))

:; The deterministic start states is a list with each element
:; a singleton list containing a nondeterministic start state.

(defn dfsa-starts (l nstates)
  (if (nlistp l)
      nil
      (list (order l nstates))))

;; The deterministic next state is the closure of dstate in nfsa over symbol.

(defn dfsa-next-state (dstate symbol M)
  (if (nlistp dstate)
      nil
      (union (next-states M (car dstate) symbol)
             (dfsa-next-state (cdr dstate) symbol M))))

;; The calculated next state for the deterministic machine is a subset
;; of the nstates.

(prove-lemma subsetp-dfsa-next-state (rewrite)
 (implies (and (wf-table M alphabet nstates)
               (subsetp dstate nstates))
          (subsetp (dfsa-next-state dstate symbol M) nstates)))

;; I construct the deterministic transition by calculating the 
;; deterministic next state and ordering it according to nfsa-states,
;; which is the basis for constructing the power-set, so that I
;; have a real member of the power-set as the next step.

(defn dfsa-next-transition (dstate symbol nfsa-table nfsa-states)
  (mk-transition dstate 
                 symbol 
                 (list (order 
                        (dfsa-next-state dstate symbol nfsa-table)
                        nfsa-states))))

;; cdring down states, which is the powerset of all nfsa-states.

(defn dfsa-table-for-symbol (symbol states nfsa-table nfsa-states)
  (if (nlistp states)
      nil
      (cons (dfsa-next-transition (car states) symbol nfsa-table nfsa-states)
            (dfsa-table-for-symbol 
             symbol (cdr states) nfsa-table nfsa-states))))

;; cdring down the alphabet...

(defn dfsa-table (alphabet states nfsa-table nfsa-states)
  (if (nlistp alphabet)
      nil
      (append (dfsa-table-for-symbol
               (car alphabet)
               states
               nfsa-table
               nfsa-states)
              (dfsa-table (cdr alphabet) states nfsa-table nfsa-states))))

(prove-lemma not-defined-next-states-nil (rewrite)
  (implies (not (definedp (cons s x)
                  (dfsa-table-for-symbol x b c d)))
           (equal (next-states (dfsa-table z b c d) s x) nil))
 ((do-not-generalize t)))

;; This is needed for some following lemmata, but it is a bad rewrite rule, 
;; as it is considered in every test for equality. It is disabled.

(prove-lemma definedp-means-equal (rewrite)
  (implies (definedp (cons s a) (dfsa-table-for-symbol x b c d))
           (equal (equal a x) t)))

(disable definedp-means-equal)

(prove-lemma next-states-dfsa-table (rewrite)
 (implies (member a alphabet)
          (equal (next-states (dfsa-table alphabet b c d) s a)
                 (next-states (dfsa-table-for-symbol a b c d) s a)))
 ((enable definedp-means-equal)))

;; All final states with at least one non-deterministic final are
;; deterministic final states.

(defn dfsa-final-states (dstates nfsa-finals)
  (if (nlistp dstates)
      nil
       (if (some-member (car dstates) nfsa-finals)
          (cons (car dstates)
                (dfsa-final-states (cdr dstates) nfsa-finals))
          (dfsa-final-states (cdr dstates) nfsa-finals))))
 
;; ********************************************
;; This is the function that generates the DFSA
;; ********************************************

(defn generate-dfsa (nfsa)
  (let ((nstates (states nfsa)))
    (let ((dstates  (all-subbags nstates))
          (alphabet (alphabet nfsa)))
      (fsa* alphabet
            dstates
            (dfsa-starts (starts nfsa) nstates)
            (dfsa-table alphabet dstates (table nfsa) nstates)
            (dfsa-final-states dstates (finals nfsa))))))

;; ----- Some theorems about the DFSA -----

;; Need to show that the deterministic starts are members of the powerset.

(prove-lemma dfsa-final-states-subsetp (rewrite)
 (subsetp (dfsa-final-states x y) x))

;; Extremely bad rewrite rule! Must be disabled!

(prove-lemma dfsa-final-states-member (rewrite)
 (implies (member z (dfsa-final-states x y))
          (member z x)))

(disable dfsa-final-states-member)

;; Need to show that the deterministic finals are going to be a set.

(prove-lemma setp-dfsa-final-states (rewrite)
  (implies (setp dstates)            
           (setp (dfsa-final-states dstates nfinals)))
 ((enable dfsa-final-states-member)))

;; When is an automaton a deterministic automaton?

;; A transition is deterministic if it is a transition over the alphabet
;; and the states, and there is at most one state in the list of nexts.

(defn deterministic-transition (tr alphabet states)
  (and (transitionp tr alphabet states)
       (leq (length (nexts tr)) 1)))

;; A table is deterministic if all the transitions are. 

(defn deterministic-table (table alphabet states)
  (if (nlistp table)
      T 
      (and (deterministic-transition (car table) alphabet states)
           (deterministic-table (cdr table) alphabet states))))

(defn dfsap (d)
  (and (fsap d)
       (deterministic-table (table d) (alphabet d) (states d))))

;; --------------------------------------------------------------------------
;; ------------- The theorems ---------------------

;;  If nfsa is a nondeterministic fsa, and dfsa the one constructed
;;  from nfsa, then
;;  1) dfsa is deterministic,
;;  2) if nfsa accepts then dfsa accepts, and
;;  3) if dfsa accepts then nfsa accepts.

;; 1) generate-dfsa gives a deterministic automaton

(prove-lemma deterministic-table-append (rewrite)
 (equal (deterministic-table (append a b) alphabet states)
        (and (deterministic-table a alphabet states)
             (deterministic-table b alphabet states)))
 ((induct (length a))))

(prove-lemma deterministic-table-dfsa-table-for-symbol1 (rewrite)
   (implies (and (wf-table m alphabet nstates)
                 (subsetp dstates (all-subbags nstates))
                 (member symbol alphabet))
            (deterministic-table 
             (dfsa-table-for-symbol symbol dstates m nstates)
             alphabet
             (all-subbags nstates))))

;; This needs subsetp-reflexive and the wierd previous lemma.

(prove-lemma deterministic-table-dfsa-table-for-symbol (rewrite)
 (let ((dstates (all-subbags nstates)))      
   (implies (and (member symbol alphabet)
                 (wf-table m alphabet nstates))
            (deterministic-table 
             (dfsa-table-for-symbol symbol dstates m nstates)
             alphabet
             dstates))))

;; The dfsa-table generated is deterministic.

(prove-lemma deterministic-table-dfsa-table (rewrite)
 (implies (and (wf-table m alphabet nstates)
               (subsetp x alphabet))
          (deterministic-table (dfsa-table x (all-subbags nstates) m nstates)
                               alphabet
                               (all-subbags nstates))))

;; ------------------------------------------------------------------------
;;      Theorem 1 : A deterministic automaton is obtained.
;; ------------------------------------------------------------------------

(prove-lemma dfsap-generate-dfsa ()
 (implies (ndfsap a)
          (dfsap (generate-dfsa a))))

;; -------------------------------------------------------------------------
;; 2) dfsa accepts if nfsa accepts

:; This function collects up all the next states for a list of states and a
:; symbol.

(defn next-states-list (table states a)
  (if (nlistp states)
      nil
      (union (next-states table (car states) a)
	     (next-states-list table (cdr states) a))))

(prove-lemma next-states-list-same-as-dfsa-next-state (rewrite)
 (equal (next-states-list m nstates symbol)
        (dfsa-next-state nstates symbol m)))

(prove-lemma next-states-dfsa-table-for-symbol (rewrite)
 (implies (member dstate dstates)
          (equal (next-states 
		  (dfsa-table-for-symbol c dstates ntab d) dstate c)
                 (nexts (dfsa-next-transition dstate c ntab d)))))

(prove-lemma dfsa-next-state-union (rewrite)
          (equal (dfsa-next-state (cons a b) c d)
                 (union (next-states d a c)
                        (dfsa-next-state b c d))))

;; This is the fifth different function I have used to define the notion
;; of acceptance in an automaton. I use the witness function some-member
;; to construct a member from the intersection of the final states reached
;; and the finals of the automaton. accept1 runs the automaton on the tape,
;; collecting up all reachable states.

(defn accept1 (table states finals tape)
 (if (nlistp tape)
     (some-member states finals)
     (accept1 table
	      (next-states-list table states (car tape))
	      finals
	      (cdr tape))))

(defn accept (fsa tape)
 (accept1 (table fsa) (starts fsa) (finals fsa) tape))

(prove-lemma member-dstate-dfsa-final-states (rewrite)
             (implies (and (some-member dstate nfinals)
                           (member dstate dstates))
                      (member dstate (dfsa-final-states dstates nfinals))))

(prove-lemma order-final-states (rewrite)
  (implies (and (subsetp nfsa-finals nfsa-states)
                (some-member w nfsa-finals))
           (member (order w nfsa-states)
                   (dfsa-final-states (all-subbags nfsa-states)
                                      nfsa-finals))))

(disable member-all-subbags)

(prove-lemma subsetp-order (rewrite)
 (subsetp (order a b) a)
 ((disable ordered-member-all-subbags)))

(prove-lemma subsetp-next-states-2 (rewrite)
 (implies (member z b)
          (subsetp (next-states v z c)
                   (dfsa-next-state b c v))))

(prove-lemma dfsa-next-state-distrib (rewrite)
 (implies (subsetp a b)
          (subsetp (dfsa-next-state a c v)
                   (dfsa-next-state b c v)))
  ((do-not-generalize t)))

(prove-lemma subsetp-dfsa-next-state-1 (rewrite)
  (subsetp (dfsa-next-state (order w d) c v)
           (dfsa-next-state w c v)))

;; This is the schema I will use for proving order-dfsa-next-state-order.

(prove-lemma equal-order-subsetp (rewrite)
 (implies (and (subsetp a b)
               (subsetp b a))
          (equal (order a c)
                 (order b c))))

;; This is one half of the conjunct. It is always true.

(prove-lemma subsetp-dfsa-next-state-2-helper (rewrite)
 (subsetp (dfsa-next-state (order x y) c v)
          (dfsa-next-state (order (cons z x) y) c v)))

;; This is the second half. It is only true when w is a subset of d.

(prove-lemma subsetp-dfsa-next-state-2 (rewrite)
 (implies (subsetp w d)
          (subsetp (dfsa-next-state w c v)
                   (dfsa-next-state (order w d) c v))))

;; This one I got in the proof checker.

(prove-lemma order-dfsa-next-state-order
             (rewrite)
             (implies (and (wf-table ntab alphabet nstates) 
                           (subsetp dstate nstates))
                      (equal (order (dfsa-next-state 
                                     (order dstate nstates) symbol ntab)
                                    nstates)
                             (order 
			      (dfsa-next-state dstate symbol ntab) nstates)))
             ((use (equal-order-subsetp
                    (b (dfsa-next-state dstate symbol ntab))
                    (a (dfsa-next-state (order dstate nstates) symbol ntab))
                    (c nstates)))))

(prove-lemma do-not-push (rewrite)
 (implies (and (subsetp dstate nstates)
               (subsetp nfinals nstates)
               (wf-table ntab alphabet nstates)
               (all-member tape alphabet)
               (accept1 ntab dstate nfinals tape))
          (accept1 (dfsa-table alphabet (all-subbags nstates) ntab nstates)
                          (list (order dstate nstates))
                          (dfsa-final-states (all-subbags nstates) nfinals)
                          tape))
 ((do-not-generalize t)))

;; ------------------------------------------------------------------------
;;      Theorem 2 : If a tape is recognized by the nondeterministic 
;;            automaton, then it is recognized by the deterministic one.
;; ------------------------------------------------------------------------

(prove-lemma nfsa-accepts=>dfsa-accepts (rewrite)
 (implies (and (ndfsap nfsa)
               (all-member tape (ALPHABET NFSA))
               (accept nfsa tape))
          (accept (generate-dfsa nfsa) tape)))

;; -------------------------------------------------------------------------
;; 3) And now for the grand finale... nfsa accepts when the dfsa does

(prove-lemma member-dfsa-final-states-some-member (rewrite)
 (implies (member x (dfsa-final-states foo bar))
          (some-member x bar)))

;; This theorem was suggested by the proof checker.

(prove-lemma not-some-member-not-member-dfsa-final-states (rewrite)
 (implies (not (some-member w z))
	  (not (member (order w d)
		       (dfsa-final-states (all-subbags d) z))))
 ((use (some-member-order (d d) (w w) (z z))
       (member-dfsa-final-states-some-member))))

(prove-lemma member-order-dfsa-final=>some-member (rewrite)
 (implies (and (subsetp w d)
	       (subsetp z d)
	       (member (order w d)
		       (dfsa-final-states (all-subbags d) z)))
	  (some-member w z)))

(prove-lemma do-not-push-theorem-3 (rewrite)
  (implies (and (subsetp w d)
		(subsetp z d)
		(wf-table v x d)
		(all-member tape x)
		(accept1 (dfsa-table x (all-subbags d) v d)
			 (list (order w d))
			 (dfsa-final-states (all-subbags d) z)
			 tape))
           (accept1 v w z tape)))

;; -------------------------------------------------------------------------
;;           Theorem 3 : If a deterministic automaton accepts
;;                       then the non-deterministic one does too
;; -------------------------------------------------------------------------

;; And it proves!

(prove-lemma dfsa-accepts=>nfsa-accepts (rewrite)
 (implies (and (ndfsap nfsa)
               (all-member tape (ALPHABET NFSA))
               (accept (generate-dfsa nfsa) tape))
          (accept nfsa tape)))

;; Main Theorem: nfsa accepts iff dfsa accepts.

(prove-lemma NFSA=DFSA ()
 (implies (and (ndfsap nfsa)
               (all-member tape (alphabet nfsa)))
          (iff (accept (generate-dfsa nfsa) tape)
               (accept nfsa tape))))

#|
; As a test I have the example given in Aho/Ullman page 117 that
; is converted correctly to a deterministic automaton. Thus one
; knows that the proof is not just vacuously true: it does compute
; something other than nil.

(setq trans (list
                (mk-transition 'q0 1 '(q0 q1))
                (mk-transition 'q0 2 '(q0 q2))
                (mk-transition 'q0 3 '(q0 q3))
                (mk-transition 'q1 1 '(q1 qf))
                (mk-transition 'q1 2 '(q1))
                (mk-transition 'q1 3 '(q1))
                (mk-transition 'q2 1 '(q2))
                (mk-transition 'q2 2 '(q2 qf))
                (mk-transition 'q2 3 '(q2))
                (mk-transition 'q3 1 '(q3))
                (mk-transition 'q3 2 '(q3))
                (mk-transition 'q3 3 '(q3 qf))))

(setq tape-bad '(1 2 1 2 1 2 3)) 
(setq tape-good  '(1 2 1 2 1 2 3 3)) 

(setq alphabet         '(1 2 3))
(setq states '(q0 q1 q2 q3 qf))
(setq starts '(q0))
(setq finals '(qf))

(setq nfsa (fsa* alphabet states starts trans finals))
(setq dfsa (generate-dfsa nfsa))

(accept nfsa tape-good)
(accept dfsa tape-good)
(accept nfsa tape-bad)
(accept dfsa tape-bad)
|#