# Module sub_goals2

``` Require Export lemmas. Require Export memory. Theorem sub_goal5 :      (np : nat)   (sp : nat)   (nn : nat)   (b : Z)   (c : Z)   (h : nat)   (l : nat)   (m : (array bound modZ))   (q : Z)   (rb : bool)   (Pre_1 : (lt (1) nn)           /\l=(div2' nn)             /\h=(minus nn (div2' nn))               /\`np+2*nn <= bound`                 /\`sp+nn <= bound`                   /\(`np+2*nn <= sp`\/`sp+nn <= np`)                     /\`q*(pow beta l)+(I m sp l) <= (pow beta l)`                       /\`0 <= q <= 1`)   (m0 : (array bound modZ))   (result : unit)   (Post_3 : `(Zsquare (I m sp l))             = (I m0 (plus np nn) (mult (S (S O)) l))`             /\((p:nat)                 `0 <= p < bound`                 ->(lt p (plus np nn))                   \/(le (plus (plus np nn) (mult (2) l)) p)                 ->(access m0 p)=(access m p)))   (rb0 : bool)   (m1 : (array bound modZ))   (result0 : unit)   (Post_4 : `(I m1 np (mult (S (S O)) l))            = (Zmultbool rb0 (pow beta (mult (S (S O)) l)))+            (I m0 np (mult (S (S O)) l))-            (I m0 (plus np nn) (mult (S (S O)) l))`            /\((p:nat)                `0 <= p < bound`                ->(lt p np)\/(le (plus np (mult (2) l)) p)                ->(access m1 p)=(access m0 p)))   (resultb : bool)   (Test_2 : ~l=h)   (rb1 : bool)   (m2 : (array bound modZ))   (result1 : unit)   (Post_5 : `(I m2 (plus np (mult (S (S O)) l)) (S O))            = (Zmultbool rb1 (pow beta (S O)))+            (I m1 (plus np (mult (S (S O)) l)) (S O))-(q+(bool2Z rb0))`            /\((p:nat)                `0 <= p < bound`                ->(lt p (plus np (mult (2) l)))                  \/(le (plus (plus np (mult (2) l)) (1)) p)                ->(access m2 p)=(access m1 p)))    `(I m2 np nn) = (c-(c-(bool2Z rb1)))*(pow beta nn)+(I m np nn)-(q*    (pow beta l)+(I m sp l))*(q*(pow beta l)+(I m sp l))`    /\((p:nat)        `0 <= p < bound`        ->~((le np p)/\(lt p (plus np (mult (2) nn))))        ->(access m2 p)=(access m p)) . ```

``` ```

Index