### Nuprl Lemma : split-at-first-rel

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].`
`  ((∀x,y:T.  Dec(R[x;y]))`
`  `` (∀L:T List`
`        (∃XY:T List × (T List) [let X,Y = XY `
`                                in (L = (X @ Y) ∈ (T List))`
`                                   ∧ (∀i:ℕ||X|| - 1. R[X[i];X[i + 1]])`
`                                   ∧ ((¬↑null(L)) `` ((¬↑null(X)) ∧ ¬R[last(X);hd(Y)] supposing ||Y|| ≥ 1 ))])))`

Proof

Definitions occuring in Statement :  last: `last(L)` select: `L[n]` length: `||as||` null: `null(as)` append: `as @ bs` hd: `hd(l)` list: `T List` int_seg: `{i..j-}` assert: `↑b` decidable: `Dec(P)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` ge: `i ≥ j ` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` spread: spread def product: `x:A × B[x]` subtract: `n - m` add: `n + m` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` top: `Top` so_apply: `x[s1;s2]` int_seg: `{i..j-}` uimplies: `b supposing a` guard: `{T}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` uiff: `uiff(P;Q)` so_apply: `x[s]` subtype_rel: `A ⊆r B` ge: `i ≥ j ` sq_exists: `∃x:A [B[x]]` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` select: `L[n]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` subtract: `n - m` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` cand: `A c∧ B` true: `True` less_than: `a < b` squash: `↓T` cons: `[a / b]` bfalse: `ff` le: `A ≤ B` less_than': `less_than'(a;b)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` label: `...\$L... t` sq_type: `SQType(T)`
Lemmas referenced :  list_induction sq_exists_wf list_wf equal_wf append_wf length_wf length-append istype-void all_wf int_seg_wf subtract_wf select_wf int_seg_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int 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 add-is-int-iff intformless_wf itermSubtract_wf int_formula_prop_less_lemma int_term_value_subtract_lemma false_wf itermAdd_wf int_term_value_add_lemma not_wf assert_wf null_wf3 subtype_rel_list top_wf istype-universe ge_wf last_wf hd_wf decidable_wf nil_wf list_ind_nil_lemma length_of_nil_lemma stuck-spread istype-base null_nil_lemma true_wf subtract-is-int-iff list-cases product_subtype_list cons_wf list_ind_cons_lemma length_of_cons_lemma null_cons_lemma squash_wf subtype_rel_self iff_weakening_equal last_cons assert_elim bfalse_wf btrue_neq_bfalse decidable__equal_int subtype_base_sq int_subtype_base intformeq_wf int_formula_prop_eq_lemma reduce_hd_cons_lemma reduce_tl_cons_lemma tl_wf length_cons_ge_one le_wf less_than_wf select-cons-tl subtract-add-cancel general_arith_equation1 add-subtract-cancel last_singleton
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality_alt productEquality hypothesis because_Cache productElimination applyLambdaEquality isect_memberEquality_alt voidElimination natural_numberEquality applyEquality setElimination rename independent_isectElimination dependent_functionElimination unionElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality independent_pairFormation universeIsType pointwiseFunctionality equalityTransitivity equalitySymmetry promote_hyp baseApply closedConclusion baseClosed addEquality functionEquality isectEquality productIsType inhabitedIsType spreadEquality functionIsType universeEquality dependent_set_memberFormation_alt independent_pairEquality minusEquality equalityIsType2 imageElimination hypothesis_subsumption functionIsTypeImplies equalityIsType1 isectIsType imageMemberEquality instantiate cumulativity intEquality hyp_replacement dependent_set_memberEquality_alt

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}x,y:T.    Dec(R[x;y]))
{}\mRightarrow{}  (\mforall{}L:T  List
(\mexists{}XY:T  List  \mtimes{}  (T  List)  [let  X,Y  =  XY
in  (L  =  (X  @  Y))
\mwedge{}  (\mforall{}i:\mBbbN{}||X||  -  1.  R[X[i];X[i  +  1]])
\mwedge{}  ((\mneg{}\muparrow{}null(L))
{}\mRightarrow{}  ((\mneg{}\muparrow{}null(X))  \mwedge{}  \mneg{}R[last(X);hd(Y)]  supposing  ||Y||  \mgeq{}  1  ))])))

Date html generated: 2019_10_15-AM-11_13_50
Last ObjectModification: 2018_10_10-PM-02_08_48

Theory : general

Home Index