anchor.diff:  		 1))))))
   
   (thm
  -  (implies (and (hyp-fn (list :v0 v0 :dv dv :g1 g1)) (nco-ok (- (1+ n)) g1 v0))
  -	   (equal (/ (* (mu) (1+ (* *alpha* (+ v0 dv))))
  -		     (1+ (* *beta* (+ (* g1 (1- n)) (equ-c v0)))))
  -		  (fdco (1- (m (- n) v0 g1)) v0 dv g1)))
  -  :hints(("Goal" :in-theory (enable equ-c equ-nc fdco m))))
  + (implies (and (hyp-fn (list :v0 v0 :dv dv :g1 g1)) (nco-ok (- (1+ n)) g1 v0))
  +          (equal (/ (* (mu) (1+ (* *alpha* (+ v0 dv))))
  +                    (1+ (* *beta* (+ (* g1 (1- n)) (equ-c v0)))))
  +                 (fdco (1- (m (- n) v0 g1)) v0 dv g1)))
  + :hints(("Goal" :in-theory (enable equ-c equ-nc fdco m))))
   
   (thm
  -  (implies (and (hyp-fn (list :v0 v0 :dv dv :g1 g1)) (nco-ok (- (1+ n)) g1 v0))
  -	   (equal (/ (* (mu) (1+ (* *alpha* (+ v0 dv))))
  -	             (1+ (* *beta* (+ (* g1 (- 1 n)) (equ-c v0)))))
  -		  (fdco (1+ (m n v0 g1)) v0 dv g1)))
  -  :hints(("Goal" :in-theory (enable equ-c equ-nc fdco m))))
  + (implies (and (hyp-fn (list :v0 v0 :dv dv :g1 g1)) (nco-ok (- (1+ n)) g1 v0))
  +          (equal (/ (* (mu) (1+ (* *alpha* (+ v0 dv))))
  +                    (1+ (* *beta* (+ (* g1 (- 1 n)) (equ-c v0)))))
  +                 (fdco (1+ (m n v0 g1)) v0 dv g1)))
  + :hints(("Goal" :in-theory (enable equ-c equ-nc fdco m))))
  +
   
   (encapsulate () ; define delta
     (local (defthm lemma-1
              (implies (and (hyp-fn (list :v0 v0 :dv dv :g1 g1 :Kt Kt)) (integerp n)
  -		  (nco-list-ok (list (1- n) (1- (- n))) g1 v0))
  -	     (and (rationalp (expt (gamma Kt) (* 2 n)))
  -		  (rationalp (expt (gamma Kt) (- (* 2 n) 1)))
  -		  (rationalp (expt (gamma Kt) (1- n)))
  -		  (rationalp (expt (gamma Kt) (- 1 n)))
  -		  (rationalp (fdco (m n v0 g1) v0 dv g1))
  -		  (rationalp (fdco (m (- n 1) v0 g1) v0 dv g1))
  -		  (rationalp (fdco (m (+ n 1) v0 g1) v0 dv g1))
  -		  (rationalp (fdco (m (- 1 n) v0 g1) v0 dv g1))))
  -    :hints(("Goal"
  -      :in-theory (enable equ-c equ-nc gamma m mu)
  -      :use(
  -	(:instance gamma-bounds (Kt Kt))
  -	(:instance rationalp-of-gamma (Kt Kt)))))))
  -
  +                         (nco-list-ok (list (1- n) (1- (- n))) g1 v0))
  +                    (and (rationalp (expt (gamma Kt) (* 2 n)))
  +                         (rationalp (expt (gamma Kt) (- (* 2 n) 1)))
  +                         (rationalp (expt (gamma Kt) (1- n)))
  +                         (rationalp (expt (gamma Kt) (- 1 n)))
  +                         (rationalp (fdco (m n v0 g1) v0 dv g1))
  +                         (rationalp (fdco (m (- n 1) v0 g1) v0 dv g1))
  +                         (rationalp (fdco (m (+ n 1) v0 g1) v0 dv g1))
  +                         (rationalp (fdco (m (- 1 n) v0 g1) v0 dv g1))))
  +           :hints(("Goal"
  +                   :in-theory (enable equ-c equ-nc gamma m mu)
  +                   :use(
  +                        (:instance gamma-bounds (Kt Kt))
  +                        (:instance rationalp-of-gamma (Kt Kt)))))))
  +  
     (local (defthm lemma-2
  -    (implies (rational-listp (list e_2n e_2n-1 e_n-1 e_1-n f0 f+1 f-1 f--1))
  -	     (rationalp (+ (* e_2n (- f-1 f0))
  -			   (* e_2n-1 (- f0 f+1))
  -			   (* e_n-1 (+ (* e_1-n (1- f--1))
  -			   (* e_n-1 (1- f+1)))))))))
  -
  +           (implies (rational-listp (list e_2n e_2n-1 e_n-1 e_1-n f0 f+1 f-1 f--1))
  +                    (rationalp (+ (* e_2n (- f-1 f0))
  +                                  (* e_2n-1 (- f0 f+1))
  +                                  (* e_n-1 (+ (* e_1-n (1- f--1))
  +                                              (* e_n-1 (1- f+1)))))))))
  +  
     (define delta (n v0 dv g1 Kt)
       :guard (and (hyp-fn (list :v0 v0 :dv dv :g1 g1 :Kt Kt)) (integerp n)
  -		(nco-list-ok (list (1- n) (1- (- n))) g1 v0))
  +                (nco-list-ok (list (1- n) (1- (- n))) g1 v0))
       :guard-hints(("Goal" :in-theory (enable equ-c equ-nc m)))
       :returns (d rationalp :hyp :guard
  -      :hints(("Goal"
  -	:in-theory (disable lemma-1 lemma-2)
  -	:use(
  -	  (:instance lemma-1 (g1 g1) (Kt Kt) (v0 v0) (dv dv))
  -	  (:instance lemma-2
  -	    (e_2n   (expt (gamma Kt) (* 2 n)))
  -	    (e_2n-1 (expt (gamma Kt) (- (* 2 n) 1)))
  -	    (e_n-1  (expt (gamma Kt) (- n 1)))
  -	    (e_1-n  (expt (gamma Kt) (- 1 n)))
  -	    (f0     (fdco (m n v0 g1) v0 dv g1))
  -	    (f+1    (fdco (m (- n 1) v0 g1) v0 dv g1))
  -	    (f-1    (fdco (m (+ n 1) v0 g1) v0 dv g1))
  -	    (f--1   (fdco (m (- 1 n) v0 g1) v0 dv g1)))))))
  +                :hints(("Goal"
  +                        :in-theory (disable lemma-1 lemma-2)
  +                        :use(
  +                             (:instance lemma-1 (g1 g1) (Kt Kt) (v0 v0) (dv dv))
  +                             (:instance lemma-2
  +                                        (e_2n   (expt (gamma Kt) (* 2 n)))
  +                                        (e_2n-1 (expt (gamma Kt) (- (* 2 n) 1)))
  +                                        (e_n-1  (expt (gamma Kt) (- n 1)))
  +                                        (e_1-n  (expt (gamma Kt) (- 1 n)))
  +                                        (f0     (fdco (m n v0 g1) v0 dv g1))
  +                                        (f+1    (fdco (m (- n 1) v0 g1) v0 dv g1))
  +                                        (f-1    (fdco (m (+ n 1) v0 g1) v0 dv g1))
  +                                        (f--1   (fdco (m (- 1 n) v0 g1) v0 dv g1)))
  +                             ))))
       (+ (* (expt (gamma Kt) (* 2 n))
  -	  (- (fdco (m (+ n 1) v0 g1) v0 dv g1)
  -	     (fdco (m n v0 g1) v0 dv g1)))
  +          (- (fdco (m (+ n 1) v0 g1) v0 dv g1)
  +             (fdco (m n v0 g1) v0 dv g1)))
          (* (expt (gamma Kt) (- (* 2 n) 1))
  -	  (- (fdco (m n v0 g1) v0 dv g1)
  -	     (fdco (m (- n 1) v0 g1) v0 dv g1)))
  +          (- (fdco (m n v0 g1) v0 dv g1)
  +             (fdco (m (- n 1) v0 g1) v0 dv g1)))
          (* (expt (gamma Kt) (1- n))
  -	  (+ (* (expt (gamma Kt) (1+ (- n)))
  -		(1- (fdco (m (- 1 n) v0 g1) v0 dv g1)))
  -	     (* (expt (gamma Kt) (1- n))
  +          (+ (* (expt (gamma Kt) (1+ (- n)))
  +                (1- (fdco (m (- 1 n) v0 g1) v0 dv g1)))
  +             (* (expt (gamma Kt) (1- n))
   		(1- (fdco (m (- n 1) v0 g1) v0 dv g1))))))))
   
   (thm
  -  (implies (and (hyp-fn (list :v0 v0 :dv dv :g1 g1))
  -		(nco-list-ok (list (1- n) (1- (- n))) g1 v0))
  -	   (equal (delta-orig n v0 dv g1 Kt)
  -		  (delta n v0 dv g1 Kt)))
  -  :hints(("Goal" :in-theory (enable delta equ-c equ-nc fdco m))))
  + (implies (and (hyp-fn (list :v0 v0 :dv dv :g1 g1))
  +               (nco-list-ok (list (1- n) (1- (- n))) g1 v0))
  +          (equal (delta-orig n v0 dv g1 Kt)
  +                 (delta n v0 dv g1 Kt)))
  + :hints(("Goal" :in-theory (enable delta equ-c equ-nc fdco m))))
   
   (defthm delta-f-diff-rewrite
     (implies (and (integerp n) (<= 3 n) (< n (/ (* 2 *beta* g1))) (rationalp g1)
  
positive.code:            :clause-processor
             (smtlink-custom-config clause (smt-std-hint "delta_f_diff_rewrite") ))))
  
  (defthm stuck-here nil)
  
  (defthm delta-f-diff-bound
    (implies (and (integerp n) (<= 3 n) (< n (/ (* 2 *beta* g1))) (rationalp g1)
                  (hyp-fn (list :v0 v0 :dv dv :g1 g1 :Kt Kt)))
  	   (and (< 0
  		   (* *beta* g1 (+ 1 (* *alpha* (+ v0 dv)))
  
negative.code: 		      (/ (+ 1 (* *alpha* v0) (* *beta* g1 (-  1 N))))
  		      (/ (+ 1 (* *alpha* v0) (* *beta* g1 (-  0 N)))))
  	           (* 4 *beta* g1))))
    :hints(("Subgoal 4"
            :clause-processor
            (smtlink-custom-config clause (smt-std-hint "delta_f_diff_found_4") ))
           ("Subgoal 3"
            :clause-processor
            (smtlink-custom-config clause (smt-std-hint "delta_f_diff_found_3") )
            )
           ("Subgoal 2"
            :clause-processor
            (smtlink-custom-config clause (smt-std-hint "delta_f_diff_found_2")))
           ("Subgoal 1"
            :clause-processor
            (smtlink-custom-config clause (smt-std-hint "delta_f_diff_found_1")))
           ))
  
  (defthm delta-f-rewrite
    (implies (and (integerp nco) (< (/ (* -2 *beta* g1)) nco) (< nco (/ (* 2 *beta* g1)))
                  (rationalp g1)
                  (hyp-fn (list :v0 v0 :dv dv :g1 g1 :Kt Kt)))
  	   (equal (1- (fdco (m nco v0 g1) v0 dv g1))
  	          (/ (+ (* *alpha* dv) (* *beta* g1 nco))
  		     (1+ (* *beta* g1 (m nco v0 g1))))))
    :hints(("Goal'''"
            :in-theory (enable delta equ-c equ-nc fdco gamma m mu)
            :clause-processor
            (smtlink-custom-config clause (smt-std-hint "delta_f_rewrite") )
            )))
  
  (defthm stop-here nil)
  
  