---

Step * of Lemma sorted-by-append1

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x:T. ∀L:T List.  (sorted-by(R;L @ [x]) ⇐⇒ sorted-by(R;L) ∧ (∀z∈L.R z x))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN (InstLemma `sorted-by-reverse` [⌜T⌝;⌜R⌝]⋅ THENA Auto)
          THEN (InstLemma `sorted-by-cons` [⌜T⌝;⌜λx,y. (R y x)⌝]⋅ THENA Auto)
          THEN (RWO "5" 0 THENA Auto)
          THEN (RWO "reverse-append" 0 THENA Auto)) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. L : T List
5. ∀L:T List. (sorted-by(R;L) ⇐⇒ sorted-by(λx,y. (R y x);rev(L)))
6. ∀x:T. ∀L:T List.  (sorted-by(λx,y. (R y x);[x / L]) ⇐⇒ sorted-by(λx,y. (R y x);L) ∧ (∀z∈L.(λx,y. (R y x)) x z))
⊢ sorted-by(λx,y. (R y x);rev([x]) @ rev(L)) ⇐⇒ sorted-by(λx,y. (R y x);rev(L)) ∧ (∀z∈L.R z x)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}x:T.  \mforall{}L:T  List.    (sorted-by(R;L  @  [x])  \mLeftarrow{}{}\mRightarrow{}  sorted-by(R;L)  \mwedge{}  (\mforall{}z\mmember{}L.R  z  x))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  (InstLemma  `sorted-by-reverse`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (InstLemma  `sorted-by-cons`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  (R  y  x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (RWO  "5"  0  THENA  Auto)
                THEN  (RWO  "reverse-append"  0  THENA  Auto))

---

Home Index