Nuprl Lemma : member-zip

[A,B:Type].  ∀xs:A List. ∀ys:B List. ∀x:A. ∀y:B.  ((<x, y> ∈ zip(xs;ys))  {(x ∈ xs) ∧ (y ∈ ys)})


Proof




Definitions occuring in Statement :  zip: zip(as;bs) l_member: (x ∈ l) list: List uall: [x:A]. B[x] guard: {T} all: x:A. B[x] implies:  Q and: P ∧ Q pair: <a, b> product: x:A × B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T so_lambda: λ2x.t[x] implies:  Q prop: and: P ∧ Q so_apply: x[s] top: Top uimplies: supposing a not: ¬A false: False iff: ⇐⇒ Q or: P ∨ Q pi2: snd(t) subtype_rel: A ⊆B pi1: fst(t) guard: {T} cand: c∧ B rev_implies:  Q
Lemmas referenced :  list_induction all_wf list_wf l_member_wf zip_wf guard_wf and_wf zip_nil_lemma null_nil_lemma btrue_wf member-implies-null-eq-bfalse nil_wf btrue_neq_bfalse cons_wf zip_cons_nil_lemma zip_cons_cons_lemma cons_member pi2_wf pi1_wf_top subtype_rel_product top_wf or_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin lemma_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality hypothesis functionEquality productEquality independent_pairEquality independent_functionElimination rename because_Cache dependent_functionElimination universeEquality isect_memberEquality voidElimination voidEquality independent_isectElimination equalityTransitivity equalitySymmetry productElimination unionElimination applyEquality inlFormation independent_pairFormation addLevel inrFormation

Latex:
\mforall{}[A,B:Type].    \mforall{}xs:A  List.  \mforall{}ys:B  List.  \mforall{}x:A.  \mforall{}y:B.    ((<x,  y>  \mmember{}  zip(xs;ys))  {}\mRightarrow{}  \{(x  \mmember{}  xs)  \mwedge{}  (y  \mmember{}  ys)\})



Date html generated: 2016_05_15-PM-03_40_40
Last ObjectModification: 2015_12_27-PM-01_17_26

Theory : general


Home Index