Nuprl Lemma : SimpleConsensus_main_nlp-ext

Cmd:ValueAllType. clients:bag(Id). cmdeq:EqDecider(Cmd). flrs:. locs:bag(Id).
  NormalLProgrammable'(Id  Message;SimpleConsensus_main{mark-simple-consensus.esh:o}(Cmd; clients; cmdeq; flrs; locs))


Proof not projected



Definitions occuring in Statement :  Message: Message,  normal-locally-programmable: NormalLProgrammable(A;X),  Id: Id,  all: x:A. B[x],  product: x:A  B[x],  int: ,  deq: EqDecider(T),  bag: bag(T),  vatype: ValueAllType
Lemmas :  product_subtype_base,  Message_wf,  unit_wf,  bag_wf,  set_subtype_base,  valueall-type_wf,  subtype_base_sq,  dataflow-program_wf,  parallel-df-prog_wf,  base-prog_wf,  deq-member_wf,  vatype_wf,  Id_wf,  deq_wf,  normal-locally-programmable_wf,  Error :SimpleConsensus_main_wf,  Error :SimpleConsensus_main_nlp
\mforall{}Cmd:ValueAllType.  \mforall{}clients:bag(Id).  \mforall{}cmdeq:EqDecider(Cmd).  \mforall{}flrs:\mBbbZ{}.  \mforall{}locs:bag(Id).
    NormalLProgrammable'(Id  \mtimes{}  Message;SimpleConsensus\_main\{mark-simple-consensus.esh:o\}(Cmd;
                                                                                                                                                                            clients;
                                                                                                                                                                            cmdeq;
                                                                                                                                                                            flrs;
                                                                                                                                                                            locs))


Date html generated: 2012_02_20-PM-03_38_44
Last ObjectModification: 2012_02_02-PM-01_57_53

Home Index