---

Step * 2 1 of Lemma lnk-decls-compatible


1. l1 : IdLnk
2. l2 : IdLnk
3. d1 : tg:Id fp-> Type
4. d2 : tg:Id fp-> Type
5. (l1 = l2 ∈ IdLnk) ⇒ d1 || d2
6. ¬(l1 = l2 ∈ IdLnk)
7. x : Knd@i
8. ↑x ∈ dom(lnk-decl(l1;d1))@i
9. ↑x ∈ dom(lnk-decl(l2;d2))@i
⊢ lnk-decl(l1;d1)(x) = lnk-decl(l2;d2)(x) ∈ Type
BY
{ ((((((((((D (-4))
           THEN Repeat (((Unfolds ``lnk-decl fpf-dom fpf-ap`` (-1)) THEN (Reduce (-1))))
           THEN Repeat (((Unfolds ``lnk-decl fpf-dom fpf-ap`` (-2)) THEN (Reduce (-2))))
           THEN DVar `d1'
           THEN DVar `d2'
           THEN All Reduce
           THEN (RWO "assert-deq-member" (-2)))
          THENA Auto
          )
         THEN (RWO "assert-deq-member" (-1))
         )
        THENA Auto
        )
       THEN (RWO "member_map" (-2))
       )
      THENA Auto
      )
     THEN (Reduce (-2))
     THEN ExRepD
     THEN (RWO "member_map" (-1)))
    THENA Auto
    )
   THEN (Reduce (-1))
   THEN ExRepD) }

1
1. l1 : IdLnk
2. l2 : IdLnk
3. d : Id List
4. d3 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
5. d4 : Id List
6. d5 : tg:{tg:Id| (tg ∈ d4)}  ─→ Type
7. (l1 = l2 ∈ IdLnk) ⇒ <d, d3> || <d4, d5>
8. x : Knd@i
9. y : Id
10. (y ∈ d)
11. x = rcv(l1,y) ∈ Knd
12. y1 : Id
13. (y1 ∈ d4)
14. x = rcv(l2,y1) ∈ Knd
⊢ l1 = l2 ∈ IdLnk

---

Latex:



1.  l1  :  IdLnk
2.  l2  :  IdLnk
3.  d1  :  tg:Id  fp->  Type
4.  d2  :  tg:Id  fp->  Type
5.  (l1  =  l2)  {}\mRightarrow{}  d1  ||  d2
6.  \mneg{}(l1  =  l2)
7.  x  :  Knd@i
8.  \muparrow{}x  \mmember{}  dom(lnk-decl(l1;d1))@i
9.  \muparrow{}x  \mmember{}  dom(lnk-decl(l2;d2))@i
\mvdash{}  lnk-decl(l1;d1)(x)  =  lnk-decl(l2;d2)(x)


By

((((((((((D  (-4))
                  THEN  Repeat  (((Unfolds  ``lnk-decl  fpf-dom  fpf-ap``  (-1))  THEN  (Reduce  (-1))))
                  THEN  Repeat  (((Unfolds  ``lnk-decl  fpf-dom  fpf-ap``  (-2))  THEN  (Reduce  (-2))))
                  THEN  DVar  `d1'
                  THEN  DVar  `d2'
                  THEN  All  Reduce
                  THEN  (RWO  "assert-deq-member"  (-2)))
                THENA  Auto
                )
              THEN  (RWO  "assert-deq-member"  (-1))
              )
            THENA  Auto
            )
          THEN  (RWO  "member\_map"  (-2))
          )
        THENA  Auto
        )
      THEN  (Reduce  (-2))
      THEN  ExRepD
      THEN  (RWO  "member\_map"  (-1)))
    THENA  Auto
    )
  THEN  (Reduce  (-1))
  THEN  ExRepD)

---

Home Index