English
The dual of a node' with left l, value x, and right r is the node' with left and right swapped and each subtree dualized: dual(node'(l, x, r)) = node'(dual(r), x, dual(l)).
Русский
Дуал узла' с левым поддеревом l, значением x и правым поддеревом r равен узлу' с левой и правой стороной, поменянной местами, а поддеревья заменены на дуалы.
LaTeX
$$$$\operatorname{dual}(\operatorname{node}'(l, x, r)) = \operatorname{node}'(\operatorname{dual}(r), x, \operatorname{dual}(l)).$$$$
Lean4
theorem dual_node3L (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
dual (node3L l x m y r) = node3R (dual r) y (dual m) x (dual l) := by simp [node3L, node3R, add_comm]
