Relación 6 - Historial de revisiones

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

2018-07-16T15:46:15Z

Texto reemplazado: «isar» por «isabelle»

2014-03-04T03:53:48Z

2014-03-04T03:51:59Z

2014-03-04T03:50:05Z

2014-03-04T03:49:05Z

2014-03-04T03:47:20Z

2014-03-04T03:45:36Z

2014-03-04T03:45:10Z

2014-03-04T03:44:27Z

2014-03-04T03:40:42Z

← Revisión anterior		Revisión del 15:46 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 1679: / Línea 1679: @@
 *}
--- "maresccas4 diecabmen1 marescpla"
+-- "maresccas4 diecabmen1 marescpla jaisalmen zoiruicha"
 lemma
@@ Línea 1796: / Línea 1796: @@
      also have "...=borraTodas x (rev (a#xs))" by simp
      finally show "rev (borraTodas x (a#xs)) = borraTodas x (rev (a#xs))" .
 qed

@@ Línea 1530: / Línea 1530: @@
 *}
--- "maresccas4 irealetei domlloriv diecabmen1 marescpla"
+-- "maresccas4 irealetei domlloriv diecabmen1 marescpla jaisalmen zoiruicha"
 lemma
@@ Línea 1650: / Línea 1650: @@
 qed
 text {*

@@ Línea 1492: / Línea 1492: @@
 *}
--- "maresccas4 irealetei juaruipav domlloriv diecabmen1 marescpla julrobrel"
+-- "maresccas4 irealetei juaruipav domlloriv diecabmen1 marescpla julrobrel jaisalmen zoiruicha"
 lemma
@@ Línea 1512: / Línea 1512: @@
 *}
--- "maresccas4 irealetei juaruipav domlloriv diecabmen1 marescpla julrobrel"
+-- "maresccas4 irealetei juaruipav domlloriv diecabmen1 marescpla julrobrel jaisalmen zoiruicha"
 lemma

← Revisión anterior		Revisión del 03:49 4 mar 2014
Línea 1462:		Línea 1462:


−		+	-- "jaisalmen zoiruicha"
		+	lemma sust_borraTodas:
		+	"sust x y (borraTodas x zs) = borraTodas x zs" (is "?P x y zs")
		+	proof (induct zs)
		+	show "?P x y []" by simp
		+	next
		+	fix a zs
		+	assume HI: "?P x y zs"
		+	show "?P x y (a#zs)"
		+	proof cases
		+	assume C1: "x=a"
		+	then have "sust x y (borraTodas x (a#zs)) = sust x y (borraTodas x zs)" by simp
		+	also have "... = borraTodas x zs" using HI by simp
		+	finally show "?P x y (a#zs)" using C1 by simp
		+	next
		+	assume C2: "x≠a"
		+	then have "sust x y (borraTodas x (a#zs)) = sust x y (a # borraTodas x zs)" by simp
		+	also have "... = a # sust x y (borraTodas x zs)" using C2 by simp
		+	also have "... = a # borraTodas x zs" using HI by simp
		+	finally show "?P x y (a#zs)" using C2 by simp
		+	qed
		+	qed

	text {*		text {*

@@ Línea 1337: / Línea 1337: @@
 *}
--- "maresccas4 irealetei domlloriv diecabmen1 marescpla julrobrel"
+-- "maresccas4 irealetei domlloriv diecabmen1 marescpla julrobrel jaisalmen zoiruicha"
 (*Domlloriv - A mi el quickcheck no me ha encontrado ningún contra ejemplo*)
 lemma

@@ Línea 1299: / Línea 1299: @@
 *}
--- "maresccas4 irealetei juaruipav domlloriv diecabmen1 marescpla julrobrel"
+-- "maresccas4 irealetei juaruipav domlloriv diecabmen1 marescpla julrobrel zoiruicha jaisalmen"
 lemma

@@ Línea 1055: / Línea 1055: @@
 *}
--- "maresccas4 diecabmen1 domlloriv marescpla"
+-- "maresccas4 diecabmen1 domlloriv marescpla jaisalmen zoiruicha"
 lemma
@@ Línea 1271: / Línea 1271: @@
      qed
    qed
 qed

@@ Línea 855: / Línea 855: @@
 *}
--- "maresccas4 domlloriv irealetei diecabmen1 juaruipav pabflomar marescpla julrobrel"
+-- "maresccas4 domlloriv irealetei diecabmen1 juaruipav pabflomar marescpla julrobrel jaisalmen zoiruicha"
 lemma
@@ Línea 1027: / Línea 1027: @@
        show "borra x (borra y xs) = borra y (borra x xs) ⟹ borra x (borra y (a # xs)) = borra y (borra x (a # xs))" using C2 by simp
      qed
 qed