Relación 5 - Historial de revisiones

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

2018-07-16T15:46:14Z

Texto reemplazado: «isar» por «isabelle»

2014-03-02T21:51:05Z

2014-03-02T21:50:26Z

2014-03-02T21:48:48Z

2014-03-02T21:38:11Z

2014-03-02T21:34:09Z

2014-03-02T21:23:21Z

2014-03-02T21:19:31Z

2014-03-02T21:18:50Z

2014-03-02T21:11:49Z

← Revisión anterior		Revisión del 15:46 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R5: Cuantificadores sobre listas *}		header {* R5: Cuantificadores sobre listas *}

@@ Línea 998: / Línea 998: @@
 *}
--- "maresccas4 irealetei diecabmen1 julrobrel domlloriv marescpla juaruipav"
+-- "maresccas4 irealetei diecabmen1 julrobrel domlloriv marescpla juaruipav jaisalmen zoiruicha"
 lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
 quickcheck

@@ Línea 915: / Línea 915: @@
 *}
--- "maresccas4 irealetei diecabmen1 julrobrel domlloriv marescpla juaruipav"
+-- "maresccas4 irealetei diecabmen1 julrobrel domlloriv marescpla juaruipav jaisalmen zoiruicha"
 lemma "sinDuplicados (borraDuplicados xs)"
 by  (induct xs) (auto simp add: estaEn_borraDuplicados)
@@ Línea 966: / Línea 966: @@
 qed
---"irealetei diecabmen1 domlloriv marescpla juaruipav"
+--"irealetei diecabmen1 domlloriv marescpla juaruipav jaisalmen zoiruicha"
 lemma sinDuplicados_borraDuplicados:
    "sinDuplicados (borraDuplicados xs)"

@@ Línea 860: / Línea 860: @@
 *}
--- "maresccas4 irealetei marescpla diecabmen1 julrobrel domlloriv juaruipav"
+-- "maresccas4 irealetei marescpla diecabmen1 julrobrel domlloriv juaruipav jaisalmen zoiruicha"
 lemma "estaEn a (borraDuplicados2 xs) = estaEn a xs"
 by (induct xs) auto
@@ Línea 886: / Línea 886: @@
 qed
--- "maesccas4 irealetei diecabmen1 domlloriv marescpla juaruipav"
+-- "maesccas4 irealetei diecabmen1 domlloriv marescpla juaruipav jaisalmen zoiruicha"
 lemma estaEn_borraDuplicados_porCasos:
   "estaEn a (borraDuplicados2 xs) = estaEn a xs"

@@ Línea 798: / Línea 798: @@
 *}
--- "diecabmen1 maresccas4 irealetei pabflomar marescpla domlloriv julrobrel juaruipav"
+-- "diecabmen1 maresccas4 irealetei pabflomar marescpla domlloriv julrobrel juaruipav jaisalmen zoiruicha"
 lemma length_borraDuplicados:
@@ Línea 841: / Línea 841: @@
 qed
---"julrobrel"
+--"julrobrel jaisalmen zoiruicha"
 lemma "length (borraDuplicados xs) ≤ length xs"
 proof (induct xs)

@@ Línea 781: / Línea 781: @@
 value " borraDuplicados [1::nat,2,4,2,3]"
--- "maresccas4 irealetei pabflomar marescpla julrobrel domlloriv juaruipav"
+-- "maresccas4 irealetei pabflomar marescpla julrobrel domlloriv juaruipav jaisalmen zoiruicha"
 fun borraDuplicados2 :: "'a list ⇒ 'a list" where
    "borraDuplicados2 [] = []"

@@ Línea 756: / Línea 756: @@
 value "sinDuplicados [1::nat,4,2,4]"
--- "maresccas4 pabflomar marescpla julrobrel domlloriv irealetei juaruipav"
+-- "maresccas4 pabflomar marescpla julrobrel domlloriv irealetei juaruipav jaisalmen zoiruicha"
 fun sinDuplicados2 :: "'a list ⇒ bool" where
    "sinDuplicados [] = True"

@@ Línea 692: / Línea 692: @@
 -- "maresccas4"
 -- "jaisalmen zoiruicha"
 lemma "algunos (λx. x=a) xs = estaEn a xs"
 proof (induct xs)

@@ Línea 641: / Línea 641: @@
 *}
---"irealetei diecabmen1 maresccas4 pabflomar marescpla julrobrel domlloriv juaruipav"
+--"irealetei diecabmen1 maresccas4 pabflomar marescpla julrobrel domlloriv juaruipav jaisalmen zoiruicha"
 fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
    "estaEn x [] = False"