Nuprl Definition : simple-swap-specification

simple-swap-specification(AType;n;prog;i;j) ==
  ∀k:ℕn. ∀A:Arr(AType).  (↑(A-eval(array-model(AType)) simple-swap-test2(array-model(AType);prog;i;j;k) A))



Definitions occuring in Statement :  simple-swap-test2: simple-swap-test2(AModel;prog;i;j;k) array-model: array-model(AType) Arr: Arr(AType) A-eval: A-eval(AModel) int_seg: {i..j-} assert: b all: x:A. B[x] apply: a natural_number: $n
Definitions occuring in definition :  int_seg: {i..j-} natural_number: $n all: x:A. B[x] Arr: Arr(AType) assert: b apply: a A-eval: A-eval(AModel) simple-swap-test2: simple-swap-test2(AModel;prog;i;j;k) array-model: array-model(AType)
FDL editor aliases :  simple-swap-specification

Latex:
simple-swap-specification(AType;n;prog;i;j)  ==
    \mforall{}k:\mBbbN{}n.  \mforall{}A:Arr(AType).
        (\muparrow{}(A-eval(array-model(AType))  simple-swap-test2(array-model(AType);prog;i;j;k)  A))



Date html generated: 2016_05_15-PM-02_20_06
Last ObjectModification: 2015_09_23-AM-07_38_42

Theory : monads


Home Index