Nuprl Lemma : decidable__l_disjoint_manames
∀nms1,nms2:MaName List. Dec(l_disjoint(MaName;nms1;nms2))
Proof
Definitions occuring in Statement :
MaName: MaName,
l_disjoint: l_disjoint(T;l1;l2),
list: T List,
decidable: Dec(P),
all: ∀x:A. B[x]
Lemmas :
decidable__l_disjoint,
MaName_wf,
decidable__equal_MaName,
list_wf
\mforall{}nms1,nms2:MaName List. Dec(l\_disjoint(MaName;nms1;nms2))
Date html generated:
2015_07_17-AM-09_14_59
Last ObjectModification:
2015_01_28-AM-07_53_49
Home
Index