Nuprl Lemma : split_tail_lemma

[A:Type]
  ∀f:A ⟶ 𝔹. ∀L:A List.
    (∀a∈L.∃L1,L2:A List. (((L (L1 L2) ∈ (A List)) ∧ (a ∈ L2) ∧ (∀b∈L2.↑f[b])) ∧ ¬↑f[last(L1)] supposing ¬↑null(L1)) 
          supposing (∀b≥a∈L.↑f[b]))


Proof




Definitions occuring in Statement :  l_all_since: (∀x≥a∈L.P[x]) l_all: (∀x∈L.P[x]) last: last(L) l_member: (x ∈ l) null: null(as) append: as bs list: List assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] not: ¬A and: P ∧ Q function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T so_lambda: λ2x.t[x] prop: uimplies: supposing a so_apply: x[s] and: P ∧ Q top: Top iff: ⇐⇒ Q rev_implies:  Q implies:  Q l_all_since: (∀x≥a∈L.P[x]) exists: x:A. B[x] cand: c∧ B squash: T true: True subtype_rel: A ⊆B guard: {T} not: ¬A false: False split_tail: split_tail(L | ∀x.f[x]) so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] pi1: fst(t) assert: b ifthenelse: if then else fi  btrue: tt bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) bfalse: ff or: P ∨ Q sq_type: SQType(T) bnot: ¬bb
Lemmas referenced :  l_all_iff l_member_wf isect_wf l_all_since_wf assert_wf exists_wf list_wf equal_wf append_wf length_wf length-append l_all_wf not_wf null_wf last_wf assert_witness l_before_wf bool_wf split_tail_wf pi1_wf pi2_wf squash_wf true_wf split_tail_rel iff_weakening_equal all_wf split_tail_max split_tail_correct l_all_fwd list_induction list_ind_nil_lemma null_nil_lemma list_ind_cons_lemma eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot list_ind_wf nil_wf cons_wf null_cons_lemma false_wf assert_functionality_wrt_uiff assert_elim bfalse_wf btrue_neq_bfalse last_cons last_singleton
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination sqequalRule lambdaEquality cumulativity hypothesis setElimination rename applyEquality functionExtensionality because_Cache productEquality applyLambdaEquality isect_memberEquality voidElimination voidEquality setEquality isectEquality independent_isectElimination productElimination independent_functionElimination independent_pairEquality functionEquality universeEquality dependent_pairFormation equalityTransitivity equalitySymmetry imageElimination natural_numberEquality imageMemberEquality baseClosed independent_pairFormation addLevel existsFunctionality andLevelFunctionality existsLevelFunctionality unionElimination equalityElimination promote_hyp instantiate impliesFunctionality levelHypothesis

Latex:
\mforall{}[A:Type]
    \mforall{}f:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:A  List.
        (\mforall{}a\mmember{}L.\mexists{}L1,L2:A  List
                      (((L  =  (L1  @  L2))  \mwedge{}  (a  \mmember{}  L2)  \mwedge{}  (\mforall{}b\mmember{}L2.\muparrow{}f[b]))  \mwedge{}  \mneg{}\muparrow{}f[last(L1)]  supposing  \mneg{}\muparrow{}null(L1)) 
                    supposing  (\mforall{}b\mgeq{}a\mmember{}L.\muparrow{}f[b]))



Date html generated: 2017_10_01-AM-08_34_59
Last ObjectModification: 2017_07_26-PM-04_25_36

Theory : list!


Home Index