Nuprl Lemma : deq-runEvents-witness_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. (deq-runEvents-witness() ∈ ∀e1,e2:runEvents(r). Dec(e1 = e2 ∈ runEvents(r)))
Proof
Definitions occuring in Statement :
deq-runEvents-witness: deq-runEvents-witness(),
runEvents: runEvents(r),
pRunType: pRunType(T.M[T]),
decidable: Dec(P),
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
member: t ∈ T,
function: x:A ─→ B[x],
universe: Type,
equal: s = t ∈ T
Lemmas :
pRunType_wf,
runEvents_wf,
decidable_wf,
equal_wf,
lifting-strict-spread,
top_wf,
has-value_wf_base,
base_wf,
lifting-strict-decide,
lifting-strict-int_eq,
lifting-strict-atom_eq2
Latex:
\mforall{}[M:Type {}\mrightarrow{} Type]. \mforall{}[r:pRunType(P.M[P])].
(deq-runEvents-witness() \mmember{} \mforall{}e1,e2:runEvents(r). Dec(e1 = e2))
Date html generated:
2015_07_23-AM-11_10_58
Last ObjectModification:
2015_01_29-AM-00_07_40
Home
Index