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: f 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: f 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