English
The reverse of a transferred walk equals the transfer of the reversed walk, up to a simple edge-condition adjustment.
Русский
Обратный обход после переноса равен переносу обращённого обхода с учётом условия ребра.
LaTeX
$$(p.transfer H hp).reverse = p.reverse.transfer H (by simp)$$
Lean4
@[simp]
theorem reverse_transfer (hp) :
(p.transfer H hp).reverse = p.reverse.transfer H (by simp only [edges_reverse, List.mem_reverse]; exact hp) := by
induction p with
| nil => simp
| cons _ _ ih => simp only [transfer_append, Walk.transfer, reverse_cons, ih]