Nuprl Definition : simple-swap-test2
simple-swap-test2(AModel;prog;i;j;k) ==
A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(λin@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(λin@j.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) k))
(λin@k.(A-bind(AModel) prog
(λx.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(λout@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(λout@j.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) k))
(λout@k.(A-return(AModel)
(((out@i =z in@j) ∧b (out@j =z in@i))
∧b ((¬b(k =z i))
∧b (¬b(k =z j)) ⇒b (out@k =z in@k)))))))))))))))))
Definitions occuring in Statement :
A-coerce: A-coerce(AModel),
A-fetch': A-fetch'(AModel),
A-bind: A-bind(AModel),
A-return: A-return(AModel),
bimplies: p ⇒b q,
band: p ∧b q,
bnot: ¬bb,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
A-bind: A-bind(AModel),
A-coerce: A-coerce(AModel),
A-fetch': A-fetch'(AModel),
lambda: λx.A[x],
apply: f a,
A-return: A-return(AModel),
bimplies: p ⇒b q,
band: p ∧b q,
bnot: ¬bb,
eq_int: (i =z j)
FDL editor aliases :
simple-swap-test2
Latex:
simple-swap-test2(AModel;prog;i;j;k) ==
A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(\mlambda{}in@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(\mlambda{}in@j.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) k))
(\mlambda{}in@k.(A-bind(AModel) prog
(\mlambda{}x.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(\mlambda{}out@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(\mlambda{}out@j....)))))))))))
Date html generated:
2016_05_15-PM-02_19_49
Last ObjectModification:
2015_09_23-AM-07_38_41
Theory : monads
Home
Index