---

Step * of Lemma assert-has-src

∀[i:Id]. ∀[k:Knd].  uiff(↑has-src(i;k);(↑isrcv(k)) c∧ (source(lnk(k)) = i ∈ Id))
BY
{ Auto⋅ }

1
1. i : Id
2. k : Knd
3. ↑has-src(i;k)
⊢ ↑isrcv(k)

2
1. i : Id
2. k : Knd
3. ↑has-src(i;k)
⊢ source(lnk(k)) = i ∈ Id

3
1. i : Id
2. k : Knd
3. (↑isrcv(k)) c∧ (source(lnk(k)) = i ∈ Id)
⊢ ↑has-src(i;k)

---

Latex:


\mforall{}[i:Id].  \mforall{}[k:Knd].    uiff(\muparrow{}has-src(i;k);(\muparrow{}isrcv(k))  c\mwedge{}  (source(lnk(k))  =  i))


By

Auto\mcdot{}

---

Home Index