---

Step * of Lemma es-decl-set-join_wf

∀[dd1,dd2:DeclSet].  (es-decl-set-join(dd1;dd2) ∈ DeclSet)
BY
{ (Auto
   THEN RepeatFor 2 (D -2)
   THEN RepeatFor 2 (D -1)
   THEN RepUR ``es-decl-set-join es-decl-set`` 0
   THEN (MemCD THENL [ Auto; MemCD; Auto⋅])
   THEN (MemCD THENL [Id ; Auto⋅])
   THEN D -1
   THEN (RWW "member-remove-repeats member_append" (-1) THENA Auto)
   THEN D (-1)
   THEN RepeatFor 2 (AutoSplit)
   THEN (GenConclTerm ⌜fpf-domain(d3 i)⌝⋅ THENA Auto)
   THEN GenConclTerm ⌜fpf-domain(d6 i)⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[dd1,dd2:DeclSet].    (es-decl-set-join(dd1;dd2)  \mmember{}  DeclSet)


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -2)
  THEN  RepeatFor  2  (D  -1)
  THEN  RepUR  ``es-decl-set-join  es-decl-set``  0
  THEN  (MemCD  THENL  [  Auto;  MemCD;  Auto\mcdot{}])
  THEN  (MemCD  THENL  [Id  ;  Auto\mcdot{}])
  THEN  D  -1
  THEN  (RWW  "member-remove-repeats  member\_append"  (-1)  THENA  Auto)
  THEN  D  (-1)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  (GenConclTerm  \mkleeneopen{}fpf-domain(d3  i)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  GenConclTerm  \mkleeneopen{}fpf-domain(d6  i)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index