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
Lemmas :
nil_wf,
cons_wf,
encryption-key_wf
Latex:
\mforall{}[k:Key]. (encryption-key-atoms(k) \mmember{} Atom1 List)
Date html generated:
2015_07_23-PM-00_01_53
Last ObjectModification:
2015_01_29-AM-07_44_33
Home
Index