### Nuprl Lemma : split_tail_trivial

`∀[A:Type]. ∀[f:A ⟶ 𝔹]. ∀[L:A List].`
`  split_tail(L | ∀x.f[x]) = <[], L> ∈ (A List × (A List)) supposing ∀b:A. ((b ∈ L) `` (↑f[b]))`

Proof

Definitions occuring in Statement :  split_tail: `split_tail(L | ∀x.f[x])` l_member: `(x ∈ l)` nil: `[]` list: `T List` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` pair: `<a, b>` product: `x:A × B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` implies: `P `` Q` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` split_tail: `split_tail(L | ∀x.f[x])` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` guard: `{T}` or: `P ∨ Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` not: `¬A` false: `False`
Lemmas referenced :  list_induction isect_wf all_wf l_member_wf assert_wf equal_wf list_wf split_tail_wf nil_wf list_ind_nil_lemma list_ind_cons_lemma bool_wf cons_wf cons_member equal-wf-T-base bnot_wf not_wf eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot list_ind_wf ifthenelse_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality functionEquality hypothesis applyEquality productEquality independent_pairEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation rename because_Cache axiomEquality equalityTransitivity equalitySymmetry universeIsType functionIsType universeEquality independent_isectElimination inhabitedIsType lambdaFormation_alt productElimination inrFormation baseClosed unionElimination equalityElimination hyp_replacement applyLambdaEquality spreadEquality inlFormation

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].
split\_tail(L  |  \mforall{}x.f[x])  =  <[],  L>  supposing  \mforall{}b:A.  ((b  \mmember{}  L)  {}\mRightarrow{}  (\muparrow{}f[b]))

Date html generated: 2019_10_15-AM-10_54_41
Last ObjectModification: 2018_09_27-AM-10_18_53

Theory : list!

Home Index