Nuprl Lemma : paxos-acceptor-state_wf
[T:Type]. (AcceptorState 
Type)
Proof not projected
Definitions occuring in Statement :
paxos-acceptor-state: AcceptorState,
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
paxos-acceptor-state: AcceptorState
Lemmas :
Id_wf,
nat_wf,
unit_wf
\mforall{}[T:Type]. (AcceptorState \mmember{} Type)
Date html generated:
2011_10_20-PM-04_26_22
Last ObjectModification:
2011_06_18-PM-01_52_48
Home
Index