---

Step * 2 of Lemma rel_path-append

.....antecedent..... 
1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. L : (a:A × b:A × (R a b)) List
4. ∀[x,y:A]. ∀[L:(a:A × b:A × (R a b)) List].  (rel_path(A;L;x;y) ∈ ℙ)
⊢ ∀aaaa:a:A × b:A × (R a b). ∀LLLL:(a:A × b:A × (R a b)) List.
    ((∀x,y,z:A. ∀r:R y z.  rel_path(A;LLLL @ [<y, z, r>];x;z) supposing rel_path(A;LLLL;x;y))
    ⇒ (∀x,y,z:A. ∀r:R y z.  rel_path(A;[aaaa / LLLL] @ [<y, z, r>];x;z) supposing rel_path(A;[aaaa / LLLL];x;y)))
BY
{ Auto }

1
1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. L : (a:A × b:A × (R a b)) List
4. ∀[x,y:A]. ∀[L:(a:A × b:A × (R a b)) List].  (rel_path(A;L;x;y) ∈ ℙ)
5. aaaa : a:A × b:A × (R a b)
6. LLLL : (a:A × b:A × (R a b)) List
7. ∀x,y,z:A. ∀r:R y z.  rel_path(A;LLLL @ [<y, z, r>];x;z) supposing rel_path(A;LLLL;x;y)
8. x : A
9. y : A
10. z : A
11. r : R y z
12. [%2] : rel_path(A;[aaaa / LLLL];x;y)
⊢ rel_path(A;[aaaa / LLLL] @ [<y, z, r>];x;z)

---

Latex:

---

Latex:
.....antecedent..... 
1.  [A]  :  Type
2.  [R]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  L  :  (a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List
4.  \mforall{}[x,y:A].  \mforall{}[L:(a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List].    (rel\_path(A;L;x;y)  \mmember{}  \mBbbP{})
\mvdash{}  \mforall{}aaaa:a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b).  \mforall{}LLLL:(a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List.
        ((\mforall{}x,y,z:A.  \mforall{}r:R  y  z.    rel\_path(A;LLLL  @  [<y,  z,  r>];x;z)  supposing  rel\_path(A;LLLL;x;y))
        {}\mRightarrow{}  (\mforall{}x,y,z:A.  \mforall{}r:R  y  z.
                    rel\_path(A;[aaaa  /  LLLL]  @  [<y,  z,  r>];x;z)  supposing  rel\_path(A;[aaaa  /  LLLL];x;y)))


By

---

Latex:
Auto

---

Home Index