---

{ nms1,nms2:MaName List.  Dec(l_disjoint(MaName;nms1;nms2)) }

{ Proof }

---

Definitions occuring in Statement :  MaName: MaName,  decidable: Dec(P),  all: x:A. B[x],  list: type List,  l_disjoint: l_disjoint(T;l1;l2)
Definitions :  all: x:A. B[x],  member: t  T,  implies: P  Q
Lemmas :  decidable__l_disjoint,  MaName_wf,  decidable__equal_MaName

---

\mforall{}nms1,nms2:MaName  List.    Dec(l\_disjoint(MaName;nms1;nms2))


Date html generated: 2010_08_26-PM-11_42_47
Last ObjectModification: 2009_03_22-PM-01_23_51

Home Index