---

Step * 2 1 2 of Lemma rel_path-append


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. rel_path(A;[aaaa / LLLL];x;y)
⊢ rel_path(A;[aaaa / LLLL] @ [<y, z, r>];x;z)
BY
{ ((Unfold `rel_path` 0 THEN Reduce 0 THEN Fold `rel_path` 0)
   THEN Unfold `rel_path` -1
   THEN Reduce -1
   THEN Try (Fold `rel_path` (-1))) }

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. ((fst(aaaa)) = x ∈ A) ∧ rel_path(A;LLLL;fst(snd(aaaa));y)
⊢ ((fst(aaaa)) = x ∈ A) ∧ rel_path(A;LLLL @ [<y, z, r>];fst(snd(aaaa));z)

---

Latex:

---

Latex:

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{})
5.  aaaa  :  a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b)
6.  LLLL  :  (a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List
7.  \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)
8.  x  :  A
9.  y  :  A
10.  z  :  A
11.  r  :  R  y  z
12.  rel\_path(A;[aaaa  /  LLLL];x;y)
\mvdash{}  rel\_path(A;[aaaa  /  LLLL]  @  [<y,  z,  r>];x;z)


By

---

Latex:
((Unfold  `rel\_path`  0  THEN  Reduce  0  THEN  Fold  `rel\_path`  0)
  THEN  Unfold  `rel\_path`  -1
  THEN  Reduce  -1
  THEN  Try  (Fold  `rel\_path`  (-1)))

---

Home Index