### Nuprl Lemma : remove-first-no_repeats-member

`∀[T:Type]`
`  ∀L:T List. ∀P:{x:T| (x ∈ L)}  ⟶ 𝔹. ∀x:T.`
`    (no_repeats(T;L)`
`    `` (∀a,b:{x:T| (x ∈ L)} .  (((↑(P a)) ∧ (↑(P b))) `` (a = b ∈ T)))`
`    `` ((x ∈ remove-first(P;L)) `⇐⇒` (x ∈ L) ∧ (↑¬b(P x))))`

Proof

Definitions occuring in Statement :  remove-first: `remove-first(P;L)` no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` list: `T List` bnot: `¬bb` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  so_apply: `x[s1;s2;s3]` top: `Top` so_lambda: so_lambda3 remove-first: `remove-first(P;L)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` uimplies: `b supposing a` so_apply: `x[s]` subtype_rel: `A ⊆r B` prop: `ℙ` so_lambda: `λ2x.t[x]` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` false: `False` not: `¬A` uiff: `uiff(P;Q)` assert: `↑b` bnot: `¬bb` guard: `{T}` sq_type: `SQType(T)` or: `P ∨ Q` exists: `∃x:A. B[x]` bfalse: `ff` ifthenelse: `if b then t else f fi ` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` rev_uimplies: `rev_uimplies(P;Q)` cand: `A c∧ B`
Lemmas referenced :  equal_wf list_ind_cons_lemma list_ind_nil_lemma list_wf bnot_wf assert_wf set_wf bool_wf subtype_rel_dep_function remove-first_wf l_member_wf iff_wf all_wf no_repeats_wf list_induction assert_witness btrue_neq_bfalse btrue_wf null_nil_lemma nil_wf member-implies-null-eq-bfalse cons_wf no_repeats_cons assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal eqff_to_assert eqtt_to_assert assert_of_bnot cons_member not_wf or_wf and_wf assert_elim not_assert_elim subtype_rel_self remove-first-member-implies bfalse_wf istype-assert list-subtype no_repeats-subtype istype-universe l_member-settype
Rules used in proof :  cut universeEquality voidEquality voidElimination isect_memberEquality dependent_functionElimination independent_functionElimination functionExtensionality productEquality rename setElimination independent_isectElimination setEquality applyEquality because_Cache hypothesis cumulativity functionEquality lambdaEquality sqequalRule hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid introduction thin lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution productElimination equalitySymmetry equalityTransitivity independent_pairFormation instantiate promote_hyp dependent_pairFormation equalityElimination unionElimination andLevelFunctionality impliesFunctionality addLevel inrFormation levelHypothesis applyLambdaEquality dependent_set_memberEquality hyp_replacement inlFormation isect_memberFormation_alt lambdaFormation_alt dependent_set_memberEquality_alt universeIsType lambdaEquality_alt setIsType functionIsType productIsType equalityIstype inhabitedIsType

Latex:
\mforall{}[T:Type]
\mforall{}L:T  List.  \mforall{}P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}.  \mforall{}x:T.
(no\_repeats(T;L)
{}\mRightarrow{}  (\mforall{}a,b:\{x:T|  (x  \mmember{}  L)\}  .    (((\muparrow{}(P  a))  \mwedge{}  (\muparrow{}(P  b)))  {}\mRightarrow{}  (a  =  b)))
{}\mRightarrow{}  ((x  \mmember{}  remove-first(P;L))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L)  \mwedge{}  (\muparrow{}\mneg{}\msubb{}(P  x))))

Date html generated: 2020_05_19-PM-09_45_37
Last ObjectModification: 2020_01_04-PM-07_59_45

Theory : list_1

Home Index