Relación 7 - Historial de revisiones

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

2018-07-16T11:11:21Z

Texto reemplazado: «isar» por «isabelle»

Pabrodmac en 09:32 31 ene 2017

2017-01-31T09:32:10Z

Pabrodmac en 09:28 31 ene 2017

2017-01-31T09:28:37Z

Jeamacpov en 16:26 13 ene 2017

2017-01-13T16:26:59Z

Antsancab1 en 11:37 3 ene 2017

2017-01-03T11:37:19Z

Antsancab1 en 11:30 3 ene 2017

2017-01-03T11:30:40Z

Jalonso: Desprotegió «Relación 7»

2017-01-03T07:17:03Z

Desprotegió «Relación 7»

Jalonso en 08:26 22 dic 2016

2016-12-22T08:26:54Z

Mostrar los cambios

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

2016-12-22T08:00:48Z

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

Lucnovdos en 20:41 21 dic 2016

2016-12-21T20:41:10Z

← Revisión anterior		Revisión del 11:11 16 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 415: / Línea 415: @@
 (* Otra forma de escribir lo mismo *)
 (* anaprarod crigomgom rubgonmar ferrenseg ivamenjim paupeddeg juacabsou
-    dancorgar bowma lucnovdos *)
+    dancorgar bowma lucnovdos pabrodmac *)
 lemma "es_abc profundidad a ⟶ (a = (abc (profundidad a)))"
 by (induct a) auto
@@ Línea 471: / Línea 471: @@
 theorem "es_abc size a = es_abc medida a"
 quickcheck
 oops
 end
 </source>

@@ Línea 48: / Línea 48: @@
 (* marpoldia1 anaprarod paupeddeg migtermor wilmorort pablucoto
     ivamenjim serrodcal crigomgom rubgonmar  danrodcha ferrenseg
-    manmorjim1 juacabsou lucnovdos dancorgar bowma antsancab1 *)
+    manmorjim1 juacabsou lucnovdos dancorgar bowma antsancab1 pabrodmac *)
 (* Es muy parecida a la definición anterior *)
 fun hojas2 :: "arbol => nat" where
@@ Línea 71: / Línea 71: @@
 (* fraortmoy marpoldia1 anaprarod migtermor wilmorort marcarmor13
-    dancorgar antsancab1 jeamacpov *)
+    dancorgar antsancab1 jeamacpov pabrodmac *)
 fun profundidad :: "arbol => nat" where
    "profundidad H = 0"
@@ Línea 81: / Línea 81: @@
 (* anaprarod wilmorort pablucoto ivamenjim serrodcal crigomgom rubgonmar
-    danrodcha ferrenseg josgarsan juacabsou lucnovdos bowma *)
+    danrodcha ferrenseg josgarsan juacabsou lucnovdos bowma pabrodmac *)
 fun profundidad2 :: "arbol => nat" where
    "profundidad2 H       = 0"
@@ Línea 125: / Línea 125: @@
 (* fraortmoy marpoldia1 anaprarod paupeddeg migtermor  wilmorort
     serrodcal crigomgom rubgonmar danrodcha ferrenseg josgarsan
-    manmorjim1 juacabsou fracorjim1 lucnovdos dancorgar bowma antsancab1 *)
+    manmorjim1 juacabsou fracorjim1 lucnovdos dancorgar bowma antsancab1 pabrodmac *)
 fun abc :: "nat ⇒ arbol" where
    "abc 0       = H"
@@ Línea 164: / Línea 164: @@
 (* marpoldia1 paupeddeg ivamenjim pablucoto marcarmor13 manmorjim1
-    dancorgar antsancab1 jeamacpov *)
+    dancorgar antsancab1 jeamacpov pabrodmac *)
 fun es_abc2 :: "(arbol => 'a) => arbol => bool" where
    "es_abc2 f H       = True"
@@ Línea 251: / Línea 251: @@
 theorem "es_abc hojas a = es_abc profundidad a"
 by (induct a) (auto simp add: rel_hojas_prof)
 text {*
@@ Línea 331: / Línea 338: @@
 theorem "es_abc hojas a = es_abc size a"
 by (induct a) (auto simp add: rel_hojas_size)
 text {*
@@ Línea 348: / Línea 365: @@
 corollary es_abc_size_profundidad: "es_abc size a = es_abc profundidad a"
 by (simp add: es_abc_profundidad_hojas es_abc_hojas_size)
 text {*
@@ Línea 356: / Línea 381: @@
 (* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal
-    crigomgom marcarmor13 paupeddeg juacabsou dancorgar lucnovdos jeamacpov *)
+    crigomgom marcarmor13 paupeddeg juacabsou dancorgar lucnovdos jeamacpov pabrodmac  *)
 lemma lej10: "es_abc profundidad (abc n)"
 by (induct n) auto

@@ Línea 39: / Línea 39: @@
 *}
-(* fraortmoy marcarmor13 josgarsan fracorjim1 *)
+(* fraortmoy marcarmor13 josgarsan fracorjim1 jeamacpov *)
 fun hojas :: "arbol => nat" where
    "hojas H       = Suc 0"
@@ Línea 71: / Línea 71: @@
 (* fraortmoy marpoldia1 anaprarod migtermor wilmorort marcarmor13
-    dancorgar antsancab1 *)
+    dancorgar antsancab1 jeamacpov *)
 fun profundidad :: "arbol => nat" where
    "profundidad H = 0"
@@ Línea 132: / Línea 132: @@
 value "abc 3 = N (N (N H H) (N H H)) (N (N H H) (N H H))"
-(* ivamenjim pablucoto marcarmor13 *)
+(* ivamenjim pablucoto marcarmor13 jeamacpov *)
 fun abc2 :: "nat ⇒ arbol" where
    "abc2 0 = H"
@@ Línea 164: / Línea 164: @@
 (* marpoldia1 paupeddeg ivamenjim pablucoto marcarmor13 manmorjim1
-    dancorgar antsancab1 *)
+    dancorgar antsancab1 jeamacpov *)
 fun es_abc2 :: "(arbol => 'a) => arbol => bool" where
    "es_abc2 f H       = True"
@@ Línea 201: / Línea 201: @@
 (* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal
-    fracorjim1 josgarsan lucnovdos bowma antsancab1 *)
+    fracorjim1 josgarsan lucnovdos bowma antsancab1 jeamacpov *)
 lemma abc_prof_num_hojas:
    assumes "es_abc profundidad a"
@@ Línea 260: / Línea 260: @@
 (* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal
-    marcarmor13 josgarsan lucnovdos bowma antsancab1 *)
+    marcarmor13 josgarsan lucnovdos bowma antsancab1 jeamacpov *)
 lemma abc_hojas_num_nodos:
    assumes "es_abc hojas a"
@@ Línea 341: / Línea 341: @@
 (* fraortmoy marpoldia1 migtermor anaprarod  wilmorort pablucoto
     serrodcal crigomgom rubgonmar danrodcha ivamenjim marcarmor13
-    paupeddeg juacabsou josgarsan bowma lucnovdos antsancab1 *)
+    paupeddeg juacabsou josgarsan bowma lucnovdos antsancab1 jeamacpov *)
 lemma lej9:  "es_abc profundidad a = es_abc size a"
 by (simp add: lej7 lej8)
@@ Línea 356: / Línea 356: @@
 (* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal
-    crigomgom marcarmor13 paupeddeg juacabsou dancorgar lucnovdos *)
+    crigomgom marcarmor13 paupeddeg juacabsou dancorgar lucnovdos jeamacpov *)
 lemma lej10: "es_abc profundidad (abc n)"
 by (induct n) auto
@@ Línea 381: / Línea 381: @@
 (* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal
-    marcarmor13 antsancab1 *)
+    marcarmor13 antsancab1 jeamacpov *)
 lemma lej11:
    assumes "es_abc profundidad a"
@@ Línea 420: / Línea 420: @@
 (* anaprarod  wilmorort pablucoto serrodcal danrodcha marcarmor13
-    ferrenseg ivamenjim paupeddeg juacabsou rubgonmar bowma lucnovdos antsancab1 *)
+    ferrenseg ivamenjim paupeddeg juacabsou rubgonmar bowma lucnovdos antsancab1 jeamacpov *)
 lemma "es_abc f a =  es_abc size a"
 quickcheck

@@ Línea 201: / Línea 201: @@
 (* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal
-    fracorjim1 josgarsan lucnovdos bowma *)
+    fracorjim1 josgarsan lucnovdos bowma antsancab1 *)
 lemma abc_prof_num_hojas:
    assumes "es_abc profundidad a"
@@ Línea 220: / Línea 220: @@
 (* fraortmoy marpoldia1 migtermor anaprarod wilmorort serrodcal
     crigomgom rubgonmar ivamenjim danrodcha marcarmor13 paupeddeg
-    juacabsou bowma *)
+    juacabsou bowma antsancab1 *)
 (* También funciona con AUX7 *)
 lemma lej7: "es_abc profundidad a = es_abc hojas a"
@@ Línea 260: / Línea 260: @@
 (* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal
-    marcarmor13 josgarsan lucnovdos bowma *)
+    marcarmor13 josgarsan lucnovdos bowma antsancab1 *)
 lemma abc_hojas_num_nodos:
    assumes "es_abc hojas a"
@@ Línea 275: / Línea 275: @@
 (* fraortmoy marpoldia1 migtermor anaprarod wilmorort pablucoto
-    serrodcal *)
+    serrodcal antsancab1 *)
 lemma lej8: "es_abc hojas a = es_abc size a"
 by (induct a) (auto simp add:abc_hojas_num_nodos [symmetric])
@@ Línea 341: / Línea 341: @@
 (* fraortmoy marpoldia1 migtermor anaprarod  wilmorort pablucoto
     serrodcal crigomgom rubgonmar danrodcha ivamenjim marcarmor13
-    paupeddeg juacabsou josgarsan bowma lucnovdos *)
+    paupeddeg juacabsou josgarsan bowma lucnovdos antsancab1 *)
 lemma lej9:  "es_abc profundidad a = es_abc size a"
 by (simp add: lej7 lej8)
@@ Línea 360: / Línea 360: @@
 by (induct n) auto
-(* anaprarod rubgonmar danrodcha ferrenseg ivamenjim paupeddeg juacabsou bowma*)
+(* anaprarod rubgonmar danrodcha ferrenseg ivamenjim
 (* con un demostrador más débil *)
 (* y en general para cualquier medida *)
@@ Línea 380: / Línea 381: @@
 (* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal
-    marcarmor13 *)
+    marcarmor13 antsancab1 *)
 lemma lej11:
    assumes "es_abc profundidad a"
@@ Línea 419: / Línea 420: @@
 (* anaprarod  wilmorort pablucoto serrodcal danrodcha marcarmor13
-    ferrenseg ivamenjim paupeddeg juacabsou rubgonmar bowma lucnovdos *)
+    ferrenseg ivamenjim paupeddeg juacabsou rubgonmar bowma lucnovdos antsancab1 *)
 lemma "es_abc f a =  es_abc size a"
 quickcheck

← Revisión anterior	Revisión del 07:17 3 ene 2017
(Sin diferencias)

← Revisión anterior	Revisión del 08:00 22 dic 2016
(Sin diferencias)