Nuprl Lemma : is-rec-class

∀[Info,T:Type].
  ∀G:es:EO+(Info) ─→ E ─→ bag(T). ∀F:es:EO+(Info) ─→ e':E ─→ T ─→ {e:E| (e' <loc e)}  ─→ bag(T). ∀es:EO+(Info). ∀e:E.
    (↑e ∈b RecClass(first e
                      G[es;e]
                    or next e after e' with value v
                        F[es;e';v;e])
    ⇐⇒ if e ∈b prior(RecClass(first e
                                 G[es;e]
                               or next e after e' with value v
                                   F[es;e';v;e]))
        then let e' = prior(RecClass(first e
                                       G[es;e]
                                     or next e after e' with value v
                                         F[es;e';v;e]))(e) in
                 #(F[es;e';RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e])(e');e]) = 1 ∈ ℤ
        else #(G[es;e]) = 1 ∈ ℤ
        fi )


Proof



Definitions occuring in Statement :  es-rec-class: es-rec-class,  es-prior-interface: prior(X),  eclass-val: X(e),  in-eclass: e ∈b X,  event-ordering+: EO+(Info),  es-locl: (e <loc e'),  es-E: E,  assert: ↑b,  ifthenelse: if b then t else f fi ,  let: let,  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2],  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  set: {x:A| B[x]} ,  function: x:A ─→ B[x],  natural_number: $n,  int: ℤ,  universe: Type,  equal: s = t ∈ T,  bag-size: #(bs),  bag: bag(T)
Lemmas :  subtype_base_sq,  int_subtype_base,  assert_wf,  eq_int_wf,  bag-size_wf,  es-E-interface_wf,  es-interface-subtype_rel2,  es-E_wf,  event-ordering+_subtype,  event-ordering+_wf,  top_wf,  nat_wf,  es-prior-interface-val,  bag_wf,  eclass-val_wf2,  es-prior-interface_wf,  eclass-val_wf,  assert_elim,  in-eclass_wf,  bool_wf,  bool_subtype_base,  es-locl_wf,  equal-wf-T-base,  assert_of_eq_int,  iff_wf
Latex:
\mforall{}[Info,T:Type].
    \mforall{}G:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  bag(T).  \mforall{}F:es:EO+(Info)  {}\mrightarrow{}  e':E  {}\mrightarrow{}  T  {}\mrightarrow{}  \{e:E|  (e'  <loc  e)\}    {}\mrightarrow{}  bag(T).
    \mforall{}es:EO+(Info).  \mforall{}e:E.
        (\muparrow{}e  \mmember{}\msubb{}  RecClass(first  e
                                            G[es;e]
                                        or  next  e  after  e'  with  value  v
                                                F[es;e';v;e])
        \mLeftarrow{}{}\mRightarrow{}  if  e  \mmember{}\msubb{}  prior(RecClass(first  e
                                                                  G[es;e]
                                                              or  next  e  after  e'  with  value  v
                                                                      F[es;e';v;e]))
                then  let  e'  =  prior(RecClass(first  e
                                                                              G[es;e]
                                                                          or  next  e  after  e'  with  value  v
                                                                                  F[es;e';v;e]))(e)  in
                                  \#(F[es;e';RecClass(first  e
                                                                            G[es;e]
                                                                        or  next  e  after  e'  with  value  v
                                                                                F[es;e';v;e])(e');e])
                                  =  1
                else  \#(G[es;e])  =  1
                fi  )


Date html generated: 2015_07_21-PM-03_17_30
Last ObjectModification: 2015_01_27-PM-07_24_36

Home Index