Horseshoe from two closed covering walks (source code)

= Horseshoe from two closed covering walks

If a <directed covering graph of an interval map> has two distinct closed walks of the same length $n$, based at the same interval and with different first edges, successive use of the <interval covering relation> produces two subintervals with disjoint interiors that $F^n$ maps across the base interval. Hence $F^n$ has a <horseshoe for an interval map>.