Nuprl Lemma : pax-message-types_wf
[Result:Type]. (pax-message-types(Result) 
(Name 
Type) List)
Proof not projected
Definitions occuring in Statement :
pax-message-types: pax-message-types(Result),
name: Name,
uall: [x:A]. B[x],
member: t T,
product: x:A B[x],
list: type List,
universe: Type
Definitions :
nil: [],
Cid: Cid(),
pax_response: pax_response(),
pax_decision: pax_decision(),
Proposal: Proposal(),
pax_propose: pax_propose(),
Command: Command(),
pax_request: pax_request(),
pax_adopted: pax_adopted(),
pax_preempted: pax_preempted(),
pax_p2b: pax_p2b(),
PValue: PValue(),
pax_p2a: pax_p2a(),
PVList: PVList(),
pax_p1b: pax_p1b(),
Ballot_Num: Ballot_Num(),
uall: [x:A]. B[x],
isect: 
x:A. B[x],
list: type List,
name: Name,
axiom: Ax,
pax-message-types: pax-message-types(Result),
universe: Type,
cons: [car / cdr],
pair: <a, b>,
pax_p1a: pax_p1a(),
equal: s = t,
product: x:A B[x],
Id: Id,
all: x:A. B[x],
function: x:A 
B[x],
member: t T
Lemmas :
pax_p1a_wf,
Id_wf,
Ballot_Num_wf,
pax_p1b_wf,
PVList_wf,
pax_p2a_wf,
PValue_wf,
pax_p2b_wf,
pax_preempted_wf,
pax_adopted_wf,
pax_request_wf,
Command_wf,
pax_propose_wf,
Proposal_wf,
pax_decision_wf,
pax_response_wf,
Cid_wf,
name_wf
\mforall{}[Result:Type]. (pax-message-types(Result) \mmember{} (Name \mtimes{} Type) List)
Date html generated:
2011_10_20-PM-11_49_26
Last ObjectModification:
2011_05_12-PM-05_05_58
Home
Index