Nuprl Definition : pa-used

pa-used(pa) ==
  let n,v = pa
  in if n =a "send" then sdata-atoms(v)
     if n =a "encrypt" then sdata-atoms(fst(v)) @ encryption-key-atoms(fst(snd(v)))
     if n =a "sign" then sdata-atoms(fst(v))
     if n =a "verify" then [snd(snd(v)) / sdata-atoms(fst(v))]
     if n =a "decrypt" then [snd(snd(v)) / encryption-key-atoms(fst(snd(v)))]
     else []
     fi

Definitions occuring in Statement : encryption-key-atoms: encryption-key-atoms(k), sdata-atoms: sdata-atoms(d), append: as @ bs, cons: [a / b], nil: [], ifthenelse: if b then t else f fi , eq_atom: x =a y, pi1: fst(t), pi2: snd(t), spread: spread def, token: "$token"
FDL editor aliases : pa-used

Latex:
pa-used(pa) == let n,v = pa in if n =a "send" then sdata-atoms(v) if n =a "encrypt" then sdata-atoms(fst(v)) @ encryption-key-atoms(fst(snd(v))) if n =a "sign" then sdata-atoms(fst(v)) if n =a "verify" then [snd(snd(v)) / sdata-atoms(fst(v))] if n =a "decrypt" then [snd(snd(v)) / encryption-key-atoms(fst(snd(v)))] else [] fi Date html generated: 2016_05_17-PM-00_37_34 Last ObjectModification: 2012_08_30-PM-04_30_02 Theory : event-logic-applications Home Index