---

Step * of Lemma add-graph-decls-declares-tag

∀dd:DeclSet. ∀G:Graph(|dd|). ∀T:Type. ∀a:Id ─→ Id ─→ Id. ∀b:Id.
  (es-decl-set-declares-tag{i:l}(dd;b;T) ⇒ es-decl-set-declares-tag{i:l}(add-graph-decls(dd;G;T;a;b);b;T))
BY
{ (Auto
   THEN D 1
   THEN D 2
   THEN All (RepUR ``es-decl-set-domain``)
   THEN RepUR ``es-decl-set-declares-tag`` -1
   THEN RepUR ``es-decl-set-declares-tag add-graph-decls`` 0
   THEN RepeatFor 3 (ParallelLast)) }

1
1. S : Id List@i'
2. d2 : {i:Id| (i ∈ S)}  ─→ x:Id fp-> Type@i'
3. d3 : i:{i:Id| (i ∈ S)}  ─→ k:{k:Knd| ↑hasloc(k;i)}  fp-> Type@i'
4. G : Graph(S)@i
5. T : Type@i'
6. a : Id ─→ Id ─→ Id@i
7. b : Id@i
8. ∀i:Id. ((i ∈ S) ⇒ (∀k:Knd. ((k ∈ fpf-domain(d3 i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (d3 i(k) = T ∈ Type))))@i'
9. i : Id@i
10. (i ∈ S)@i
11. ∀k:Knd. ((k ∈ fpf-domain(d3 i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (d3 i(k) = T ∈ Type))
12. k : Knd@i
13. (k ∈ fpf-domain(d3 i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (d3 i(k) = T ∈ Type)
⊢ (k ∈ fpf-domain(graph-rcvs(S;G;a;b;i) |-fpf-> T ⊕ d3 i))
⇒ (↑isrcv(k))
⇒ (tag(k) = b ∈ Id)
⇒ (graph-rcvs(S;G;a;b;i) |-fpf-> T ⊕ d3 i(k) = T ∈ Type)

---

Latex:


\mforall{}dd:DeclSet.  \mforall{}G:Graph(|dd|).  \mforall{}T:Type.  \mforall{}a:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Id.  \mforall{}b:Id.
    (es-decl-set-declares-tag\{i:l\}(dd;b;T)
    {}\mRightarrow{}  es-decl-set-declares-tag\{i:l\}(add-graph-decls(dd;G;T;a;b);b;T))


By

(Auto
  THEN  D  1
  THEN  D  2
  THEN  All  (RepUR  ``es-decl-set-domain``)
  THEN  RepUR  ``es-decl-set-declares-tag``  -1
  THEN  RepUR  ``es-decl-set-declares-tag  add-graph-decls``  0
  THEN  RepeatFor  3  (ParallelLast))

---

Home Index