Relación 6 - Historial de revisiones

Jalonso en 18:42 14 jul 2018

2018-07-14T18:42:11Z

Rafferrod en 00:01 18 ene 2018

2018-01-18T00:01:25Z

Jospermon1 en 23:59 17 ene 2018

2018-01-17T23:59:26Z

Jospermon1 en 23:58 17 ene 2018

2018-01-17T23:58:57Z

Rafferrod en 23:02 17 ene 2018

2018-01-17T23:02:29Z

Davperriv en 21:30 17 ene 2018

2018-01-17T21:30:15Z

Cesgongut en 21:19 17 ene 2018

2018-01-17T21:19:47Z

Cesgongut en 21:12 17 ene 2018

2018-01-17T21:12:53Z

Jescudero en 20:49 17 ene 2018

2018-01-17T20:49:17Z

Jescudero en 17:29 17 ene 2018

2018-01-17T17:29:56Z

← Revisión anterior		Revisión del 18:42 14 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	chapter {* R7: Árboles binarios completos *}		chapter {* R7: Árboles binarios completos *}

@@ Línea 126: / Línea 126: @@
-(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv jospermon1*)
+(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv jospermon1 rafferrod*)
 (* blast no funciona, ¿cómo eliminar la conjunción sin recurrir a auto? *)
 lemma hojas_prof:
@@ Línea 151: / Línea 151: @@
 *}
-(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv jospermon1*)
+(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv jospermon1 rafferrod*)
 lemma hojas_size:
 " es_abc hojas a ⟶ hojas a = Suc (size a)"
@@ Línea 167: / Línea 167: @@
 *}
-(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon*)
+(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon rafferrod*)
   theorem "es_abc profundidad a = es_abc size a"
    by (simp_all add:comp_p_h comp_h_s)
@@ Línea 198: / Línea 198: @@
 *}
-(*anddonram luicedval oscgonesc macmerflo diwu2 rafcabgon*)
+(*anddonram luicedval oscgonesc macmerflo diwu2 rafcabgon rafferrod*)
   theorem "es_abc profundidad a =(a=abc (profundidad a)) "
    by (induct a) auto

@@ Línea 38: / Línea 38: @@
    ---------------------------------------------------------------------
 *}
-  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod*)
+  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod jospermon1*)
 fun hojas :: "arbol => nat" where
    "hojas H = 1"

@@ Línea 54: / Línea 54: @@
 *}
-  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv rafferrod*)
+  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv rafferrod jospermon1*)
 fun profundidad :: "arbol => nat" where
    "profundidad H = 0"
@@ Línea 71: / Línea 71: @@
 *}
-  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod*)
+  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod jospermon1*)
 fun abc :: "nat ⇒ arbol" where
    "abc 0 = H"
@@ Línea 92: / Línea 92: @@
 *}
-  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv rafferrod*)
+  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv rafferrod jospermon1*)
 fun es_abc :: "(arbol => 'a) => arbol => bool" where
    "es_abc f H = True"
@@ Línea 126: / Línea 126: @@
-(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv *)
+(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv jospermon1*)
 (* blast no funciona, ¿cómo eliminar la conjunción sin recurrir a auto? *)
 lemma hojas_prof:
@@ Línea 151: / Línea 151: @@
 *}
-(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv *)
+(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv jospermon1*)
 lemma hojas_size:
 " es_abc hojas a ⟶ hojas a = Suc (size a)"

@@ Línea 38: / Línea 38: @@
    ---------------------------------------------------------------------
 *}
-  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv *)
+  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod*)
 fun hojas :: "arbol => nat" where
    "hojas H = 1"
@@ Línea 54: / Línea 54: @@
 *}
-  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv *)
+  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv rafferrod*)
 fun profundidad :: "arbol => nat" where
    "profundidad H = 0"
@@ Línea 71: / Línea 71: @@
 *}
-  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv  *)
+  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod*)
 fun abc :: "nat ⇒ arbol" where
    "abc 0 = H"
@@ Línea 92: / Línea 92: @@
 *}
-  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv *)
+  (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv rafferrod*)
 fun es_abc :: "(arbol => 'a) => arbol => bool" where
    "es_abc f H = True"
@@ Línea 177: / Línea 177: @@
 *}
-(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon*)
+(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon rafferrod*)
    theorem "es_abc f (abc n) "
    by (induct n) auto

@@ Línea 127: / Línea 127: @@
 (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut *)
 lemma hojas_prof:
 "es_abc profundidad a ⟶ hojas a = 2^profundidad a"