Relación 5 - Historial de revisiones

Jalonso en 18:41 14 jul 2018

2018-07-14T18:41:26Z

Jospermon1 en 11:57 1 mar 2018

2018-03-01T11:57:02Z

Jalonso: Desprotegió «Relación 5»

2018-02-10T05:42:30Z

Desprotegió «Relación 5»

Jalonso: Protegió «Relación 5» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2018-01-11T10:24:03Z

Protegió «Relación 5» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Cesgongut en 23:48 10 ene 2018

2018-01-10T23:48:37Z

Rafferrod en 22:27 10 ene 2018

2018-01-10T22:27:08Z

Rafferrod en 21:29 10 ene 2018

2018-01-10T21:29:33Z

Jescudero en 19:23 10 ene 2018

2018-01-10T19:23:35Z

Jescudero en 19:14 10 ene 2018

2018-01-10T19:14:55Z

Jescudero en 19:03 10 ene 2018

2018-01-10T19:03:56Z

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

@@ Línea 36: / Línea 36: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut *)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
 fun preOrden :: "'a arbol ⇒ 'a list" where
    "preOrden (H x) = [x]"
@@ Línea 55: / Línea 55: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut *)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
 fun postOrden :: "'a arbol ⇒ 'a list" where
    "postOrden (H x) = [x]"
@@ Línea 74: / Línea 74: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut *)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
 fun inOrden :: "'a arbol ⇒ 'a list" where
     "inOrden (H x) = [x]"
@@ Línea 92: / Línea 92: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut *)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
 fun espejo :: "'a arbol ⇒ 'a arbol" where
    "espejo (H x) = (H x)"
@@ Línea 107: / Línea 107: @@
 *}
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod*)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod jospermon1*)
 lemma  "preOrden (espejo a) = rev (postOrden a)"
    by (induct a) auto
@@ Línea 176: / Línea 176: @@
 *}
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut *)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1 *)
 lemma "postOrden (espejo a) = rev (preOrden a)"
    by (induct a) auto
@@ Línea 225: / Línea 225: @@
 *}
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut *)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
 theorem "inOrden (espejo a) = rev (inOrden a)"
    by (induct a) auto
@@ Línea 276: / Línea 276: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut *)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
 fun raiz :: "'a arbol ⇒ 'a" where
    "raiz (H x) = x"
@@ Línea 293: / Línea 293: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut *)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
 fun extremo_izquierda :: "'a arbol ⇒ 'a" where
    "extremo_izquierda (H x) = x"
@@ Línea 310: / Línea 310: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut *)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
 fun extremo_derecha :: "'a arbol ⇒ 'a" where
    "extremo_derecha (H x) = x"
@@ Línea 348: / Línea 348: @@
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut *)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
 lemma inOrdenNoVacio: "inOrden a ≠ []" by (cases a) auto
 (* Créditos Andrés, no sabía como hacerlo *)
@@ Línea 396: / Línea 396: @@
 qed
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut *)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut jospermon1*)
 theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
 proof (induct a)
@@ Línea 511: / Línea 511: @@
-(* luicedval rafcabgon macmerflo rafferrod cesgongut *)
+(* luicedval rafcabgon macmerflo rafferrod cesgongut jospermon1*)
 theorem "hd (preOrden a) = raiz a" (is "?P a")
 proof (induct a)
@@ Línea 543: / Línea 543: @@
 *}
-  (*anddonram luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut *)
+  (*anddonram luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut jospermon1*)
 theorem "hd (inOrden a) = raiz a"
    quickcheck
@@ Línea 581: / Línea 581: @@
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo rafferrod cesgongut *)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo rafferrod cesgongut jospermon1*)
 theorem "last (postOrden a) = raiz a" (is "?P a")
 proof (induct a)

@@ Línea 36: / Línea 36: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod*)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut *)
 fun preOrden :: "'a arbol ⇒ 'a list" where
    "preOrden (H x) = [x]"
@@ Línea 55: / Línea 55: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod*)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut *)
 fun postOrden :: "'a arbol ⇒ 'a list" where
    "postOrden (H x) = [x]"
@@ Línea 74: / Línea 74: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod*)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut *)
 fun inOrden :: "'a arbol ⇒ 'a list" where
     "inOrden (H x) = [x]"
@@ Línea 92: / Línea 92: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod*)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut *)
 fun espejo :: "'a arbol ⇒ 'a arbol" where
    "espejo (H x) = (H x)"
@@ Línea 148: / Línea 148: @@
    finally show "preOrden (espejo (N x1a a1 a2)) = rev (postOrden (N x1a a1 a2)) "
      by simp
 qed
@@ Línea 157: / Línea 176: @@
 *}
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod*)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut *)
 lemma "postOrden (espejo a) = rev (preOrden a)"
    by (induct a) auto
@@ Línea 206: / Línea 225: @@
 *}
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod*)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut *)
 theorem "inOrden (espejo a) = rev (inOrden a)"
    by (induct a) auto
@@ Línea 257: / Línea 276: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod *)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut *)
 fun raiz :: "'a arbol ⇒ 'a" where
    "raiz (H x) = x"
@@ Línea 274: / Línea 293: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod*)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut *)
 fun extremo_izquierda :: "'a arbol ⇒ 'a" where
    "extremo_izquierda (H x) = x"
@@ Línea 291: / Línea 310: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod *)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut *)
 fun extremo_derecha :: "'a arbol ⇒ 'a" where
    "extremo_derecha (H x) = x"
@@ Línea 329: / Línea 348: @@
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod *)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut *)
 lemma inOrdenNoVacio: "inOrden a ≠ []" by (cases a) auto
 (* Créditos Andrés, no sabía como hacerlo *)
@@ Línea 377: / Línea 396: @@
 qed
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod *)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod cesgongut *)
 theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
 proof (induct a)
@@ Línea 445: / Línea 464: @@
    fix x i d
    show "?P (N x i d)" by simp
 qed
@@ Línea 473: / Línea 511: @@
-(* luicedval rafcabgon macmerflo rafferrod*)
+(* luicedval rafcabgon macmerflo rafferrod cesgongut *)
 theorem "hd (preOrden a) = raiz a" (is "?P a")
 proof (induct a)
@@ Línea 505: / Línea 543: @@
 *}
-  (*anddonram luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod*)
+  (*anddonram luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod cesgongut *)
 theorem "hd (inOrden a) = raiz a"
    quickcheck
@@ Línea 543: / Línea 581: @@
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo rafferrod *)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo rafferrod cesgongut *)
 theorem "last (postOrden a) = raiz a" (is "?P a")
 proof (induct a)

@@ Línea 422: / Línea 422: @@
-(* luicedval rafcabgon *)
+(* luicedval rafcabgon rafferrod*)
 theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
 proof (induct a)
@@ Línea 473: / Línea 473: @@
-(* luicedval rafcabgon macmerflo*)
+(* luicedval rafcabgon macmerflo rafferrod*)
 theorem "hd (preOrden a) = raiz a" (is "?P a")
 proof (induct a)
@@ Línea 505: / Línea 505: @@
 *}
-  (*anddonram luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero*)
+  (*anddonram luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod*)
 theorem "hd (inOrden a) = raiz a"
    quickcheck
@@ Línea 543: / Línea 543: @@
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo *)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo rafferrod *)
 theorem "last (postOrden a) = raiz a" (is "?P a")
 proof (induct a)

@@ Línea 36: / Línea 36: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero*)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod*)
 fun preOrden :: "'a arbol ⇒ 'a list" where
    "preOrden (H x) = [x]"
@@ Línea 55: / Línea 55: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero*)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod*)
 fun postOrden :: "'a arbol ⇒ 'a list" where
    "postOrden (H x) = [x]"
@@ Línea 74: / Línea 74: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero*)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod*)
 fun inOrden :: "'a arbol ⇒ 'a list" where
     "inOrden (H x) = [x]"
@@ Línea 92: / Línea 92: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero*)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod*)
 fun espejo :: "'a arbol ⇒ 'a arbol" where
    "espejo (H x) = (H x)"
@@ Línea 107: / Línea 107: @@
 *}
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid *)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod*)
 lemma  "preOrden (espejo a) = rev (postOrden a)"
    by (induct a) auto
@@ Línea 157: / Línea 157: @@
 *}
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero*)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid jescudero rafferrod*)
 lemma "postOrden (espejo a) = rev (preOrden a)"
    by (induct a) auto
@@ Línea 206: / Línea 206: @@
 *}
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid*)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod*)
 theorem "inOrden (espejo a) = rev (inOrden a)"
    by (induct a) auto
@@ Línea 257: / Línea 257: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid *)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod *)
 fun raiz :: "'a arbol ⇒ 'a" where
    "raiz (H x) = x"
@@ Línea 274: / Línea 274: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid*)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod*)
 fun extremo_izquierda :: "'a arbol ⇒ 'a" where
    "extremo_izquierda (H x) = x"
@@ Línea 291: / Línea 291: @@
 *}
-(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid*)
+(* luicedval anddonram oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod *)
 fun extremo_derecha :: "'a arbol ⇒ 'a" where
    "extremo_derecha (H x) = x"
@@ Línea 329: / Línea 329: @@
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid *)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod *)
 lemma inOrdenNoVacio: "inOrden a ≠ []" by (cases a) auto
 (* Créditos Andrés, no sabía como hacerlo *)
@@ Línea 377: / Línea 377: @@
 qed
-(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid*)
+(* luicedval oscgonesc diwu2 rafcabgon macmerflo edupalhid rafferrod *)
 theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
 proof (induct a)

← Revisión anterior	Revisión del 05:42 10 feb 2018
(Sin diferencias)

← Revisión anterior	Revisión del 10:24 11 ene 2018
(Sin diferencias)