Nuprl Definition : CR-initiator2

CR-initiator2{i:l}(s) ==  A ⟶ B: ["new"(m); "send"(data(m))] @ ["rcv"(<data(n), data(s)>)]


Definitions occuring in Statement :  basic-seq-1-3: A ⟶ B: pas[A; B; m; n; x],  mk-pa: n(v),  sdata-pair: <d1, d2>,  atom-sdata: data(a),  append: as @ bs,  cons: [a / b],  nil: [],  token: "$token"
FDL editor aliases :  CR-initiator2
Latex:
CR-initiator2\{i:l\}(s)  ==    A  {}\mrightarrow{}  B:  ["new"(m);  "send"(data(m))]  @  ["rcv"(<data(n),  data(s)>)]


Date html generated: 2016_05_17-PM-00_47_23
Last ObjectModification: 2012_08_30-PM-05_45_30

Theory : event-logic-applications


Home Index