:: deftheorem Def5 defines .replaceWith GLIB_006:def 5 :
for G being _Graph
for W1, W2, W3 being Walk of G holds
( ( W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() implies W1 .replaceWith (W2,W3) = ((W1 .cut (1,(W1 .findFirstVertex W2))) .append W3) .append (W1 .cut ((W1 .findLastVertex W2),(len W1))) ) & ( ( not W2 is_odd_substring_of W1, 0 or not W2 .first() = W3 .first() or not W2 .last() = W3 .last() ) implies W1 .replaceWith (W2,W3) = W1 ) );