### Nuprl Lemma : sorted-by-eq-rels

`∀T:Type. ∀R1,R2:T ⟶ T ⟶ ℙ. ∀L:T List.`
`  ((∀x∈L.(∀y∈L.R1[x;y] `⇐⇒` R2[x;y])) `` sorted-by(λx,y. R1[x;y];L) `` sorted-by(λx,y. R2[x;y];L))`

Proof

Definitions occuring in Statement :  sorted-by: `sorted-by(R;L)` l_all: `(∀x∈L.P[x])` list: `T List` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  l-ordered-is-sorted-by l-ordered-eq-rels sorted-by_wf l_member_wf l_all_wf2 iff_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination sqequalRule lambdaEquality applyEquality hypothesis productElimination independent_pairFormation independent_functionElimination because_Cache setElimination rename setEquality functionEquality cumulativity universeEquality

Latex:
\mforall{}T:Type.  \mforall{}R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}L:T  List.
((\mforall{}x\mmember{}L.(\mforall{}y\mmember{}L.R1[x;y]  \mLeftarrow{}{}\mRightarrow{}  R2[x;y]))  {}\mRightarrow{}  sorted-by(\mlambda{}x,y.  R1[x;y];L)  {}\mRightarrow{}  sorted-by(\mlambda{}x,y.  R2[x;y];L))

Date html generated: 2016_05_15-PM-04_38_16
Last ObjectModification: 2015_12_27-PM-02_43_06

Theory : general

Home Index