Step
*
of Lemma
lpath_cons
∀[l:IdLnk]. ∀[p:IdLnk List].
uiff(lpath([l / p]);lpath(p)
∧ (destination(l) = source(hd(p)) ∈ Id) ∧ (¬(hd(p) = lnk-inv(l) ∈ IdLnk)) supposing ¬(||p|| = 0 ∈ ℤ))
BY
{ Auto' }
1
1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
⊢ lpath(p)
2
1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
4. ¬(||p|| = 0 ∈ ℤ)
⊢ destination(l) = source(hd(p)) ∈ Id
3
1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
4. ¬(||p|| = 0 ∈ ℤ)
⊢ ¬(hd(p) = lnk-inv(l) ∈ IdLnk)
4
1. l : IdLnk
2. p : IdLnk List
3. lpath(p)
4. (destination(l) = source(hd(p)) ∈ Id) ∧ (¬(hd(p) = lnk-inv(l) ∈ IdLnk)) supposing ¬(||p|| = 0 ∈ ℤ)
⊢ lpath([l / p])
Latex:
\mforall{}[l:IdLnk]. \mforall{}[p:IdLnk List].
uiff(lpath([l / p]);lpath(p)
\mwedge{} (destination(l) = source(hd(p))) \mwedge{} (\mneg{}(hd(p) = lnk-inv(l))) supposing \mneg{}(||p|| = 0))
By
Auto'
Home
Index