### Nuprl Lemma : iseg-remainder-as-filter

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[sa,s,sb:T List].`
`  (∀[dR:T ⟶ T ⟶ 𝔹]`
`     (sb = filter(dR last(sa);s) ∈ (T List)) supposing ((¬↑null(sa)) and (∀x,y:T.  (↑(dR x y) `⇐⇒` R x y)))) supposing `
`     (Trans(T;a,b.R a b) and `
`     sorted-by(R;s) and `
`     (s = (sa @ sb) ∈ (T List)) 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)` last: `last(L)` null: `null(as)` filter: `filter(P;l)` append: `as @ bs` 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` apply: `f a` 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` iseg: `l1 ≤ l2` exists: `∃x:A. B[x]` 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]` not: `¬A` false: `False` guard: `{T}` irrefl: `Irrefl(T;x,y.E[x; y])` set-equal: `set-equal(T;x;y)` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` cand: `A c∧ B` or: `P ∨ Q` l_member: `(x ∈ l)` squash: `↓T` int_seg: `{i..j-}` nat: `ℕ` lelt: `i ≤ j < k` ge: `i ≥ j ` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` less_than: `a < b` true: `True` subtract: `n - m` sq_type: `SQType(T)` uiff: `uiff(P;Q)` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` cons: `[a / b]` bfalse: `ff` le: `A ≤ B` less_than': `less_than'(a;b)` last: `last(L)` sorted-by: `sorted-by(R;L)` anti_sym: `AntiSym(T;x,y.R[x; y])`
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination independent_isectElimination independent_functionElimination dependent_pairFormation cumulativity applyEquality lambdaEquality isect_memberEquality voidElimination voidEquality because_Cache sqequalRule axiomEquality equalityTransitivity equalitySymmetry functionExtensionality functionEquality instantiate universeEquality setEquality setElimination rename lambdaFormation addLevel productElimination independent_pairFormation impliesFunctionality andLevelFunctionality productEquality inrFormation hyp_replacement applyLambdaEquality dependent_set_memberEquality imageElimination addEquality unionElimination natural_numberEquality int_eqEquality intEquality computeAll imageMemberEquality baseClosed pointwiseFunctionality promote_hyp baseApply closedConclusion hypothesis_subsumption minusEquality

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

Date html generated: 2018_05_21-PM-06_47_12
Last ObjectModification: 2017_07_26-PM-04_56_33

Theory : general

Home Index