Module div_goals13

Require Export lemmas.
Require Export tacdef.

Theorem div_goal13 :
  
  (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)`)
  (rb0 : bool)
  (m0 : (array bound modZ))
  (result : unit)
  (Post_2 : `(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)))
  (rb1 : bool)
  (m1 : (array bound modZ))
  (result0 : unit)
  (Post_3 : `(I m0 (plus np l) nn)
            = ((Zmultbool rb1 (pow beta (minus nn h)))+
            (I m1 sp (minus nn h)))*(I m0 (plus sp l) h)+
            (I m1 (plus np l) h)`
            /\`(I m1 (plus np l) h) < (I m0 (plus sp l) h)`
              /\((p:nat)
                  `0 <= p < bound`
                  ->((lt p sp)\/(le (plus sp (minus nn h)) p))
                    /\((lt p (plus np l))\/(le (plus (plus np l) h) p))
                  ->(access m1 p)=(access m0 p)))
  (rz0 : Z)
  (result1 : unit)
  (Post_4 : `rz0 = (modZtoZ (isEvenOrOdd m1 sp))`)
  (m2 : (array bound modZ))
  (result2 : unit)
  (Post_5 : `(I m1 sp l) = 2*(I m2 sp l)+(modZtoZ (isEvenOrOdd m1 sp))`
            /\((p:nat)
                `0 <= p < bound`
                ->(lt p sp)\/(le (plus sp l) p)
                ->(access m2 p)=(access m1 p)))
   `0 <= (plus sp (pred l)) < bound`
.


Index
This page has been generated by coqdoc