Nuprl Lemma : rec-class-unique

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


Definitions occuring in Statement :  es-rec-class: es-rec-class es-prior-interface: prior(X) eclass-val: X(e) in-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-locl: (e <loc e') es-E: E ifthenelse: if then else fi  let: let uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2;s3;s4] so_apply: x[s1;s2] all: x:A. B[x] set: {x:A| B[x]}  apply: a function: x:A ─→ B[x] universe: Type equal: t ∈ T bag: bag(T)
Lemmas :  all_wf event-ordering+_wf es-E_wf event-ordering+_subtype equal_wf bag_wf in-eclass_wf es-prior-interface_wf1 es-interface-subtype_rel2 top_wf subtype_top es-E-interface_wf bool_wf eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot eclass_wf es-locl_wf es-rec-class_wf es-causl-swellfnd nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf int_seg_wf int_seg_subtype-nat decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel decidable__equal_int subtype_rel-int_seg le_weakening int_seg_properties le_wf nat_wf zero-le-nat lelt_wf es-causl_wf decidable__lt not-equal-2 le-add-cancel-alt not-le-2 sq_stable__le add-mul-special zero-mul squash_wf true_wf es-prior-interface-equal assert_wf or_wf eq_int_wf bag-size_wf es-causl_weakening assert_functionality_wrt_uiff eclass-val_wf2 es-prior-interface_wf set_wf subtype_rel_dep_function subtype_rel_sets event_ordering_wf iff_weakening_equal subtype_rel_self Id_wf es-loc-prior-interface es-loc_wf es-prior-interface-causl es-prior-interface-val bag-only_wf2 single-valued-bag_wf assert_of_eq_int single-valued-bag-if-le1 le_antisymmetry_iff is-prior-interface eclass-val_wf es-E-interface-property

\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{}[X:EClass(T)].
    X  =  RecClass(first  e    G[es;e]or  next  e  after  e'  with  value  v        F[es;e';v;e]) 
    supposing  \mforall{}es:EO+(Info).  \mforall{}e:E.
                            ((X  es  e)
                            =  if  e  \mmember{}\msubb{}  prior(X)  then  let  e'  =  prior(X)(e)  in  F[es;e';X(e');e]  else  G[es;e]  fi  )

Date html generated: 2015_07_21-PM-03_21_45
Last ObjectModification: 2015_02_04-PM-06_18_50

Home Index