anchor.diff:  (include-book "ihs/ihs-init" :dir :system) ; for disable-theory and enable-theory
   
   (deftheory before-arith (current-theory :here))
  -(include-book "arithmetic/top-with-meta" :dir :system)
  +(include-book "arithmetic-5/top" :dir :system)
   (deftheory after-arith (current-theory :here))
   (deftheory arithmetic-book-only (set-difference-theories (theory 'after-arith) (theory 'before-arith)))
   
   ;; for the clause processor to work
  -(include-book "../../top" :ttags :all)
  +(include-book "../smtlink/SMT-connect" :ttags :all)
   (logic)
   :set-state-ok t
   :set-ignore-ok t
  
positive.code: ;; Copyright (C) 2015, University of British Columbia
  ;; Written (originally) by Mark Greenstreet (13th March, 2014)
  ;; Adapted from DPLL_proof.lisp and global.lisp
  ;;
  ;; License: A 3-clause BSD license.
  ;; See the LICENSE file distributed with this software
  
  (in-package "ACL2")
  (include-book "std/util/define" :dir :system)
  (include-book "misc/eval" :dir :system) ; Define must-succeed and must-fail macros.
  
negative.code:   (if (endp h-list) t
        (and (h-ok (car h-list) g1 v0) (h-list-ok (cdr h-list) g1 v0))))
  
  
  (encapsulate ()
    (local (defthm lemma-1  ; needed for guard conjecture
      (implies (and (rationalp Kt) (< *Kt-min* Kt) (< Kt *Kt-max*))
               (and (rationalp (gamma Kt)) (< 0 (gamma Kt))))))
  
    (define B-term-expt (Kt h)
      :guard (and (integerp h) (hyp-fn (list :Kt Kt)))
      :returns (x rationalp :hyp :guard)
      (expt (gamma Kt) (- h))))
  
  (encapsulate ()
    (local (in-theory (enable equ-c mu))) ; needed to discharge guard conjecture for B-term-rest
    (define B-term-rest (h v0 dv g1)
      :guard (and (integerp h) (hyp-fn (list :v0 v0 :dv dv :g1 g1)) (h-ok h g1 v0))
      :returns (x rationalp :hyp :guard)
      (- (* (mu) (/ (+ 1 (* *alpha* (+ v0 dv))) (+ 1 (* *beta* (+ (* h g1) (equ-c v0)))))) 1)))
  
  (encapsulate ()
    ; here is an exercise in guiding ACL2 step-by-step to get a proof.
    ; The proofs for B-term worked fine when I had mistakenly included arithmetic/top-with-meta
    ; instead of arithmetic-5/top.  When I changed what book to include, I needed to add the
    ; two lemmas here to get the proof of rationalp-of-B-term to go through.
    (local (defthm lemma-1
      (implies (and (integerp h) (hyp-fn (list :v0 v0 :dv dv :g1 g1 :Kt Kt)) (h-ok h g1 v0))
  	     (and (rationalp (B-term-expt Kt h)) (rationalp (B-term-rest h v0 dv g1))))))
  
    (local (defthm lemma-2
      (implies (and (integerp h) (hyp-fn (list :v0 v0 :dv dv :g1 g1 :Kt Kt)) (h-ok h g1 v0))
  		  (rationalp (* (B-term-expt Kt h) (B-term-rest h v0 dv g1))))
      :hints(("Goal"
        :in-theory (disable lemma-1)
        :use((:instance lemma-1 (v0 v0) (g1 g1) (dv dv) (Kt Kt)))))))
    
    (define B-term (h v0 dv g1 Kt)
      :guard (and (integerp h) (hyp-fn (list :v0 v0 :dv dv :g1 g1 :Kt Kt)) (h-ok h g1 v0))
      :returns (x rationalp :hyp :guard)
      (* (B-term-expt Kt h) (B-term-rest h v0 dv g1))))
  
  
  (encapsulate()
    (local (defthm lemma-1 ; needed for rationalp-of-B-sum
      (implies (and (integerp h_lo) (integerp h_hi) (<= 0 h_lo) (<= h_lo (1+ h_hi))
  		(hyp-fn (list :v0 v0 :dv dv :g1 g1 :Kt Kt))
  		(h-list-ok (list h_lo (- h_hi)) g1 v0)
  		(>= h_hi h_lo))
  	      (rationalp (B-term h_hi v0 dv g1 Kt)))))
  
    (define B_sum (h_lo h_hi v0 dv g1 Kt)
      :guard (and (integerp h_lo) (integerp h_hi) (<= 0 h_lo) (<= h_lo (1+ h_hi))
  