Nuprl Lemma : split_rel_last

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


Definitions occuring in Statement :  l_all: (∀x∈L.P[x]) last: last(L) null: null(as) append: as bs list: List assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] 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 :  implies:  Q top: Top and: P ∧ Q prop: so_apply: x[s] so_apply: x[s1;s2] uimplies: supposing a so_lambda: λ2x.t[x] member: t ∈ T all: x:A. B[x] uall: [x:A]. B[x] assert: b ifthenelse: if then else fi  btrue: tt not: ¬A false: False true: True decidable: Dec(P) or: P ∨ Q exists: x:A. B[x] cons: [a b] bfalse: ff guard: {T} select: L[n] subtract: m last: last(L) so_apply: x[s1;s2;s3] so_lambda: so_lambda(x,y,z.t[x; y; z]) rev_implies:  Q iff: ⇐⇒ Q it: nil: [] list_ind: list_ind append: as bs cand: c∧ B uiff: uiff(P;Q) squash: T subtype_rel: A ⊆B sq_type: SQType(T)
Lemmas referenced :  bool_wf l_member_wf last_wf l_all_wf length-append length_wf append_wf equal_wf list_wf exists_wf null_wf not_wf assert_wf all_wf isect_wf list_induction null_nil_lemma assert_witness true_wf decidable__assert cons_wf product_subtype_list null_cons_lemma list-cases null_wf2 not_assert_elim btrue_wf length_of_nil_lemma length_of_cons_lemma list_ind_nil_lemma l_all_single btrue_neq_bfalse bfalse_wf assert_elim nil_wf false_wf assert_of_null nat_wf length_wf_nat squash_wf last_cons subtype_rel_self iff_weakening_equal l_all_cons top_wf subtype_rel_list last_cons2 and_wf iff_weakening_uiff equal-wf-T-base iff_functionality_wrt_iff iff_imp_equal_bool bool_subtype_base subtype_base_sq list_ind_cons_lemma
Rules used in proof :  universeEquality universeIsType functionEquality dependent_functionElimination because_Cache independent_functionElimination isectEquality setEquality independent_isectElimination rename setElimination voidEquality voidElimination isect_memberEquality applyLambdaEquality productEquality hypothesis applyEquality lambdaEquality sqequalRule hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid introduction thin cut lambdaFormation isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution natural_numberEquality functionIsType inhabitedIsType unionElimination productElimination hypothesis_subsumption promote_hyp functionExtensionality cumulativity equalitySymmetry equalityTransitivity independent_pairFormation dependent_pairFormation hyp_replacement dependent_set_memberEquality imageElimination imageMemberEquality baseClosed instantiate

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

Date html generated: 2019_10_15-AM-10_54_33
Last ObjectModification: 2018_09_27-AM-10_47_46

Theory : list!

Home Index