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: b q band: p ∧b q bnot: ¬bb eq_int: (i =z j) apply: 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: a A-return: A-return(AModel) bimplies: 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