Module memory

Require Export Gomega.

Theorem others_are_unchanged :
  (A:Set)(np, sp, nn,l,h:nat)(m3,m2,m1,m0,m:(array bound A))
(lt (1) nn)->(`np+2*nn <= sp`\/`sp+nn <= np`) ->
(l=(div2' nn))->(h=(minus nn (div2' nn)))->
((p:nat)`0 <= p < bound`/\`p <> (plus sp (pred l))`
               ->(access m3 p)=(access m2 p)) ->
((p:nat)`0 <= p < bound`
               ->(lt p sp)\/(le (plus sp l) p)
               ->(access m2 p)=(access m1 p)) ->
((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)) ->
((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)) ->
(p:nat)`0 <= p < bound`->~((le sp p)/\(lt p (plus sp l))
         \/(le (plus np l) p)
           /\(lt p (plus np (plus (plus l l) h))))->(access m3 p)=(access m p).

Lemma m2_m :
  (A:Set)(np, sp, nn:nat)(m,m0,m1,m2:(array bound A))
 (H3:(p:nat)
  `0 <= p < bound`
  ->(lt p np)\/(le (plus np nn) p)
  ->(access m0 p)=(access m p))
 (H2:(p:nat)
  `0 <= p < bound`
  ->(lt p np)\/(le (plus np nn) p)
  ->(access m1 p)=(access m0 p))
 (H1 : (p:nat)
  `0 <= p < bound`
  ->(lt p sp)\/(le (plus sp nn) p)
  ->(access m2 p)=(access m1 p))

   (p:nat)
    `0 <= p < bound`
    ->~((le sp p)/\(lt p (plus sp nn))
        \/(le np p)/\(lt p (plus np (mult (2) nn))))
    ->(access m2 p)=(access m p).

Lemma m1_m :
 (A:Set)(np, nn,l:nat)(m,m0,m1:(array bound A))(lt (1) nn)->
          l=(div2' nn) ->(mult (2) l)=nn->
(H1:(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))
(H0 : (p:nat)
        `0 <= p < bound`
        ->(lt p np)\/(le (plus np (mult (2) l)) p)
        ->(access m1 p)=(access m0 p))

   (p:nat)
    `0 <= p < bound`
    ->~((le np p)/\(lt p (plus np (mult (2) nn))))
    ->(access m1 p)=(access m p).

Lemma m2_m' :
 (A:Set)(np, nn,l:nat)(m,m0,m1,m2:(array bound A))(lt (1) nn)->
(Hnn:(plus (mult (2) l) (1))=nn)
(H0 : (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))
(H2 : (p:nat)
        `0 <= p < bound`
        ->(lt p np)\/(le (plus np (mult (2) l)) p)
        ->(access m1 p)=(access m0 p))
(H4 : (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))
  (p:nat)
    `0 <= p < bound`
    ->~((le np p)/\(lt p (plus np (mult (2) nn))))
    ->(access m2 p)=(access m p).

Theorem length_n_decompose :
  (pos, n:nat)(m:(array bound modZ))
   `(I m (plus pos (div2' n)) (minus n (div2' n)))*(pow beta (div2' n))+
        (I m pos (div2' n)) = (I m pos n)`.