Relación 6 - Historial de revisiones

WikiSysop: Texto reemplazado: «isar» por «isabelle»

2018-07-16T11:11:20Z

Texto reemplazado: «isar» por «isabelle»

Antsancab1 en 22:12 28 dic 2016

2016-12-28T22:12:01Z

Antsancab1 en 22:00 28 dic 2016

2016-12-28T22:00:45Z

Antsancab1 en 21:21 28 dic 2016

2016-12-28T21:21:47Z

Antsancab1 en 18:09 28 dic 2016

2016-12-28T18:09:35Z

Antsancab1 en 18:07 28 dic 2016

2016-12-28T18:07:22Z

Antsancab1 en 17:43 28 dic 2016

2016-12-28T17:43:53Z

Anaprarod en 14:49 18 dic 2016

2016-12-18T14:49:57Z

Mostrar los cambios

Jalonso: Desprotegió «Relación 6»

2016-12-18T11:54:30Z

Desprotegió «Relación 6»

Jalonso en 11:38 15 dic 2016

2016-12-15T11:38:31Z

Mostrar los cambios

← Revisión anterior		Revisión del 11:11 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	chapter {* R6: Recorridos de árboles *}		chapter {* R6: Recorridos de árboles *}

@@ Línea 1428: / Línea 1428: @@
    finally show "?p (N t i d)" by simp
 qed
 (* migtermor *)

@@ Línea 699: / Línea 699: @@
 by (induct a) simp_all
-(* ivamenjim marpoldia1 paupeddeg anaprarod *)
+(* ivamenjim marpoldia1 paupeddeg anaprarod antsancab1 *)
 (* Igual que la anterior, pero poniendo solo by simp en el primer have *)
 theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
@@ Línea 928: / Línea 928: @@
 qed
-(* ivamenjim marpoldia1 wilmorort paupeddeg rubgonmar *)
+(* ivamenjim marpoldia1 wilmorort paupeddeg rubgonmar antsancab1 *)
 theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
 proof (induct a)
@@ Línea 1069: / Línea 1069: @@
 qed
-(* ivamenjim serrodcal *)
+(* ivamenjim serrodcal antsancab1 *)
 theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
 proof (induct a)
@@ Línea 1308: / Línea 1308: @@
    fix x i d
    show "?P (N x i d)" by simp
 qed
@@ Línea 1319: / Línea 1335: @@
 (* crigomgom pablucoto bowma migtermor ivamenjim wilmorort lucnovdos
     juacabsou pabrodmac serrodcal ferrenseg jeamacpov paupeddeg rubgonmar
-    marcarmor13 fraortmoy dancorgar anaprarod *)
+    marcarmor13 fraortmoy dancorgar anaprarod antsancab1 *)
 theorem "hd (inOrden a) = raiz a"
 quickcheck
@@ Línea 1506: / Línea 1522: @@
 end
 </source>

@@ Línea 310: / Línea 310: @@
 qed
 (* Le he puesto el nombre para utilizarlo en la siguiente demostración *)
 lemma  pre_es_rev_post: "preOrden (espejo a) = rev (postOrden a)" (is "?P a")

@@ Línea 441: / Línea 441: @@
 (* antsancab1 *)
-(* Como hemos demostrado que
+(* Después de hacerlo como en la anterior demostración se me ocurrió cómo
 preOrden (espejo a) = rev (postOrden a)
 a la inversa también queda demostrado *)

@@ Línea 308: / Línea 308: @@
      finally show ?thesis .
    qed
 qed
@@ Línea 318: / Línea 333: @@
 (* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal
-    dancorgar josgarsan*)
+    dancorgar josgarsan antsancab1 *)
 lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
 proof (induct a)
@@ Línea 424: / Línea 439: @@
    qed
 qed
 text {*
@@ Línea 433: / Línea 458: @@
 (* ivamenjim crigomgom bowma migtermor wilmorort juacabsou serrodcal
-    dancorgar josgarsan *)
+    dancorgar josgarsan antsancab1 *)
 theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
 proof (induct a)
@@ Línea 562: / Línea 587: @@
     migtermor marpoldia1 wilmorort lucnovdos  juacabsou serrodcal
     ferrenseg paupeddeg rubgonmar jeamacpov marcarmor13 fraortmoy
-    fracorjim1 josgarsan dancorgar anaprarod *)
+    fracorjim1 josgarsan dancorgar anaprarod antsancab1 *)
 fun raiz :: "'a arbol ⇒ 'a" where
    "raiz (H x)     = x"
@@ Línea 582: / Línea 607: @@
     migtermor marpoldia1 wilmorort lucnovdos  juacabsou serrodcal
     pabrodmac ferrenseg jeamacpov paupeddeg rubgonmar marcarmor13
-    fraortmoy fracorjim1 josgarsan dancorgar  anaprarod *)
+    fraortmoy fracorjim1 josgarsan dancorgar  anaprarod antsancab1 *)
 fun extremo_izquierda :: "'a arbol ⇒ 'a" where
    "extremo_izquierda (H x)     = x"
@@ Línea 614: / Línea 639: @@
     migtermor marpoldia1 wilmorort lucnovdos  juacabsou pabrodmac
     serrodcal ferrenseg jeamacpov paupeddeg rubgonmar marcarmor13
-    fraortmoy fracorjim1 josgarsan dancorgar anaprarod *)
+    fraortmoy fracorjim1 josgarsan dancorgar anaprarod antsancab1 *)
 fun extremo_derecha :: "'a arbol ⇒ 'a" where
    "extremo_derecha (H x) = x"

@@ Línea 24: / Línea 24: @@
     juacabsou serrodcal pabrodmac ferrenseg rubgonmar paupeddeg
     crigomgom danrodcha jeamacpov marcarmor13 josgarsan fraortmoy
-    dancorgar fracorjim1 anaprarod *)
+    dancorgar fracorjim1 anaprarod antsancab1 *)
 datatype 'a arbol = H "'a" | N "'a" "'a arbol" "'a arbol"
@@ Línea 43: / Línea 43: @@
 (* ivamenjim marpoldia1 pablucoto bowma fraortmoy migtermor
     wilmorort lucnovdos serrodcal pabrodmac jeamacpov paupeddeg
-    marcarmor13 josgarsan dancorgar anaprarod *)
+    marcarmor13 josgarsan dancorgar anaprarod antsancab1 *)
 fun preOrden :: "'a arbol ⇒ 'a list" where
@@ Línea 78: / Línea 78: @@
      pablucoto bowma fraortmoy migtermor wilmorort lucnovdos
      juacabsou serrodcal pabrodmac  ferrenseg jeamacpov
-     rubgonmar paupeddeg marcarmor13 josgarsan dancorgar fracorjim1 anaprarod *)
+     rubgonmar paupeddeg marcarmor13 josgarsan dancorgar fracorjim1 anaprarod antsancab1 *)
 fun postOrden :: "'a arbol ⇒ 'a list" where
@@ Línea 101: / Línea 101: @@
     migtermor wilmorort lucnovdos juacabsou serrodcal pabrodmac
     ferrenseg jeamacpov rubgonmar paupeddeg marcarmor13 josgarsan
-    dancorgar anaprarod *)
+    dancorgar anaprarod antsancab1 *)
 fun inOrden :: "'a arbol ⇒ 'a list" where
    "inOrden (H t)     = [t]"
@@ Línea 135: / Línea 135: @@
     pablucoto bowma fraortmoy migtermor wilmorort lucnovdos
     juacabsou serrodcal pabrodmac ferrenseg jeamacpov rubgonmar
-    paupeddeg marcarmor13 josgarsan dancorgar fracorjim1 anaprarod *)
+    paupeddeg marcarmor13 josgarsan dancorgar fracorjim1 anaprarod antsancab1 *)
 fun espejo :: "'a arbol ⇒ 'a arbol" where
    "espejo (H t)     = H t"

← Revisión anterior	Revisión del 11:54 18 dic 2016
(Sin diferencias)