Nuprl Lemma : loop-class-state-prior

[Info,B:Type]. ∀[X:EClass(B ─→ B)]. ∀[init:Id ─→ bag(B)].
  ∀es:EO+(Info). ∀e:E.
    ∀[v:B]
      uiff(v ∈ Prior(loop-class-state(X;init))?init(e);((↑first(e)) ∧ v ↓∈ init loc(e))
      ∨ ((¬↑first(e)) ∧ v ∈ loop-class-state(X;init)(pred(e))))


Proof




Definitions occuring in Statement :  loop-class-state: loop-class-state(X;init) primed-class-opt: Prior(X)?b classrel: v ∈ X(e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-first: first(e) es-pred: pred(e) es-loc: loc(e) es-E: E Id: Id assert: b uiff: uiff(P;Q) uall: [x:A]. B[x] all: x:A. B[x] not: ¬A or: P ∨ Q and: P ∧ Q apply: a function: x:A ─→ B[x] universe: Type bag-member: x ↓∈ bs bag: bag(T)
Lemmas :  primed-class-opt-classrel loop-class-state_wf sq_stable__bag-member es-loc_wf event-ordering+_subtype es-locl-first assert_elim btrue_neq_bfalse classrel_wf es-locl_wf es-E_wf exists_wf es-p-local-pred_wf squash_wf sq_stable__classrel es-pred_wf es-pred_property es-pred-locl es-causl_weakening true_wf event-ordering+_wf eclass_wf iff_weakening_equal es-loc-pred loop-class-state-exists subtype_base_sq Id_wf atom2_subtype_base es-init_wf es-init-locl bag-size-bag-member es-loc-init and_wf equal_wf bag_wf bag-member_wf all_wf not_wf es-locl_transitivity2 es-le_weakening_eq es-locl_irreflexivity es-causl_transitivity2 es-causle_weakening es-causl_irreflexivity

Latex:
\mforall{}[Info,B:Type].  \mforall{}[X:EClass(B  {}\mrightarrow{}  B)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].
    \mforall{}es:EO+(Info).  \mforall{}e:E.
        \mforall{}[v:B]
            uiff(v  \mmember{}  Prior(loop-class-state(X;init))?init(e);((\muparrow{}first(e))  \mwedge{}  v  \mdownarrow{}\mmember{}  init  loc(e))
            \mvee{}  ((\mneg{}\muparrow{}first(e))  \mwedge{}  v  \mmember{}  loop-class-state(X;init)(pred(e))))



Date html generated: 2015_07_21-PM-02_33_11
Last ObjectModification: 2015_02_04-PM-06_23_04

Home Index