(in-package "ACL2")

(include-book "inference")

(in-theory (disable ste-thm ste-thm-forward ste-thm-backward
		    fundamental-theorem-of-ste-pre))

(defconst *nand-delay*
	`( x
	   (not (and 0 2))
	   1
	   nil
	   ))






;;;
;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;

(defthm nand-operation-thm1 
  (implies (and (booleanp b1)
		(booleanp b2))
	   (ste-thm *nand-delay*
		    `(and (and (is 0 ,b1)
			       (is 2 ,b2))
			  (and (is 3 nil)
			       (next (is 3 nil))))
		    `(and (next (is 1 ,(not (and b1 b2))))
			  (and (is 3 nil)
			       (next (is 3 nil))))))
  :hints (("Goal"
	   :in-theory `((:DEFINITION IMPLIES)
			(:REWRITE FUNDAMENTAL-THEOREM-OF-STE)
			(:DEFINITION R-LTE)
			(:REWRITE R-LTE-REFLEXIVE)
			(:COMPOUND-RECOGNIZER BOOLEANP-COMPOUND-RECOGNIZER)
			(:REWRITE DEFTRAJ-CONS-EXPAND)
			(:DEFINITION R-DEFTRAJ)
			(:EXECUTABLE-COUNTERPART BOOLEANP)
			(:EXECUTABLE-COUNTERPART NTH)
			(:EXECUTABLE-COUNTERPART E-EVAL)
			(:REWRITE NTH-ADD1)
			(:REWRITE NTH-0-CONS)
			(:DEFINITION LEN)
			(:DEFINITION B-AND)
			(:DEFINITION B-NOT)
			(:REWRITE E-EVAL-IS-B-P)
			(:DEFINITION C-EVAL)
			(:DEFINITION E-EVAL)
			(:DEFINITION N-P)
			(:EXECUTABLE-COUNTERPART E-P)
			(:EXECUTABLE-COUNTERPART CONS)
			(:EXECUTABLE-COUNTERPART R-LUB)
			(:REWRITE HOOYAH-3)
			(:EXECUTABLE-COUNTERPART S-LTE)
			(:DEFINITION B-LTE)
			(:DEFINITION S-LTE)
			(:EXECUTABLE-COUNTERPART B-LTE)
			(:REWRITE R-P-CONS-1)
			(:REWRITE L-EVAP-N-IF-L-EVALP-N-MINUS-1)
			(:DEFINITION B-LUB)
			(:DEFINITION S-LUB)
			(:EXECUTABLE-COUNTERPART B-LUB)
			(:REWRITE S-P-CONS)
			(:EXECUTABLE-COUNTERPART S-P)
			(:REWRITE BOOLEANP-IS-B-P)
			(:EXECUTABLE-COUNTERPART B-P)
			(:EXECUTABLE-COUNTERPART S-LUB)
			(:DEFINITION UPDATE-NTH)
			(:EXECUTABLE-COUNTERPART ZP)
			(:EXECUTABLE-COUNTERPART S-MAKE)
			(:DEFINITION L-DEFSEQ)
			(:REWRITE R-P-CDR)
			(:TYPE-PRESCRIPTION R-P)
			(:TYPE-PRESCRIPTION L-DEFSEQ-IS-R-P)
			(:DEFINITION R-LUB)
			(:REWRITE L-DEFSEQ-CONSP)
			(:EXECUTABLE-COUNTERPART R-P)
			(:REWRITE L-DEFSEQ-IS-R-P)
			(:EXECUTABLE-COUNTERPART L-DEFSEQ)
			(:DEFINITION L-EVALP)
			(:TYPE-PRESCRIPTION L-EVALP-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-EVALP)
			(:DEFINITION L-DEPTH)
			(:EXECUTABLE-COUNTERPART L-DEPTH)
			(:EXECUTABLE-COUNTERPART LEN)
			(:EXECUTABLE-COUNTERPART BINARY-+)
			(:DEFINITION L-MAXN)
			(:DEFINITION MAX)
			(:EXECUTABLE-COUNTERPART L-MAXN)
			(:EXECUTABLE-COUNTERPART C-P)
			(:EXECUTABLE-COUNTERPART <)
			(:EXECUTABLE-COUNTERPART INTEGERP)
			(:DEFINITION L-P)
			(:TYPE-PRESCRIPTION L-P-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-P)
			(:EXECUTABLE-COUNTERPART CAR)
			(:EXECUTABLE-COUNTERPART CDR)
			(:EXECUTABLE-COUNTERPART CONSP)
			(:REWRITE CDR-CONS)
			(:EXECUTABLE-COUNTERPART EQUAL)
			(:REWRITE CAR-CONS)
					;(:FAKE-RUNE-FOR-TYPE-SET NIL)
			(:DEFINITION NOT)
			(:TYPE-PRESCRIPTION STE-THM)))))


(defthm delay-operation-thm1
  (implies (booleanp b1)
	   (ste-thm *nand-delay*
		    `(and (is 1 ,b1)
			  (and (is 3 nil)
			       (next (is 3 nil))))
		    `(and (next (is 2 ,b1))
			  (and (is 3 nil)
			       (next (is 3 nil))))))
  :hints (("Goal"
	   :in-theory `((:DEFINITION IMPLIES)
			(:REWRITE FUNDAMENTAL-THEOREM-OF-STE)
			(:DEFINITION R-LTE)
			(:REWRITE R-LTE-REFLEXIVE)
			(:COMPOUND-RECOGNIZER BOOLEANP-COMPOUND-RECOGNIZER)
			(:REWRITE R-P-CONS-1)
			(:REWRITE DEFTRAJ-CONS-EXPAND)
			(:DEFINITION R-DEFTRAJ)
			(:TYPE-PRESCRIPTION B-P)
			(:DEFINITION S-P)
			(:EXECUTABLE-COUNTERPART E-EVAL)
			(:EXECUTABLE-COUNTERPART BOOLEANP)
			(:REWRITE NTH-ADD1)
			(:EXECUTABLE-COUNTERPART NTH)
			(:REWRITE NTH-0-CONS)
			(:DEFINITION LEN)
			(:DEFINITION B-AND)
			(:DEFINITION B-NOT)
			(:REWRITE E-EVAL-IS-B-P)
			(:DEFINITION C-EVAL)
			(:DEFINITION E-EVAL)
			(:DEFINITION N-P)
			(:EXECUTABLE-COUNTERPART E-P)
			(:REWRITE HOOYAH-3)
			(:EXECUTABLE-COUNTERPART S-LTE)
			(:DEFINITION B-LTE)
			(:DEFINITION S-LTE)
			(:EXECUTABLE-COUNTERPART B-LTE)
			(:EXECUTABLE-COUNTERPART CONS)
			(:REWRITE L-EVAP-N-IF-L-EVALP-N-MINUS-1)
			(:DEFINITION B-LUB)
			(:DEFINITION S-LUB)
			(:EXECUTABLE-COUNTERPART B-LUB)
			(:REWRITE S-P-CONS)
			(:EXECUTABLE-COUNTERPART S-P)
			(:REWRITE BOOLEANP-IS-B-P)
			(:EXECUTABLE-COUNTERPART B-P)
			(:EXECUTABLE-COUNTERPART S-LUB)
			(:DEFINITION UPDATE-NTH)
			(:EXECUTABLE-COUNTERPART ZP)
			(:EXECUTABLE-COUNTERPART S-MAKE)
			(:DEFINITION L-DEFSEQ)
			(:REWRITE R-P-CDR)
			(:TYPE-PRESCRIPTION R-P)
			(:TYPE-PRESCRIPTION L-DEFSEQ-IS-R-P)
			(:DEFINITION R-LUB)
			(:REWRITE L-DEFSEQ-CONSP)
			(:EXECUTABLE-COUNTERPART R-P)
			(:REWRITE L-DEFSEQ-IS-R-P)
			(:EXECUTABLE-COUNTERPART L-DEFSEQ)
			(:DEFINITION L-EVALP)
			(:TYPE-PRESCRIPTION L-EVALP-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-EVALP)
			(:DEFINITION L-DEPTH)
			(:EXECUTABLE-COUNTERPART L-DEPTH)
			(:EXECUTABLE-COUNTERPART LEN)
			(:EXECUTABLE-COUNTERPART BINARY-+)
			(:DEFINITION L-MAXN)
			(:DEFINITION MAX)
			(:EXECUTABLE-COUNTERPART L-MAXN)
			(:EXECUTABLE-COUNTERPART C-P)
			(:EXECUTABLE-COUNTERPART <)
			(:EXECUTABLE-COUNTERPART INTEGERP)
			(:DEFINITION L-P)
			(:TYPE-PRESCRIPTION L-P-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-P)
			(:EXECUTABLE-COUNTERPART CAR)
			(:EXECUTABLE-COUNTERPART CDR)
			(:EXECUTABLE-COUNTERPART CONSP)
			(:REWRITE CDR-CONS)
			(:EXECUTABLE-COUNTERPART EQUAL)
			(:REWRITE CAR-CONS)
					;(:FAKE-RUNE-FOR-TYPE-SET NIL)
			(:TYPE-PRESCRIPTION STE-THM)))))


(in-theory (disable fundamental-theorem-of-ste))

;;;
;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;



(defthm p3
  (implies (and (booleanp b0)
		(booleanp b2))
	   (ste-thm *nand-delay*
		    `(and (and (is 0 ,b0)
			       (is 2 ,b2))
			  (next (next (is 3 nil))))
		    `(and (next (next (is 2 ,(or (not b0) (not b2)))))
			  (next (next (is 3 nil))))
		    ))
  :rule-classes nil
  :hints (("Goal"
	   :in-theory `((:DEFINITION IMPLIES)
			(:REWRITE FUNDAMENTAL-THEOREM-OF-STE)
			(:EXECUTABLE-COUNTERPART R-LTE)
			(:DEFINITION R-LTE)
			(:COMPOUND-RECOGNIZER BOOLEANP-COMPOUND-RECOGNIZER)
			(:REWRITE DEFTRAJ-CONS-EXPAND)
			(:DEFINITION R-DEFTRAJ)
			(:TYPE-PRESCRIPTION B-P)
			(:DEFINITION S-P)
			(:EXECUTABLE-COUNTERPART BOOLEANP)
			(:EXECUTABLE-COUNTERPART NTH)
			(:EXECUTABLE-COUNTERPART E-EVAL)
			(:REWRITE NTH-ADD1)
			(:REWRITE NTH-0-CONS)
			(:DEFINITION LEN)
			(:DEFINITION B-AND)
			(:DEFINITION B-NOT)
			(:REWRITE E-EVAL-IS-B-P)
			(:DEFINITION C-EVAL)
			(:DEFINITION E-EVAL)
			(:DEFINITION N-P)
			(:EXECUTABLE-COUNTERPART E-P)
			(:EXECUTABLE-COUNTERPART CONS)
			(:EXECUTABLE-COUNTERPART R-LUB)
			(:REWRITE HOOYAH-3)
			(:EXECUTABLE-COUNTERPART S-LTE)
			(:DEFINITION B-LTE)
			(:DEFINITION S-LTE)
			(:EXECUTABLE-COUNTERPART B-LTE)
			(:REWRITE R-P-CONS-1)
			(:REWRITE L-EVAP-N-IF-L-EVALP-N-MINUS-1)
			(:DEFINITION B-LUB)
			(:DEFINITION S-LUB)
			(:EXECUTABLE-COUNTERPART B-LUB)
			(:REWRITE S-P-CONS)
			(:EXECUTABLE-COUNTERPART S-P)
			(:REWRITE BOOLEANP-IS-B-P)
			(:EXECUTABLE-COUNTERPART B-P)
			(:EXECUTABLE-COUNTERPART S-LUB)
			(:DEFINITION UPDATE-NTH)
			(:EXECUTABLE-COUNTERPART ZP)
			(:EXECUTABLE-COUNTERPART S-MAKE)
			(:DEFINITION L-DEFSEQ)
			(:REWRITE R-P-CDR)
			(:TYPE-PRESCRIPTION R-P)
			(:TYPE-PRESCRIPTION L-DEFSEQ-IS-R-P)
			(:DEFINITION R-LUB)
			(:REWRITE L-DEFSEQ-CONSP)
			(:EXECUTABLE-COUNTERPART R-P)
			(:REWRITE L-DEFSEQ-IS-R-P)
			(:EXECUTABLE-COUNTERPART L-DEFSEQ)
			(:DEFINITION L-EVALP)
			(:TYPE-PRESCRIPTION L-EVALP-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-EVALP)
			(:DEFINITION L-DEPTH)
			(:EXECUTABLE-COUNTERPART L-DEPTH)
			(:EXECUTABLE-COUNTERPART LEN)
			(:EXECUTABLE-COUNTERPART BINARY-+)
			(:DEFINITION L-MAXN)
			(:DEFINITION MAX)
			(:EXECUTABLE-COUNTERPART L-MAXN)
			(:EXECUTABLE-COUNTERPART C-P)
			(:EXECUTABLE-COUNTERPART <)
			(:EXECUTABLE-COUNTERPART INTEGERP)
			(:DEFINITION L-P)
			(:TYPE-PRESCRIPTION L-P-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-P)
			(:EXECUTABLE-COUNTERPART CAR)
			(:EXECUTABLE-COUNTERPART CDR)
			(:EXECUTABLE-COUNTERPART CONSP)
			(:REWRITE CDR-CONS)
			(:EXECUTABLE-COUNTERPART EQUAL)
			(:REWRITE CAR-CONS)
					;(:FAKE-RUNE-FOR-TYPE-SET NIL)
			(:EXECUTABLE-COUNTERPART NOT)
			(:DEFINITION NOT)
			(:TYPE-PRESCRIPTION STE-THM)))))

(defthm p4
  (implies (and (booleanp b1)
		(booleanp b3))
	   
	   (ste-thm *nand-delay*
		    `(and (and (is 1 ,b1)
			       (next (is 0 ,b3)))
			  (next (next (is 3 nil))))
		    `(and (next (next (is 1 ,(not (and b1 b3)))))
			  (next (next (is 3 nil))))
		    )
	   )
  :rule-classes nil
  :hints (("Goal"
	   :in-theory `((:DEFINITION IMPLIES)
			(:REWRITE FUNDAMENTAL-THEOREM-OF-STE)
			(:COMPOUND-RECOGNIZER BOOLEANP-COMPOUND-RECOGNIZER)
			(:REWRITE DEFTRAJ-CONS-EXPAND)
			(:DEFINITION R-DEFTRAJ)
			(:EXECUTABLE-COUNTERPART E-EVAL)
			(:EXECUTABLE-COUNTERPART BOOLEANP)
			(:REWRITE NTH-ADD1)
			(:EXECUTABLE-COUNTERPART NTH)
			(:REWRITE NTH-0-CONS)
			(:DEFINITION LEN)
			(:DEFINITION B-AND)
			(:DEFINITION B-NOT)
			(:REWRITE E-EVAL-IS-B-P)
			(:DEFINITION C-EVAL)
			(:DEFINITION E-EVAL)
			(:DEFINITION N-P)
			(:EXECUTABLE-COUNTERPART E-P)
			(:REWRITE HOOYAH-3)
			(:EXECUTABLE-COUNTERPART B-LTE)
			(:EXECUTABLE-COUNTERPART CONS)
			(:REWRITE R-LUB-R-LTE-REWRITE-2)
			(:DEFINITION R-LTE)
			(:EXECUTABLE-COUNTERPART R-LTE)
			(:DEFINITION S-LTE)
			(:EXECUTABLE-COUNTERPART S-LTE)
			(:DEFINITION B-LTE)
			(:REWRITE R-P-CONS-1)
			(:REWRITE L-EVAP-N-IF-L-EVALP-N-MINUS-1)
			(:DEFINITION B-LUB)
			(:DEFINITION S-LUB)
			(:EXECUTABLE-COUNTERPART B-LUB)
			(:REWRITE S-P-CONS)
			(:EXECUTABLE-COUNTERPART S-P)
			(:REWRITE BOOLEANP-IS-B-P)
			(:EXECUTABLE-COUNTERPART B-P)
			(:EXECUTABLE-COUNTERPART S-LUB)
			(:DEFINITION UPDATE-NTH)
			(:EXECUTABLE-COUNTERPART ZP)
			(:EXECUTABLE-COUNTERPART S-MAKE)
			(:DEFINITION L-DEFSEQ)
			(:REWRITE R-P-CDR)
			(:TYPE-PRESCRIPTION R-P)
			(:TYPE-PRESCRIPTION L-DEFSEQ-IS-R-P)
			(:DEFINITION R-LUB)
			(:REWRITE L-DEFSEQ-CONSP)
			(:EXECUTABLE-COUNTERPART R-P)
			(:REWRITE L-DEFSEQ-IS-R-P)
			(:EXECUTABLE-COUNTERPART L-DEFSEQ)
			(:DEFINITION L-EVALP)
			(:TYPE-PRESCRIPTION L-EVALP-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-EVALP)
			(:DEFINITION L-DEPTH)
			(:EXECUTABLE-COUNTERPART L-DEPTH)
			(:EXECUTABLE-COUNTERPART LEN)
			(:EXECUTABLE-COUNTERPART BINARY-+)
			(:DEFINITION L-MAXN)
			(:DEFINITION MAX)
			(:EXECUTABLE-COUNTERPART L-MAXN)
			(:EXECUTABLE-COUNTERPART C-P)
			(:EXECUTABLE-COUNTERPART <)
			(:EXECUTABLE-COUNTERPART INTEGERP)
			(:DEFINITION L-P)
			(:TYPE-PRESCRIPTION L-P-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-P)
			(:EXECUTABLE-COUNTERPART CAR)
			(:EXECUTABLE-COUNTERPART CDR)
			(:EXECUTABLE-COUNTERPART CONSP)
			(:REWRITE CDR-CONS)
			(:EXECUTABLE-COUNTERPART EQUAL)
			(:REWRITE CAR-CONS)
					;(:FAKE-RUNE-FOR-TYPE-SET NIL)
			(:DEFINITION NOT)
			(:TYPE-PRESCRIPTION STE-THM)))))



(defthm p2
  (implies (and (booleanp b0)
		(booleanp b1)
		(booleanp b2)
		(booleanp b3)

		(ste-thm *nand-delay*
			 `(and (and (is 0 ,b0)
				    (is 2 ,b2))
			       (next (next (is 3 nil))))
			 `(and (next (next (is 2 ,(or (not b0) (not b2)))))
			       (next (next (is 3 nil))))
			 )
		(ste-thm *nand-delay*
			 `(and (and (is 1 ,b1)
				    (next (is 0 ,b3)))
			       (next (next (is 3 nil))))
			 `(and (next (next (is 1 ,(not (and b1 b3)))))
			       (next (next (is 3 nil))))
			 )
		)
		
	   (ste-thm *nand-delay*
		    `(and (and (and (is 0 ,b0)
				    (is 2 ,b2))
			       (next (next (is 3 nil))))
			  (and (and (is 1 ,b1)
				    (next (is 0 ,b3)))
			       (next (next (is 3 nil))))
			  )
		    `(and (and (next (next (is 2 ,(or (not b0) (not b2)))))
			       (next (next (is 3 nil))))
			  (and (next (next (is 1 ,(not (and b1 b3)))))
			       (next (next (is 3 nil))))
			  )
		    ))
  :rule-classes nil
  :hints (("Goal"
	   :in-theory `((:EXECUTABLE-COUNTERPART C-P)
			(:EXECUTABLE-COUNTERPART LEN)
			(:DEFINITION IMPLIES)
			(:DEFINITION L-DEPTH)
			(:EXECUTABLE-COUNTERPART L-DEPTH)
			(:EXECUTABLE-COUNTERPART NOT)
			(:EXECUTABLE-COUNTERPART BINARY-+)
			(:DEFINITION L-MAXN)
			(:DEFINITION MAX)
			(:EXECUTABLE-COUNTERPART L-MAXN)
			(:EXECUTABLE-COUNTERPART <)
			(:EXECUTABLE-COUNTERPART INTEGERP)
			(:DEFINITION L-P)
			(:TYPE-PRESCRIPTION L-P-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-P)
			(:EXECUTABLE-COUNTERPART CAR)
			(:EXECUTABLE-COUNTERPART CDR)
			(:EXECUTABLE-COUNTERPART CONSP)
			(:REWRITE CDR-CONS)
			(:EXECUTABLE-COUNTERPART EQUAL)
			(:REWRITE CAR-CONS)
			;(:FAKE-RUNE-FOR-TYPE-SET NIL)
			(:DEFINITION NOT)
			(:COMPOUND-RECOGNIZER BOOLEANP-COMPOUND-RECOGNIZER)
			(:EXECUTABLE-COUNTERPART CONS)
			(:TYPE-PRESCRIPTION STE-THM))
	   :use ((:instance ste-thm-conjoin
			    (ckt *nand-delay*)
			    (a1 `(and (and (is 0 ,b0)
					   (is 2 ,b2))
				      (next (next (is 3 nil)))))
			    (c1 `(and (next (next (is 2 ,(or (not b0) (not b2)))))
				      (next (next (is 3 nil)))))
			    (a2 `(and (and (is 1 ,b1)
					   (next (is 0 ,b3)))
				      (next (next (is 3 nil)))))
			    (c2 `(and (next (next (is 1 ,(not (and b1 b3)))))
				      (next (next (is 3 nil)))))))))
  )

(defthm p1
  (implies (and (booleanp b0)
		(booleanp b1)
		(booleanp b2)
		(booleanp b3)
		(ste-thm *nand-delay*
			 `(and (and (and (is 0 ,b0)
					 (is 2 ,b2))
				    (next (next (is 3 nil))))
			       (and (and (is 1 ,b1)
					 (next (is 0 ,b3)))
				    (next (next (is 3 nil))))
			       )
			 `(and (and (next (next (is 2 ,(or (not b0) (not b2)))))
				    (next (next (is 3 nil))))
			       (and (next (next (is 1 ,(not (and b1 b3)))))
				    (next (next (is 3 nil))))
			       )
			 ))
	   (ste-thm *nand-delay*
		    `(and (and (and (is 0 ,b0)
				    (is 1 ,b1))
			       (and (is 2 ,b2)
				    (next (is 0 ,b3))))
			  (next (next (is 3 nil))))
		    
		    `(and (and (next (next (is 1 ,(not (and b1 b3)))))
			       (next (next (is 2 ,(or (not b0) (not b2))))))
			  (next (next (is 3 nil))))
		    ))
  :rule-classes nil
  :hints (("Goal"
	   :in-theory `((:DEFINITION IMPLIES)
			;(:REWRITE FUNDAMENTAL-THEOREM-OF-STE)
			(:EXECUTABLE-COUNTERPART B-LTE)
			(:COMPOUND-RECOGNIZER BOOLEANP-COMPOUND-RECOGNIZER)
			(:REWRITE DEFTRAJ-CONS-EXPAND)
			(:DEFINITION R-DEFTRAJ)
			(:TYPE-PRESCRIPTION B-P)
			(:DEFINITION S-P)
			(:EXECUTABLE-COUNTERPART NTH)
			(:REWRITE NTH-ADD1)
			(:REWRITE NTH-0-CONS)
			(:DEFINITION LEN)
			(:DEFINITION B-AND)
			(:DEFINITION B-NOT)
			(:REWRITE E-EVAL-IS-B-P)
			(:DEFINITION C-EVAL)
			(:DEFINITION E-EVAL)
			(:DEFINITION N-P)
			(:EXECUTABLE-COUNTERPART E-P)
			(:EXECUTABLE-COUNTERPART CONS)
			(:REWRITE R-LUB-R-LTE-REWRITE-2)
			(:DEFINITION R-LTE)
			(:EXECUTABLE-COUNTERPART R-LTE)
			(:REWRITE L-EVAP-N-IF-L-EVALP-N-MINUS-1)
			(:EXECUTABLE-COUNTERPART R-LUB)
			(:REWRITE HOOYAH-3)
			(:DEFINITION S-LTE)
			(:EXECUTABLE-COUNTERPART S-LTE)
			(:DEFINITION B-LTE)
			(:DEFINITION B-LUB)
			(:DEFINITION S-LUB)
			(:EXECUTABLE-COUNTERPART B-LUB)
			(:EXECUTABLE-COUNTERPART S-LUB)
			(:REWRITE R-P-CONS-1)
			(:REWRITE S-P-CONS)
			(:REWRITE BOOLEANP-IS-B-P)
			(:EXECUTABLE-COUNTERPART B-P)
			(:EXECUTABLE-COUNTERPART S-P)
			(:DEFINITION UPDATE-NTH)
			(:EXECUTABLE-COUNTERPART ZP)
			(:EXECUTABLE-COUNTERPART S-MAKE)
			(:DEFINITION L-DEFSEQ)
			(:REWRITE R-P-CDR)
			(:TYPE-PRESCRIPTION R-P)
			(:TYPE-PRESCRIPTION L-DEFSEQ-IS-R-P)
			(:DEFINITION R-LUB)
			(:REWRITE L-DEFSEQ-CONSP)
			(:EXECUTABLE-COUNTERPART R-P)
			(:REWRITE L-DEFSEQ-IS-R-P)
			(:EXECUTABLE-COUNTERPART L-DEFSEQ)
			(:DEFINITION L-EVALP)
			(:TYPE-PRESCRIPTION L-EVALP-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-EVALP)
			(:DEFINITION L-DEPTH)
			(:EXECUTABLE-COUNTERPART L-DEPTH)
			(:EXECUTABLE-COUNTERPART LEN)
			(:EXECUTABLE-COUNTERPART BINARY-+)
			(:DEFINITION L-MAXN)
			(:DEFINITION MAX)
			(:EXECUTABLE-COUNTERPART L-MAXN)
			(:EXECUTABLE-COUNTERPART C-P)
			(:EXECUTABLE-COUNTERPART <)
			(:EXECUTABLE-COUNTERPART INTEGERP)
			(:DEFINITION L-P)
			(:TYPE-PRESCRIPTION L-P-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-P)
			(:EXECUTABLE-COUNTERPART CAR)
			(:EXECUTABLE-COUNTERPART CDR)
			(:EXECUTABLE-COUNTERPART CONSP)
			(:REWRITE CDR-CONS)
			(:EXECUTABLE-COUNTERPART EQUAL)
			(:REWRITE CAR-CONS)
					;(:FAKE-RUNE-FOR-TYPE-SET NIL)
			(:EXECUTABLE-COUNTERPART NOT)
			(:DEFINITION NOT)
			(:TYPE-PRESCRIPTION STE-THM))
	   :use ((:instance ste-thm-weaken-strengthen
			    (ckt *nand-delay*)
			    (a `(and (and (and (is 0 ,b0)
					       (is 2 ,b2))
					  (next (next (is 3 nil))))
				     (and (and (is 1 ,b1)
					       (next (is 0 ,b3)))
					  (next (next (is 3 nil))))
				     ))
			    (c `(and (and (next (next (is 2 ,(or (not b0) (not b2)))))
					  (next (next (is 3 nil))))
				     (and (next (next (is 1 ,(not (and b1 b3)))))
					  (next (next (is 3 nil))))
				     ))
			    (a1 `(and (and (and (is 0 ,b0)
						(is 1 ,b1))
					   (and (is 2 ,b2)
						(next (is 0 ,b3))))
				      (next (next (is 3 nil)))))
			    (c1 `(and (and (next (next (is 1 ,(not (and b1 b3)))))
					   (next (next (is 2 ,(or (not b0) (not b2))))))
				      (next (next (is 3 nil))))))
		 ))))


(defthm nand-delay-2cycle
  (implies (and (booleanp b0)
		(booleanp b1)
		(booleanp b2)
		(booleanp b3))
	   (ste-thm *nand-delay*
		    `(and (and (and (is 0 ,b0)
				    (is 1 ,b1))
			       (and (is 2 ,b2)
				    (next (is 0 ,b3))))
			  (next (next (is 3 nil))))

		    `(and (and (next (next (is 1 ,(not (and b1 b3)))))
			       (next (next (is 2 ,(or (not b0) (not b2))))))
			  (next (next (is 3 nil))))
		    ))
  :rule-classes nil
  :hints (("Goal"
	   :use ((:instance p1)(:instance p2)(:instance p3)(:instance p4))
	   ))
  )


;;;
;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;

(defthm nand-delay-2cycle-via-simulation
  (implies (and (booleanp b0)
		(booleanp b1)
		(booleanp b2)
		(booleanp b3))
	   (ste-thm *nand-delay*
		    `(and (and (and (is 0 ,b0)
				    (is 1 ,b1))
			       (and (is 2 ,b2)
				    (next (is 0 ,b3))))
			  (next (next (is 3 nil))))

		    `(and (and (next (next (is 1 ,(not (and b1 b3)))))
			       (next (next (is 2 ,(or (not b0) (not b2))))))
			  (next (next (is 3 nil))))
		    ))
  :rule-classes nil
  :hints (("Goal"
	   :in-theory `((:DEFINITION IMPLIES)
			(:REWRITE FUNDAMENTAL-THEOREM-OF-STE)
			(:EXECUTABLE-COUNTERPART B-LTE)
			(:COMPOUND-RECOGNIZER BOOLEANP-COMPOUND-RECOGNIZER)
			(:REWRITE DEFTRAJ-CONS-EXPAND)
			(:DEFINITION R-DEFTRAJ)
			(:TYPE-PRESCRIPTION B-P)
			(:DEFINITION S-P)
			(:EXECUTABLE-COUNTERPART NTH)
			(:REWRITE NTH-ADD1)
			(:REWRITE NTH-0-CONS)
			(:DEFINITION LEN)
			(:DEFINITION B-AND)
			(:DEFINITION B-NOT)
			(:REWRITE E-EVAL-IS-B-P)
			(:DEFINITION C-EVAL)
			(:DEFINITION E-EVAL)
			(:DEFINITION N-P)
			(:EXECUTABLE-COUNTERPART E-P)
			(:EXECUTABLE-COUNTERPART CONS)
			(:REWRITE R-LUB-R-LTE-REWRITE-2)
			(:DEFINITION R-LTE)
			(:EXECUTABLE-COUNTERPART R-LTE)
			(:REWRITE L-EVAP-N-IF-L-EVALP-N-MINUS-1)
			(:EXECUTABLE-COUNTERPART R-LUB)
			(:REWRITE HOOYAH-3)
			(:DEFINITION S-LTE)
			(:EXECUTABLE-COUNTERPART S-LTE)
			(:DEFINITION B-LTE)
			(:DEFINITION B-LUB)
			(:DEFINITION S-LUB)
			(:EXECUTABLE-COUNTERPART B-LUB)
			(:EXECUTABLE-COUNTERPART S-LUB)
			(:REWRITE R-P-CONS-1)
			(:REWRITE S-P-CONS)
			(:REWRITE BOOLEANP-IS-B-P)
			(:EXECUTABLE-COUNTERPART B-P)
			(:EXECUTABLE-COUNTERPART S-P)
			(:DEFINITION UPDATE-NTH)
			(:EXECUTABLE-COUNTERPART ZP)
			(:EXECUTABLE-COUNTERPART S-MAKE)
			(:DEFINITION L-DEFSEQ)
			(:REWRITE R-P-CDR)
			(:TYPE-PRESCRIPTION R-P)
			(:TYPE-PRESCRIPTION L-DEFSEQ-IS-R-P)
			(:DEFINITION R-LUB)
			(:REWRITE L-DEFSEQ-CONSP)
			(:EXECUTABLE-COUNTERPART R-P)
			(:REWRITE L-DEFSEQ-IS-R-P)
			(:EXECUTABLE-COUNTERPART L-DEFSEQ)
			(:DEFINITION L-EVALP)
			(:TYPE-PRESCRIPTION L-EVALP-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-EVALP)
			(:DEFINITION L-DEPTH)
			(:EXECUTABLE-COUNTERPART L-DEPTH)
			(:EXECUTABLE-COUNTERPART LEN)
			(:EXECUTABLE-COUNTERPART BINARY-+)
			(:DEFINITION L-MAXN)
			(:DEFINITION MAX)
			(:EXECUTABLE-COUNTERPART L-MAXN)
			(:EXECUTABLE-COUNTERPART C-P)
			(:EXECUTABLE-COUNTERPART <)
			(:EXECUTABLE-COUNTERPART INTEGERP)
			(:DEFINITION L-P)
			(:TYPE-PRESCRIPTION L-P-IS-BOOLEANP)
			(:EXECUTABLE-COUNTERPART L-P)
			(:EXECUTABLE-COUNTERPART CAR)
			(:EXECUTABLE-COUNTERPART CDR)
			(:EXECUTABLE-COUNTERPART CONSP)
			(:REWRITE CDR-CONS)
			(:EXECUTABLE-COUNTERPART EQUAL)
			(:REWRITE CAR-CONS)
					;(:FAKE-RUNE-FOR-TYPE-SET NIL)
			(:EXECUTABLE-COUNTERPART NOT)
			(:DEFINITION NOT)
			(:TYPE-PRESCRIPTION STE-THM))))
  )

 


			   


;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;