### Nuprl Lemma : member-insert-by

`∀[T:Type]`
`  ∀eq,r:T ⟶ T ⟶ 𝔹.`
`    ∀x:T. ∀L:T List. ∀z:T.  ((z ∈ insert-by(eq;r;x;L)) `⇐⇒` (z = x ∈ T) ∨ (z ∈ L)) `
`    supposing ∀a,b:T.  (↑(eq a b) `⇐⇒` a = b ∈ T)`

Proof

Definitions occuring in Statement :  insert-by: `insert-by(eq;r;x;l)` l_member: `(x ∈ l)` list: `T List` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` or: `P ∨ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` prop: `ℙ` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` insert-by: `insert-by(eq;r;x;l)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` or: `P ∨ Q` false: `False` guard: `{T}` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff`
Lemmas referenced :  assert_wf assert_witness equal_wf list_induction all_wf iff_wf l_member_wf insert-by_wf or_wf list_wf list_ind_nil_lemma false_wf nil_member nil_wf member_singleton cons_wf list_ind_cons_lemma bool_wf cons_member equal-wf-T-base bnot_wf not_wf eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality productElimination independent_pairEquality axiomEquality hypothesis extract_by_obid isectElimination applyEquality functionExtensionality cumulativity independent_functionElimination rename because_Cache isect_memberEquality voidElimination voidEquality independent_pairFormation inlFormation unionElimination addLevel impliesFunctionality orFunctionality functionEquality universeEquality equalityTransitivity equalitySymmetry inrFormation baseClosed equalityElimination independent_isectElimination hyp_replacement dependent_set_memberEquality applyLambdaEquality setElimination

Latex:
\mforall{}[T:Type]
\mforall{}eq,r:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}.
\mforall{}x:T.  \mforall{}L:T  List.  \mforall{}z:T.    ((z  \mmember{}  insert-by(eq;r;x;L))  \mLeftarrow{}{}\mRightarrow{}  (z  =  x)  \mvee{}  (z  \mmember{}  L))
supposing  \mforall{}a,b:T.    (\muparrow{}(eq  a  b)  \mLeftarrow{}{}\mRightarrow{}  a  =  b)

Date html generated: 2017_04_17-AM-08_26_08
Last ObjectModification: 2017_02_27-PM-04_48_20

Theory : list_1

Home Index