### 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|| ≥ ))])))

Proof

Definitions occuring in Statement :  last: last(L) select: L[n] length: ||as|| null: null(as) append: as bs hd: hd(l) list: List int_seg: {i..j-} assert: b decidable: Dec(P) uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s1;s2] ge: i ≥  all: x:A. B[x] sq_exists: x:A [B[x]] not: ¬A implies:  Q and: P ∧ Q function: x:A ⟶ B[x] spread: spread def product: x:A × B[x] subtract: m add: m natural_number: \$n universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  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: 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 ⊆B ge: i ≥  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: λ2y.t[x; y] subtract: m assert: b ifthenelse: if then else fi  btrue: tt cand: 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: ⇐⇒ Q rev_implies:  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