Nuprl Lemma : sm-response-msg_wf
[R:Type]. [r:sm-response(R)]. (sm-response-msg(R;r) 
Message 
Id)
Proof not projected
Definitions occuring in Statement :
sm-response-msg: sm-response-msg(R;r),
sm-response: sm-response(R),
Message: Message,
Id: Id,
uall: [x:A]. B[x],
member: t T,
product: x:A B[x],
universe: Type
Definitions :
atom: Atom,
list: type List,
nil: [],
token: "$token",
cons: [car / cdr],
make-Msg: make-Msg(hdr;typ;val),
pair: <a, b>,
spread: spread def,
fpf: a:A fp-> B[a],
subtype: S 
T,
uimplies: b supposing a,
subtype_rel: A r B,
eclass: EClass(A[eo; e]),
atom: Atom$n,
spreadn: spread3,
int: 
,
bool: 
,
function: x:A 
B[x],
all: x:A. B[x],
product: x:A B[x],
Message: Message,
Id: Id,
sm-response-msg: sm-response-msg(R;r),
axiom: Ax,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
sm-response: sm-response(R),
member: t T,
equal: s = t,
universe: Type
Lemmas :
sm-response_wf,
Id_wf,
Message_wf,
member_wf,
make-Msg_wf
\mforall{}[R:Type]. \mforall{}[r:sm-response(R)]. (sm-response-msg(R;r) \mmember{} Message \mtimes{} Id)
Date html generated:
2011_10_20-PM-04_08_21
Last ObjectModification:
2011_05_05-AM-10_50_13
Home
Index