{"id":4930,"date":"2015-06-01T19:44:14","date_gmt":"2015-06-01T17:44:14","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4930"},"modified":"2015-06-02T19:45:01","modified_gmt":"2015-06-02T17:45:01","slug":"i1m2014-demostracion-de-propiedades-de-programas-por-induccion-sobre-arboles","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2014-demostracion-de-propiedades-de-programas-por-induccion-sobre-arboles\/","title":{"rendered":"I1M2014: Demostraci\u00f3n de propiedades de programas por inducci\u00f3n sobre \u00e1rboles"},"content":{"rendered":"<p>En la segunda parte de la clase de hoy de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-14\">Inform\u00e1tica de 1\u00ba del Grado en Matem\u00e1ticas<\/a> hemos comentado las soluciones a los ejercicios de la relaci\u00f3n 40 sobre demostraci\u00f3n de propiedades de programas por inducci\u00f3n sobre \u00e1rboles.<\/p>\n<p>Los ejercicios y su soluci\u00f3n se muestran a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"haskell\">\n-- ---------------------------------------------------------------------\n-- Introducci\u00f3n                                                       --\n-- ---------------------------------------------------------------------\n\n-- En esta relaci\u00f3n se plantean ejercicios de demostraci\u00f3n por inducci\u00f3n\n-- de propiedades de programas por inducci\u00f3n sobre \u00e1rboles.\n--\n-- Las transparencias del tema correspondiente se encuentran en \n--    http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-14\/temas\/tema-8.pdf\n\n-- ---------------------------------------------------------------------\n-- Importaci\u00f3n de librer\u00edas                                           --\n-- ---------------------------------------------------------------------\n\nimport Control.Monad\nimport Data.List\nimport Test.QuickCheck\n\n-- ---------------------------------------------------------------------\n-- Nota 1. En los siguientes ejercicios se demostrar\u00e1n\n-- propiedades de los \u00e1rboles binarios definidos como sigue\n--    data Arbol a = Hoja \n--                 | Nodo a (Arbol a) (Arbol a)\n--                 deriving (Show, Eq)\n-- En los ejemplos se usar\u00e1 el siguiente \u00e1rbol\n--    arbol = Nodo 9\n--                   (Nodo 3 \n--                         (Nodo 2 Hoja Hoja) \n--                         (Nodo 4 Hoja Hoja)) \n--                   (Nodo 7 Hoja Hoja)\n-- ---------------------------------------------------------------------\n\ndata Arbol a = Hoja \n             | Nodo a (Arbol a) (Arbol a)\n             deriving (Show, Eq)\n\narbol = Nodo 9\n               (Nodo 3 \n                     (Nodo 2 Hoja Hoja) \n                     (Nodo 4 Hoja Hoja)) \n               (Nodo 7 Hoja Hoja)\n\n-- ---------------------------------------------------------------------\n-- Nota 2. Para comprobar propiedades de \u00e1rboles con QuickCheck se\n-- utilizar\u00e1 el siguiente generador.\n-- ---------------------------------------------------------------------\n\ninstance Arbitrary a => Arbitrary (Arbol a) where\n  arbitrary = sized arbol\n    where\n      arbol 0       = return Hoja \n      arbol n | n>0 = oneof [return Hoja,\n                             liftM3 Nodo arbitrary subarbol subarbol]\n                      where subarbol = arbol (div n 2)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 1. Definir la funci\u00f3n\n--    espejo :: Arbol a -> Arbol a\n-- tal que (espejo x) es la imagen especular del \u00e1rbol x. Por ejemplo,\n--    ghci> espejo arbol\n--    Nodo 9 \n--         (Nodo 7 Hoja Hoja) \n--         (Nodo 3 \n--               (Nodo 4 Hoja Hoja) \n--               (Nodo 2 Hoja Hoja))\n-- ---------------------------------------------------------------------\n\nespejo :: Arbol a -> Arbol a\nespejo Hoja         = Hoja\nespejo (Nodo x i d) = Nodo x (espejo d) (espejo i)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 2. Comprobar con QuickCheck que para todo \u00e1rbol x,\n--    espejo (espejo x) = x\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_espejo :: Arbol Int -> Bool\nprop_espejo x =\n    espejo (espejo x) == x\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_espejo\n--    +++ OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 3. Demostrar por inducci\u00f3n que para todo \u00e1rbol x,\n--    espejo (espejo x) = x\n-- ---------------------------------------------------------------------\n\n{-\n Demostraci\u00f3n por inducci\u00f3n en x\n\n Caso base: Hay que demostrar que\n    espejo (espejo Hoja) = Hoja\n En efecto,\n    espejo (espejo Hoja)\n    = espejo Hoja          [por espejo.1]\n    = Hoja                 [por espejo.1]\n\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\n    espejo (espejo i) = i\n    espejo (espejo d) = d\n Hay que demostrar que\n    espejo (espejo (Nodo x i d)) = Nodo x i d\n En efecto,\n    espejo (espejo (Nodo x i d))\n    = espejo (Nodo x (espejo d) (espejo i))             [por espejo.2]\n    = Nodo x (espejo (espejo i)) (espejo (espejo d))    [por espejo.2]\n    = Nodo x i d                                        [por hip. inducci\u00f3n]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 4. Definir la funci\u00f3n\n--    preorden :: Arbol a -> [a]\n-- tal que (preorden x) es la lista correspondiente al recorrido\n-- preorden del \u00e1rbol x; es decir, primero visita la ra\u00edz del \u00e1rbol, a\n-- continuaci\u00f3n recorre el sub\u00e1rbol izquierdo y, finalmente, recorre el\n-- sub\u00e1rbol derecho. Por ejemplo,\n--    ghci> arbol\n--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)\n--    ghci> preorden arbol\n--    [9,3,2,4,7]\n-- ---------------------------------------------------------------------\n\npreorden :: Arbol a -> [a]\npreorden Hoja         = []\npreorden (Nodo x i d) = x : (preorden i ++ preorden d)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 5. Definir la funci\u00f3n\n--    postorden :: Arbol a -> [a]\n-- tal que (postorden x) es la lista correspondiente al recorrido\n-- postorden del \u00e1rbol x; es decir, primero recorre el sub\u00e1rbol\n-- izquierdo, a continuaci\u00f3n el sub\u00e1rbol derecho y, finalmente, la ra\u00edz\n-- del \u00e1rbol. Por ejemplo,\n--    ghci> arbol\n--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)\n--    ghci> postorden arbol\n--    [2,4,3,7,9]\n-- ---------------------------------------------------------------------\n\npostorden :: Arbol a -> [a]\npostorden Hoja         = []\npostorden (Nodo x i d) = postorden i ++ postorden d ++ [x]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 6. Comprobar con QuickCheck que para todo \u00e1rbol x,\n--    postorden (espejo x) = reverse (preorden x)\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_recorrido :: Arbol Int -> Bool\nprop_recorrido x =\n   postorden (espejo x) == reverse (preorden x)\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_recorrido\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 7. Demostrar por inducci\u00f3n que para todo \u00e1rbol x,\n--    postorden (espejo x) = reverse (preorden x)\n-- ---------------------------------------------------------------------\n\n{-\n Demostraci\u00f3n por inducci\u00f3n en x.\n\n Caso base: Hay que demostrar que \n    postorden (espejo Hoja) = reverse (preorden Hoja)\n En efecto,\n    postorden (espejo Hoja)\n    = postorden Hoja           [por espejo.1]\n    = []                       [por postorden.1]\n    = reverse []               [por reverse.1]\n    = reverse (preorden Hoja)  [por preorden.1]\n\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\n    postorden (espejo i) = reverse (preorden i)\n    postorden (espejo d) = reverse (preorden d)\n Hay que demostrar que\n    postorden (espejo (Nodo x i d)) = reverse (preorden (Nodo x i d))\n En efecto,\n    postorden (espejo (Nodo x i d))\n    = postorden (Nodo x (espejo d) (espejo i))   [por espejo.2]\n    = postorden (espejo d) ++ postorden (espejo i) ++ [x]                \n                                                 [por postorden.2]\n    = reverse (preorden d) ++ reverse (preorden i) ++ x\n                                                 [por hip. inducci\u00f3n]\n    = reverse ([x] ++ preorden (espejo i) ++ preorden (espejo d))      \n                                                 [por ejercicio 1]\n    = reverse (preorden (Nodo x i d))            [por preorden.1]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 8. Comprobar con QuickCheck que para todo \u00e1rbol binario\n-- x, se tiene que\n--    reverse (preorden (espejo x)) = postorden x\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_reverse_preorden_espejo :: Arbol Int -> Bool\nprop_reverse_preorden_espejo x =\n   reverse (preorden (espejo x)) == postorden x\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_reverse_preorden_espejo\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 9. Demostrar que para todo \u00e1rbol binario x, se tiene que\n--    reverse (preorden (espejo x)) = preorden x\n-- ---------------------------------------------------------------------\n\n{-\n Demostraci\u00f3n:\n    reverse (preorden (espejo x))\n    = postorden (espejo (espejo x))    [por ejercicio 7]\n    = postorden x                      [por ejercicio 3]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 10. Definir la funci\u00f3n\n--    nNodos :: Arbol a -> Int\n-- tal que (nNodos x) es el n\u00famero de nodos del \u00e1rbol x. Por ejemplo,\n--    ghci> arbol\n--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)\n--    ghci> nNodos arbol\n--    5\n-- ---------------------------------------------------------------------\n\nnNodos :: Arbol a -> Int\nnNodos Hoja         = 0\nnNodos (Nodo x i d) = 1 + nNodos i + nNodos d\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 11. Comprobar con QuickCheck que el n\u00famero de nodos de la\n-- imagen especular de un \u00e1rbol es el mismo que el n\u00famero de nodos del\n-- \u00e1rbol. \n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_nNodos_espejo :: Arbol Int -> Bool\nprop_nNodos_espejo x =\n   nNodos (espejo x) == nNodos x\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_nNodos_espejo\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 12. Demostrar por inducci\u00f3n que el n\u00famero de nodos de la\n-- imagen especular de un \u00e1rbol es el mismo que el n\u00famero de nodos del\n-- \u00e1rbol. \n-- ---------------------------------------------------------------------\n\n{-\n Demostraci\u00f3n: Hay que demostrar, por inducci\u00f3n en x, que \n    nNodos (espejo x) == nNodos x\n \n Caso base: Hay que demostrar que\n    nNodos (espejo Hoja) == nNodos Hoja\n En efecto,\n    nNodos (espejo Hoja)\n    = nNodos Hoja          [por espejo.1]\n\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\n    nNodos (espejo i) == nNodos i\n    nNodos (espejo d) == nNodos d\n Hay que demostrar que\n    nNodos (espejo (Nodo x i d)) == nNodos (Nodo x i d)\n En efecto,\n    nNodos (espejo (Nodo x i d))\n    = nNodos (Nodo x (espejo d) (espejo i))       [por espejo.2]\n    = 1 + nNodos (espejo d) + nNodos (espejo i)   [por nNodos.2]\n    = 1 + nNodos d + nNodos i                     [por hip.de inducci\u00f3n]\n    = 1 + nNodos i + nNodos d                     [por aritm\u00e9tica]\n    = nNodos (Nodo x i d)                         [por nNodos.2]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 13. Comprobar con QuickCheck que la longitud de la lista\n-- obtenida recorriendo un \u00e1rbol en sentido preorden es igual al n\u00famero\n-- de nodos del \u00e1rbol.\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_length_preorden :: Arbol Int -> Bool\nprop_length_preorden x =\n   length (preorden x) == nNodos x\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_length_preorden\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 14. Demostrar por inducci\u00f3n que la longitud de la lista\n-- obtenida recorriendo un \u00e1rbol en sentido preorden es igual al n\u00famero\n-- de nodos del \u00e1rbol.\n-- ---------------------------------------------------------------------\n\n{-\n Demostraci\u00f3n: Por inducci\u00f3n en x, hay que demostrar que\n    length (preorden x) == nNodos x\n  \n Caso base: Hay que demostrar que \n    length (preorden Hoja) = nNodos Hoja\n En efecto,\n    length (preorden Hoja)\n    = length []              [por preorden.1]\n    = 0                      [por length.1]\n    = nNodos Hoja            [por nNodos.1]\n\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\n    length (preorden i) == nNodos i\n    length (preorden d) == nNodos d\n Hay que demostrar que\n    length (preorden (Nodo x i d)) == nNodos (Nodo x i d)\n En efecto,\n    length (preorden (Nodo x i d))\n    = length ([x] ++ (peorden i) ++ (preorden d))   \n         [por preorden.2]\n    = length [x] + length (preorden i) + length (preorden d) \n         [propiedad de length: length (xs++ys) = length xs + length ys]\n    = 1 + length (preorden i) + length (preorden d) \n         [por def. de length]\n    = 1 + nNodos i + nNodos d\n         [por hip. de inducci\u00f3n]\n    = nNodos (x i d)\n         [por nNodos.2]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 15. Definir la funci\u00f3n\n--    profundidad :: Arbol a -> Int\n-- tal que (profundidad x) es la profundidad del \u00e1rbol x. Por ejemplo,\n--    ghci> arbol\n--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)\n--    ghci> profundidad arbol\n--    3\n-- ---------------------------------------------------------------------\n\nprofundidad :: Arbol a -> Int\nprofundidad Hoja = 0\nprofundidad (Nodo x i d) = 1 + max (profundidad i) (profundidad d)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 16. Comprobar con QuickCheck que para todo \u00e1rbol binario\n-- x, se tiene que\n--    nNodos x <= 2^(profundidad x) - 1\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_nNodosProfundidad :: Arbol Int -> Bool\nprop_nNodosProfundidad x =\n   nNodos x <= 2^(profundidad x) - 1\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_nNodosProfundidad\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 17. Demostrar por inducci\u00f3n que para todo \u00e1rbol binario\n-- x, se tiene que\n--    nNodos x <= 2^(profundidad x) - 1\n-- ---------------------------------------------------------------------\n\n{-\n Demostraci\u00f3n por inducci\u00f3n en x\n \n Caso base: Hay que demostrar que \n    nNodos Hoja <= 2^(profundidad Hoja) - 1\n En efecto,\n    nNodos Hoja\n    = 0                            [por nNodos.1]\n    = 2^0 - 1                      [por aritm\u00e9tica]\n    = 2^(profundidad Hoja) - 1     [por profundidad.1]\n\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\n    nNodos i <= 2^(profundidad i) - 1    \n    nNodos d <= 2^(profundidad d) - 1    \n Hay que demostrar que \n    nNodos (Nodo x i d) <= 2^(profundidad (Nodo x i d)) - 1    \n En efecto,\n    nNodos (Nodo x i d)\n    =  1 + nNodos i + nNodos d    \n          [por nNodos.1]\n    <= 1 + (2^(profundidad i) - 1) + (2^(profundidad d) - 1)\n          [por hip. de inducci\u00f3n]\n    =  2^(profundidad i) + 2^(profundidad d) - 1   \n          [por aritm\u00e9tica]\n    <= 2^m\u00e1x(profundidad i,profundidad d)+2^m\u00e1x(profundidad i,profundidad d)-1\n          [por aritm\u00e9tica]\n    =  2*2^m\u00e1x(profundidad i,profundidad d) - 1\n          [por aritm\u00e9tica]\n    =  2^(1+m\u00e1x(profundidad i,profundidad d)) - 1\n          [por aritm\u00e9tica]\n    =  2^profundidad(Nodo x i d) - 1\n          [por profundidad.2]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 18. Definir la funci\u00f3n\n--    nHojas :: Arbol a -> Int\n-- tal que (nHojas x) es el n\u00famero de hojas del \u00e1rbol x. Por ejemplo,\n--    ghci> arbol\n--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)\n--    ghci> nHojas arbol\n--    6\n-- ---------------------------------------------------------------------\n\nnHojas :: Arbol a -> Int\nnHojas Hoja         = 1\nnHojas (Nodo x i d) = nHojas i + nHojas d\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 19. Comprobar con QuickCheck que en todo \u00e1rbol binario el\n-- n\u00famero de sus hojas es igual al n\u00famero de sus nodos m\u00e1s uno.\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_nHojas :: Arbol Int -> Bool\nprop_nHojas x =\n    nHojas x == nNodos x + 1\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_nHojas\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 20. Demostrar por inducci\u00f3n que en todo \u00e1rbol binario el\n-- n\u00famero de sus hojas es igual al n\u00famero de sus nodos m\u00e1s uno.\n-- ---------------------------------------------------------------------\n\n{-\n Demostraci\u00f3n: Hay que demostrar, por inducci\u00f3n en x, que\n    nHojas x = nNodos x + 1\n\n Caso base: Hay que demotrar que\n    nHojas Hoja = nNodos Hoja + 1\n En efecto, \n    nHojas Hoja\n    = 1                 [por nHojas.1]\n    = 0 + 1             [por aritm\u00e9tica]\n    = nNodos Hoja + 1   [por nNodos.1]\n\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\n    nHojas i = nNodos i + 1\n    nHojas d = nNodos d + 1\n Hay que demostrar que\n    nHojas (Nodo x i d) = nNodos (Nodo x i d) + 1\n En efecto,\n    nHojas (Nodo x i d)\n    = nHojas i + nHojas d               [por nHojas.2]\n    = (nNodos i + 1) + (nNodos d +1)    [por hip. de inducci\u00f3n]\n    = (1 + nNodos i + nNodos d) + 1     [por aritm\u00e9tica]\n    = nNodos (Nodo x i d) + 1           [por nNodos.2]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 21. Definir, usando un acumulador, la funci\u00f3n\n--    preordenIt :: Arbol a -> [a]\n-- tal que (preordenIt x) es la lista correspondiente al recorrido\n-- preorden del \u00e1rbol x; es decir, primero visita la ra\u00edz del \u00e1rbol, a\n-- continuaci\u00f3n recorre el sub\u00e1rbol izquierdo y, finalmente, recorre el\n-- sub\u00e1rbol derecho. Por ejemplo,\n--    ghci> arbol\n--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)\n--    ghci> preordenIt arbol\n--    [9,3,2,4,7]\n-- Nota: No usar (++) en la definici\u00f3n\n-- ---------------------------------------------------------------------\n\npreordenIt :: Arbol a -> [a]\npreordenIt x = preordenItAux x []\n\npreordenItAux :: Arbol a -> [a] -> [a]\npreordenItAux Hoja xs         = xs\npreordenItAux (Nodo x i d) xs = x : preordenItAux i (preordenItAux d xs)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 22. Comprobar con QuickCheck que preordenIt es\n-- equivalente a preorden.\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_preordenIt :: Arbol Int -> Bool\nprop_preordenIt x =\n    preordenIt x == preorden x\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_preordenIt\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 23. Demostrar que preordenIt es equivalente a preorden.\n-- ---------------------------------------------------------------------\n\nprop_preordenItAux :: Arbol Int -> [Int] -> Bool\nprop_preordenItAux x ys =\n   preordenItAux x ys == preorden x ++ ys\n\n{-\n Demostraci\u00f3n: La propiedad es consecuencia del siguiente lema:\n \n Lema: Para todo \u00e1rbol binario x, se tiene que \n    para toda ys, preordenItAux x ys = preorden x ++ ys\n\n Demostraci\u00f3n de la propiedad usando el lema:\n    preordenIt x\n    = preordenItAux x []    [por preordnIt]\n    = preorden x ++ []      [por el lema]\n    = preorden x            [propiedad de ++]\n\n Demostraci\u00f3n del lema: Por inducci\u00f3n en x.\n\n Caso base: Hay que demotrar que\n    para toda ys, preordenItAux Hoja ys = preorden Hoja ++ ys\n En efecto, \n    preordenItAux Hoja ys\n    = ys                     [por preordenItAux.1]\n    = [] ++ ys               [por propiedad de ++]\n    = preorden Hoja ++ ys    [por preorden.1]\n    \n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\n    para toda ys, preordenItAux i ys = preorden i ++ ys\n    para toda ys, preordenItAux d ys = preorden d ++ ys\n Hay que demostrar que\n    para toda ys, preordenItAux (Nodo x i d) ys = preorden (Nodo x i d) ++ ys\n En efecto,\n    preordenItAux (Nodo x i d) ys\n    = x : (preordenItAux i (preordenItAux d ys))   [por preordenItAux.2]\n    = x : (preordenItAux i (preorden d ++ ys))     [por hip. de inducci\u00f3n]\n    = x : (preorden i ++ (preorden d ++ ys))       [por hip. de inducci\u00f3n]\n    = ([x] ++ preorden i ++ preorden d) ++ ys      [por prop. de listas]\n    = preorden (Nodo x i d) ++ ys                  [por preorden.2]\n-}\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la segunda parte de la clase de hoy de Inform\u00e1tica de 1\u00ba del Grado en Matem\u00e1ticas hemos comentado las soluciones a los ejercicios de la relaci\u00f3n 40 sobre demostraci\u00f3n de propiedades de programas por inducci\u00f3n sobre \u00e1rboles. Los ejercicios y su soluci\u00f3n se muestran a continuaci\u00f3n<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[270,305,126],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4930"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4930"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4930\/revisions"}],"predecessor-version":[{"id":4931,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4930\/revisions\/4931"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4930"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4930"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4930"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}