### Nuprl Lemma : append_split

`∀[T:Type]`
`  ∀L:T List`
`    ∀[P:T ⟶ ℙ]`
`      ((∀x:ℕ||L||. Dec(P L[x]))`
`      `` (∀i,j:ℕ||L||.  ((P L[i]) `` P L[j] supposing i < j))`
`      `` (∃L1,L2:T List`
`           (((L = (L1 @ L2) ∈ (T List)) ∧ (∀i:ℕ||L1||. (¬(P L1[i]))) ∧ (∀i:ℕ||L2||. (P L2[i])))`
`           ∧ (∀x∈L.(P x) `` (x ∈ L2)))))`

Proof

Definitions occuring in Statement :  l_all: `(∀x∈L.P[x])` l_member: `(x ∈ l)` select: `L[n]` length: `||as||` append: `as @ bs` list: `T List` int_seg: `{i..j-}` less_than: `a < b` decidable: `Dec(P)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type` equal: `s = 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: `ℙ` implies: `P `` Q` int_seg: `{i..j-}` uimplies: `b supposing a` guard: `{T}` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` less_than: `a < b` squash: `↓T` so_apply: `x[s]` subtype_rel: `A ⊆r B` select: `L[n]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` cand: `A c∧ B` ge: `i ≥ j ` le: `A ≤ B` uiff: `uiff(P;Q)` subtract: `n - m` less_than': `less_than'(a;b)` nat_plus: `ℕ+` true: `True` cons: `[a / b]` iff: `P `⇐⇒` Q` sq_type: `SQType(T)` rev_implies: `P `` Q` l_all: `(∀x∈L.P[x])`
Lemmas referenced :  list_induction uall_wf all_wf int_seg_wf length_wf decidable_wf select_wf int_seg_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma less_than_wf exists_wf list_wf equal_wf append_wf length-append not_wf l_all_wf l_member_wf length_of_nil_lemma stuck-spread base_wf length_of_cons_lemma nil_wf list_ind_nil_lemma l_all_nil equal-wf-base-T intformeq_wf int_formula_prop_eq_lemma l_all_wf_nil cons_wf non_neg_length itermAdd_wf int_term_value_add_lemma add-member-int_seg2 subtract_wf itermSubtract_wf int_term_value_subtract_lemma lelt_wf select_cons_tl_sq member-less_than select-cons-tl add-subtract-cancel false_wf add_nat_plus length_wf_nat nat_plus_wf nat_plus_properties add-is-int-iff squash_wf true_wf select-cons-hd select_append_front iff_weakening_equal length_zero decidable__equal_int subtype_base_sq int_subtype_base select_cons_tl l_all_cons cons_member list_ind_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesisEquality sqequalRule lambdaEquality functionEquality because_Cache universeEquality natural_numberEquality hypothesis applyEquality functionExtensionality setElimination rename independent_isectElimination productElimination dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll imageElimination isectEquality productEquality applyLambdaEquality setEquality independent_functionElimination baseClosed equalityTransitivity equalitySymmetry addEquality dependent_set_memberEquality imageMemberEquality pointwiseFunctionality promote_hyp baseApply closedConclusion hyp_replacement inlFormation inrFormation

Latex:
\mforall{}[T:Type]
\mforall{}L:T  List
\mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}]
((\mforall{}x:\mBbbN{}||L||.  Dec(P  L[x]))
{}\mRightarrow{}  (\mforall{}i,j:\mBbbN{}||L||.    ((P  L[i])  {}\mRightarrow{}  P  L[j]  supposing  i  <  j))
{}\mRightarrow{}  (\mexists{}L1,L2:T  List
(((L  =  (L1  @  L2))  \mwedge{}  (\mforall{}i:\mBbbN{}||L1||.  (\mneg{}(P  L1[i])))  \mwedge{}  (\mforall{}i:\mBbbN{}||L2||.  (P  L2[i])))
\mwedge{}  (\mforall{}x\mmember{}L.(P  x)  {}\mRightarrow{}  (x  \mmember{}  L2)))))

Date html generated: 2017_10_01-AM-08_34_35
Last ObjectModification: 2017_07_26-PM-04_25_29

Theory : list!

Home Index