### Nuprl Lemma : split_tail_max

`∀[A:Type]`
`  ∀f:A ⟶ 𝔹. ∀L:A List. ∀a:A.`
`    ((a ∈ L) `` ((a ∈ snd(split_tail(L | ∀x.f[x])))) supposing ((∀b:A. (a before b ∈ L `` (↑f[b]))) and (↑f[a])))`

Proof

Definitions occuring in Statement :  split_tail: `split_tail(L | ∀x.f[x])` l_before: `x before y ∈ l` l_member: `(x ∈ l)` list: `T List` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` pi2: `snd(t)` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` uimplies: `b supposing a` so_apply: `x[s]` 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]` pi2: `snd(t)` l_member: `(x ∈ l)` select: `L[n]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` cand: `A c∧ B` nat: `ℕ` iff: `P `⇐⇒` Q` and: `P ∧ Q` or: `P ∨ Q` rev_implies: `P `` Q` not: `¬A` false: `False` bool: `𝔹` unit: `Unit` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` guard: `{T}`
Lemmas referenced :  list_induction all_wf l_member_wf isect_wf assert_wf l_before_wf split_tail_wf list_wf pi2_wf equal_wf list_ind_nil_lemma list_ind_cons_lemma bool_wf length_of_nil_lemma stuck-spread base_wf assert_witness nil_wf exists_wf nat_wf less_than_wf equal-wf-T-base cons_wf cons_member split_tail_trivial cons_before bnot_wf not_wf assert_elim not_assert_elim and_wf btrue_neq_bfalse 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 lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality functionEquality hypothesis applyEquality productEquality equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination isect_memberEquality voidElimination voidEquality rename because_Cache universeIsType universeEquality baseClosed independent_isectElimination functionIsType inhabitedIsType setElimination natural_numberEquality productElimination unionElimination hyp_replacement applyLambdaEquality inlFormation independent_pairFormation dependent_set_memberEquality equalityElimination spreadEquality dependent_pairEquality inrFormation independent_pairEquality

Latex:
\mforall{}[A:Type]
\mforall{}f:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:A  List.  \mforall{}a:A.
((a  \mmember{}  L)
{}\mRightarrow{}  ((a  \mmember{}  snd(split\_tail(L  |  \mforall{}x.f[x]))))  supposing
((\mforall{}b:A.  (a  before  b  \mmember{}  L  {}\mRightarrow{}  (\muparrow{}f[b])))  and
(\muparrow{}f[a])))

Date html generated: 2019_10_15-AM-10_54_46
Last ObjectModification: 2018_09_27-AM-10_18_51

Theory : list!

Home Index