### Nuprl Lemma : split_rel_last

`∀[A:Type]`
`  ∀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])))`

Proof

Definitions occuring in Statement :  l_all: `(∀x∈L.P[x])` last: `last(L)` null: `null(as)` append: `as @ bs` list: `T List` assert: `↑b` bool: `𝔹` uimplies: `b 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: `s = t ∈ T`
Definitions unfolded in proof :  implies: `P `` Q` top: `Top` and: `P ∧ Q` prop: `ℙ` so_apply: `x[s]` so_apply: `x[s1;s2]` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` member: `t ∈ T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` assert: `↑b` ifthenelse: `if b then t else f 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: `n - m` last: `last(L)` so_apply: `x[s1;s2;s3]` so_lambda: `so_lambda(x,y,z.t[x; y; z])` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` it: `⋅` nil: `[]` list_ind: list_ind append: `as @ bs` cand: `A c∧ B` uiff: `uiff(P;Q)` squash: `↓T` subtype_rel: `A ⊆r 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

Latex:
\mforall{}[A:Type]
\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