---

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

---

Definitions :  basic-seq-1-3: A  B: pas[A; B; m; n; x],  id-sdata: data(x),  pair: <a, b>,  cons: [car / cdr],  mk-pa: n(v),  token: "$token",  sdata-pair: <d1, d2>,  atom-sdata: data(a),  nil: []
FDL editor aliases :  CR-responder1

---

CR-responder1\{i:l\}(s)  ==
    B  {}\mrightarrow{}  A:  ["rcv"(data(m)); 
                     
                      "new"(n);  "sign"(<<data(n),  <data(A),  data(m)>>,  B,  s>);  "send"(<data(n),  data(s)>)]


Date html generated: 2010_08_28-AM-11_47_24
Last ObjectModification: 2010_03_15-PM-09_18_14

Home Index