---

{ [T:Id  Type]. [tab:secret-table(T)]. [kx: + Atom1  Atom1].
    (decrypt(tab;kx)  data(T)?) }

{ Proof }

---

Definitions occuring in Statement :  st-decrypt: decrypt(tab;kval),  secret-table: secret-table(T),  data: data(T),  Id: Id,  nat: ,  uall: [x:A]. B[x],  unit: Unit,  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  union: left + right,  universe: Type,  atom: Atom$n
Definitions :  uall: [x:A]. B[x],  member: t  T,  st-decrypt: decrypt(tab;kval),  prop: ,  bfalse: ff,  ifthenelse: if b then t else f fi ,  all: x:A. B[x],  implies: P  Q,  btrue: tt,  uimplies: b supposing a,  unit: Unit,  bool: ,  iff: P  Q,  and: P  Q,  it:
Lemmas :  nat_wf,  secret-table_wf,  Id_wf,  isl_wf,  data_wf,  unit_wf,  st-lookup_wf,  bool_wf,  assert_wf,  outl_wf,  ifthenelse_wf,  st-key-match_wf,  it_wf,  not_wf,  bnot_wf,  iff_weakening_uiff,  eqtt_to_assert,  uiff_transitivity,  eqff_to_assert,  assert_of_bnot

---

\mforall{}[T:Id  {}\mrightarrow{}  Type].  \mforall{}[tab:secret-table(T)].  \mforall{}[kx:\mBbbN{}  +  Atom1  \mtimes{}  Atom1].    (decrypt(tab;kx)  \mmember{}  data(T)?)


Date html generated: 2011_08_16-AM-11_00_32
Last ObjectModification: 2011_06_18-AM-09_34_07

Home Index