Nuprl Lemma : encryption-key-atoms_wf
∀[k:Key]. (encryption-key-atoms(k) ∈ Atom1 List)
Proof
Definitions occuring in Statement :
encryption-key-atoms: encryption-key-atoms(k),
encryption-key: Key,
list: T List,
atom: Atom$n,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
encryption-key-atoms: encryption-key-atoms(k),
encryption-key: Key
Latex:
\mforall{}[k:Key]. (encryption-key-atoms(k) \mmember{} Atom1 List)
Date html generated:
2016_05_17-AM-11_40_41
Last ObjectModification:
2015_12_29-PM-06_45_02
Theory : event-logic-applications
Home
Index