---

Step * 1 of Lemma make-lg_wf_dag

.....set predicate..... 
1. T : Type
2. L : T List
⊢ is-dag(make-lg(L))
BY
{ (RepUR ``is-dag make-lg lg-size lg-edge lg-in-edges`` 0
   THEN (RWO "length-map-sq" 0 THENA Auto)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN ((RWO "select-map" 0 THENM Reduce 0) THENA Auto)
   THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  T  :  Type
2.  L  :  T  List
\mvdash{}  is-dag(make-lg(L))


By

---

Latex:
(RepUR  ``is-dag  make-lg  lg-size  lg-edge  lg-in-edges``  0
  THEN  (RWO  "length-map-sq"  0  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ((RWO  "select-map"  0  THENM  Reduce  0)  THENA  Auto)
  THEN  Auto)

---

Home Index