Nuprl Lemma : iseg-as-filter

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


Proof



Definitions occuring in Statement :  sorted-by: sorted-by(R;L),  iseg: l1 ≤ l2,  last: last(L),  null: null(as),  filter: filter(P;l),  list: T 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: b supposing a,  uall: ∀[x:A]. B[x],  prop: ℙ,  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  not: ¬A,  or: P ∨ Q,  apply: f a,  lambda: λx.A[x],  function: x:A ⟶ B[x],  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  all: ∀x:A. B[x],  uimplies: b supposing a,  implies: P ⇒ Q,  not: ¬A,  false: False,  prop: ℙ,  subtype_rel: A ⊆r B,  top: Top,  so_lambda: λ2x.t[x],  so_apply: x[s],  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  or: P ∨ Q,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  and: P ∧ Q,  guard: {T},  irrefl: Irrefl(T;x,y.E[x; y]),  set-equal: set-equal(T;x;y),  cand: A 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
Latex:
\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