Nuprl Lemma : l-ordered-decomp

[T:Type]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x:T].
  ∀[L:T List]. (filter(λy.R[y;x];L) filter(λy.(¬bR[y;x]);L)) ∈ (T List) supposing l-ordered(T;x,y.↑R[x;y];L) 
  supposing Trans(T;x,y.↑R[x;y])


Proof




Definitions occuring in Statement :  l-ordered: l-ordered(T;x,y.R[x; y];L) filter: filter(P;l) append: as bs list: List trans: Trans(T;x,y.E[x; y]) bnot: ¬bb assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_lambda: λ2x.t[x] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] prop: all: x:A. B[x] so_apply: x[s] implies:  Q top: Top append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] iff: ⇐⇒ Q and: P ∧ Q true: True bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bnot: ¬bb bfalse: ff squash: T subtype_rel: A ⊆B guard: {T} rev_implies:  Q exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) assert: b false: False not: ¬A trans: Trans(T;x,y.E[x; y])
Lemmas referenced :  list_induction isect_wf l-ordered_wf assert_wf equal_wf list_wf append_wf filter_wf5 l_member_wf bnot_wf filter_nil_lemma list_ind_nil_lemma nil_wf true_wf l-ordered-nil-true equal-wf-base filter_cons_lemma bool_wf eqtt_to_assert list_ind_cons_lemma cons_wf iff_weakening_equal eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot filter_is_nil l_all_iff not_wf l-ordered-cons all_wf trans_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination because_Cache sqequalRule lambdaEquality cumulativity hypothesisEquality applyEquality functionExtensionality hypothesis lambdaFormation setElimination rename setEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality addLevel independent_isectElimination productElimination natural_numberEquality isectEquality baseClosed unionElimination equalityElimination equalityTransitivity equalitySymmetry imageElimination imageMemberEquality dependent_pairFormation promote_hyp instantiate productEquality functionEquality axiomEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:T].
    \mforall{}[L:T  List]
        L  =  (filter(\mlambda{}y.R[y;x];L)  @  filter(\mlambda{}y.(\mneg{}\msubb{}R[y;x]);L))  supposing  l-ordered(T;x,y.\muparrow{}R[x;y];L) 
    supposing  Trans(T;x,y.\muparrow{}R[x;y])



Date html generated: 2018_05_21-PM-07_38_36
Last ObjectModification: 2017_07_26-PM-05_12_50

Theory : general


Home Index