Nuprl Lemma : encryption-key-atoms

{

[k:Key]. (encryption-key-atoms(k)

Atom1 List) }

{ Proof }

Definitions occuring in Statement : encryption-key-atoms: encryption-key-atoms(k), encryption-key: Key, uall:

[x:A]. B[x], member: t

T, list: type List, atom: Atom$n
Definitions : uall:

[x:A]. B[x], encryption-key: Key, member: t

T, encryption-key-atoms: encryption-key-atoms(k)
Lemmas : encryption-key_wf

\mforall{}[k:Key]. (encryption-key-atoms(k) \mmember{} Atom1 List) Date html generated: 2011_08_17-PM-07_11_20 Last ObjectModification: 2011_06_18-PM-12_55_44 Home Index