Nuprl Lemma : ohc_v2_roundout2_wf

[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [flrs:]. [learners,locs:bag(Id)].
  (ohc_v2_roundout2(Cmd;cmdeq;flrs;learners;locs)  Id
                                                     Cmd
                                                         (Cmd?)  Id
                                                     (Cmd?) List  (Id List)
                                                     bag(Id  Message))


Proof not projected



Definitions occuring in Statement :  ohc_v2_roundout2: ohc_v2_roundout2(Cmd;cmdeq;flrs;learners;locs),  Message: Message,  Id: Id,  uall: [x:A]. B[x],  unit: Unit,  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  union: left + right,  list: type List,  int: ,  deq: EqDecider(T),  bag: bag(T),  vatype: ValueAllType
Definitions :  uall: [x:A]. B[x],  vatype: ValueAllType,  member: t  T,  ohc_v2_roundout2: ohc_v2_roundout2(Cmd;cmdeq;flrs;learners;locs),  ifthenelse: if b then t else f fi ,  let: let,  all: x:A. B[x],  implies: P  Q,  btrue: tt,  assert: b,  top: Top,  subtype: S  T,  guard: {T},  true: True,  bfalse: ff,  unit: Unit,  bool: ,  uimplies: b supposing a,  uiff: uiff(P;Q),  prop: ,  and: P  Q,  nat: ,  sq_type: SQType(T),  it:
Lemmas :  eq_int_wf,  length_wf,  unit_wf2,  bool_wf,  uiff_transitivity,  equal_wf,  assert_wf,  eqtt_to_assert,  assert_of_eq_int,  null_wf3,  mapfilter_wf,  top_wf,  isl_wf,  assert_of_null,  poss-maj_wf,  outl_wf,  subtype_base_sq,  bool_subtype_base,  nat_wf,  ifthenelse_wf,  bag_wf,  Id_wf,  Message_wf,  bag-append_wf,  ohc_v2_notify'broadcast_wf,  valueall-type_wf,  ohc_v2_decided'broadcast_wf,  single-bag_wf,  ohc_v2_retry'send_wf,  bnot_wf,  not_wf,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_uiff,  empty-bag_wf,  deq_wf,  assert_elim
\mforall{}[Cmd:ValueAllType].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[flrs:\mBbbZ{}].  \mforall{}[learners,locs:bag(Id)].
    (ohc\_v2\_roundout2(Cmd;cmdeq;flrs;learners;locs)  \mmember{}  Id
                                                                                                        {}\mrightarrow{}  Cmd
                                                                                                        {}\mrightarrow{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  (Cmd?)  \mtimes{}  Id
                                                                                                        {}\mrightarrow{}  (Cmd?)  List  \mtimes{}  (Id  List)
                                                                                                        {}\mrightarrow{}  bag(Id  \mtimes{}  Message))


Date html generated: 2012_02_20-PM-05_47_00
Last ObjectModification: 2012_02_17-PM-10_31_22

Home Index