Relación 7

header {* R7: Recorridos de árboles *}

theory R7
imports Main 
begin 

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir el tipo de datos arbol para representar los
  árboles binarios que tiene información en los nodos y en las hojas. 
  Por ejemplo, el árbol
          e
         / \
        /   \
       c     g
      / \   / \
     a   d f   h 
  se representa por "N e (N c (H a) (H d)) (N g (H f) (H h))".
  --------------------------------------------------------------------- 
*}

datatype 'a arbol = H "'a" | N "'a" "'a arbol" "'a arbol"

value "N e (N c (H a) (H d)) (N g (H f) (H h))" 

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 2. Definir la función 
     preOrden :: "'a arbol ⇒ 'a list"
  tal que (preOrden a) es el recorrido pre orden del árbol a. Por
  ejemplo, 
     preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
     = [e,c,a,d,g,f,h] 
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic, carvelcab, domcadgom, marnajgom"
fun preOrden :: "'a arbol ⇒ 'a list" where
  "preOrden (H x) = [x]"
 |"preOrden (N x yy zz) = x#(preOrden yy @ preOrden zz)"

value "preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
 = [e,c,a,d,g,f,h]" -- "True"

value "preOrden (N e (N c (N a1 (H a2) (H a3)) (H d)) (N g (H f) (H h))) 
 = [e, c, a1, a2, a3, d, g, f, h]" -- "True"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 3. Definir la función 
     postOrden :: "'a arbol ⇒ 'a list"
  tal que (postOrden a) es el recorrido post orden del árbol a. Por
  ejemplo, 
     postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
     = [a,d,c,f,h,g,e]
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom, marnajgom"
fun postOrden :: "'a arbol ⇒ 'a list" where
  "postOrden (H x) = [x]"
 |"postOrden (N x yy zz)= postOrden yy @ postOrden zz @ [x]"

value "postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
 = [a,d,c,f,h,g,e]" -- "True"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 4. Definir la función 
     inOrden :: "'a arbol ⇒ 'a list"
  tal que (inOrden a) es el recorrido in orden del árbol a. Por
  ejemplo, 
     inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
     = [a,c,d,e,f,g,h]
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom, marnajgom"
fun inOrden :: "'a arbol ⇒ 'a list" where
  "inOrden (H x) = [x]"
 |"inOrden (N x yy zz) = inOrden yy @ [x] @ inOrden zz"

value "inOrden (N e (N c (H a) (H d)) (N g (H f) (H h))) 
 = [a,c,d,e,f,g,h]" -- "True"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 5. Definir la función 
     espejo :: "'a arbol ⇒ 'a arbol"
  tal que (espejo a) es la imagen especular del árbol a. Por ejemplo, 
     espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
     = N e (N g (H h) (H f)) (N c (H d) (H a))
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom, marnajgom"
fun espejo :: "'a arbol ⇒ 'a arbol" where
  "espejo (H x) = (H x)"
 |"espejo (N x yy zz) = (N x (espejo zz) (espejo yy))"

value "espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
 = N e (N g (H h) (H f)) (N c (H d) (H a))" -- "True"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar que
     preOrden (espejo a) = rev (postOrden a)
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic,carvelcab"
lemma  "preOrden (espejo a) = rev (postOrden a)"
by (induct a, simp_all)

--"jeshorcob,davoremar,carvelcab"
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x yy zz
  assume h1: "?P yy"
  assume h2: "?P zz"
  have "preOrden (espejo (N x yy zz))
    = preOrden (N x (espejo zz) (espejo yy))" by simp
  also have "... = x#(preOrden(espejo zz)@preOrden(espejo yy))" by simp
  also have "... = x#rev(postOrden zz)@rev(postOrden yy)" 
    using h1 h2 by simp
  also have "... = rev((postOrden yy)@(postOrden zz)@[x])" by simp
  finally show "?P (N x yy zz)" by simp
qed

-- "juacorvic, domcadgom, marnajgom (Igual pero un paso más. Se usan variables sugeridas)" 
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
  fix a
  show "?P (H a)" by simp
next
  fix a1 a2 a3
  assume h1: "?P a2"
  assume h2: "?P a3"
  have "preOrden (espejo (N a1 a2 a3)) = preOrden (N a1 (espejo a3) 
     (espejo a2))" by simp
  also have "... = a1#(preOrden (espejo a3) @ preOrden (espejo a2))"
      by simp 
  also have "... = a1#(rev (postOrden a3) @ rev(postOrden a2))" 
      using h1 h2 by simp
  also have "... = rev( (postOrden a2) @ (postOrden a3) @[a1] )" 
       by simp 
  also have "... = rev (postOrden (N a1 a2 a3))" by simp
  finally show "?P (N a1 a2 a3)" by simp
qed



text {*  
  --------------------------------------------------------------------- 
  Ejercicio 7. Demostrar que
     postOrden (espejo a) = rev (preOrden a)
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induct a, simp_all)

--"jeshorcob,davoremar,carvelcab"
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x y z
  assume h1: "?P y"
  assume h2: "?P z"
  have "postOrden (espejo (N x y z)) = 
    postOrden (N x (espejo z) (espejo y))" by simp
  also have "... = postOrden(espejo z)@postOrden(espejo y)@[x]" by simp
  also have "... = rev(preOrden z)@rev(preOrden y)@[x]" 
    using h1 h2 by simp
  also have "... = rev(x#(preOrden y)@(preOrden z))" by simp
  finally show "?P (N x y z)" by simp
qed

-- "juacorvic, domcadgom, marnajgom (Igual pero un paso más. Se usan variables sugeridas)" 
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof  (induct a)
  fix a
  show "?P (H a)" by simp
next
  fix a1 a2 a3
  assume h1: "?P a2"
  assume h2: "?P a3"
  have "postOrden (espejo (N a1 a2 a3)) = postOrden (N a1 (espejo a3) 
      (espejo a2))" by simp
  also have "... = postOrden (espejo a3) @  postOrden (espejo a2) @ [a1]" 
       by simp
  also have "... = rev (preOrden a3) @ rev (preOrden a2) @ [a1]" 
       using h1 h2 by simp
  also have "... = rev(a1#(preOrden a2)@(preOrden a3))" by simp
  also have "... = rev(preOrden (N a1 a2 a3))" by simp  
  finally show "?P (N a1 a2 a3)" by simp
qed


text {*  
  --------------------------------------------------------------------- 
  Ejercicio 8. Demostrar que
     inOrden (espejo a) = rev (inOrden a)
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a, simp_all)

--"jeshorcob,davoremar,carvelcab"
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x y z
  assume h1: "?P y"
  assume h2: "?P z"
  have "inOrden(espejo (N x y z)) = 
    inOrden(N x (espejo z) (espejo y))" by simp
  also have "... = inOrden(espejo z)@[x]@inOrden(espejo y)" by simp
  also have "... = rev(inOrden z)@[x]@rev(inOrden y)" using h1 h2 by simp
  also have "... = rev(inOrden y @ [x] @ inOrden z)" by simp
  finally show "?P (N x y z)" by simp
qed

-- "juacorvic, domcadgom, marnajgom (Igual pero un paso más. Se usan variables sugeridas)" 
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
  fix a
  show "?P (H a)" by simp
next
  fix a1 a2 a3
  assume h1: "?P a2"
  assume h2: "?P a3"
  have "inOrden (espejo (N a1 a2 a3)) = inOrden (N a1 (espejo a3) 
     (espejo a2))" by simp
  also have "... = inOrden (espejo a3) @ [a1] @ inOrden (espejo a2)"
      by simp
  also have "... = rev (inOrden a3) @ [a1] @ rev (inOrden a2)" 
      using h1 h2 by simp
  also have "... = rev (inOrden a2 @ [a1] @ inOrden a3)" by simp
  also have "... = rev (inOrden (N a1 a2 a3))" by simp
  finally show "?P (N a1 a2 a3)" by simp
qed



text {*  
  --------------------------------------------------------------------- 
  Ejercicio 9. Definir la función 
     raiz :: "'a arbol ⇒ 'a"
  tal que (raiz a) es la raiz del árbol a. Por ejemplo, 
     raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e
  --------------------------------------------------------------------- 
*}
--"jeshorcob,davoremar, domcadgom"
fun raiz :: "'a arbol ⇒ 'a" where
  "raiz (H x) = x"
 |"raiz (N x _ _ ) = x"

--"juacorvic,carvelcab, marnajgom"
fun raiz2 :: "'a arbol ⇒ 'a" where
   "raiz2 (H x) = x"
|  "raiz2 (N x yy zz) = x"

(*juacorvic: A partir de aquí en mis definiciones cambio variables por _ .
Pero, ¿Existe alguna diferencia si usamos variables en vez de _?, ¿Es 
solo por ahorrarnos escribir?
*)

value "raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e" -- "True"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 10. Definir la función 
     extremo_izquierda :: "'a arbol ⇒ 'a"
  tal que (extremo_izquierda a) es el nodo más a la izquierda del árbol
  a. Por ejemplo,  
     extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h))) = a
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom, marnajgom"
fun extremo_izquierda :: "'a arbol ⇒ 'a" where
  "extremo_izquierda (H x) = x"
 |"extremo_izquierda (N _ yy _) = extremo_izquierda yy"

value "extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h)))" -- "= a"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 11. Definir la función 
     extremo_derecha :: "'a arbol ⇒ 'a"
  tal que (extremo_derecha a) es el nodo más a la derecha del árbol
  a. Por ejemplo,  
     extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic, carvelcab, domcadgom, marnajgom"
fun extremo_derecha :: "'a arbol ⇒ 'a" where
  "extremo_derecha (H x) = x"
 |"extremo_derecha (N _ _ zz) = extremo_derecha zz"

value "extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h)))" -- "= h"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 12. Demostrar o refutar
     last (inOrden a) = extremo_derecha a
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
(*jeshorcob: al intentar hacer la prueba automática, el sistema se 
pregunta por el caso en el que la lista sea vacía. Debemos indicar que
esto no puede ocurrir y para ello añadimos un lema auxiliar.*)
lemma a1: "inOrden a ≠ []"
by (induct a, simp_all)

--"jeshorcob,davoremar,juacorvic, domcadgom"
theorem "last (inOrden a) = extremo_derecha a"
by (induct a, simp_all add: a1)

--"jeshorcob,davoremar,juacorvic, domcadgom"
lemma  "inOrden a ≠ []"
proof (induct a)
  fix x::"'a" show "inOrden (H x) ≠ []" by simp
next
  fix x::"'a" and y z::"'a arbol"
  assume h1: "inOrden y ≠ []"
  assume h2: "inOrden z ≠ []"
  show "inOrden (N x y z) ≠ []" using h1 h2 by simp  
qed

--"jeshorcob,davoremar,carvelcab, domcadgom"
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x y z
  assume h2: "?P z"
  have "last(inOrden(N x y z))=last(inOrden y @[x]@ inOrden z)" by simp
  also have "... = last(inOrden z)" by (simp add: a1)
  also have "... = extremo_derecha z" using h2 by simp
  finally show "?P (N x y z)" by simp
qed

--"juacorvic"
(* En mi demostración no uso patrones y no consigo demostrar *)
theorem "last (inOrden a) = extremo_derecha a"
proof (induct a)
  fix a::"'a"
  show "last (inOrden (H a)) = extremo_derecha (H a)" by simp
next
  fix a1::"'a"
  fix a2 a3::"'a arbol" 
  assume  h1: "last (inOrden a2) = extremo_derecha a2"
  assume  h2: "last (inOrden a3) = extremo_derecha a3"
  have "last (inOrden (N a1 a2 a3)) = last(inOrden a2 @[a1]@ inOrden a3)" 
        by simp
  then have "... = last (inOrden a3)" by (simp add: a1)
  then have "... = extremo_derecha a3" using h2 by simp
  thus "last (inOrden(N a1 a2 a3))=extremo_derecha(N a1 a2 a3)" by simp
qed
oops

--"Pedrosrei"
theorem "last (inOrden a) = extremo_derecha a"
apply (induct a, simp_all) apply (metis append_is_Nil_conv arbol.exhaust
  inOrden.simps(1) inOrden.simps(2) list.distinct(1)) done

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 13. Demostrar o refutar
     hd (inOrden a) = extremo_izquierda a
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic, domcadgom, marnajgom"
(*jeshorcob: aquí necesitamos el mismo lema por un motivo similar*)
theorem "hd (inOrden a) = extremo_izquierda a"
by (induct a, simp_all add: a1)

--"jeshorcob,davoremar,carvelcab, domcadgom"
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x y z
  assume h1: "?P y"
  have "hd(inOrden(N x y z))=hd(inOrden y @[x]@ inOrden z)" by simp
  also have "... = hd(inOrden y)" by (simp add: a1)
  also have "... = extremo_izquierda y" using h1 by simp
  finally show "?P (N x y z)" by simp
qed

--"juacorvic" 
(*Sin patrones, pero esta si funciona. ¿Porque no la del ejercicio 12?*)
theorem "hd (inOrden a) = extremo_izquierda a"
proof (induct a)
  fix a::"'a"
  show " hd (inOrden (H a)) = extremo_izquierda (H a)" by simp
next
  fix a1::"'a"
  fix a2::"'a arbol"
  fix a3::"'a arbol"
  assume h1: "hd(inOrden a2) = extremo_izquierda a2"
  assume h2: "hd (inOrden a3) = extremo_izquierda a3"
  have "hd (inOrden (N a1 a2 a3)) = hd (inOrden a2 @[a1]@ inOrden a3)"
     by simp
  also have "... = hd (inOrden a2)" by (simp add: a1)
  also have "... = extremo_izquierda a2" using h1 by simp
  finally show " hd (inOrden (N a1 a2 a3)) = 
     extremo_izquierda (N a1 a2 a3)" by simp
qed

--"Pedrosrei"
theorem "hd (inOrden a) = extremo_izquierda a"
apply (induct a, simp_all) apply (metis Nil_is_append_conv
  extremo_izquierda.cases hd_append inOrden.simps(1) inOrden.simps(2)
  list.distinct(1)) done

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 14. Demostrar o refutar
     hd (preOrden a) = last (postOrden a)
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic, domcadgom"
theorem "hd (preOrden a) = last (postOrden a)"
by (induct a, simp_all)

--"jeshorcob,davoremar,juacorvic, marnajgom"
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x::"'a" and y z
  have "hd(preOrden(N x y z)) = hd(x#(preOrden y @ preOrden z))" by simp
  also have "... = x" by simp
  also have "... = last(postOrden y @ postOrden z @[x])" by simp
  finally show "?P (N x y z)" by simp
qed

--"juacorvic" 
(* Muy detallada *)
theorem "hd (preOrden a) = last (postOrden a)"
proof (induct a)
 fix a::"'a"
 show "hd (preOrden (H a)) = last (postOrden (H a))" by simp
next
 fix a1::"'a"
 fix a2::"'a arbol"
 fix a3::"'a arbol"
 (*La siguiente línea puede eliminarse. No se usa hipótesis h1*)
 assume h1: "hd (preOrden a2) = last (postOrden a2)" 
 (*La siguiente línea puede eliminarse. No se usa hipótesis h2*)
 assume h2: " hd (preOrden a3) = last (postOrden a3)" 
 have "hd(preOrden (N a1 a2 a3))= hd(a1#(preOrden a2 @ preOrden a3))"
   by simp
 also have "... = hd [a1]" by simp
 also have "... = a1" by simp
 also have "... = last(postOrden a2 @  postOrden a3 @ [a1])" by simp
 also have "... = last (postOrden (N a1 a2 a3))" by simp
 finally show "hd (preOrden (N a1 a2 a3)) = 
    last (postOrden (N a1 a2 a3))" by simp
qed

--"carvelcab, domcadgom"

theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x ii dd
assume h1: "?P ii"
assume h2: "?P dd"
have "hd (preOrden (N x ii dd)) = hd (x#(preOrden ii @ preOrden dd))" by simp
also have "... = x" by simp
finally show "?P (N x ii dd)" by simp
qed 
 
-- es una orden mas corta que la primera

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 15. Demostrar o refutar
     hd (preOrden a) = raiz a
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,carvelcab, domcadgom"
theorem "hd (preOrden a) = raiz a"
by (induct a, simp_all)

--"jeshorcob,davoremar"
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x::"'a" and y z
  have "hd(preOrden(N x y z)) = hd(x#(preOrden y @ preOrden z))" by simp
  also have "... = x" by simp
  finally show "?P (N x y z)" by simp
qed

--"juacorvic"
(* Muy detallada *)
theorem "hd (preOrden a) = raiz a"
proof (induct a)
  fix a::"'a"
  show " hd (preOrden (H a)) = raiz (H a)" by simp
next 
  fix a1::"'a"
  fix a2::"'a arbol"
  fix a3::"'a arbol"
  (*La siguiente línea puede eliminarse. No se usa hipótesis h1*)
  assume h1: "hd (preOrden a2) = raiz a2"
  (*La siguiente línea puede eliminarse. No se usa hipótesis h2*)
  assume h2: " hd (preOrden a3) = raiz a3"
  have "hd (preOrden (N a1 a2 a3)) = hd(a1#(preOrden a2 @ preOrden a3))"
    by simp
  also have "... = a1" by simp
  also have "... = raiz (N a1 a2 a3)" by simp
  finally show "hd (preOrden (N a1 a2 a3)) = raiz (N a1 a2 a3)" by simp
qed

--"carvelcab, domcadgom,marnajgom"

theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x ii dd
assume h1: "?P ii"
assume h2: "?P dd"
have "hd (preOrden (N x ii dd)) = hd (x# preOrden ii @ preOrden dd)" by simp
also have "... = x" by simp
also have "... = raiz (N x ii dd)" by simp
finally show "?P (N x ii dd)" by simp
qed
 
-- esta tambien es una orden mas corta que la primera, pero a pesar de no usar las hipotesis, me da una advertencia si las quito.

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 16. Demostrar o refutar
     hd (inOrden a) = raiz a
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom, marnajgom"
theorem "hd (inOrden a) = raiz a"
quickcheck
oops
(*Encuentra el contrajemplo:
a = N a⇩1 (H a⇩2) (H a⇩1)

ya que evaluando se ve que son distindos:
hd (inOrden a) = a⇩2
raiz a = a⇩1
*)

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 17. Demostrar o refutar
     last (postOrden a) = raiz a
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar, domcadgom"
theorem "last (postOrden a) = raiz a"
by (induct a, simp_all)

--"jeshorcob,davoremar"
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x::"'a" and y z
  have "last(postOrden(N x y z)) = 
    last(postOrden y @ postOrden z @ [x])" by simp
  also have "... = x" by simp
  finally show "?P (N x y z)" by simp
qed

--"juacorvic"
(*Muy detallada*)
theorem "last (postOrden a) = raiz a"
proof (induct a)
  fix a::"'a"
  show " last (postOrden (H a)) = raiz (H a)" by simp
next
  fix a1::"'a"
  fix a2::"'a arbol"
  fix a3::"'a arbol"
  (*La siguiente línea puede eliminarse. No se usa hipótesis h1*)
  assume h1:"last (postOrden a2) = raiz a2"
 (*La siguiente línea puede eliminarse. No se usa hipótesis h2*)
  assume h2:"last (postOrden a3) = raiz a3"
  have "last (postOrden (N a1 a2 a3)) =
    last(postOrden a2 @  postOrden a3 @ [a1])" by simp
  also have "... = a1" by simp
  also have "... = raiz (N a1 a2 a3)" by simp
  thus "last (postOrden (N a1 a2 a3)) = raiz (N a1 a2 a3)" by simp
qed

--"carvelcab, domcadgom,marnajgom"
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x ii dd
assume h1:"?P ii"
assume h2:"?P dd"
have "last (postOrden (N x ii dd)) = last (postOrden ii @ postOrden dd @[x])" by simp
also have "... = x" by simp
finally show "?P (N x ii dd)" by simp
qed

-- Lo mismo de antes, con una orden menos.
end