Nuprl Definition : A-shift-upto-spec

A-shift-upto-spec(AType; Val; n; prog; j) ==
  ∀A:Arr(AType). ∀i:ℕn.
    if i <z j - 1
    then A-post-val(AType;prog;A;i) = A-pre-val(AType;A;i + 1) ∈ Val
    else A-post-val(AType;prog;A;i) = A-pre-val(AType;A;i) ∈ Val
    fi 


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-},  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  all: ∀x:A. B[x],  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-},  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  subtract: n - m,  add: n + m,  natural_number: $n,  equal: s = t ∈ T,  A-post-val: A-post-val(AType;prog;A;i),  A-pre-val: A-pre-val(AType;A;i)
Latex:
A-shift-upto-spec(AType;  Val;  n;  prog;  j)  ==
    \mforall{}A:Arr(AType).  \mforall{}i:\mBbbN{}n.
        if  i  <z  j  -  1
        then  A-post-val(AType;prog;A;i)  =  A-pre-val(AType;A;i  +  1)
        else  A-post-val(AType;prog;A;i)  =  A-pre-val(AType;A;i)
        fi 


Date html generated: 2016_05_15-PM-02_21_11
Last ObjectModification: 2015_09_23-AM-07_38_53

Theory : monads


Home Index