Nuprl Lemma : ses-act-has-atom

s:SES
  (ActionsDisjoint  (es:EO+(Info). e:Act. a:Atom1.  ((e has a)  (a  UseableAtoms(e))  (a  UsedAtoms(e)))))


Proof not projected



Definitions occuring in Statement :  ses-useable-atoms: UseableAtoms(e),  ses-used-atoms: UsedAtoms(e),  ses-disjoint: ActionsDisjoint,  event-has: (e has a),  ses-act: Act,  ses-info: Info,  security-event-structure: SES,  event-ordering+: EO+(Info),  all: x:A. B[x],  iff: P  Q,  implies: P  Q,  or: P  Q,  l_member: (x  l),  atom: Atom$n
Definitions :  bfalse: ff,  false: False,  btrue: tt,  so_lambda: x y.t[x; y],  top: Top,  true: True,  squash: T,  member: t  T,  not: A,  assert: b,  ifthenelse: if b then t else f fi ,  class-value-has: X(e) has a,  ses-used-atoms: UsedAtoms(e),  ses-useable-atoms: UseableAtoms(e),  or: P  Q,  event-has: (e has a),  implies: P  Q,  all: x:A. B[x],  pi2: snd(t),  pi1: fst(t),  ses-signer: signer(e),  ses-signed: signed(e),  ses-sig: signature(e),  guard: {T},  rev_implies: P  Q,  iff: P  Q,  cand: A c B,  and: P  Q,  prop: ,  es-E-interface: E(X),  ses-verify-signer: signer(e),  ses-verify-signed: signed(e),  ses-verify-sig: signature(e),  uiff: uiff(P;Q),  unit: Unit,  bool: ,  so_apply: x[s1;s2],  uimplies: b supposing a,  sq_type: SQType(T),  uall: [x:A]. B[x],  sq_stable: SqStable(P),  ses-action: Action(e),  exists: x:A. B[x],  ses-act: Act,  ses-disjoint: ActionsDisjoint,  it: ,  subtype: S  T
Lemmas :  assert_of_bnot,  eqff_to_assert,  uiff_transitivity,  eqtt_to_assert,  ses-verify_wf,  ses-send_wf,  ses-new_wf,  ses-decrypt_wf,  encryption-key_wf,  ses-encrypt_wf,  Id_wf,  ses-sign_wf,  not_wf,  bnot_wf,  assert_wf,  equal_wf,  bool_wf,  top_wf,  event-ordering+_inc,  es-E_wf,  sdata_wf,  es-interface-subtype_rel2,  ses-rcv_wf,  in-eclass_wf,  security-event-structure_wf,  ses-disjoint_wf,  ses-info_wf,  event-ordering+_wf,  ses-act_wf,  int_subtype_base,  subtype_base_sq,  decidable__ses-action,  ses-action_wf,  sq_stable_from_decidable,  eclass-val_wf,  free-from-atom-Id-rw,  free-from-atom-atom,  and_functionality_wrt_iff,  and_functionality_wrt_uiff3,  sdata-free-from-atom,  and_functionality_wrt_uiff2,  not_functionality_wrt_iff,  free-from-atom-pair-iff,  not_functionality_wrt_uiff,  iff_weakening_uiff,  iff_functionality_wrt_iff,  true_wf,  free-from-atom_wf,  sdata-atoms_wf,  l_member_wf,  or_wf,  ses-signer_wf,  ses-signed_wf,  ses-sig_wf,  ses-verify-signer_wf,  ses-verify-signed_wf,  ses-verify-sig_wf
\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}e:Act.  \mforall{}a:Atom1.    ((e  has  a)  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  UseableAtoms(e))  \mvee{}  (a  \mmember{}  UsedAtoms(e)))))


Date html generated: 2012_01_23-PM-01_36_08
Last ObjectModification: 2011_12_11-PM-12_22_07

Home Index