Relación 2 - Historial de revisiones

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

2018-07-16T11:11:19Z

Texto reemplazado: «isar» por «isabelle»

Juacabsou en 12:36 12 feb 2017

2017-02-12T12:36:48Z

Fracorjim1 en 12:12 5 ene 2017

2017-01-05T12:12:18Z

Antsancab1 en 12:08 10 dic 2016

2016-12-10T12:08:18Z

Jalonso: Desprotegió «Relación 2»

2016-12-08T17:46:13Z

Desprotegió «Relación 2»

Jalonso en 12:17 10 nov 2016

2016-11-10T12:17:04Z

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

2016-11-10T12:12:59Z

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

Josgarsan20 en 11:26 10 nov 2016

2016-11-10T11:26:46Z

Josgarsan20 en 11:12 10 nov 2016

2016-11-10T11:12:55Z

Dancorgar en 01:02 10 nov 2016

2016-11-10T01:02:47Z

← Revisión anterior		Revisión del 11:11 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *}		chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *}

@@ Línea 67: / Línea 67: @@
 value "sumaImpares2 5 = 25"
-(* anaprarod danrodcha crigomgom migtermor pabrodmac*)
+(* anaprarod danrodcha crigomgom migtermor pabrodmac juacabsou *)
 fun sumaImpares3 :: "nat ⇒ nat" where
    "sumaImpares3 0 = 0"
@@ Línea 103: / Línea 103: @@
 (* ivamenjim wilmorort anaprarod crigomgom manmorjim1 pablucoto
     serrodcal marcarmor13 rubgonmar pabrodmac marpoldia1 josgarsan
-    jeamacpov dancorgar antsancab1 fracorjim1 *)
+    jeamacpov dancorgar antsancab1 fracorjim1 juacabsou *)
 lemma "sumaImpares n = n*n"
 apply (induct n)
@@ Línea 181: / Línea 181: @@
 (* fraortmoy anaprarod danrodcha crigomgom migtermor manmorjim1
-    fracorjim1 paupeddeg josgarsan dancorgar antsancab1 *)
+    fracorjim1 paupeddeg josgarsan dancorgar antsancab1 juacabsou *)
 fun sumaPotenciasDeDosMasUno2 :: "nat ⇒ nat" where
    "sumaPotenciasDeDosMasUno2 0 = 2"
@@ Línea 203: / Línea 203: @@
 (* wilmorort ivamenjim fraortmoy anaprarod crigomgom pablucoto serrodcal
     manmorjim1 marcarmor13 rubgonmar pabrodmac josgarsan jeamacpov
-    dancorgar antsancab1 *)
+    dancorgar antsancab1 juacabsou *)
 (* esta demostración funciona con sumaPotenciasDeDosMasUno2 *)
@@ Línea 245: / Línea 245: @@
 (* danrodcha crigomgom migtermor manmorjim1 fracorjim1 pabrodmac
-    paupeddeg josgarsan dancorgar antsancab1 *)
+    paupeddeg josgarsan dancorgar antsancab1 juacabsou *)
 fun copia2 :: "nat ⇒ 'a ⇒ 'a list" where
    "copia2 0 x = []"
@@ Línea 282: / Línea 282: @@
 (* fraortmoy anaprarod danrodcha crigomgom migtermor ivamenjim serrodcal
     pablucoto ferrenseg rubgonmar pabrodmac paupeddeg marcarmor13
-    jeamacpov dancorgar josgarsan antsancab1 fracorjim1 *)
+    jeamacpov dancorgar josgarsan antsancab1 fracorjim1 juacabsou *)
 fun todos1 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos1 p []     = True"
@@ Línea 304: / Línea 304: @@
 (* wilmorort fraortmoy anaprarod crigomgom ivamenjim serrodcal
     manmorjim1 pablucoto rubgonmar pabrodmac marcarmor13 dancorgar
-    josgarsan antsancab1 *)
+    josgarsan antsancab1 juacabsou *)
 lemma "todos (λy. y=x) (copia n x)"
 apply (induct n)
@@ Línea 339: / Línea 339: @@
 (* wilmorort fraortmoy anaprarod crigomgom migtermor ivamenjim serrodcal
     manmorjim1 pablucoto ferrenseg rubgonmar pabrodmac paupeddeg
-    marcarmor13 jeamacpov dancorgar josgarsan antsancab1 fracorjim1 *)
+    marcarmor13 jeamacpov dancorgar josgarsan antsancab1 fracorjim1 juacabsou *)
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
     "amplia [] y     = [y] "
@@ Línea 353: / Línea 353: @@
 (* wilmorort fraortmoy anaprarod crigomgom ivamenjim serrodcal
     manmorjim1 pablucoto rubgonmar pabrodmac marcarmor13 jeamacpov
-    dancorgar josgarsan antsancab1 fracorjim1 *)
+    dancorgar josgarsan antsancab1 fracorjim1 juacabsou *)
 lemma "amplia xs y = xs @ [y]"
 apply (induct xs)

@@ Línea 103: / Línea 103: @@
 (* ivamenjim wilmorort anaprarod crigomgom manmorjim1 pablucoto
     serrodcal marcarmor13 rubgonmar pabrodmac marpoldia1 josgarsan
-    jeamacpov dancorgar antsancab1 *)
+    jeamacpov dancorgar antsancab1 fracorjim1 *)
 lemma "sumaImpares n = n*n"
 apply (induct n)
@@ Línea 282: / Línea 282: @@
 (* fraortmoy anaprarod danrodcha crigomgom migtermor ivamenjim serrodcal
     pablucoto ferrenseg rubgonmar pabrodmac paupeddeg marcarmor13
-    jeamacpov dancorgar josgarsan antsancab1 *)
+    jeamacpov dancorgar josgarsan antsancab1 fracorjim1 *)
 fun todos1 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos1 p []     = True"
@@ Línea 322: / Línea 322: @@
    thus "?P (Suc n)" by simp
 qed
 text {* ---------------------------------------------------------------
@@ Línea 333: / Línea 339: @@
 (* wilmorort fraortmoy anaprarod crigomgom migtermor ivamenjim serrodcal
     manmorjim1 pablucoto ferrenseg rubgonmar pabrodmac paupeddeg
-    marcarmor13 jeamacpov dancorgar josgarsan antsancab1 *)
+    marcarmor13 jeamacpov dancorgar josgarsan antsancab1 fracorjim1 *)
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
     "amplia [] y     = [y] "
@@ Línea 347: / Línea 353: @@
 (* wilmorort fraortmoy anaprarod crigomgom ivamenjim serrodcal
     manmorjim1 pablucoto rubgonmar pabrodmac marcarmor13 jeamacpov
-    dancorgar josgarsan antsancab1 *)
+    dancorgar josgarsan antsancab1 fracorjim1 *)
 lemma "amplia xs y = xs @ [y]"
 apply (induct xs)

@@ Línea 60: / Línea 60: @@
   *)
-(* fraortmoy *)
+(* fraortmoy antsancab1 *)
 fun sumaImpares2 :: "nat ⇒ nat" where
    "sumaImpares2 0 = 0"
@@ Línea 103: / Línea 103: @@
 (* ivamenjim wilmorort anaprarod crigomgom manmorjim1 pablucoto
     serrodcal marcarmor13 rubgonmar pabrodmac marpoldia1 josgarsan
-    jeamacpov dancorgar *)
+    jeamacpov dancorgar antsancab1 *)
 lemma "sumaImpares n = n*n"
 apply (induct n)
@@ Línea 181: / Línea 181: @@
 (* fraortmoy anaprarod danrodcha crigomgom migtermor manmorjim1
-    fracorjim1 paupeddeg josgarsan dancorgar *)
+    fracorjim1 paupeddeg josgarsan dancorgar antsancab1 *)
 fun sumaPotenciasDeDosMasUno2 :: "nat ⇒ nat" where
    "sumaPotenciasDeDosMasUno2 0 = 2"
@@ Línea 203: / Línea 203: @@
 (* wilmorort ivamenjim fraortmoy anaprarod crigomgom pablucoto serrodcal
     manmorjim1 marcarmor13 rubgonmar pabrodmac josgarsan jeamacpov
-    dancorgar *)
+    dancorgar antsancab1 *)
 (* esta demostración funciona con sumaPotenciasDeDosMasUno2 *)
@@ Línea 245: / Línea 245: @@
 (* danrodcha crigomgom migtermor manmorjim1 fracorjim1 pabrodmac
-    paupeddeg josgarsan dancorgar *)
+    paupeddeg josgarsan dancorgar antsancab1 *)
 fun copia2 :: "nat ⇒ 'a ⇒ 'a list" where
    "copia2 0 x = []"
@@ Línea 282: / Línea 282: @@
 (* fraortmoy anaprarod danrodcha crigomgom migtermor ivamenjim serrodcal
     pablucoto ferrenseg rubgonmar pabrodmac paupeddeg marcarmor13
-    jeamacpov dancorgar josgarsan *)
+    jeamacpov dancorgar josgarsan antsancab1 *)
 fun todos1 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos1 p []     = True"
@@ Línea 304: / Línea 304: @@
 (* wilmorort fraortmoy anaprarod crigomgom ivamenjim serrodcal
     manmorjim1 pablucoto rubgonmar pabrodmac marcarmor13 dancorgar
-    josgarsan *)
+    josgarsan antsancab1 *)
 lemma "todos (λy. y=x) (copia n x)"
 apply (induct n)
@@ Línea 333: / Línea 333: @@
 (* wilmorort fraortmoy anaprarod crigomgom migtermor ivamenjim serrodcal
     manmorjim1 pablucoto ferrenseg rubgonmar pabrodmac paupeddeg
-    marcarmor13 jeamacpov dancorgar josgarsan*)
+    marcarmor13 jeamacpov dancorgar josgarsan antsancab1 *)
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
     "amplia [] y     = [y] "
@@ Línea 347: / Línea 347: @@
 (* wilmorort fraortmoy anaprarod crigomgom ivamenjim serrodcal
     manmorjim1 pablucoto rubgonmar pabrodmac marcarmor13 jeamacpov
-    dancorgar josgarsan *)
+    dancorgar josgarsan antsancab1 *)
 lemma "amplia xs y = xs @ [y]"
 apply (induct xs)

@@ Línea 102: / Línea 102: @@
 (* ivamenjim wilmorort anaprarod crigomgom manmorjim1 pablucoto
-    serrodcal marcarmor13 rubgonmar pabrodmac marpoldia1 josgarsan jeamacpov dancorgar *)
+    serrodcal marcarmor13 rubgonmar pabrodmac marpoldia1 josgarsan
 lemma "sumaImpares n = n*n"
 apply (induct n)
@@ Línea 201: / Línea 202: @@
 (* wilmorort ivamenjim fraortmoy anaprarod crigomgom pablucoto serrodcal
-    manmorjim1 marcarmor13 rubgonmar pabrodmac josgarsan jeamacpov dancorgar *)
+    manmorjim1 marcarmor13 rubgonmar pabrodmac josgarsan jeamacpov
 (* esta demostración funciona con sumaPotenciasDeDosMasUno2 *)
@@ Línea 279: / Línea 281: @@
 (* fraortmoy anaprarod danrodcha crigomgom migtermor ivamenjim serrodcal
-    pablucoto ferrenseg rubgonmar pabrodmac paupeddeg marcarmor13 jeamacpov dancorgar
+    pablucoto ferrenseg rubgonmar pabrodmac paupeddeg marcarmor13
-   josgarsan *)
+   jeamacpov dancorgar josgarsan *)
 fun todos1 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos1 p []     = True"
@@ Línea 301: / Línea 303: @@
 (* wilmorort fraortmoy anaprarod crigomgom ivamenjim serrodcal
-    manmorjim1 pablucoto rubgonmar pabrodmac marcarmor13 dancorgar josgarsan *)
+    manmorjim1 pablucoto rubgonmar pabrodmac marcarmor13 dancorgar
 lemma "todos (λy. y=x) (copia n x)"
 apply (induct n)
@@ Línea 343: / Línea 346: @@
 (* wilmorort fraortmoy anaprarod crigomgom ivamenjim serrodcal
-    manmorjim1 pablucoto rubgonmar pabrodmac marcarmor13 jeamacpov dancorgar
+    manmorjim1 pablucoto rubgonmar pabrodmac marcarmor13 jeamacpov
-    josgarsan *)
+    dancorgar josgarsan *)
 lemma "amplia xs y = xs @ [y]"
 apply (induct xs)

← Revisión anterior	Revisión del 17:46 8 dic 2016
(Sin diferencias)

← Revisión anterior	Revisión del 12:12 10 nov 2016
(Sin diferencias)