Nuprl Definition : pa-useable

pa-useable(pa) ==
  let n,v = pa
  in if n =a "new" then [v]
     if n =a "rcv" then sdata-atoms(v)
     if n =a "encrypt" then [snd(snd(v))]
     if n =a "decrypt" then sdata-atoms(fst(v))
     if n =a "sign" then [snd(snd(v))]
     else []
     fi

Definitions occuring in Statement : sdata-atoms: sdata-atoms(d), 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-useable

Latex:
pa-useable(pa) == let n,v = pa in if n =a "new" then [v] if n =a "rcv" then sdata-atoms(v) if n =a "encrypt" then [snd(snd(v))] if n =a "decrypt" then sdata-atoms(fst(v)) if n =a "sign" then [snd(snd(v))] else [] fi Date html generated: 2015_07_23-PM-00_14_01 Last ObjectModification: 2012_08_30-PM-04_30_10 Home Index