### Nuprl Lemma : set-equal-cons2

`∀[T:Type]`
`  ∀eq:EqDecider(T). ∀u:T. ∀v,bs:T List.`
`    (set-equal(T;[u / v];bs) `⇐⇒` (u ∈ bs) ∧ set-equal(T;filter(λx.(¬b(eq x u));v);filter(λx.(¬b(eq x u));bs)))`

Proof

Definitions occuring in Statement :  set-equal: `set-equal(T;x;y)` l_member: `(x ∈ l)` filter: `filter(P;l)` cons: `[a / b]` list: `T List` deq: `EqDecider(T)` bnot: `¬bb` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` apply: `f a` lambda: `λx.A[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` set-equal: `set-equal(T;x;y)` member: `t ∈ T` rev_implies: `P `` Q` or: `P ∨ Q` prop: `ℙ` deq: `EqDecider(T)` guard: `{T}` not: `¬A` false: `False` eqof: `eqof(d)` uiff: `uiff(P;Q)` uimplies: `b supposing a` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` bfalse: `ff` exists: `∃x:A. B[x]` sq_type: `SQType(T)` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` cand: `A c∧ B`
Lemmas referenced :  cons_member l_member_wf set-equal_wf cons_wf filter_wf5 bnot_wf list_wf deq_wf or_wf equal_wf assert_witness assert_wf member_filter iff_wf eqof_wf not_wf iff_transitivity iff_weakening_uiff assert_of_bnot safe-assert-deq bool_wf eqtt_to_assert and_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation sqequalHypSubstitution cut hypothesis dependent_functionElimination thin hypothesisEquality productElimination independent_functionElimination introduction extract_by_obid isectElimination because_Cache inlFormation cumulativity productEquality lambdaEquality applyEquality setElimination rename setEquality universeEquality promote_hyp sqequalRule inrFormation addLevel impliesFunctionality unionElimination voidElimination independent_isectElimination levelHypothesis equalityElimination equalityTransitivity equalitySymmetry hyp_replacement dependent_set_memberEquality applyLambdaEquality dependent_pairFormation instantiate

Latex:
\mforall{}[T:Type]
\mforall{}eq:EqDecider(T).  \mforall{}u:T.  \mforall{}v,bs:T  List.
(set-equal(T;[u  /  v];bs)
\mLeftarrow{}{}\mRightarrow{}  (u  \mmember{}  bs)  \mwedge{}  set-equal(T;filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v);filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));bs)))

Date html generated: 2017_04_17-AM-07_37_16
Last ObjectModification: 2017_02_27-PM-04_12_15

Theory : list_1

Home Index