{"id":5859,"date":"2017-11-30T19:05:49","date_gmt":"2017-11-30T18:05:49","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5859"},"modified":"2017-12-02T09:06:51","modified_gmt":"2017-12-02T08:06:51","slug":"ra2017-razonamiento-por-casos-y-por-induccion-en-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2017-razonamiento-por-casos-y-por-induccion-en-isabellehol\/","title":{"rendered":"RA2017: Razonamiento por casos y por inducci\u00f3n en Isabelle\/HOL"},"content":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-17\">Razonamiento autom\u00e1tico<\/a> hemos profundizado en el estudio de las demostraciones por casos y por inducci\u00f3n. En concreto, se ha estudiado<\/p>\n<ul>\n<li>el razonamiento por casos booleanos,<\/li>\n<li>el razonamiento por casos booleanos sobre una variable,<\/li>\n<li>el razonamiento por casos sobre listas,<\/li>\n<li>el razonamiento por inducci\u00f3n sobre n\u00fameros naturales con patrones,<\/li>\n<li>el razonamiento sobre definiciones con existenciales,<\/li>\n<li>el uso de librer\u00edas auxiliares (como Parity) y<\/li>\n<li>el uso de otros m\u00e9todos de demostraci\u00f3n (como presburg).<\/li>\n<\/ul>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter {* Tema 4: Razonamiento por casos y por inducci\u00f3n *}\n\ntheory T4_Razonamiento_por_casos_y_por_induccion\nimports Main Parity\nbegin\n\ntext {*\n  En este tema se ampl\u00edan los m\u00e9todos de demostraci\u00f3n por casos y por\n  inducci\u00f3n iniciados en el tema anterior.\n*}\n\nsection {* Razonamiento por distinci\u00f3n de casos *}\n\nsubsection {* Distinci\u00f3n de casos booleanos *}\n\ntext {*\n  Ejemplo de demostraci\u00f3n por distinci\u00f3n de casos booleanos:\n  Demostrar \"\u00acA \u2228 A\".\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"\u00acA \u2228 A\" \nproof cases\n  assume \"A\" \n  then show \"\u00acA \u2228 A\" ..\nnext\n  assume \"\u00acA\" \n  then show \"\u00acA \u2228 A\" ..\nqed\n\ntext {*\n  Comentarios de la demostraci\u00f3n anterior:\n  \u00b7 \"proof cases\" indica que el m\u00e9todo de demostraci\u00f3n ser\u00e1 por\n    distinci\u00f3n de casos. \n  \u00b7 Se generan 2 casos:\n       1. ?P \u27f9 \u00acA \u2228 A\n       2. \u00ac?P \u27f9 \u00acA \u2228 A\n    donde ?P es una variable sobre las f\u00f3rmulas.\n  \u00b7 (assume \"A\") indica que se est\u00e1 usando \"A\" en lugar de la variable\n    ?P.\n  \u00b7 \"then\" indica usando la f\u00f3rmula anterior.\n  \u00b7 \"..\" indica usando la regla l\u00f3gica necesaria (las reglas l\u00f3gicas se\n    estudiar\u00e1n en los siguientes temas).\n  \u00b7 \"next\" indica el siguiente caso (se puede observar c\u00f3mo ha\n    sustituido \u00ac?P por \u00acA.\n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"\u00acA \u2228 A\" \nby auto\n\ntext {*\n  Ejemplo de demostraci\u00f3n por distinci\u00f3n de casos booleanos con nombres: \n  Demostrar \"\u00acA \u2228 A\".\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"\u00acA \u2228 A\" \nproof (cases \"A\")\n  case True \n  then show \"\u00acA \u2228 A\" ..\nnext\n  case False \n  thus \"\u00acA \u2228 A\" .. \nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 (cases \"A\") indica que la demostraci\u00f3n se har\u00e1 por casos seg\u00fan los\n    distintos valores de \"A\".\n  \u00b7 Como \"A\" es una f\u00f3rmula, sus posibles valores son verdadero o falso.\n  \u00b7 \"case True\" indica que se est\u00e1 suponiendo que A es verdadera. Es\n    equivalente a \"assume A\".\n  \u00b7 \"case False\" indica que se est\u00e1 suponiendo que A es falsa. Es\n    equivalente a \"assume \u00acA\".\n  \u00b7 En general, \n    \u00b7 el m\u00e9todo (cases F) es una abreviatura de la aplicaci\u00f3n de la regla\n         \u27e6F \u27f9 Q; \u00acF \u27f9 Q\u27e7 \u27f9 Q  \n    \u00b7 La expresi\u00f3n \"case True\" es una abreviatura de F.\n    \u00b7 La expresi\u00f3n \"case False\" es una abreviatura de \u00acF.\n  \u00b7 Ventajas de \"cases\" con nombre: \n    \u00b7 reduce la escritura de la f\u00f3rmula y\n    \u00b7 es independiente del orden de los casos.\n*}\n\nsubsection {* Distinci\u00f3n de casos sobre otros tipos de datos *}\n\ntext {*\n  Ejemplo de distinci\u00f3n de casos sobre listas: \n  Demostrar que la longitud del resto de una lista es la longitud de la\n  lista menos 1. \n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"length (tl xs) = length xs - 1\" \nproof (cases xs)\n  assume \"xs = []\"\n  then show \"length (tl xs) = length xs - 1\" by simp\nnext\n  fix y ys\n  assume \"xs = y#ys\"\n  then show \"length(tl xs) = length xs - 1\" by simp \nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 \"(cases xs)\" indica que la demostraci\u00f3n se har\u00e1 por casos sobre los\n    posibles valores de xs.\n  \u00b7 Como xs es una lista, sus posibles valores son la lista vac\u00eda ([]) o\n    una lista no vac\u00eda (de la forma (y#ys)).\n  \u00b7 Se generan 2 casos:\n       1. xs = [] \u27f9 length (tl xs) = length xs - 1\n       2. \u22c0a list. xs = a # list \u27f9 length (tl xs) = length xs - 1\n*}\n\n-- \"La demostraci\u00f3n simplificada es\"\nlemma \"length (tl xs) = length xs - 1\" \nproof (cases xs)\n  case Nil \n  then show ?thesis by simp\nnext\n  case Cons \n  then show ?thesis by simp \nqed\n\ntext {*\n  Comentarios sobre la dmostraci\u00f3n anterior:\n  \u00b7 \"case Nil\" es una abreviatura de \n       \"assume xs =[]\".\n  \u00b7 \"case Cons\" es una abreviatura de \n       \"fix y ys assume xs = y#ys\"\n  \u00b7 ?thesis es una abreviatura de la conclusi\u00f3n del lema.\n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"length (tl xs) = length xs - 1\" \nby auto\n\ntext {*\n  Een el siguiente ejemplo vamos a demostrar una propiedad de la funci\u00f3n\n  drop que est\u00e1 definida en la teor\u00eda List de forma que (drop n xs) la\n  lista obtenida eliminando en xs} los n primeros elementos. Su\n  definici\u00f3n es la siguiente   \n     drop_Nil:  \"drop n []     = []\" \n     drop_Cons: \"drop n (x#xs) = (case n of \n                                    0 => x#xs | \n                                    Suc(m) => drop m xs)\"\n*}\n\ntext {*\n  Ejemplo de an\u00e1lisis de casos:\n  Demostrar que el resultado de eliminar los n+1 primeros elementos de\n  xs es el mismo que eliminar los n primeros elementos del resto de xs.  \n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"drop (n + 1) xs = drop n (tl xs)\"\nproof (cases xs)\n  case Nil \n  then show ?thesis by simp\nnext\n  case Cons \n  then show ?thesis by simp\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"drop (n + 1) xs = drop n (tl xs)\"\nby (cases xs) auto\n\nsection {* Inducci\u00f3n matem\u00e1tica *}\n\ntext {*\n  [Principio de inducci\u00f3n matem\u00e1tica]\n  Para demostrar una propiedad P para todos los n\u00fameros naturales basta\n  probar que el 0 tiene la propiedad P y que si n tiene la propiedad P,\n  entonces n+1 tambi\u00e9n la tiene. \n     \u27e6P 0; \u22c0n. P n \u27f9 P (Suc n)\u27e7 \u27f9 P m\n\n  En Isabelle el principio de inducci\u00f3n matem\u00e1tica est\u00e1 formalizado en\n  el teorema nat.induct y puede verse con\n     thm nat.induct\n*}\n\ntext {*  \n  Ejemplo de demostraci\u00f3n por inducci\u00f3n: Usaremos el principio de\n  inducci\u00f3n matem\u00e1tica para demostrar que \n     1 + 3 + ... + (2n-1) = n^2\n\n  Definici\u00f3n. [Suma de los primeros impares] \n  (suma_impares n) la suma de los n n\u00fameros impares. Por ejemplo,\n     suma_impares 3  =  9\n*}\n\nfun suma_impares :: \"nat \u21d2 nat\" where\n  \"suma_impares 0 = 0\" \n| \"suma_impares (Suc n) = (2*(Suc n) - 1) + suma_impares n\"\n\nvalue \"suma_impares 3\"\n\ntext {*\n  Ejemplo de demostraci\u00f3n por inducci\u00f3n matem\u00e1tica:\n  Demostrar que la suma de los n primeros n\u00fameros impares es n^2.\n*}\n\n-- \"Demostraci\u00f3n del lema anterior por inducci\u00f3n y razonamiento ecuacional\"\nlemma \"suma_impares n = n * n\"\nproof (induct n)\n  show \"suma_impares 0 = 0 * 0\" by simp\nnext\n  fix n assume HI: \"suma_impares n = n * n\"\n  have \"suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n\" \n    by simp\n  also have \"\u2026 = (2 * (Suc n) - 1) + n * n\" using HI by simp\n  also have \"\u2026 = n * n + 2 * n + 1\" by simp\n  finally show \"suma_impares (Suc n) = (Suc n) * (Suc n)\" by simp\nqed\n\n-- \"Demostraci\u00f3n del lema anterior con patrones y razonamiento ecuacional\"\nlemma \"suma_impares n = n * n\" (is \"?P n\")\nproof (induct n)\n  show \"?P 0\" by simp\nnext\n  fix n \n  assume HI: \"?P n\"\n  have \"suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n\" \n    by simp\n  also have \"\u2026 = (2 * (Suc n) - 1) + n * n\" using HI by simp\n  also have \"\u2026 = n * n + 2 * n + 1\" by simp\n  finally show \"?P (Suc n)\" by simp\nqed\n\ntext {*\n  Comentario sobre la demostraci\u00f3n anterior:\n  \u00b7 Con la expresi\u00f3n\n       \"suma_impares n = n * n\" (is \"?P n\")\n    se abrevia \"suma_impares n = n * n\" como \"?P n\". Por tanto, \n       \"?P 0\"       es una abreviatura de \"suma_impares 0 = 0 * 0\"\n       \"?P (Suc n)\" es una abreviatura de \"suma_impares (Suc n) = (Suc n) * (Suc n)\"\n  \u00b7 En general, cualquier f\u00f3rmula seguida de (is patr\u00f3n) equipara el\n    patr\u00f3n con la f\u00f3rmula. \n*}\n\n-- \"La demostraci\u00f3n usando patrones es\"\nlemma \"suma_impares n = n * n\" (is \"?P n\")\nproof (induct n)\n  show \"?P 0\" by simp\nnext\n  fix n \n  assume \"?P n\"\n  then show \"?P (Suc n)\" by simp\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"suma_impares n = n * n\"\nby (induct n) auto\n\ntext {* \n  Ejemplo de definici\u00f3n con existenciales. \n  Un n\u00famero natural n es par si existe un natural m tal que n=m+m.   \n*}\n\ndefinition par :: \"nat \u21d2 bool\" where\n  \"par n \u2261 \u2203m. n=m+m\"\n\ntext {* \n  Ejemplo de inducci\u00f3n y existenciales: \n  Demostrar que para todo n\u00famero natural n, se verifica que n*(n+1) par. \n*}\n\n-- \"Demostraci\u00f3n detallada por inducci\u00f3n\"\nlemma \n  fixes n :: \"nat\"\n  shows \"par (n*(n+1))\"\nproof (induct n)\n  show \"par (0*(0+1))\" by (simp add: par_def)\nnext\n  fix n \n  assume \"par (n*(n+1))\"\n  then have \"\u2203m. n*(n+1) = m+m\" by (simp add:par_def)\n  then obtain m where m: \"n*(n+1) = m+m\" ..\n  then have \"(Suc n)*((Suc n)+1) = (m+n+1)+(m+n+1)\" by auto\n  then have \"\u2203m. (Suc n)*((Suc n)+1) = m+m\" ..\n  then show \"par ((Suc n)*((Suc n)+1))\" by (simp add:par_def)\nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 (fixes n :: \"nat\") es una abreviatura de \"sea n un n\u00famero natural\".\n*}\n\ntext {*\n  En Isabelle puede demostrarse de manera m\u00e1s simple un lema equivalente\n  usando en lugar de la funci\u00f3n \"par\" la funci\u00f3n \"even\" definida en la\n  teor\u00eda Parity por\n     even x \u27f7 x mod 2 = 0\"\n*}\n\nlemma \n  fixes n :: \"nat\"\n  shows \"even (n*(n+1))\"\nby auto\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 Para poder usar la funci\u00f3n \"even\" de la librer\u00eda Parity es necesario\n    importar dicha librer\u00eda. Por ello, antes del inicio de la teor\u00eda\n    aparece \n       imports Main Parity\n*}\n\ntext {*\n  Para completar la demostraci\u00f3n basta demostrar la equivalencia de las\n  funciones \"par\" y \"even\". \n*}\n\nlemma \n  fixes n :: \"nat\"\n  shows \"par n = even n\"\nproof - \n  have \"par n = (\u2203m. n = m+m)\" by (simp add:par_def)\n  then show \"par n = even n\" by presburger\nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 \"by presburger\" indica que se use como m\u00e9todo de demostraci\u00f3n el\n    algoritmo de decisi\u00f3n de la aritm\u00e9tica de Presburger.\n*}\n\nsection {* Inducci\u00f3n estructural *}\n\ntext {*\n  Inducci\u00f3n estructural:\n  \u00b7 En Isabelle puede hacerse inducci\u00f3n estructural sobre cualquier tipo\n    recursivo.\n  \u00b7 La inducci\u00f3n matem\u00e1tica es la inducci\u00f3n estructural sobre el tipo de\n    los naturales.\n  \u00b7 El esquema de inducci\u00f3n estructural sobre listas es\n    \u00b7 list.induct: \u27e6P []; \u22c0x ys. P ys \u27f9 P (x # ys)\u27e7 \u27f9 P zs\n  \u00b7 Para demostrar una propiedad para todas las listas basta demostrar\n    que la lista vac\u00eda tiene la propiedad y que al a\u00f1adir un elemento a una\n    lista que tiene la propiedad se obtiene una lista que tambi\u00e9n tiene la\n    propiedad. \n  \u00b7 En Isabelle el principio de inducci\u00f3n sobre listas est\u00e1 formalizado\n    mediante el teorema list.induct que puede verse con \n       thm list.induct\n*}\n\ntext {*\n  Concatenaci\u00f3n de listas:\n  En la teor\u00eda List.thy est\u00e1 definida la concatenaci\u00f3n de listas (que\n  se representa por @) como sigue\n     append_Nil:  \"[]@ys     = ys\"\n     append_Cons: \"(x#xs)@ys = x#(xs@ys)\"\n*}\n\ntext {*\n  Lema. [Ejemplo de inducci\u00f3n sobre listas]\n  Demostrar que la concatenaci\u00f3n de listas es asociativa.\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma conc_asociativa: \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\nproof (induct xs)\n  show \"[] @ (ys @ zs) = ([] @ ys) @ zs\"\n  proof -\n    have \"[] @ (ys @ zs) = ys @ zs\" by simp\n    also have \"\u2026 = ([] @ ys) @ zs\" by simp\n    finally show ?thesis .\n  qed\nnext\n  fix x xs\n  assume HI: \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\n  show \"(x#xs) @ (ys @ zs) = ((x#xs) @ ys) @ zs\"\n  proof -\n    have \"(x#xs) @ (ys @ zs) = x#(xs @ (ys @ zs))\" by simp\n    also have \"\u2026 = x#((xs @ ys) @ zs)\" using HI by simp\n    also have \"\u2026 = (x#(xs @ ys)) @ zs\" by simp\n    also have \"\u2026 = ((x#xs) @ ys) @ zs\" by simp\n    finally show ?thesis .\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma conc_asociativa_1: \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\nby (induct xs) auto\n\nsection {* Heur\u00edsticas para la inducci\u00f3n *}\n\ntext {*\n  Definici\u00f3n. [Definici\u00f3n recursiva de inversa]\n  (inversa xs) la inversa de la lista xs. Por ejemplo,\n     inversa [a,b,c] = [c,b,a] \n*}\n\nfun inversa :: \"'a list \u21d2 'a list\" where\n  \"inversa [] = []\" \n| \"inversa (x#xs) = (inversa xs) @ [x]\"\n\nvalue \"inversa [a,b,c]\"\n\ntext {* \n  Definici\u00f3n. [Definici\u00f3n de inversa con acumuladores]\n  (inversaAc xs) es la inversa de la lista xs calculada con\n  acumuladores. Por ejemplo,\n     inversaAc [a,b,c]       = [c,b,a] \n     inversaAcAux [a,b,c] [] = [c,b,a] \n*}\n\nfun inversaAcAux :: \"'a list \u21d2 'a list \u21d2 'a list\" where\n  \"inversaAcAux [] ys     = ys\" \n| \"inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)\"\n\ndefinition inversaAc :: \"'a list \u21d2 'a list\" where\n  \"inversaAc xs \u2261 inversaAcAux xs []\"\n\nvalue \"inversaAcAux [a,b,c] []\"\nvalue \"inversaAc [a,b,c]\"\n\ntext {* \n  Lema. [Ejemplo de equivalencia entre las definiciones]\n  La inversa de [a,b,c] es lo mismo calculada con la primera definici\u00f3n\n  que con la segunda.\n*}\n\nlemma \"inversaAc [a,b,c] = inversa [a,b,c]\"\nby (simp add: inversaAc_def)\n\ntext {*\n  Nota. [Ejemplo fallido de demostraci\u00f3n por inducci\u00f3n]\n  El siguiente intento de demostrar que para cualquier lista xs, se\n  tiene que  \"inversaAc xs = inversa xs\" falla.\n*}\n\nlemma \"inversaAc xs = inversa xs\"\nproof (induct xs)\n  show \"inversaAc [] = inversa []\" by (simp add: inversaAc_def)\nnext\n  fix a xs assume HI: \"inversaAc xs = inversa xs\"\n  have \"inversaAc (a#xs) = inversaAcAux (a#xs) []\" \n    by (simp add: inversaAc_def)\n  also have \"\u2026 = inversaAcAux xs [a]\" by simp\n  also have \"\u2026 = inversa (a#xs)\"\n  -- \"Problema: la hip\u00f3tesis de inducci\u00f3n no es aplicable.\"\noops\n\ntext {* \n  Nota. [Heur\u00edstica de generalizaci\u00f3n]\n  Cuando se use demostraci\u00f3n estructural, cuantificar universalmente las \n  variables libres (o, equivalentemente, considerar las variables libres\n  como variables arbitrarias).\n\n  Lema. [Lema con generalizaci\u00f3n]\n  Para toda lista ys se tiene \n     inversaAcAux xs ys = (inversa xs) @ ys\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma inversaAcAux_es_inversa:\n  \"inversaAcAux xs ys = (inversa xs)@ys\"\nproof (induct xs arbitrary: ys)\n  show \"\u22c0ys. inversaAcAux [] ys = (inversa [])@ys\" by simp\nnext\n  fix a xs \n  assume HI: \"\u22c0ys. inversaAcAux xs ys = inversa xs@ys\"\n  show \"\u22c0ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys\"\n  proof -\n    fix ys\n    have \"inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)\" by simp\n    also have \"\u2026 = inversa xs@(a#ys)\" using HI by simp\n    also have \"\u2026 = inversa (a#xs)@ys\" using [[simp_trace]] by simp \n    finally show \"inversaAcAux (a#xs) ys = inversa (a#xs)@ys\" by simp\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma inversaAcAux_es_inversa_1:\n  \"inversaAcAux xs ys = (inversa xs)@ys\"\nby (induct xs arbitrary: ys) auto\n\ntext {*\n  Corolario.  Para cualquier lista xs, se tiene que\n     inversaAc xs = inversa xs\n*}\n\ncorollary \"inversaAc xs = inversa xs\"\nby (simp add: inversaAcAux_es_inversa inversaAc_def)\n\ntext {*\n  Nota. En el paso \"inversa xs@(a#ys) = inversa (a#xs)@ys\" se usan\n  lemas de la teor\u00eda List. Se puede observar, insertano \n     using [[simp_trace]]\n  entre la igualdad y by simp, que los lemas usados son \n  \u00b7 List.append_simps_1: []@ys = ys\n  \u00b7 List.append_simps_2: (x#xs)@ys = x#(xs@ys)\n  \u00b7 List.append_assoc:   (xs @ ys) @ zs = xs @ (ys @ zs)\n  Las dos primeras son las ecuaciones de la definici\u00f3n de append.\n\n  En la siguiente demostraci\u00f3n se detallan los lemas utilizados.\n*}\n\nlemma \"(inversa xs)@(a#ys) = (inversa (a#xs))@ys\"\nproof -\n  have \"(inversa xs)@(a#ys) = (inversa xs)@(a#([]@ys))\" \n    by (simp only: append.simps(1))\n  also have \"\u2026 = (inversa xs)@([a]@ys)\" by (simp only: append.simps(2))\n  also have \"\u2026 = ((inversa xs)@[a])@ys\" by (simp only: append_assoc)\n  also have \"\u2026 = (inversa (a#xs))@ys\" by (simp only: inversa.simps(2))\n  finally show ?thesis .\nqed\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de Razonamiento autom\u00e1tico hemos profundizado en el estudio de las demostraciones por casos y por inducci\u00f3n. En concreto, se ha estudiado el razonamiento por casos booleanos, el razonamiento por casos booleanos sobre una variable, el razonamiento por casos sobre listas, el razonamiento por inducci\u00f3n&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","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":[266],"tags":[85,144,317],"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\/5859"}],"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=5859"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5859\/revisions"}],"predecessor-version":[{"id":5860,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5859\/revisions\/5860"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5859"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5859"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5859"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}