### 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)].`
`∀[X:EClass(T)].`
`  X = RecClass(first e  G[es;e]or next e 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))`

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` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-locl: `(e <loc e')` es-E: `E` 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]` all: `∀x:A. B[x]` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` equal: `s = 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

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{}[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