Nuprl Definition : ses-used-atoms

UsedAtoms(e) ==
  if e ∈_b Send then sdata-atoms(Send(e))
  if e ∈_b Sign then sdata-atoms(signed(e))
  if e ∈_b Verify then [signature(e) / sdata-atoms(signed(e))]
  if e ∈_b Encrypt then sdata-atoms(plainText(e)) @ encryption-key-atoms(key(e))
  if e ∈_b Decrypt then [cipherText(e) / encryption-key-atoms(key(e))]
  else []
  fi

Definitions occuring in Statement : ses-cipher: cipherText(e), ses-decryption-key: key(e), ses-decrypt: Decrypt, ses-encryption-key: key(e), ses-encrypted: plainText(e), ses-encrypt: Encrypt, ses-verify-sig: signature(e), ses-verify-signed: signed(e), ses-verify: Verify, ses-signed: signed(e), ses-sign: Sign, ses-send: Send, encryption-key-atoms: encryption-key-atoms(k), sdata-atoms: sdata-atoms(d), eclass-val: X(e), in-eclass: e ∈_b X, append: as @ bs, cons: [a / b], nil: [], ifthenelse: if b then t else f fi
FDL editor aliases : ses-used-atoms

Latex:
UsedAtoms(e) == if e \mmember{}\msubb{} Send then sdata-atoms(Send(e)) if e \mmember{}\msubb{} Sign then sdata-atoms(signed(e)) if e \mmember{}\msubb{} Verify then [signature(e) / sdata-atoms(signed(e))] if e \mmember{}\msubb{} Encrypt then sdata-atoms(plainText(e)) @ encryption-key-atoms(key(e)) if e \mmember{}\msubb{} Decrypt then [cipherText(e) / encryption-key-atoms(key(e))] else [] fi Date html generated: 2016_05_17-PM-00_31_11 Last ObjectModification: 2012_08_30-PM-04_28_12 Theory : event-logic-applications Home Index