---

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


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)
BY
{ (RWO "fpf-join-ap-sq" 0 THEN Auto) }

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)
14. (k ∈ fpf-domain(graph-rcvs(S;G;a;b;i) |-fpf-> T ⊕ d3 i))@i
15. ↑isrcv(k)@i
16. tag(k) = b ∈ Id@i
⊢ if k ∈ dom(graph-rcvs(S;G;a;b;i) |-fpf-> T) then graph-rcvs(S;G;a;b;i) |-fpf-> T(k) else d3 i(k) fi  = T ∈ Type

---

Latex:



1.  S  :  Id  List@i'
2.  d2  :  \{i:Id|  (i  \mmember{}  S)\}    {}\mrightarrow{}  x:Id  fp->  Type@i'
3.  d3  :  i:\{i:Id|  (i  \mmember{}  S)\}    {}\mrightarrow{}  k:\{k:Knd|  \muparrow{}hasloc(k;i)\}    fp->  Type@i'
4.  G  :  Graph(S)@i
5.  T  :  Type@i'
6.  a  :  Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Id@i
7.  b  :  Id@i
8.  \mforall{}i:Id
          ((i  \mmember{}  S)
          {}\mRightarrow{}  (\mforall{}k:Knd.  ((k  \mmember{}  fpf-domain(d3  i))  {}\mRightarrow{}  (\muparrow{}isrcv(k))  {}\mRightarrow{}  (tag(k)  =  b)  {}\mRightarrow{}  (d3  i(k)  =  T))))@i'
9.  i  :  Id@i
10.  (i  \mmember{}  S)@i
11.  \mforall{}k:Knd.  ((k  \mmember{}  fpf-domain(d3  i))  {}\mRightarrow{}  (\muparrow{}isrcv(k))  {}\mRightarrow{}  (tag(k)  =  b)  {}\mRightarrow{}  (d3  i(k)  =  T))
12.  k  :  Knd@i
13.  (k  \mmember{}  fpf-domain(d3  i))  {}\mRightarrow{}  (\muparrow{}isrcv(k))  {}\mRightarrow{}  (tag(k)  =  b)  {}\mRightarrow{}  (d3  i(k)  =  T)
\mvdash{}  (k  \mmember{}  fpf-domain(graph-rcvs(S;G;a;b;i)  |-fpf->  T  \moplus{}  d3  i))
{}\mRightarrow{}  (\muparrow{}isrcv(k))
{}\mRightarrow{}  (tag(k)  =  b)
{}\mRightarrow{}  (graph-rcvs(S;G;a;b;i)  |-fpf->  T  \moplus{}  d3  i(k)  =  T)


By

(RWO  "fpf-join-ap-sq"  0  THEN  Auto)

---

Home Index