Nuprl Lemma : ses-legal-thread-has-atom

s:SES
  (ActionsDisjoint
   (∀es:EO+(Info). ∀A:Id. ∀thr:Thread.
        (Legal(thr)@A
         (∀a:Atom1. ∀e:Act.
              (e ∈ thr
               (e has a)
               ((∃e':Act. ((e' <loc e) ∧ (e' has a) ∧ e' ∈ thr))
                 ∨ (a ∈ UseableAtoms(e))
                 ∨ (a Private(A) ∈ Atom1)))))))


Proof




Definitions occuring in Statement :  ses-legal-thread: Legal(thr)@A ses-useable-atoms: UseableAtoms(e) ses-thread-member: e ∈ thr ses-thread: Thread ses-disjoint: ActionsDisjoint event-has: (e has a) ses-act: Act ses-private: Private(A) ses-info: Info security-event-structure: SES event-ordering+: EO+(Info) es-locl: (e <loc e') Id: Id l_member: (x ∈ l) atom: Atom$n all: x:A. B[x] exists: x:A. B[x] implies:  Q or: P ∨ Q and: P ∧ Q equal: t ∈ T
Lemmas :  sq_stable_from_decidable ses-action_wf decidable__ses-action ses-act-has-atom equal-wf-base-T atom1_subtype_base ses-private_wf exists_wf es-locl_wf event-has_wf ses-thread-member_wf ses-act_wf ses-legal-thread_wf ses-thread_wf Id_wf event-ordering+_wf ses-info_wf ses-disjoint_wf security-event-structure_wf decidable__atom_equal_1 l_member_wf ses-useable-atoms_wf event-ordering+_subtype or_wf ses-thread-order l_all_iff ses-used-atoms_wf select_wf sq_stable__le cons_wf concat_wf map_wf le_wf less_than_wf list_wf less_than_transitivity2 length_wf le_weakening2 from-upto_wf squash_wf true_wf es-E_wf iff_weakening_equal cons_member member-concat member_map lelt_wf decidable__le false_wf not-le-2 condition-implies-le minus-add minus-one-mul zero-add add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel decidable__lt less-iff-le add-swap all_wf int_seg_wf subtract_wf le-add-cancel2 equal_wf

Latex:
\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}A:Id.  \mforall{}thr:Thread.
                (Legal(thr)@A
                {}\mRightarrow{}  (\mforall{}a:Atom1.  \mforall{}e:Act.
                            (e  \mmember{}  thr
                            {}\mRightarrow{}  (e  has  a)
                            {}\mRightarrow{}  ((\mexists{}e':Act.  ((e'  <loc  e)  \mwedge{}  (e'  has  a)  \mwedge{}  e'  \mmember{}  thr))
                                  \mvee{}  (a  \mmember{}  UseableAtoms(e))
                                  \mvee{}  (a  =  Private(A))))))))



Date html generated: 2015_07_23-PM-00_11_14
Last ObjectModification: 2015_02_04-PM-03_37_53

Home Index