Module div_goals2

Require Export lemmas.
Require Export tacdef.

Theorem div_goal2 :
  
  (np : nat)
  (sp : nat)
  (nn : nat)
  (c : Z)
  (h : nat)
  (l : nat)
  (m : (array bound modZ))
  (q : Z)
  (rb : bool)
  (rz : Z)
  (Pre_1 : (lt (1) nn)
          /\l=(div2' nn)
            /\h=(minus nn (div2' nn))
              /\(`q = 0`\/`q = 1`)
                /\`np+2*nn <= bound`
                  /\`sp+nn <= bound`
                    /\(`np+2*nn <= sp`\/`sp+nn <= np`)
                      /\(`q = 1`
                         ->`(I m (plus np (mult (S (S O)) l)) h)
                           < (I m (plus sp l) h)`)
                        /\`(pow beta h) <= 2*(I m (plus sp l) h)`)
  (resultb : bool)
  (Test_2 : `q <> 0`)
  (rb0 : bool)
  (m0 : (array bound modZ))
  (result : unit)
  (Post_3 : `(I m0 (plus np (mult (S (S O)) l)) h)
           = (Zmultbool rb0 (pow beta h))+
           (I m (plus np (mult (S (S O)) l)) h)-
           (I m (plus sp l) h)`
           /\((p:nat)
               `0 <= p < bound`
               ->(lt p (plus np (mult (2) l)))
                 \/(le (plus (plus np (mult (2) l)) h) p)
               ->(access m0 p)=(access m p)))
   `(I m (plus np (mult (S (S O)) l)) h)+q*(pow beta h)-q*
   (I m (plus sp l) h) = (I m0 (plus np (mult (S (S O)) l)) h)`
   /\((p:nat)
       `0 <= p < bound`
       ->~((le (plus np (mult (2) l)) p)
           /\(lt p (plus np (plus (mult (2) l) h))))
       ->(access m0 p)=(access m p))
.


Index
This page has been generated by coqdoc