Nuprl Lemma : l_disjoint_append

[T:Type]. ∀[a,b,c:T List].  uiff(l_disjoint(T;a;b c);l_disjoint(T;a;b) ∧ l_disjoint(T;a;c))


Proof




Definitions occuring in Statement :  l_disjoint: l_disjoint(T;l1;l2) append: as bs list: List uiff: uiff(P;Q) uall: [x:A]. B[x] and: P ∧ Q universe: Type
Definitions unfolded in proof :  l_disjoint: l_disjoint(T;l1;l2) uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a member: t ∈ T all: x:A. B[x] not: ¬A implies:  Q false: False cand: c∧ B or: P ∨ Q prop: uall: [x:A]. B[x] guard: {T} so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  l_member_wf all_wf not_wf or_wf member_append append_wf uiff_wf l_disjoint_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut independent_pairFormation isect_memberFormation introduction lambdaFormation thin hypothesis sqequalHypSubstitution dependent_functionElimination hypothesisEquality productElimination independent_functionElimination inlFormation extract_by_obid isectElimination productEquality voidElimination because_Cache sqequalRule inrFormation independent_pairEquality lambdaEquality addLevel independent_isectElimination cumulativity universeEquality isect_memberEquality equalityTransitivity equalitySymmetry unionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[a,b,c:T  List].    uiff(l\_disjoint(T;a;b  @  c);l\_disjoint(T;a;b)  \mwedge{}  l\_disjoint(T;a;c))



Date html generated: 2019_06_20-PM-01_27_06
Last ObjectModification: 2018_08_24-PM-11_13_00

Theory : list_1


Home Index