Nuprl Lemma : assert-int-list-member

i:ℤ. ∀xs:ℤ List.  (↑int-list-member(i;xs) ⇐⇒ (i ∈ xs))


Proof




Definitions occuring in Statement :  int-list-member: int-list-member(i;xs) l_member: (x ∈ l) list: List assert: b all: x:A. B[x] iff: ⇐⇒ Q int:
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] so_apply: x[s] implies:  Q int-list-member: int-list-member(i;xs) top: Top assert: b ifthenelse: if then else fi  bfalse: ff prop: iff: ⇐⇒ Q and: P ∧ Q false: False rev_implies:  Q uimplies: supposing a not: ¬A or: P ∨ Q guard: {T} subtype_rel: A ⊆B uiff: uiff(P;Q)
Lemmas referenced :  list_induction iff_wf assert_wf int-list-member_wf l_member_wf list_wf reduce_nil_lemma reduce_cons_lemma false_wf null_nil_lemma btrue_wf member-implies-null-eq-bfalse nil_wf btrue_neq_bfalse equal-wf-base or_wf int_subtype_base cons_member cons_wf bor_wf eq_int_wf iff_transitivity iff_weakening_uiff assert_of_bor assert_of_eq_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination intEquality sqequalRule lambdaEquality dependent_functionElimination hypothesisEquality hypothesis independent_functionElimination isect_memberEquality voidElimination voidEquality rename because_Cache independent_pairFormation independent_isectElimination equalityTransitivity equalitySymmetry productElimination unionElimination inlFormation inrFormation applyEquality addLevel impliesFunctionality orFunctionality

Latex:
\mforall{}i:\mBbbZ{}.  \mforall{}xs:\mBbbZ{}  List.    (\muparrow{}int-list-member(i;xs)  \mLeftarrow{}{}\mRightarrow{}  (i  \mmember{}  xs))



Date html generated: 2018_05_21-PM-07_31_48
Last ObjectModification: 2017_07_26-PM-05_07_00

Theory : general


Home Index