Pruebas de que la función espejo de los árboles binarios es involutiva

El árbol correspondiente a

se puede representar por el término

usado el tipo de dato arbol definido por

La imagen especular del árbol anterior es

cuyo término es

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

Demostrar que la función espejo es involutiva; es decir,

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]

Escribe un comentario