---

{ [T:Type]. [eq:EqDecider(T)]. [a,b,c:T List].
    l_disjoint(T;l_intersection(eq;b;c);a) 
    supposing l_disjoint(T;b;a)  l_disjoint(T;c;a) }

{ Proof }

---

Definitions occuring in Statement :  l_intersection: l_intersection(eq;L1;L2),  uimplies: b supposing a,  uall: [x:A]. B[x],  or: P  Q,  list: type List,  universe: Type,  l_disjoint: l_disjoint(T;l1;l2),  deq: EqDecider(T)
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  or: P  Q,  l_disjoint: l_disjoint(T;l1;l2),  member: t  T,  all: x:A. B[x],  not: A,  and: P  Q,  implies: P  Q,  false: False,  prop: ,  rev_implies: P  Q,  iff: P  Q
Lemmas :  l_member_wf,  l_intersection_wf,  l_disjoint_wf,  deq_wf,  not_functionality_wrt_iff,  and_functionality_wrt_iff,  member-intersection

---

\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[a,b,c:T  List].
    l\_disjoint(T;l\_intersection(eq;b;c);a)  supposing  l\_disjoint(T;b;a)  \mvee{}  l\_disjoint(T;c;a)


Date html generated: 2011_08_10-AM-07_48_59
Last ObjectModification: 2011_06_18-AM-08_13_19

Home Index