Relación 4 - Historial de revisiones

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

2018-07-16T15:46:14Z

Texto reemplazado: «isar» por «isabelle»

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

2013-12-07T07:57:05Z

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

Pabflomar en 11:34 5 dic 2013

2013-12-05T11:34:52Z

Marescpla en 10:12 5 dic 2013

2013-12-05T10:12:31Z

Juaruipav en 22:40 4 dic 2013

2013-12-04T22:40:43Z

Jaisalmen en 22:08 4 dic 2013

2013-12-04T22:08:03Z

Jaisalmen en 22:06 4 dic 2013

2013-12-04T22:06:37Z

Diecabmen1 en 22:45 3 dic 2013

2013-12-03T22:45:28Z

Domlloriv en 16:29 3 dic 2013

2013-12-03T16:29:22Z

Irealetei en 07:15 2 dic 2013

2013-12-02T07:15:53Z

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

@@ Línea 73: / Línea 73: @@
 (* maresccas4 - ¿Tiene sentido realizar la demostración automática por simplificación y
 posteriormente hacerla detallada haciendo uso de la inducción? *)
 -- "pabflomar diecabmen1"

@@ Línea 17: / Línea 17: @@
    ---------------------------------------------------------------------
 *}
--- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen juaruipav"
+-- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen juaruipav marescpla"
 fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
    "snoc [] a = [a]"
@@ Línea 30: / Línea 30: @@
    ---------------------------------------------------------------------
 *}
--- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen juaruipav"
+-- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen juaruipav marescpla"
 lemma "snoc xs a = xs @ [a]"
 by (induct xs) auto
@@ Línea 41: / Línea 41: @@
    ---------------------------------------------------------------------
 *}
--- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen juaruipav"
+-- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen juaruipav marescpla"
 lemma snoc_append: "snoc xs a = xs @ [a]"
 proof (induct xs)
@@ Línea 60: / Línea 60: @@
 *}
--- "pabflomar irealetei maresccas4 domlloriv jaisalmen juaruipav"
+-- "pabflomar irealetei maresccas4 domlloriv jaisalmen juaruipav marescpla"
 lemma "rev (x # xs) = snoc (rev xs) x"
 by (simp add: snoc_append)
@@ Línea 87: / Línea 87: @@
--- "maresccas4 irealetei domlloriv jaisalmen juaruipav" (* Marco, como siempre, tiene razón. Abandono el barco, Pablo*)(*definitivamente esto es magia callejera para mi. Marco podrías poner una breve explicación de como obtuviste la definición de rev para poner el rev.simp?, diecabmen1*)
+-- "maresccas4 irealetei domlloriv jaisalmen juaruipav marescpla" (* Marco, como siempre, tiene razón. Abandono el barco, Pablo*)(*definitivamente esto es magia callejera para mi. Marco podrías poner una breve explicación de como obtuviste la definición de rev para poner el rev.simp?, diecabmen1*)
 lemma "rev (x # xs) = snoc (rev xs) x"
 proof -

@@ Línea 17: / Línea 17: @@
    ---------------------------------------------------------------------
 *}
--- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen"
+-- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen juaruipav"
 fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
    "snoc [] a = [a]"
@@ Línea 30: / Línea 30: @@
    ---------------------------------------------------------------------
 *}
--- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen"
+-- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen juaruipav"
 lemma "snoc xs a = xs @ [a]"
 by (induct xs) auto
@@ Línea 41: / Línea 41: @@
    ---------------------------------------------------------------------
 *}
--- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen"
+-- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen juaruipav"
 lemma snoc_append: "snoc xs a = xs @ [a]"
 proof (induct xs)
@@ Línea 60: / Línea 60: @@
 *}
--- "pabflomar irealetei maresccas4 domlloriv jaisalmen"
+-- "pabflomar irealetei maresccas4 domlloriv jaisalmen juaruipav"
 lemma "rev (x # xs) = snoc (rev xs) x"
 by (simp add: snoc_append)
@@ Línea 87: / Línea 87: @@
--- "maresccas4 irealetei domlloriv jaisalmen" (* Marco, como siempre, tiene razón. Abandono el barco, Pablo*)(*definitivamente esto es magia callejera para mi. Marco podrías poner una breve explicación de como obtuviste la definición de rev para poner el rev.simp?, diecabmen1*)
+-- "maresccas4 irealetei domlloriv jaisalmen juaruipav" (* Marco, como siempre, tiene razón. Abandono el barco, Pablo*)(*definitivamente esto es magia callejera para mi. Marco podrías poner una breve explicación de como obtuviste la definición de rev para poner el rev.simp?, diecabmen1*)
 lemma "rev (x # xs) = snoc (rev xs) x"
 proof -

@@ Línea 87: / Línea 87: @@
--- "maresccas4 irealetei domlloriv" (* Marco, como siempre, tiene razón. Abandono el barco, Pablo*)(*definitivamente esto es magia callejera para mi. Marco podrías poner una breve explicación de como obtuviste la definición de rev para poner el rev.simp?, diecabmen1*)
+-- "maresccas4 irealetei domlloriv jaisalmen" (* Marco, como siempre, tiene razón. Abandono el barco, Pablo*)(*definitivamente esto es magia callejera para mi. Marco podrías poner una breve explicación de como obtuviste la definición de rev para poner el rev.simp?, diecabmen1*)
 lemma "rev (x # xs) = snoc (rev xs) x"
 proof -

← Revisión anterior	Revisión del 07:57 7 dic 2013
(Sin diferencias)

@@ Línea 86: / Línea 86: @@
 qed
--- "maresccas4"
+-- "maresccas4 irealetei" (* Marco, como siempre, tiene razón. Abandono el barco, Pablo*)
 lemma "rev (x # xs) = snoc (rev xs) x"
 proof -