Nuprl - list 3 jlc Citations of disjoint

list 3 jlc Sections Support(jlc) Doc

Def disjoint(eq;L1;L2) ==

L1.

eq) L2

is mentioned by

Thm* eq:{T=}, L,M:T List. disjoint(eq;L;M) (x:T. x(eq) L & x(eq) M) [not_disjoint_is_member_lemma]

Thm* eq:{T}, L,M:T List. disjoint(eq;L;M) disjoint(eq;L;M) [disjoint_iff_assert_disjoint2]

Thm* eq:(TT), L1,L2:T List, x:T. disjoint(eq;(x.L1);L2) disjoint(eq;L1;L2) [disjoint_tail]

Thm* eq:(TT), L1,L2:T List. Dec(disjoint(eq;L1;L2)) [decidable__disjoint]

list 3 jlc Sections Support(jlc) Doc

`Thm* eq:{T=}, L,M:T List. disjoint(eq;L;M) (x:T. x(eq) L & x(eq) M)`	[not_disjoint_is_member_lemma]
`Thm* eq:{T}, L,M:T List. disjoint(eq;L;M) disjoint(eq;L;M)`	[disjoint_iff_assert_disjoint2]
`Thm* eq:(TT), L1,L2:T List, x:T. disjoint(eq;(x.L1);L2) disjoint(eq;L1;L2)`	[disjoint_tail]
`Thm* eq:(TT), L1,L2:T List. Dec(disjoint(eq;L1;L2))`	[decidable__disjoint]