; ~/events/epsilon.events
(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)))

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

(prove-lemma subsetp-union-anything (rewrite)
 (implies (subsetp x y)
	  (subsetp x (union anything y))))

;; ---------------------------------------------------------------------------
;; ----- 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)))

(prove-lemma union-right-id (rewrite)
 (implies (plistp foo)
	  (equal (union foo nil) foo)))

(prove-lemma plistp-union (rewrite)
 (implies (plistp y)
	  (plistp (union anything y))))

;; ---------------------------------------------------------------------------
;;      order
;; ---------------------------------------------------------------------------
;; To simulate set equality, I 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-order (rewrite)
 (implies (and (member z x)
	       (member z v))
	  (member z (order x v))))

(prove-lemma order-cons (rewrite)
  (implies (member z x)
	   (equal (order (cons z x) v)
		  (order x v))))

(prove-lemma order-cons2 (rewrite)
  (implies (not (member z v))
	   (equal (order (cons z x) v)
		  (order x v))))

(prove-lemma order-cons4 (rewrite)
  (implies (member z x)
	   (equal (order (cons z (order x v)) v)
		  (order (order x v) v)))
  ((use (member-order))
   (disable member-order)))

(prove-lemma order-idempotent (rewrite)
  (equal (order (order x y) y) (order x y)))

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

(prove-lemma subsetp-order-4 (rewrite)
 (implies (and (subsetp a b)
	       (member x a))
	  (member x (order a b))))
	       
; ---- 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 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))))

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

;; ---------------------------------------------------------------------------
;;      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))

;; Not being able to determine if the epsilon representation is a member
;; of the alphabet is not a GOOD THING. Therefore an explicit
;; representation will be used.

(defn epsilon () 'epsilon)
  
;; 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 nfsa-transitionp (trans alphabet states)
 (and (or (member (input trans) alphabet)
	  (equal (input trans) (epsilon)))
      (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 all-nfsa-transitions (table alphabet states)
  (if (nlistp table)
      (equal table nil)
      (and (nfsa-transitionp (car table) alphabet states)
	   (all-nfsa-transitions (cdr table) alphabet states))))

(defn wf-nfsa-table (table alphabet states)
  (and (all-nfsa-transitions table alphabet states)
       (not (member (epsilon) alphabet))))

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

(defn ndfsap (a)
  (and (fsap a)
       (wf-nfsa-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))))

(prove-lemma subsetp-next-states (rewrite)
 (implies (all-nfsa-transitions M alphabet nstates)
	  (subsetp (next-states M state symbol)
		   nstates)))

;; ---------------------------------------------------------------------------
;; Epsilon closure

;; For all states in the list, take an epsilon step

(defn one-epsilon-step-all (states table)
 (if (nlistp states)
     nil
     (union
      (next-states table (car states) (epsilon)) 
      (one-epsilon-step-all (cdr states) table))))

;; This will only prove on (length b), not on (length a)! It seems to depend
;; on the structure of the function 'union!

(prove-lemma not-lessp-length-union (rewrite)
	  (not (lessp (length (union a b))
		      (length b))))

;; This is the epsilon closure without needing a clock.
;; The termination argument: if they are the same length, they are the same.

(defn epsilon-closure (table states all-states)
    (let ((next-set (union (one-epsilon-step-all states table) states)))
      (if (or (equal (length states) (length next-set))
	      (not (lessp (length next-set) (length all-states))))
	  states
	(epsilon-closure table next-set all-states)))
 ((lessp (difference (length all-states) (length states)))))

;; Take a step from state on sym, and then take the epsilon closure.

(defn next-with-epsilon-closure (table state sym all-states)
  (epsilon-closure table  (next-states table state sym) all-states))

;; This lemma needed three levels of induction.

(prove-lemma subsetp-one-epsilon-step-all1 (rewrite)
 (implies (and (all-nfsa-transitions M alphabet nstates)
	       (subsetp states nstates))
	  (subsetp (one-epsilon-step-all states M)
		   nstates)))

(prove-lemma subsetp-epsilon-closure (rewrite)
 (implies (and (all-nfsa-transitions m alphabet nstates)
	       (subsetp states nstates))
	  (subsetp (epsilon-closure m states nstates) nstates)))

(prove-lemma subsetp-epsilon-closure-2 (Rewrite)
 (subsetp states
	  (epsilon-closure m states all-states)))

;; 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 containing the
;; epsilon-closure of all the nondeterministic start states.

(defn dfsa-starts (l table nstates)
  (list (order (epsilon-closure table l nstates) nstates)))		

;; The function next-states-list collects up all the next states for a list
;; of states and a symbol. I have to take the epsilon closure for the
;; deterministic automaton. It won't hurt the deterministic one if it is
;; shown that there are no epsilon productions in the generated automaton !

(defn next-states-list (states a table all-states)
  (if (nlistp states)
      nil
      (union
       (next-with-epsilon-closure table (car states) a all-states)
       (next-states-list (cdr states) a table all-states))))

(prove-lemma plistp-next-states-list (rewrite)
 (implies (all-nfsa-transitions table alphabet nstates)
  (plistp  (next-states-list dstates symbol table nstates)))) 

(prove-lemma subsetp-next-states-list (rewrite)
 (implies (and (subsetp dstates nstates)
	       (all-nfsa-transitions table alphabet nstates))
	  (subsetp (next-states-list dstates symbol table nstates) nstates)))

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

(defn dfsa-next-state (dstate symbol M all-states)
  (if (nlistp dstate)
      nil
      (next-states-list (epsilon-closure M dstate all-states)
			symbol M all-states)))

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

(prove-lemma subsetp-dfsa-next-state (rewrite)
 (implies (and (all-nfsa-transitions  M alphabet nstates)
	       (subsetp dstate nstates))
	  (subsetp (dfsa-next-state dstate symbol M nstates) 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)
			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))))

;; This lemma, too, needs three levels of induction, be patient.

(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 lemma, 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)

; proves with next-states append, just give it time!
(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 nondeterministic 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))
	  (table    (table nfsa))
	  (alphabet (alphabet nfsa)))
      (fsa* alphabet
	    dstates
	    (dfsa-starts (starts nfsa) (table nfsa) nstates)
	    (dfsa-table alphabet dstates table 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))

;; This 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 dfsa-transitionp (trans alphabet states)
 (and (member (input trans) alphabet)
      (member (state trans) states)
      (subsetp (nexts trans) states)
      (plistp (nexts trans))
      (leq (length (nexts trans)) 1)))

; A table is deterministic is all the transitions are. 

(defn all-dfsa-transitions (table alphabet states)
  (if (nlistp table)
      T 
      (and (dfsa-transitionp (car table) alphabet states)
	   (all-dfsa-transitions (cdr table) alphabet states))))

(defn wf-dfsa-table
      (table alphabet states)
      (and (all-dfsa-transitions table alphabet states)
           (not (member (epsilon) alphabet))))

(defn dfsap (d)
  (and (fsap d)
       (wf-dfsa-table (table d) (alphabet d) (states d))))

;; ---------------------------------------------------------------------------
;; Many proofs are the same as without epsilon-closure.
;; ------------- 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 all-dfsa-transitions-append (rewrite)
 (equal (all-dfsa-transitions (append a b) alphabet states)
	(and (all-dfsa-transitions a alphabet states)
	     (all-dfsa-transitions b alphabet states))) ((induct (length a))))

;; This is STRANGE! It is necessary for the following proof to go through. 
;; It seems to be just a method to force the prover to induct on dstates! 
;; If I use EQUAL instead of SUBSETP (which is "truer"), then the prover
;; selects the extremely stupid induction on M, and cannot be
;; convinced, even by hint, to try an induction on dstates.

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

;; Needed subsetp-reflexive and the wierd previous lemma.

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

;; The dfsa-table generated is deterministic.

(prove-lemma all-dfsa-transitions-dfsa-table (rewrite)
 (implies (and (wf-nfsa-table m alphabet nstates)
	       (subsetp x alphabet))
	  (all-dfsa-transitions
               (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

(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)))))

;; ---------------------------------------------------------------------------
;; The proof in the Hopcroft/Ullman book is not acceptance, but involves
;; the set of states reached on a tape (input).

(defn reached (table states tape all-states)
 (if (nlistp tape) 
     states
     (reached table
	      (next-states-list states (car tape) table all-states)
	      (cdr tape)
	      all-states)))

(prove-lemma reached-append (rewrite)
 (equal (reached table states (append a b) all-states)
	(reached table (reached table states a all-states) b all-states)))

(prove-lemma subsetp-reached (rewrite)
 (implies (and (subsetp starts nstates)
	       (all-nfsa-transitions table alphabet nstates))
	  (subsetp (reached table starts tape nstates) nstates)))

(prove-lemma plistp-reached (rewrite)
 (implies (and (all-nfsa-transitions ntab alphabet nstates)
	       (plistp starts)
	       (subsetp starts nstates))
	  (plistp (reached ntab starts tape nstates))))

(prove-lemma plistp-epsilon-closure (rewrite)
 (implies (plistp states)
	  (plistp (epsilon-closure table states all-states))))

(prove-lemma next-states-list-nil (rewrite)
 (equal (next-states-list nil symbol table states)
	nil))

;; ---------------------------------------------------------------------------
;; Here are the axioms that I strongly believe.
;; ---------------------------------------------------------------------------

(axiom next-states-list-order-equal (rewrite)
 (implies (subsetp a b)
	  (equal (next-states-list (order a b) symbol table states)
		 (order (next-states-list a symbol table states) b))))

(axiom epsilon-closure-dfsa-identity (rewrite)
	  (equal (epsilon-closure (DFSA-TABLE ALPHABET dstates NTAB NSTATES)
				  x
				  dstates)
		 x))

;; If we reached a state, it has just been epsilon-closed, so another
;; epsilon-closure won't change anything.

(axiom next-states-list-epsilon-closure-reached (rewrite)
  (equal (next-states-list 
           (epsilon-closure ntab
             (order (reached ntab starts tape nstates) nstates)
             nstates)
           symbol ntab nstates)
	 (next-states-list (order (reached ntab starts tape nstates) nstates)
			   symbol ntab nstates)))

;; This should be the main result helper, but it uses a "wrong"
;; induction structure.

(prove-lemma reaches-nfsa-reaches-dfsa (rewrite)
 (implies (and (subsetp starts nstates)
	       (listp tape)
	       (all-nfsa-transitions ntab alphabet nstates)
	       (member symbol alphabet)
	       (listp (order (reached ntab starts tape nstates) nstates))
	       (equal (reached (dfsa-table alphabet
					   (all-subbags nstates)
					   ntab nstates)
			       (dfsa-starts starts nfsa nstates)
			       tape
			       (all-subbags nstates))
		      (list 
		       (order (reached ntab starts tape nstates) nstates))))
	  (equal (reached (dfsa-table alphabet
				      (all-subbags nstates)
				      ntab nstates)
			  (dfsa-starts starts nfsa nstates)
			  (append tape (list symbol))
			  (all-subbags nstates))
		 (list (order (reached ntab starts
				       (append tape (list symbol))
				       nstates)
			      nstates))))
           ((INSTRUCTIONS PROMOTE
                          (DIVE 1)
                          (REWRITE REACHED-APPEND)
                          (DIVE 2)
                          = TOP
                          (DIVE 2 1 1)
                          (REWRITE REACHED-APPEND)
                          TOP
                          (DIVE 1)
                          X X
                          (REWRITE UNION-RIGHT-ID)
                          (DIVE 2)
                          (REWRITE NEXT-STATES-DFSA-TABLE)
                          (REWRITE NEXT-STATES-DFSA-TABLE-FOR-SYMBOL)
                          S UP
                          (REWRITE EPSILON-CLOSURE-DFSA-IDENTITY)
                          TOP S
                          (DIVE 2 1)
                          X TOP
                          (DIVE 1 1)
                          (REWRITE NEXT-STATES-LIST-EPSILON-CLOSURE-REACHED)
                          (REWRITE NEXT-STATES-LIST-ORDER-EQUAL)
                          UP
                          (REWRITE ORDER-IDEMPOTENT)
			  TOP PROVE PROVE PROVE PROVE )))

;; This is the fifth different acceptance function.

(defn accept (fsa tape)
 (some-member 
  (reached (table fsa) (starts fsa) tape (states fsa))
  (finals fsa)))

;; --------------------------------------------------------------------------
;; The following are the formulations of the next theorems. There were,
;; however, not completed as the axioms could not be removed from the
;; previous proof.

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

;;; need to do the induction "backwards", from the back.

;(prove-lemma nfsa-accepts=>dfsa-accepts (rewrite)
; (implies (and (ndfsap nfsa)
;	       (all-member tape (ALPHABET NFSA))
;	       (accept nfsa tape))
;	  (accept (generate-dfsa nfsa) tape))
; ((disable  wf-nfsa-table reached dfsa-starts)))

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

;(prove-lemma dfsa-accepts=>nfsa-accepts (rewrite)
; (implies (and (ndfsap nfsa)
;	       (all-member tape (alphabet nfsa))
;	       (listp tape) ; only valid for non-empty tapes!
;	       (accept (generate-dfsa nfsa) tape))
;	  (accept nfsa tape)))

;;; Main Theorem: iff statt equal

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