Nuprl Definition : ses-useable-atoms

UseableAtoms(e) ==
  if e ∈b Rcv then sdata-atoms(Rcv(e))
  if e ∈b Sign then [signature(e)]
  if e ∈b Encrypt then [cipherText(e)]
  if e ∈b Decrypt then sdata-atoms(plainText(e))
  if e ∈b New then [New(e)]
  else []
  fi 


Definitions occuring in Statement :  ses-decrypted: plainText(e),  ses-decrypt: Decrypt,  ses-crypt: cipherText(e),  ses-encrypt: Encrypt,  ses-sig: signature(e),  ses-sign: Sign,  ses-rcv: Rcv,  ses-new: New,  sdata-atoms: sdata-atoms(d),  eclass-val: X(e),  in-eclass: e ∈b X,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi 
FDL editor aliases :  ses-useable-atoms
Latex:
UseableAtoms(e)  ==
    if  e  \mmember{}\msubb{}  Rcv  then  sdata-atoms(Rcv(e))
    if  e  \mmember{}\msubb{}  Sign  then  [signature(e)]
    if  e  \mmember{}\msubb{}  Encrypt  then  [cipherText(e)]
    if  e  \mmember{}\msubb{}  Decrypt  then  sdata-atoms(plainText(e))
    if  e  \mmember{}\msubb{}  New  then  [New(e)]
    else  []
    fi 


Date html generated: 2016_05_17-PM-00_31_22
Last ObjectModification: 2012_08_30-PM-04_28_20

Theory : event-logic-applications


Home Index