---

Step * 1 of Lemma sorted-by-append1


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)
BY
{ ((Reduce 0 THEN (InstHyp [⌜x⌝;⌜rev(L)⌝] 6⋅ THENA Auto))
   THEN Reduce (-1)
   THEN (RepeatFor 2 (ParallelLast) THEN (RWW "l_all_iff" (-1) THENA Auto) THEN (RWW "l_all_iff" 0 THENA Auto))
   THEN RepeatFor 2 ((ParallelLast
                      THEN Try (Complete ((((Reduce 0 THEN RWW "length-append length-reverse" 0 THEN Reduce 0)
                                            THEN Reduce (-1)
                                            THEN RWW "length-append length-reverse" (-1)
                                            THEN Reduce (-1))
                                           THEN Auto
                                           )))
                      ))⋅
   THEN (Try ((BLemma `member-reverse`  THEN Complete (Auto)))
         THEN Try ((FLemma `member-reverse` [-1] THEN Auto))
         THEN NthHypSq (-1)
         THEN Subst' rev([x]) ~ [x] 0
         THEN Reduce 0
         THEN Auto
         THEN SymbComp 0⋅
         THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  x  :  T
4.  L  :  T  List
5.  \mforall{}L:T  List.  (sorted-by(R;L)  \mLeftarrow{}{}\mRightarrow{}  sorted-by(\mlambda{}x,y.  (R  y  x);rev(L)))
6.  \mforall{}x:T.  \mforall{}L:T  List.
          (sorted-by(\mlambda{}x,y.  (R  y  x);[x  /  L])  \mLeftarrow{}{}\mRightarrow{}  sorted-by(\mlambda{}x,y.  (R  y  x);L)  \mwedge{}  (\mforall{}z\mmember{}L.(\mlambda{}x,y.  (R  y  x))  x  z))
\mvdash{}  sorted-by(\mlambda{}x,y.  (R  y  x);rev([x])  @  rev(L))  \mLeftarrow{}{}\mRightarrow{}  sorted-by(\mlambda{}x,y.  (R  y  x);rev(L))  \mwedge{}  (\mforall{}z\mmember{}L.R  z  x)


By

---

Latex:
((Reduce  0  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}rev(L)\mkleeneclose{}]  6\mcdot{}  THENA  Auto))
  THEN  Reduce  (-1)
  THEN  (RepeatFor  2  (ParallelLast)
              THEN  (RWW  "l\_all\_iff"  (-1)  THENA  Auto)
              THEN  (RWW  "l\_all\_iff"  0  THENA  Auto))
  THEN  RepeatFor  2  ((ParallelLast
                                        THEN  Try  (Complete  ((((Reduce  0
                                                                                      THEN  RWW  "length-append  length-reverse"  0
                                                                                      THEN  Reduce  0)
                                                                                    THEN  Reduce  (-1)
                                                                                    THEN  RWW  "length-append  length-reverse"  (-1)
                                                                                    THEN  Reduce  (-1))
                                                                                  THEN  Auto
                                                                                  )))
                                        ))\mcdot{}
  THEN  (Try  ((BLemma  `member-reverse`    THEN  Complete  (Auto)))
              THEN  Try  ((FLemma  `member-reverse`  [-1]  THEN  Auto))
              THEN  NthHypSq  (-1)
              THEN  Subst'  rev([x])  \msim{}  [x]  0
              THEN  Reduce  0
              THEN  Auto
              THEN  SymbComp  0\mcdot{}
              THEN  Auto)\mcdot{})

---

Home Index