Relación 7 - Historial de revisiones

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

2018-07-16T15:46:15Z

Texto reemplazado: «isar» por «isabelle»

Jaisalmen en 04:30 4 mar 2014

2014-03-04T04:30:15Z

Marescpla en 13:41 9 ene 2014

2014-01-09T13:41:42Z

Marescpla en 13:27 9 ene 2014

2014-01-09T13:27:30Z

Marescpla en 13:02 9 ene 2014

2014-01-09T13:02:52Z

Marescpla en 12:56 9 ene 2014

2014-01-09T12:56:59Z

Marescpla en 12:48 9 ene 2014

2014-01-09T12:48:04Z

Juaruipav en 08:14 9 ene 2014

2014-01-09T08:14:33Z

Pabflomar en 03:55 9 ene 2014

2014-01-09T03:55:20Z

Pabflomar en 03:52 9 ene 2014

2014-01-09T03:52:47Z

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

@@ Línea 36: / Línea 36: @@
 *}
--- "diecabmen1 maresccas4 domlloriv pabflomar juaruipav"
+-- "diecabmen1 maresccas4 domlloriv pabflomar juaruipav jaisalmen zoiruicha"
 fun preOrden :: "'a arbol ⇒ 'a list" where
@@ Línea 66: / Línea 66: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla jaisalmen zoiruicha"
 fun postOrden :: "'a arbol ⇒ 'a list" where
@@ Línea 86: / Línea 86: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav jaisalmen zoiruicha"
 fun inOrden :: "'a arbol ⇒ 'a list" where
@@ Línea 116: / Línea 116: @@
 *}
--- "diecabmen1 maresccas4 domlloriv pabflomar juaruipav marescpla"
+-- "diecabmen1 maresccas4 domlloriv pabflomar juaruipav marescpla jaisalmen zoiruicha"
 fun espejo :: "'a arbol ⇒ 'a arbol" where
@@ Línea 139: / Línea 139: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav jaisalmen zoiruicha"
 lemma  "preOrden (espejo a) = rev (postOrden a)"
@@ Línea 214: / Línea 214: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav jaisalmen zoiruicha"
 lemma "postOrden (espejo a) = rev (preOrden a)"
@@ Línea 291: / Línea 291: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav jaisalmen zoiruicha"
 theorem "inOrden (espejo a) = rev (inOrden a)"
@@ Línea 370: / Línea 370: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla jaisalmen zoiruicha"
 fun raiz :: "'a arbol ⇒ 'a" where
@@ Línea 388: / Línea 388: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla jaisalmen zoiruicha"
 fun extremo_izquierda :: "'a arbol ⇒ 'a" where
@@ Línea 406: / Línea 406: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla jaisalmen zoiruicha"
 fun extremo_derecha :: "'a arbol ⇒ 'a" where
@@ Línea 443: / Línea 443: @@
 qed
---"irealetei"
+--"irealetei jaisalmen zoiruicha"
 lemma inOrdenNoPuedeSerVacio: "inOrden a ≠ []"
 by (induct a) auto
@@ Línea 579: / Línea 579: @@
      finally show "hd (inOrden (N a x y)) = extremo_izquierda (N a x y)" by simp
    qed
 text {*
@@ Línea 587: / Línea 591: @@
 *}
--- "diecabmen1 maresccas4 domlloriv juaruipav"
+-- "diecabmen1 maresccas4 domlloriv juaruipav jaisalmen zoiruicha"
 theorem "hd (preOrden a) = last (postOrden a)"
@@ Línea 662: / Línea 666: @@
 *}
--- "diecabmen1 maresccas4 domlloriv juaruipav"
+-- "diecabmen1 maresccas4 domlloriv juaruipav zoiruicha jaisalmen"
 theorem "hd (preOrden a) = raiz a"
@@ Línea 734: / Línea 738: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv juaruipav marescpla"
+-- "diecabmen1 maresccas4 irealetei domlloriv juaruipav marescpla jaisalmen zoiruicha"
 theorem "hd (inOrden a) = raiz a"
@@ Línea 754: / Línea 758: @@
 *}
--- "diecabmen1 maresccas4 domlloriv juaruipav"
+-- "diecabmen1 maresccas4 domlloriv juaruipav jaisalmen zoiruicha"
 theorem "last (postOrden a) = raiz a"

@@ Línea 635: / Línea 635: @@
 --"marescpla"
-theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
+theorem T1: "hd (preOrden a) = last (postOrden a)" (is "?P a")
 proof (cases a)
    fix a:: "'a arbol"
@@ Línea 709: / Línea 709: @@
 --"marescpla"
-theorem "hd (preOrden a) = raiz a" (is "?P a")
+theorem T2: "hd (preOrden a) = raiz a" (is "?P a")
 proof (cases a)
    fix a ::"'a arbol"
@@ Línea 734: / Línea 734: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv juaruipav"
+-- "diecabmen1 maresccas4 irealetei domlloriv juaruipav marescpla"
 theorem "hd (inOrden a) = raiz a"
@@ Línea 800: / Línea 800: @@
      also have "... = raiz (N data a1 a2)" by simp
      finally show ?thesis using A by simp
 qed
 end
 </source>

@@ Línea 560: / Línea 560: @@
    qed
 qed
 text {*
@@ Línea 612: / Línea 631: @@
      finally show ?thesis using A by simp
 qed
 text {*
@@ Línea 664: / Línea 706: @@
      finally show ?thesis using A by simp
 qed
 text {*

@@ Línea 339: / Línea 339: @@
    qed
 qed
 text {*
@@ Línea 349: / Línea 370: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla"
 fun raiz :: "'a arbol ⇒ 'a" where
@@ Línea 367: / Línea 388: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla"
 fun extremo_izquierda :: "'a arbol ⇒ 'a" where
@@ Línea 385: / Línea 406: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar juaruipav marescpla"
 fun extremo_derecha :: "'a arbol ⇒ 'a" where
@@ Línea 447: / Línea 468: @@
    qed
 qed
 text {*

@@ Línea 45: / Línea 45: @@
 -- "= [e,c,a,d,g,f,h]"
--- "irealetei"
+-- "irealetei marescpla"
 fun preOrden2 :: "'a arbol ⇒ 'a list" where
    "preOrden2 (H a) = [a]"

@@ Línea 297: / Línea 297: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar"
 fun raiz :: "'a arbol ⇒ 'a" where
@@ Línea 315: / Línea 315: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar"
 fun extremo_izquierda :: "'a arbol ⇒ 'a" where
@@ Línea 333: / Línea 333: @@
 *}
--- "diecabmen1 maresccas4 irealetei domlloriv"
+-- "diecabmen1 maresccas4 irealetei domlloriv pabflomar"
 fun extremo_derecha :: "'a arbol ⇒ 'a" where