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