for G being _Graph
for W being closed Walk of G
for n being odd Element of NAT st n < len W holds
( (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is_Walk_from W . (n + 2),W . n & ( W is Trail-like implies ( (W .cut ((n + 2),(len W))) .edges() misses (W .cut (1,n)) .edges() & ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))} ) ) & ( W is Path-like implies ( ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) = {(W .first())} & ( not W . (n + 1) in G .loops() implies (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is open ) & (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like ) ) )