Razonamiento sobre árboles binarios: Aplanamiento e imagen especular

El árbol correspondiente a

se puede representar por el término

usando el tipo de dato arbol definido por

La imagen especular del árbol anterior es

y la lista obtenida aplanándolo (recorriéndolo en orden infijo) es

La definición de la función que calcula la imagen especular es

y la que aplana el árbol es

Demostrar que

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]