Relación 5 - Historial de revisiones

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

2018-07-16T11:11:20Z

Texto reemplazado: «isar» por «isabelle»

Antsancab1 en 18:07 26 dic 2016

2016-12-26T18:07:26Z

Marcarmor13 en 17:34 11 dic 2016

2016-12-11T17:34:35Z

Rubgonmar en 09:17 1 dic 2016

2016-12-01T09:17:05Z

Jalonso: Desprotegió «Relación 5»

2016-12-01T04:51:55Z

Desprotegió «Relación 5»

Jalonso en 04:51 1 dic 2016

2016-12-01T04:51:40Z

Mostrar los cambios

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

2016-12-01T04:04:51Z

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

Pablucoto en 02:04 1 dic 2016

2016-12-01T02:04:21Z

Lucnovdos en 20:27 30 nov 2016

2016-11-30T20:27:47Z

Jeamacpov en 20:18 30 nov 2016

2016-11-30T20:18:23Z

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

@@ Línea 28: / Línea 28: @@
 (* ivamenjim ferrenseg josgarsan juacabsou dancorgar pabrodmac lucnovdos
-    fracorjim1 *)
+    fracorjim1 antsancab1 *)
 (* Igual que la anterior pero con x en lugar de _ en el caso base *)
 fun estaEn1 :: "'a ⇒ 'a list ⇒ bool" where
@@ Línea 64: / Línea 64: @@
     serrodcal anaprarod migtermor paupeddeg fraortmoy marpoldia1
     ferrenseg josgarsan danrodcha manmorjim1 juacabsou dancorgar
-    pabrodmac lucnovdos jeamacpov marcarmor13 *)
+    pabrodmac lucnovdos jeamacpov marcarmor13 antsancab1 *)
 fun sinDuplicados :: "'a list ⇒ bool" where
    "sinDuplicados []     = True"
@@ Línea 108: / Línea 108: @@
     anaprarod migtermor paupeddeg fraortmoy marpoldia1 ferrenseg
     josgarsan danrodcha juacabsou dancorgar manmorjim1 pabrodmac
-    lucnovdos jeamacpov marcarmor13*)
+    lucnovdos jeamacpov marcarmor13 antsancab1 *)
 fun borraDuplicados :: "'a list ⇒ 'a list" where
    "borraDuplicados []     = []"
@@ Línea 183: / Línea 183: @@
 (* rubgonmar wilmorort pablucoto serrodcal migtermor paupeddeg
     fraortmoy marpoldia1 danrodcha juacabsou dancorgar josgarsan
-    pabrodmac lucnovdos *)
+    pabrodmac lucnovdos antsancab1 *)
 lemma length_borraDuplicados2:
    "length ( borraDuplicados xs ) ≤ length xs"
@@ Línea 380: / Línea 380: @@
        by simp
 qed
 text {*
@@ Línea 389: / Línea 408: @@
 (* crigomgom rubgonmar  wilmorort pablucoto serrodcal bowma
-    migtermor fraortmoy marpoldia1 ferrenseg danrodcha  juacabsou paupeddeg pabrodmac lucnovdos dancorgar jeamacpov marcarmor13 *)
+   migtermor fraortmoy marpoldia1 ferrenseg danrodcha  juacabsou
 lemma estaEn_borraDuplicados:
    "estaEn a (borraDuplicados xs) = estaEn a xs"
@@ Línea 732: / Línea 752: @@
 apply auto
 apply (simp add: noEsta_tras_borrarDuplicados)
 done
@@ Línea 767: / Línea 795: @@
 (* ivamenjim migtermor crigomgom rubgonmar fraortmoy marpoldia1
     ferrenseg bowma juacabsou serrodcal josgarsan pabrodmac dancorgar
-    jeamacpov lucnovdos *)
+    jeamacpov lucnovdos antsancab1 *)
 lemma sinDuplicados_borraDuplicados_2b:
    "sinDuplicados (borraDuplicados xs)"
@@ Línea 846: / Línea 874: @@
 *}
-(*crigomgom rubgonmar ivamenjim wilmorort pablucoto migtermor
+(* crigomgom rubgonmar ivamenjim wilmorort pablucoto migtermor
     anaprarod fraortmoy ferrenseg marpoldia1 bowma danrodcha juacabsou
     paupeddeg manmorjim1 serrodcal josgarsan pabrodmac lucnovdos
-    dancorgar jeamacpov marcarmor13*)
+    dancorgar jeamacpov marcarmor13 antsancab1 *)
 lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
 quickcheck

@@ Línea 19: / Línea 19: @@
 (* crigomgom rubgonmar bowma wilmorort pablucoto serrodcal
     anaprarod migtermor paupeddeg fraortmoy marpoldia1
-    danrodcha manmorjim1 jeamacpov *)
+    danrodcha manmorjim1 jeamacpov marcarmor13*)
 fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
    "estaEn _ []     = False"
@@ Línea 64: / Línea 64: @@
     serrodcal anaprarod migtermor paupeddeg fraortmoy marpoldia1
     ferrenseg josgarsan danrodcha manmorjim1 juacabsou dancorgar
-    pabrodmac lucnovdos jeamacpov *)
+    pabrodmac lucnovdos jeamacpov marcarmor13 *)
 fun sinDuplicados :: "'a list ⇒ bool" where
    "sinDuplicados []     = True"
@@ Línea 108: / Línea 108: @@
     anaprarod migtermor paupeddeg fraortmoy marpoldia1 ferrenseg
     josgarsan danrodcha juacabsou dancorgar manmorjim1 pabrodmac
-    lucnovdos jeamacpov *)
+    lucnovdos jeamacpov marcarmor13*)
 fun borraDuplicados :: "'a list ⇒ 'a list" where
    "borraDuplicados []     = []"
@@ Línea 188: / Línea 188: @@
 by (induct xs) auto
-(* manmorjim1 *)
+(* manmorjim1 marcarmor13 *)
 (* soy de ponerlo mejor por pasos *)
 lemma length_borraDuplicados3:
@@ Línea 284: / Línea 284: @@
 qed
-(* pablucoto jeamacpov *)
+(* pablucoto jeamacpov marcarmor13*)
 lemma length_borraDuplicados_2d:
    "length (borraDuplicados xs) ≤ length xs"
@@ Línea 389: / Línea 389: @@
 (* crigomgom rubgonmar  wilmorort pablucoto serrodcal bowma
-     migtermor fraortmoy marpoldia1 ferrenseg danrodcha  juacabsou paupeddeg pabrodmac lucnovdos dancorgar jeamacpov *)
+     migtermor fraortmoy marpoldia1 ferrenseg danrodcha  juacabsou paupeddeg pabrodmac lucnovdos dancorgar jeamacpov marcarmor13 *)
 lemma estaEn_borraDuplicados:
    "estaEn a (borraDuplicados xs) = estaEn a xs"
@@ Línea 543: / Línea 543: @@
 qed
-(* crigomgom paupeddeg pabrodmac*)
+(* crigomgom paupeddeg pabrodmac marcarmor13*)
 lemma estaEn_borraDuplicados_2d:
    "estaEn a (borraDuplicados xs) = estaEn a xs"
@@ Línea 706: / Línea 706: @@
 (* ivamenjim wilmorort serrodcal crigomgom anaprarod fraortmoy
     marpoldia1 ferrenseg danrodcha juacabsou paupeddeg josgarsan
-    pabrodmac dancorgar jeamacpov rubgonmar *)
+    pabrodmac dancorgar jeamacpov rubgonmar marcarmor13 *)
 lemma sinDuplicados_borraDuplicados:
    "sinDuplicados (borraDuplicados xs)"
@@ Línea 741: / Línea 741: @@
 *}
-(* wilmorort pablucoto *)
+(* wilmorort pablucoto marcarmor13*)
 lemma sinDuplicados_borraDuplicados_2a:
    "sinDuplicados (borraDuplicados xs)"
@@ Línea 849: / Línea 849: @@
     anaprarod fraortmoy ferrenseg marpoldia1 bowma danrodcha juacabsou
     paupeddeg manmorjim1 serrodcal josgarsan pabrodmac lucnovdos
-    dancorgar jeamacpov *)
+    dancorgar jeamacpov marcarmor13*)
 lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
 quickcheck

@@ Línea 706: / Línea 706: @@
 (* ivamenjim wilmorort serrodcal crigomgom anaprarod fraortmoy
     marpoldia1 ferrenseg danrodcha juacabsou paupeddeg josgarsan
-    pabrodmac dancorgar jeamacpov *)
+    pabrodmac dancorgar jeamacpov rubgonmar *)
 lemma sinDuplicados_borraDuplicados:
    "sinDuplicados (borraDuplicados xs)"

@@ Línea 659: / Línea 659: @@
 qed
-(* danrodcha *)
+(* danrodcha pablucoto*)
 (* es como la de ruben pero con diferencias de estilo *)
 lemma estaEn_borraDuplicados_2g:
@@ Línea 735: / Línea 735: @@
 *}
-(*wilmorort*)
+(*wilmorort pablucoto*)
 -- "La demostración estructurada es"

← Revisión anterior	Revisión del 04:51 1 dic 2016
(Sin diferencias)

← Revisión anterior	Revisión del 04:04 1 dic 2016
(Sin diferencias)

@@ Línea 759: / Línea 759: @@
 qed
-(* ivamenjim migtermor crigomgom rubgonmar fraortmoy marpoldia1 ferrenseg bowma juacabsou serrodcal josgarsan pabrodmac dancorgar jeamacpov *)
+(* ivamenjim migtermor crigomgom rubgonmar fraortmoy marpoldia1 ferrenseg bowma juacabsou serrodcal josgarsan pabrodmac dancorgar jeamacpov lucnovdos *)
 lemma sinDuplicados_borraDuplicados_2: