---

Step * of Lemma assert-hasloc

∀[i:Id]. ∀[k:Knd].  uiff(↑hasloc(k;i);destination(lnk(k)) = i ∈ Id supposing ↑isrcv(k))
BY
{ (Auto
   THEN (DVar `k' THEN Try ((DVar `x' THEN DVar `x1')))
   THEN All (RepUR ``isrcv hasloc lnk ldst``)⋅
   THEN Try (Trivial)
   THEN (All (RW assert_pushdownC) THENA Auto)) }

1
1. i : Id
2. x3 : Id
3. x4 : Id × Id
4. x2 : Id
5. ¬¬((fst(x4)) = i ∈ Id)
6. True
⊢ (fst(x4)) = i ∈ Id

2
1. i : Id
2. x3 : Id
3. x4 : Id × Id
4. x2 : Id
5. (fst(x4)) = i ∈ Id supposing True
⊢ ¬¬((fst(x4)) = i ∈ Id)

---

Latex:


\mforall{}[i:Id].  \mforall{}[k:Knd].    uiff(\muparrow{}hasloc(k;i);destination(lnk(k))  =  i  supposing  \muparrow{}isrcv(k))


By

(Auto
  THEN  (DVar  `k'  THEN  Try  ((DVar  `x'  THEN  DVar  `x1')))
  THEN  All  (RepUR  ``isrcv  hasloc  lnk  ldst``)\mcdot{}
  THEN  Try  (Trivial)
  THEN  (All  (RW  assert\_pushdownC)  THENA  Auto))

---

Home Index