### Nuprl Lemma : sorted-cons

`∀[T:Type]. ∀[x:T]. ∀[L:T List].  uiff(sorted([x / L]);sorted(L) ∧ (∀z∈L.x ≤ z)) supposing T ⊆r ℤ`

Proof

Definitions occuring in Statement :  l_all: `(∀x∈L.P[x])` sorted: `sorted(L)` cons: `[a / b]` list: `T List` uiff: `uiff(P;Q)` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` le: `A ≤ B` and: `P ∧ Q` int: `ℤ` universe: `Type`
Definitions unfolded in proof :  sorted: `sorted(L)` all: `∀x:A. B[x]` member: `t ∈ T` top: `Top` uall: `∀[x:A]. B[x]` uimplies: `b supposing a` uiff: `uiff(P;Q)` and: `P ∧ Q` int_seg: `{i..j-}` le: `A ≤ B` not: `¬A` implies: `P `` Q` false: `False` subtype_rel: `A ⊆r B` lelt: `i ≤ j < k` guard: `{T}` prop: `ℙ` l_all: `(∀x∈L.P[x])` sq_stable: `SqStable(P)` squash: `↓T` so_lambda: `λ2x.t[x]` exists: `∃x:A. B[x]` nat: `ℕ` so_apply: `x[s]` subtract: `n - m` nat_plus: `ℕ+` less_than: `a < b` less_than': `less_than'(a;b)` true: `True` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` select: `L[n]` cons: `[a / b]` sq_type: `SQType(T)`
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis isect_memberFormation independent_pairFormation lambdaFormation isectElimination natural_numberEquality setElimination rename hypothesisEquality cumulativity productElimination independent_pairEquality lambdaEquality because_Cache applyEquality independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry independent_functionElimination imageMemberEquality baseClosed imageElimination addEquality dependent_pairFormation sqequalIntensionalEquality intEquality promote_hyp productEquality setEquality universeEquality multiplyEquality minusEquality dependent_set_memberEquality unionElimination instantiate

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[L:T  List].    uiff(sorted([x  /  L]);sorted(L)  \mwedge{}  (\mforall{}z\mmember{}L.x  \mleq{}  z))  supposing  T  \msubseteq{}r  \mBbbZ{}

Date html generated: 2017_04_14-AM-08_44_06
Last ObjectModification: 2017_02_27-PM-03_32_54

Theory : list_0

Home Index