Nuprl Definition : A-shift-spec

A-shift-spec(AType; Val; n; prog) ==
  ∀A:Arr(AType). ∀i:ℕn.
    ((i < n - 2 ⇒ (A-post-val(AType;prog;A;i) = A-pre-val(AType;A;i + 1) ∈ Val))
    ∧ (A-post-val(AType;prog;A;n - 1) = A-pre-val(AType;A;0) ∈ Val))


Definitions occuring in Statement :  A-post-val: A-post-val(AType;prog;A;i),  Arr: Arr(AType),  A-pre-val: A-pre-val(AType;A;i),  int_seg: {i..j-},  less_than: a < b,  all: ∀x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  subtract: n - m,  add: n + m,  natural_number: $n,  equal: s = t ∈ T
Definitions occuring in definition :  Arr: Arr(AType),  all: ∀x:A. B[x],  int_seg: {i..j-},  and: P ∧ Q,  implies: P ⇒ Q,  less_than: a < b,  add: n + m,  equal: s = t ∈ T,  A-post-val: A-post-val(AType;prog;A;i),  subtract: n - m,  A-pre-val: A-pre-val(AType;A;i),  natural_number: $n
Latex:
A-shift-spec(AType;  Val;  n;  prog)  ==
    \mforall{}A:Arr(AType).  \mforall{}i:\mBbbN{}n.
        ((i  <  n  -  2  {}\mRightarrow{}  (A-post-val(AType;prog;A;i)  =  A-pre-val(AType;A;i  +  1)))
        \mwedge{}  (A-post-val(AType;prog;A;n  -  1)  =  A-pre-val(AType;A;0)))


Date html generated: 2016_05_15-PM-02_21_06
Last ObjectModification: 2015_09_23-AM-07_38_52

Theory : monads


Home Index