Nuprl Lemma : SM-replica_wf
[R:Type]. [M:EClass(sm-response(R) List)]. (SM-replica(R;M) 
EClass(Message 
Id))
Proof not projected
Definitions occuring in Statement :
SM-replica: SM-replica(R;M),
sm-response: sm-response(R),
Message: Message,
eclass: EClass(A[eo; e]),
Id: Id,
uall: [x:A]. B[x],
member: t T,
product: x:A B[x],
list: type List,
universe: Type
Definitions :
label: ...$L... t,
member: t T,
uall: [x:A]. B[x],
SM-replica: SM-replica(R;M),
so_lambda: 
x.t[x],
event-ordering+: EO+(Info),
eclass-compose1: f o X,
eclass: EClass(A[eo; e]),
so_apply: x[s]
Lemmas :
sm-response_wf,
eclass_wf3,
eclass-compose1_wf,
es-base-E_wf,
event_ordering_wf,
record+_subtype_rel,
es-E_wf,
Id_wf,
Message_wf,
bag-combine_wf
\mforall{}[R:Type]. \mforall{}[M:EClass(sm-response(R) List)]. (SM-replica(R;M) \mmember{} EClass(Message \mtimes{} Id))
Date html generated:
2012_01_23-PM-01_41_03
Last ObjectModification:
2011_12_11-PM-12_22_42
Home
Index