For any graph x,y,z:V. x-the_graph- > *y y-the_graph- > *z x-the_graph- > *z

Auto
THEN
All (Unfold `connect`)
THEN
ExRepD
THEN
All (Unfolds [`last`;`path`])
THEN
ExRepD
THEN
InstConcl [p1 @ tl(p)]
THEN
ExRepD
THEN
Try ((RWO Thm* as,bs:T List, i:||as||. (as @ bs)[i] = as[i] 0) THEN (Complete Auto))

1	1. the_graph: Graph 2. x: Vertices(the_graph) 3. y: Vertices(the_graph) 4. z: Vertices(the_graph) 5. p1: Vertices(the_graph) List 6. 0 < ||p1|| 7. i:(||p1||-1). p1[i]-the_graph- > p1[(i+1)] 8. p1[0] = x 9. p1[(||p1||-1)] = y 10. p: Vertices(the_graph) List 11. 0 < ||p|| 12. i:(||p||-1). p[i]-the_graph- > p[(i+1)] 13. p[0] = y 14. p[(||p||-1)] = z 15. i: (||p1 @ tl(p)||-1) (p1 @ tl(p))[i]-the_graph- > (p1 @ tl(p))[(i+1)]	8 steps
2	1. the_graph: Graph 2. x: Vertices(the_graph) 3. y: Vertices(the_graph) 4. z: Vertices(the_graph) 5. p1: Vertices(the_graph) List 6. 0 < ||p1|| 7. i:(||p1||-1). p1[i]-the_graph- > p1[(i+1)] 8. p1[0] = x 9. p1[(||p1||-1)] = y 10. p: Vertices(the_graph) List 11. 0 < ||p|| 12. i:(||p||-1). p[i]-the_graph- > p[(i+1)] 13. p[0] = y 14. p[(||p||-1)] = z (p1 @ tl(p))[(||p1 @ tl(p)||-1)] = z	12 steps

About: