Nuprl Lemma : paxos-state-info_wf
[T:Type]. [s:AcceptorState]. (Info(s) 
T?)
Proof not projected
Definitions occuring in Statement :
paxos-state-info: Info(s),
paxos-acceptor-state: AcceptorState,
nat: ,
uall: [x:A]. B[x],
unit: Unit,
member: t T,
product: x:A B[x],
union: left + right,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
paxos-state-info: Info(s),
so_lambda: 
x.t[x],
paxos-acceptor-state: AcceptorState,
so_apply: x[s]
Lemmas :
pi2_wf,
Id_wf,
nat_wf,
unit_wf,
paxos-acceptor-state_wf
\mforall{}[T:Type]. \mforall{}[s:AcceptorState]. (Info(s) \mmember{} \mBbbN{} \mtimes{} T?)
Date html generated:
2011_10_20-PM-04_27_11
Last ObjectModification:
2011_06_18-PM-01_54_06
Home
Index