---

Step * 1 2 of Lemma lpath-members-connected


1. p : IdLnk List
2. i : ℕ||p||
3. j : ℕi + 1
4. lpath(p)
⊢ ((||l_interval(p;j;i)|| = 0 ∈ ℤ) ⇒ (source(p[j]) = source(p[i]) ∈ Id))
∧ ((¬(||l_interval(p;j;i)|| = 0 ∈ ℤ))
  ⇒ ((source(p[j]) = source(hd(l_interval(p;j;i))) ∈ Id) ∧ (source(p[i]) = destination(last(l_interval(p;j;i))) ∈ Id)))
BY
{ (Auto THEN AllHyps h.((RWO "length_l_interval" h) THEN Auto') ) }

1
1. p : IdLnk List
2. i : ℕ||p||
3. j : ℕi + 1
4. lpath(p)
5. (i - j) = 0 ∈ ℤ
⊢ source(p[j]) = source(p[i]) ∈ Id

2
1. p : IdLnk List
2. i : ℕ||p||
3. j : ℕi + 1
4. lpath(p)
5. ((i - j) = 0 ∈ ℤ) ⇒ (source(p[j]) = source(p[i]) ∈ Id)
6. ¬((i - j) = 0 ∈ ℤ)
7. source(p[j]) = source(hd(l_interval(p;j;i))) ∈ Id
⊢ source(p[i]) = destination(last(l_interval(p;j;i))) ∈ Id

---

Latex:



1.  p  :  IdLnk  List
2.  i  :  \mBbbN{}||p||
3.  j  :  \mBbbN{}i  +  1
4.  lpath(p)
\mvdash{}  ((||l\_interval(p;j;i)||  =  0)  {}\mRightarrow{}  (source(p[j])  =  source(p[i])))
\mwedge{}  ((\mneg{}(||l\_interval(p;j;i)||  =  0))
    {}\mRightarrow{}  ((source(p[j])  =  source(hd(l\_interval(p;j;i))))
          \mwedge{}  (source(p[i])  =  destination(last(l\_interval(p;j;i))))))


By

(Auto  THEN  AllHyps  h.((RWO  "length\_l\_interval"  h)  THEN  Auto')  )

---

Home Index