Nuprl Lemma : es-LnkTag-deq_wf
es-LnkTag-deq ∈ EqDecider(IdLnk × Id)
Proof
Definitions occuring in Statement :
es-LnkTag-deq: es-LnkTag-deq,
IdLnk: IdLnk,
Id: Id,
deq: EqDecider(T),
member: t ∈ T,
product: x:A × B[x]
Definitions unfolded in proof :
es-LnkTag-deq: es-LnkTag-deq,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Latex:
es-LnkTag-deq \mmember{} EqDecider(IdLnk \mtimes{} Id)
Date html generated:
2016_05_16-PM-00_58_31
Last ObjectModification:
2015_12_29-PM-01_42_58
Theory : event-ordering
Home
Index