Nuprl Lemma : iterated_classrel_invariant3

[Info,A,S:Type]. ∀[init:Id ─→ bag(S)]. ∀[f:A ─→ S ─→ S]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[P:S ─→ ℙ].
  ((∀s:S. SqStable(P[s]))
   (∀e:E. ∀v:S.
        ((∀s:S. (s ↓∈ init loc(e)  P[s]))
         (∀a:A. ∀e':E.  (e' ≤loc e   a ∈ X(e')  (∀s:S. (s ∈ prior(X*(f,init,e'))  P[s]  P[f s]))))
         iterated_classrel(es;S;A;f;init;X;e;v)
         P[v])))


Proof




Definitions occuring in Statement :  prior_iterated_classrel: s ∈ prior(X*(f,init,e)) iterated_classrel: iterated_classrel(es;S;A;f;init;X;e;v) classrel: v ∈ X(e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-le: e ≤loc e'  es-loc: loc(e) es-E: E Id: Id sq_stable: SqStable(P) uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] implies:  Q apply: a function: x:A ─→ B[x] universe: Type bag-member: x ↓∈ bs bag: bag(T)
Lemmas :  es-causl-swellfnd less_than_transitivity1 less_than_irreflexivity int_seg_wf decidable__equal_int subtype_rel-int_seg false_wf le_weakening subtract_wf int_seg_properties le_wf nat_wf zero-le-nat lelt_wf es-causl_wf es-first_wf2 bool_cases subtype_base_sq bool_wf bool_subtype_base eqtt_to_assert eqff_to_assert assert_of_bnot iterated_classrel_wf all_wf es-le_wf classrel_wf prior_iterated_classrel_wf bag-member_wf es-loc_wf equal_wf int_seg_subtype-nat decidable__lt not-equal-2 condition-implies-le minus-add minus-minus minus-one-mul add-swap add-commutes add-associates add_functionality_wrt_le zero-add le-add-cancel-alt less-iff-le le-add-cancel set_wf less_than_wf primrec-wf2 decidable__le not-le-2 sq_stable__le add-zero add-mul-special zero-mul es-E_wf event-ordering+_subtype sq_stable_wf event-ordering+_wf eclass_wf Id_wf bag_wf es-le-self not_wf assert_wf es-pred_wf iff_weakening_equal and_wf member_wf es-pred-locl es-causl_weakening es-locl_transitivity1 es-le_weakening es-loc-pred
\mforall{}[Info,A,S:Type].  \mforall{}[init:Id  {}\mrightarrow{}  bag(S)].  \mforall{}[f:A  {}\mrightarrow{}  S  {}\mrightarrow{}  S].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].
\mforall{}[P:S  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}s:S.  SqStable(P[s]))
    {}\mRightarrow{}  (\mforall{}e:E.  \mforall{}v:S.
                ((\mforall{}s:S.  (s  \mdownarrow{}\mmember{}  init  loc(e)  {}\mRightarrow{}  P[s]))
                {}\mRightarrow{}  (\mforall{}a:A.  \mforall{}e':E.
                            (e'  \mleq{}loc  e    {}\mRightarrow{}  a  \mmember{}  X(e')  {}\mRightarrow{}  (\mforall{}s:S.  (s  \mmember{}  prior(X*(f,init,e'))  {}\mRightarrow{}  P[s]  {}\mRightarrow{}  P[f  a  s]))))
                {}\mRightarrow{}  iterated\_classrel(es;S;A;f;init;X;e;v)
                {}\mRightarrow{}  P[v])))



Date html generated: 2015_07_17-PM-00_25_41
Last ObjectModification: 2015_02_04-PM-05_35_18

Home Index