Nuprl Lemma : Memory-classrel1

[Info,B,A:Type]. [f:A  B  B]. [init:Id  bag(B)]. [X:EClass(A)]. [es:EO+(Info)]. [e:E]. [v:B].
  uiff(v  Memory-class(f;init;X)(e);((first(e))  v  init loc(e))
                                       ((first(e))
                                         ((a:A
                                             (a  X(pred(e))
                                              (b:B. (b  Memory-class(f;init;X)(pred(e))  (v = (f a b))))))
                                           ((a:A. (a  X(pred(e))))  v  Memory-class(f;init;X)(pred(e))))))


Proof not projected



Definitions occuring in Statement :  Memory-class: Memory-class(f;init;X),  classrel: v  X(e),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-pred: pred(e),  es-first: first(e),  es-loc: loc(e),  es-E: E,  Id: Id,  assert: b,  uiff: uiff(P;Q),  uall: [x:A]. B[x],  all: x:A. B[x],  exists: x:A. B[x],  not: A,  squash: T,  or: P  Q,  and: P  Q,  apply: f a,  function: x:A  B[x],  universe: Type,  equal: s = t,  bag-member: x  bs,  bag: bag(T)
Definitions :  or: P  Q,  and: P  Q,  exists: x:A. B[x],  all: x:A. B[x],  member: t  T,  prop: ,  cand: A c B,  so_lambda: x.t[x],  so_lambda: x y.t[x; y],  Id: Id,  classrel: v  X(e),  Memory-class: Memory-class(f;init;X),  ifthenelse: if b then t else f fi ,  primed-class-opt: Prior(X)?b,  es-local-pred: last(P),  ycomb: Y,  implies: P  Q,  btrue: tt,  bfalse: ff,  assert: b,  uiff: uiff(P;Q),  bag-member: x  bs,  squash: T,  true: True,  uimplies: b supposing a,  guard: {T},  rev_implies: P  Q,  iff: P  Q,  not: A,  false: False,  uall: [x:A]. B[x],  so_apply: x[s],  so_apply: x[s1;s2],  bool: ,  unit: Unit,  sq_type: SQType(T),  nat: ,  le: A  B,  subtype: S  T,  eclass: EClass(A[eo; e]),  it:
Lemmas :  classrel_wf,  Memory-class_wf,  squash_wf,  or_wf,  assert_wf,  es-first_wf,  event-ordering+_inc,  bag-member_wf,  es-loc_wf,  not_wf,  exists_wf,  es-pred_wf,  all_wf,  es-E_wf,  event-ordering+_wf,  eclass_wf,  Id_wf,  bag_wf,  bool_wf,  eqtt_to_assert,  uiff_transitivity,  equal_wf,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  lt_int_wf,  bag-size_wf,  Accum-class_wf,  subtype_base_sq,  atom2_subtype_base,  es-loc-pred,  true_wf,  and_wf,  nat_wf,  less_than_wf,  assert_of_lt_int,  le_int_wf,  le_wf,  assert_functionality_wrt_uiff,  bnot_of_lt_int,  assert_of_le_int,  bag-size-bag-member,  false_wf,  squash_functionality_wrt_uiff,  exists_functionality_wrt_iff,  Accum-classrel-Memory,  uiff_functionality_wrt_uiff2,  not_functionality_wrt_iff,  not_functionality_wrt_uiff
\mforall{}[Info,B,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
\mforall{}[v:B].
    uiff(v  \mmember{}  Memory-class(f;init;X)(e);\mdownarrow{}((\muparrow{}first(e))  \mwedge{}  v  \mdownarrow{}\mmember{}  init  loc(e))
                                                                            \mvee{}  ((\mneg{}\muparrow{}first(e))
                                                                                \mwedge{}  ((\mexists{}a:A
                                                                                          (a  \mmember{}  X(pred(e))
                                                                                          \mwedge{}  (\mexists{}b:B
                                                                                                  (b  \mmember{}  Memory-class(f;init;X)(pred(e))
                                                                                                  \mwedge{}  (v  =  (f  a  b))))))
                                                                                    \mvee{}  ((\mforall{}a:A.  (\mneg{}a  \mmember{}  X(pred(e))))
                                                                                        \mwedge{}  v  \mmember{}  Memory-class(f;init;X)(pred(e))))))


Date html generated: 2012_01_23-PM-12_58_14
Last ObjectModification: 2012_01_11-PM-12_00_45

Home Index