Nuprl Lemma : rec-class-val

∀[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].
  RecClass(first e
             G[es;e]
           or next e after e' with value v
               F[es;e';v;e])(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
             only(F[es;e';RecClass(first e
                                     G[es;e]
                                   or next e after e' with value v
                                       F[es;e';v;e])(e');e])
    else only(G[es;e])
    fi 
  ∈ T 
  supposing ↑e ∈b RecClass(first e
                             G[es;e]
                           or next e after e' with value v
                               F[es;e';v;e])


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,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2],  set: {x:A| B[x]} ,  function: x:A ─→ B[x],  universe: Type,  equal: s = t ∈ T,  bag-only: only(bs),  bag: bag(T)
Lemmas :  es-rec-class_wf,  es-locl_wf,  eclass_wf,  assert_wf,  in-eclass_wf,  es-interface-subtype_rel2,  es-E_wf,  event-ordering+_subtype,  bag_wf,  event-ordering+_wf,  es-prior-interface_wf,  top_wf,  es-E-interface_wf,  eq_int_wf,  bag-size_wf,  bool_wf,  eqtt_to_assert,  assert_of_eq_int,  nat_wf,  eqff_to_assert,  equal_wf,  bool_cases_sqequal,  subtype_base_sq,  bool_subtype_base,  assert-bnot,  neg_assert_of_eq_int,  equal-wf-T-base,  eclass-val_wf,  es-E-interface-property,  eclass-val_wf2,  es-prior-interface_wf0,  assert_functionality_wrt_uiff,  subtype_top,  squash_wf,  true_wf,  Id_wf,  es-loc-prior-interface,  es-loc_wf,  iff_weakening_equal,  es-prior-interface-causl,  bag-only_wf2,  single-valued-bag-if-le1,  le_weakening,  and_wf,  le_wf,  decidable__lt,  false_wf,  le_antisymmetry_iff,  add_functionality_wrt_le,  add-commutes,  zero-add,  le-add-cancel,  zero-le-nat,  not-equal-2,  add-zero
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].
    RecClass(first  e
                          G[es;e]
                      or  next  e  after  e'  with  value  v
                              F[es;e';v;e])(e)
    =  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
                          only(F[es;e';RecClass(first  e
                                                                          G[es;e]
                                                                      or  next  e  after  e'  with  value  v
                                                                              F[es;e';v;e])(e');e])
        else  only(G[es;e])
        fi   
    supposing  \muparrow{}e  \mmember{}\msubb{}  RecClass(first  e
                                                          G[es;e]
                                                      or  next  e  after  e'  with  value  v
                                                              F[es;e';v;e])


Date html generated: 2015_07_21-PM-03_17_42
Last ObjectModification: 2015_02_04-PM-06_18_27

Home Index