Step
*
of Lemma
l-ordered-is-sorted-by
∀[T:Type]. ∀R:T ⟶ T ⟶ ℙ. ∀L:T List. (l-ordered(T;x,y.R[x;y];L)
⇐⇒ sorted-by(λx,y. R[x;y];L))
BY
{ xxx(RepUR ``l-ordered sorted-by`` 0
THEN Auto
THEN Try (Complete ((BackThruSomeHyp THEN BLemma `l_before_select` THEN Auto)))
THEN RepUR ``l_before sublist`` (-1)
THEN ExRepD
THEN InstHyp [⌜f 1⌝;⌜f 0⌝] (-6)⋅
THEN Auto
THEN RWO "-2<" (-1)
THEN Auto
THEN Reduce 0
THEN RWO "-2<" 0
THEN Reduce 0
THEN Auto)xxx }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}. \mforall{}L:T List. (l-ordered(T;x,y.R[x;y];L) \mLeftarrow{}{}\mRightarrow{} sorted-by(\mlambda{}x,y. R[x;y];L))
By
Latex:
xxx(RepUR ``l-ordered sorted-by`` 0
THEN Auto
THEN Try (Complete ((BackThruSomeHyp THEN BLemma `l\_before\_select` THEN Auto)))
THEN RepUR ``l\_before sublist`` (-1)
THEN ExRepD
THEN InstHyp [\mkleeneopen{}f 1\mkleeneclose{};\mkleeneopen{}f 0\mkleeneclose{}] (-6)\mcdot{}
THEN Auto
THEN RWO "-2<" (-1)
THEN Auto
THEN Reduce 0
THEN RWO "-2<" 0
THEN Reduce 0
THEN Auto)xxx
Home
Index