Nuprl Lemma : split_tail_max

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


Definitions occuring in Statement :  split_tail: split_tail(L | ∀x.f[x]) l_before: before y ∈ l l_member: (x ∈ l) list: List assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] pi2: snd(t) all: x:A. B[x] implies:  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:  Q prop: uimplies: 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: λ2y.t[x; y] so_apply: x[s1;s2] cand: c∧ B nat: iff: ⇐⇒ Q and: P ∧ Q or: P ∨ Q rev_implies:  Q not: ¬A false: False bool: 𝔹 unit: Unit btrue: tt uiff: uiff(P;Q) ifthenelse: if then else 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

    \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 

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

Theory : list!

Home Index