---

Step * of Lemma quicksort-int-null

∀[L:ℤ List]. uiff(↑null(quicksort-int(L));↑null(L))
BY
{ (Auto
   THEN Repeat (AllPushDown)
   THEN Try ((FLemma `length_of_null_list` [-1]
              THEN Auto
              THEN (RWO "quicksort-int-length<" (-1) THENA Auto)
              THEN RWO "length_zero" (-1)
              THEN Auto))
   THEN RWO "-1" 0
   THEN Auto
   THEN RWO "quicksort-int-nil" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  uiff(\muparrow{}null(quicksort-int(L));\muparrow{}null(L))


By

---

Latex:
(Auto
  THEN  Repeat  (AllPushDown)
  THEN  Try  ((FLemma  `length\_of\_null\_list`  [-1]
                        THEN  Auto
                        THEN  (RWO  "quicksort-int-length<"  (-1)  THENA  Auto)
                        THEN  RWO  "length\_zero"  (-1)
                        THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  RWO  "quicksort-int-nil"  0
  THEN  Auto)

---

Home Index