---

Step * of Lemma assert-graph-rcvset

∀a:Id ─→ Id ─→ Id. ∀b:Id. ∀S:Id List. ∀G:Graph(S). ∀k:Knd.
  (↑graph-rcvset(a;b;S;G;k) ⇐⇒ ∃i,j:Id. ((i ∈ S) ∧ (j ∈ S) ∧ (i─→j)∈G ∧ (k = rcv((link(a i j) from i to j),b) ∈ Knd)))
BY
{ Auto }

1
1. a : Id ─→ Id ─→ Id@i
2. b : Id@i
3. S : Id List@i
4. G : Graph(S)@i
5. k : Knd@i
6. ↑graph-rcvset(a;b;S;G;k)@i
⊢ ∃i,j:Id. ((i ∈ S) ∧ (j ∈ S) ∧ (i─→j)∈G ∧ (k = rcv((link(a i j) from i to j),b) ∈ Knd))

2
1. a : Id ─→ Id ─→ Id@i
2. b : Id@i
3. S : Id List@i
4. G : Graph(S)@i
5. k : Knd@i
6. ∃i,j:Id. ((i ∈ S) ∧ (j ∈ S) ∧ (i─→j)∈G ∧ (k = rcv((link(a i j) from i to j),b) ∈ Knd))@i
⊢ ↑graph-rcvset(a;b;S;G;k)

---

Latex:


\mforall{}a:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Id.  \mforall{}b:Id.  \mforall{}S:Id  List.  \mforall{}G:Graph(S).  \mforall{}k:Knd.
    (\muparrow{}graph-rcvset(a;b;S;G;k)
    \mLeftarrow{}{}\mRightarrow{}  \mexists{}i,j:Id.  ((i  \mmember{}  S)  \mwedge{}  (j  \mmember{}  S)  \mwedge{}  (i{}\mrightarrow{}j)\mmember{}G  \mwedge{}  (k  =  rcv((link(a  i  j)  from  i  to  j),b))))


By

Auto

---

Home Index