---

Step * of Lemma add-graph-decls_wf

∀[dd:DeclSet]. ∀[G:Graph(|dd|)]. ∀[T:Type]. ∀[a:Id ─→ Id ─→ Id]. ∀[b:Id].  (add-graph-decls(dd;G;T;a;b) ∈ DeclSet)
BY
{ ((D 0 THENA Auto) THEN RepeatFor 2 (D -1) THEN RepUR ``es-decl-set add-graph-decls es-decl-set-domain`` 0 THEN Auto) }

---

Latex:


\mforall{}[dd:DeclSet].  \mforall{}[G:Graph(|dd|)].  \mforall{}[T:Type].  \mforall{}[a:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Id].  \mforall{}[b:Id].
    (add-graph-decls(dd;G;T;a;b)  \mmember{}  DeclSet)


By

((D  0  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  RepUR  ``es-decl-set  add-graph-decls  es-decl-set-domain``  0
  THEN  Auto)

---

Home Index