Nuprl Lemma : iseg-as-filter

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[sa,sb:T List].
  (∀[dR:T ⟶ T ⟶ 𝔹]
     (sa filter(λx.(dR last(sa));sb) ∈ (T List)) supposing 
        ((¬↑null(sa)) and 
        (∀x,y:T.  (↑(dR y) ⇐⇒ (R y) ∨ (x y ∈ T))))) supposing 
     (Trans(T;a,b.R b) and 
     sorted-by(R;sb) and 
     sa ≤ sb and 
     AntiSym(T;x,y.R y) and 
     Irrefl(T;x,y.R y))


Definitions occuring in Statement :  sorted-by: sorted-by(R;L) iseg: l1 ≤ l2 last: last(L) null: null(as) filter: filter(P;l) list: List irrefl: Irrefl(T;x,y.E[x; y]) anti_sym: AntiSym(T;x,y.R[x; y]) trans: Trans(T;x,y.E[x; y]) assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] prop: all: x:A. B[x] iff: ⇐⇒ Q not: ¬A or: P ∨ Q apply: a 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 all: x:A. B[x] uimplies: supposing a implies:  Q not: ¬A false: False prop: subtype_rel: A ⊆B top: Top so_lambda: λ2x.t[x] so_apply: x[s] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] or: P ∨ Q iff: ⇐⇒ Q rev_implies:  Q and: P ∧ Q guard: {T} irrefl: Irrefl(T;x,y.E[x; y]) set-equal: set-equal(T;x;y) cand: c∧ B
Lemmas referenced :  member-iseg-sorted-by sorted-by-strict-unique filter_wf5 last_wf l_member_wf not_wf assert_wf null_wf3 subtype_rel_list top_wf all_wf iff_wf or_wf equal_wf bool_wf trans_wf sorted-by_wf subtype_rel_dep_function subtype_rel_self set_wf iseg_wf anti_sym_wf irrefl_wf member_filter and_wf sorted-by-filter iseg-sorted-by
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality introduction dependent_functionElimination independent_isectElimination independent_functionElimination lambdaFormation applyEquality voidElimination because_Cache lambdaEquality setElimination rename setEquality isect_memberEquality voidEquality sqequalRule axiomEquality equalityTransitivity equalitySymmetry functionEquality cumulativity instantiate universeEquality addLevel productElimination independent_pairFormation impliesFunctionality andLevelFunctionality unionElimination inrFormation inlFormation

\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[sa,sb:T  List].
    (\mforall{}[dR:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}]
          (sa  =  filter(\mlambda{}x.(dR  x  last(sa));sb))  supposing 
                ((\mneg{}\muparrow{}null(sa))  and 
                (\mforall{}x,y:T.    (\muparrow{}(dR  x  y)  \mLeftarrow{}{}\mRightarrow{}  (R  x  y)  \mvee{}  (x  =  y)))))  supposing 
          (Trans(T;a,b.R  a  b)  and 
          sorted-by(R;sb)  and 
          sa  \mleq{}  sb  and 
          AntiSym(T;x,y.R  x  y)  and 
          Irrefl(T;x,y.R  x  y))

Date html generated: 2016_05_15-PM-03_51_49
Last ObjectModification: 2015_12_27-PM-01_24_14

Theory : general

Home Index