### Nuprl Lemma : select-filter-from-upto-order-preserving

`∀[n,m:ℤ]. ∀[P:{n..m-} ⟶ 𝔹]. ∀[i,j:ℕ||filter(P;[n, m))||].  uiff(i < j;filter(P;[n, m))[i] < filter(P;[n, m))[j])`

Proof

Definitions occuring in Statement :  from-upto: `[n, m)` select: `L[n]` length: `||as||` filter: `filter(P;l)` int_seg: `{i..j-}` bool: `𝔹` less_than: `a < b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` member: `t ∈ T` implies: `P `` Q` prop: `ℙ` nat: `ℕ` subtype_rel: `A ⊆r B` so_apply: `x[s]` uimplies: `b supposing a` all: `∀x:A. B[x]` istype: `istype(T)` int_seg: `{i..j-}` guard: `{T}` ge: `i ≥ j ` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` less_than: `a < b` squash: `↓T` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` from-upto: `[n, m)` cand: `A c∧ B` le: `A ≤ B` uiff: `uiff(P;Q)` subtract: `n - m` less_than': `less_than'(a;b)` true: `True` select: `L[n]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` bool: `𝔹` unit: `Unit` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` has-value: `(a)↓` sq_type: `SQType(T)`
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin sqequalRule Error :lambdaEquality_alt,  closedConclusion intEquality because_Cache functionEquality hypothesisEquality hypothesis setElimination rename natural_numberEquality applyEquality Error :universeIsType,  setEquality Error :setIsType,  independent_isectElimination Error :lambdaFormation_alt,  productElimination dependent_functionElimination Error :inhabitedIsType,  equalityTransitivity equalitySymmetry unionElimination imageElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination independent_pairFormation Error :functionIsType,  Error :productIsType,  baseApply baseClosed Error :dependent_set_memberEquality_alt,  addEquality minusEquality multiplyEquality equalityElimination Error :equalityIstype,  callbyvalueReduce pointwiseFunctionality promote_hyp applyLambdaEquality lambdaEquality productEquality lambdaFormation dependent_pairFormation isect_memberEquality voidEquality computeAll isect_memberFormation independent_pairEquality dependent_set_memberEquality instantiate cumulativity

Latex:
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[P:\{n..m\msupminus{}\}  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[i,j:\mBbbN{}||filter(P;[n,  m))||].
uiff(i  <  j;filter(P;[n,  m))[i]  <  filter(P;[n,  m))[j])

Date html generated: 2019_06_20-PM-01_34_24
Last ObjectModification: 2019_01_21-PM-01_56_58

Theory : list_1

Home Index