Nuprl Lemma : replica-state_wf
[RepState:Type]. (replica-state(RepState) 
Type)
Proof not projected
Definitions occuring in Statement :
replica-state: replica-state(RepState),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
equal: s = t,
member: t T,
function: x:A 
B[x],
all: x:A. B[x],
Proposal: Proposal(),
list: type List,
product: x:A 
B[x],
int: 
,
universe: Type,
replica-state: replica-state(RepState),
axiom: Ax,
isect: 
x:A. B[x],
uall: [x:A]. B[x]
Lemmas :
Proposal_wf
\mforall{}[RepState:Type]. (replica-state(RepState) \mmember{} Type)
Date html generated:
2011_10_20-PM-11_52_16
Last ObjectModification:
2011_05_10-PM-02_03_16
Home
Index