Relación 6 - Historial de revisiones

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

2018-07-16T08:23:48Z

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

Domcadgom en 11:04 4 dic 2014

2014-12-04T11:04:54Z

Domcadgom en 10:31 4 dic 2014

2014-12-04T10:31:12Z

Marnajgom en 10:00 27 nov 2014

2014-11-27T10:00:40Z

Pedrosrei en 12:22 26 nov 2014

2014-11-26T12:22:49Z

Juacorvic en 08:49 25 nov 2014

2014-11-25T08:49:57Z

Juacorvic en 08:46 25 nov 2014

2014-11-25T08:46:37Z

Juacorvic en 08:43 25 nov 2014

2014-11-25T08:43:08Z

Juacorvic en 08:37 25 nov 2014

2014-11-25T08:37:46Z

Juacorvic en 08:27 25 nov 2014

2014-11-25T08:27:01Z

← Revisión anterior		Revisión del 08:23 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R6: Sustitución, inversión y eliminación *}		header {* R6: Sustitución, inversión y eliminación *}

@@ Línea 217: / Línea 217: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma "borraTodas y (sust x y xs) = borraTodas x xs"
 quickcheck
@@ Línea 234: / Línea 234: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma "sust x y (borraTodas x zs) = borraTodas x zs"
 by (induct zs, simp_all)
@@ Línea 245: / Línea 245: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma "sust x y (borraTodas z zs) = borraTodas z (sust x y zs)"
 quickcheck
@@ Línea 263: / Línea 263: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma "rev (borra x xs) = borra x (rev xs)"
 quickcheck
@@ Línea 279: / Línea 279: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma borraTodas_append:
    "borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
@@ Línea 291: / Línea 291: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma "rev (borraTodas x xs) = borraTodas x (rev xs)"
 by (induct xs, simp_all add: borraTodas_append)

@@ Línea 20: / Línea 20: @@
 *}
---"jeshorcob, emimarriv,davoremar,juacorvic,marnajgom"
+--"jeshorcob, emimarriv,davoremar,juacorvic,marnajgom, domcadgom"
 fun sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list" where
    "sust x y [] = []"
@@ Línea 34: / Línea 34: @@
 *}
---"jeshorcob, emimarriv,davoremar,juacorvic,marnajgom"
+--"jeshorcob, emimarriv,davoremar,juacorvic,marnajgom, domcadgom"
 lemma sust_append:
    "sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
@@ Línea 48: / Línea 48: @@
 *}
---"jeshorcob,davoremar,marnajgom"
+--"jeshorcob,davoremar,marnajgom, domcadgom"
 lemma rev_sust:
    "rev(sust x y zs) = sust x y (rev zs)"
@@ Línea 66: / Línea 66: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma "sust x y (sust u v zs) = sust u v (sust x y zs)"
 quickcheck
@@ Línea 84: / Línea 84: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma "sust y z (sust x y zs) = sust x z zs"
 quickcheck
@@ Línea 107: / Línea 107: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 fun borra :: "'a ⇒ 'a list ⇒ 'a list" where
    "borra x [] = []"
@@ Línea 124: / Línea 124: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 fun borraTodas :: "'a ⇒ 'a list ⇒ 'a list" where
    "borraTodas x [] = []"
@@ Línea 139: / Línea 139: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma l1: "borra x (borraTodas x xs) = borraTodas x xs"
 by (induct xs, simp_all)
@@ Línea 150: / Línea 150: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma "borraTodas x (borraTodas x xs) = borraTodas x xs"
 by (induct xs, simp_all)
@@ Línea 161: / Línea 161: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma borraTodas_borra:
    "borraTodas x (borra x xs) = borraTodas x xs"
@@ Línea 173: / Línea 173: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma "borra x (borra y xs) = borra y (borra x xs)"
 by (induct xs, simp_all)
@@ Línea 200: / Línea 200: @@
 *}
---"jeshorcob,davoremar,juacorvic,marnajgom"
+--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
 lemma "borra y (sust x y xs) = borra x xs"
 quickcheck

@@ Línea 20: / Línea 20: @@
 *}
---"jeshorcob, emimarriv,davoremar,juacorvic"
+--"jeshorcob, emimarriv,davoremar,juacorvic,marnajgom"
 fun sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list" where
    "sust x y [] = []"
@@ Línea 34: / Línea 34: @@
 *}
---"jeshorcob, emimarriv,davoremar,juacorvic"
+--"jeshorcob, emimarriv,davoremar,juacorvic,marnajgom"
 lemma sust_append:
    "sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
@@ Línea 48: / Línea 48: @@
 *}
---"jeshorcob,davoremar"
+--"jeshorcob,davoremar,marnajgom"
 lemma rev_sust:
    "rev(sust x y zs) = sust x y (rev zs)"
@@ Línea 66: / Línea 66: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma "sust x y (sust u v zs) = sust u v (sust x y zs)"
 quickcheck
@@ Línea 84: / Línea 84: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma "sust y z (sust x y zs) = sust x z zs"
 quickcheck
@@ Línea 107: / Línea 107: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 fun borra :: "'a ⇒ 'a list ⇒ 'a list" where
    "borra x [] = []"
@@ Línea 124: / Línea 124: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 fun borraTodas :: "'a ⇒ 'a list ⇒ 'a list" where
    "borraTodas x [] = []"
@@ Línea 139: / Línea 139: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma l1: "borra x (borraTodas x xs) = borraTodas x xs"
 by (induct xs, simp_all)
@@ Línea 150: / Línea 150: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma "borraTodas x (borraTodas x xs) = borraTodas x xs"
 by (induct xs, simp_all)
@@ Línea 161: / Línea 161: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma borraTodas_borra:
    "borraTodas x (borra x xs) = borraTodas x xs"
@@ Línea 173: / Línea 173: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma "borra x (borra y xs) = borra y (borra x xs)"
 by (induct xs, simp_all)
@@ Línea 200: / Línea 200: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma "borra y (sust x y xs) = borra x xs"
 quickcheck
@@ Línea 217: / Línea 217: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma "borraTodas y (sust x y xs) = borraTodas x xs"
 quickcheck
@@ Línea 234: / Línea 234: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma "sust x y (borraTodas x zs) = borraTodas x zs"
 by (induct zs, simp_all)
@@ Línea 245: / Línea 245: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma "sust x y (borraTodas z zs) = borraTodas z (sust x y zs)"
 quickcheck
@@ Línea 263: / Línea 263: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma "rev (borra x xs) = borra x (rev xs)"
 quickcheck
@@ Línea 279: / Línea 279: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma borraTodas_append:
    "borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
@@ Línea 291: / Línea 291: @@
 *}
---"jeshorcob,davoremar,juacorvic"
+--"jeshorcob,davoremar,juacorvic,marnajgom"
 lemma "rev (borraTodas x xs) = borraTodas x (rev xs)"
 by (induct xs, simp_all add: borraTodas_append)

@@ Línea 37: / Línea 37: @@
 lemma sust_append:
    "sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
 by (induct xs) auto
 text {*
@@ Línea 188: / Línea 190: @@
 --"davoremar"
 lemma "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
 by (induct xs, simp_all add: borraTodas_borra)
 text {*