### Nuprl Lemma : iseg-sorted-by

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀sa,sb:T List.  (sa ≤ sb `` sorted-by(R;sb) `` sorted-by(R;sa))`

Proof

Definitions occuring in Statement :  sorted-by: `sorted-by(R;L)` iseg: `l1 ≤ l2` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  sublist-sorted-by iseg_wf list_wf sublist_iseg
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation dependent_functionElimination independent_functionElimination functionEquality cumulativity universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}sa,sb:T  List.    (sa  \mleq{}  sb  {}\mRightarrow{}  sorted-by(R;sb)  {}\mRightarrow{}  sorted-by(R;sa))

Date html generated: 2016_05_14-PM-01_48_18
Last ObjectModification: 2015_12_26-PM-05_34_57

Theory : list_1

Home Index