Relación 2 - Historial de revisiones

Jalonso: Protegió «Relación 2» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2019-03-06T18:48:53Z

Protegió «Relación 2» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Jalonso en 13:03 28 feb 2019

2019-02-28T13:03:53Z

Jalonso en 10:51 28 feb 2019

2019-02-28T10:51:46Z

Chrgencar en 09:26 24 ene 2019

2019-01-24T09:26:18Z

Aribatval en 14:31 23 ene 2019

2019-01-23T14:31:38Z

Antramhur en 21:42 13 ene 2019

2019-01-13T21:42:13Z

Antramhur en 21:33 13 ene 2019

2019-01-13T21:33:27Z

Antramhur en 21:29 13 ene 2019

2019-01-13T21:29:07Z

Alikan en 10:21 13 ene 2019

2019-01-13T10:21:37Z

Jalonso en 10:09 10 ene 2019

2019-01-10T10:09:48Z

@@ Línea 2: / Línea 2: @@
 chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *}
-theory R2_Razonamiento_automatico_sobre_programas_alu
+theory R2_Razonamiento_automatico_sobre_programas
 imports Main
 begin

@@ Línea 17: / Línea 17: @@
 (* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
-    hugrubsan enrparalv gleherlop chrgencar giafus1 pabbergue alikan aribatval *)
+    hugrubsan enrparalv gleherlop chrgencar giafus1 pabbergue alikan
 fun sumaImpares :: "nat ⇒ nat" where
    "sumaImpares 0 = 0" |
@@ Línea 124: / Línea 125: @@
    ------------------------------------------------------------------ *}
-(* manperjim pabalagon cammonagu josgomrom4 hugrubsan benber gleherlop chrgencar
+(* manperjim pabalagon cammonagu josgomrom4 hugrubsan benber gleherlop
-    pabbergue alikan antramhur aribatval *)
+    chrgencar pabbergue alikan antramhur aribatval *)
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
    "copia 0 x = []" |
@@ Línea 208: / Línea 209: @@
 (* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
-  josgomrom4 hugrubsan gleherlop enrparalv benber chrgencar giafus1
+   josgomrom4 hugrubsan gleherlop enrparalv benber chrgencar giafus1
-  pabbergue alikan aribatval *)
+   pabbergue alikan aribatval *)
 lemma "amplia xs y = xs @ [y]"
    apply (induction xs)

@@ Línea 124: / Línea 124: @@
    ------------------------------------------------------------------ *}
-(* manperjim pabalagon cammonagu josgomrom4 hugrubsan benber gleherlop
+(* manperjim pabalagon cammonagu josgomrom4 hugrubsan benber gleherlop chrgencar
     pabbergue alikan antramhur aribatval *)
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
@@ Línea 172: / Línea 172: @@
 (* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
-    josgomrom4 hugrubsan enrparalv benber giafus1 pabbergue alikan aribatval *)
+    josgomrom4 hugrubsan enrparalv benber giafus1 pabbergue alikan
 lemma "todos (λy. y=x) (copia n x)"
    apply (induction n)

@@ Línea 17: / Línea 17: @@
 (* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
-    hugrubsan enrparalv gleherlop chrgencar giafus1 pabbergue alikan*)
+    hugrubsan enrparalv gleherlop chrgencar giafus1 pabbergue alikan aribatval *)
 fun sumaImpares :: "nat ⇒ nat" where
    "sumaImpares 0 = 0" |
@@ Línea 41: / Línea 41: @@
 (* manperjim pabalagon cammonagu juacanrod josgomrom4 hugrubsan
-    enrparalv gleherlop benber chrgencar giafus1 alikan*)
+    enrparalv gleherlop benber chrgencar giafus1 alikan aribatval *)
 lemma "sumaImpares n = n*n"
    apply (induction n)
@@ Línea 72: / Línea 72: @@
 (* manperjim pabalagon cammonagu chrgencar hugrubsan gleherlop benber
-    pabbergue *)
+    pabbergue aribatval *)
 fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
    "sumaPotenciasDeDosMasUno 0 = 2" |
@@ Línea 102: / Línea 102: @@
 (* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
     josgomrom4 hugrubsan enrparalv benber chrgencar gleherlop  giafus1
-    pabbergue alikan*)
+    pabbergue alikan aribatval *)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
    apply (induction n)
@@ Línea 125: / Línea 125: @@
 (* manperjim pabalagon cammonagu josgomrom4 hugrubsan benber gleherlop
-    pabbergue alikan antramhur*)
+    pabbergue alikan antramhur aribatval *)
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
    "copia 0 x = []" |
@@ Línea 158: / Línea 158: @@
 (* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
     josgomrom4 marfruman1 hugrubsan enrparalv benber chrgencar giafus1
-    gleherlop pabbergue alikan antramhur*)
+    gleherlop pabbergue alikan antramhur aribatval *)
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p [] = True" |
@@ Línea 172: / Línea 172: @@
 (* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
-    josgomrom4 hugrubsan enrparalv benber giafus1 pabbergue alikan*)
+    josgomrom4 hugrubsan enrparalv benber giafus1 pabbergue alikan aribatval *)
 lemma "todos (λy. y=x) (copia n x)"
    apply (induction n)
@@ Línea 194: / Línea 194: @@
 (* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
     josgomrom4 marfruman1 hugrubsan enrparalv benber chrgencar gleherlop
-    giafus1 pabbergue alikan antramhur *)
+    giafus1 pabbergue alikan antramhur aribatval *)
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
    "amplia [] y = [y]" |
@@ Línea 208: / Línea 208: @@
 (* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
    josgomrom4 hugrubsan gleherlop enrparalv benber chrgencar giafus1
-   pabbergue alikan*)
+   pabbergue alikan aribatval *)
 lemma "amplia xs y = xs @ [y]"
    apply (induction xs)

@@ Línea 194: / Línea 194: @@
 (* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
     josgomrom4 marfruman1 hugrubsan enrparalv benber chrgencar gleherlop
-    giafus1 pabbergue alikan*)
+    giafus1 pabbergue alikan antramhur *)
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
    "amplia [] y = [y]" |
@@ Línea 214: / Línea 214: @@
    done
-(* pabalagon *)
+(* pabalagon antramhur *)
 lemma "amplia xs y = xs @ [y]"
    by (induction xs) simp_all

← Revisión anterior	Revisión del 18:48 6 mar 2019
(Sin diferencias)

@@ Línea 26: / Línea 26: @@
 value "sumaImpares 5  = 25"
-(* josgomrom4 marfruman1 benber *)
+(* josgomrom4 marfruman1 benber antramhur *)
 fun sumaImpares2 :: "nat ⇒ nat" where
    "sumaImpares2 0 = 0" |
@@ Línea 54: / Línea 54: @@
    done
-(* pabalagon *)
+(* pabalagon antramhur *)
 lemma "sumaImpares n = n*n"
    by (induction n) simp_all
@@ Línea 80: / Línea 80: @@
 value "sumaPotenciasDeDosMasUno 3  =  16"
-(* juacanrod josgomrom4 marfruman1*)
+(* juacanrod josgomrom4 marfruman1 antramhur *)
 fun sumaPotenciasDeDosMasUno2 :: "nat ⇒ nat" where
    "sumaPotenciasDeDosMasUno2 0 = 2" |
@@ Línea 108: / Línea 108: @@
    done
-(* pabalagon *)
+(* pabalagon antramhur *)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
    by (induction n) simp_all

@@ Línea 2: / Línea 2: @@
 chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *}
-theory R2_Razonamiento_automatico_sobre_programas
+theory R2_Razonamiento_automatico_sobre_programas_alu
 imports Main
 begin
@@ Línea 16: / Línea 16: @@
    ------------------------------------------------------------------ *}
-(* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2 hugrubsan enrparalv gleherlop chrgencar giafus1 pabbergue *)
+(* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
 fun sumaImpares :: "nat ⇒ nat" where
    "sumaImpares 0 = 0" |
    "sumaImpares n = 2*n-1 + sumaImpares (n-1)"
 (* josgomrom4 marfruman1 benber *)
@@ Línea 36: / Línea 40: @@
    ------------------------------------------------------------------- *}
-(* manperjim pabalagon cammonagu juacanrod josgomrom4 hugrubsan enrparalv gleherlop benber chrgencar giafus1 *)
+(* manperjim pabalagon cammonagu juacanrod josgomrom4 hugrubsan
 lemma "sumaImpares n = n*n"
    apply (induction n)
@@ Línea 66: / Línea 71: @@
    ------------------------------------------------------------------ *}
-(* manperjim pabalagon cammonagu chrgencar hugrubsan gleherlop benber pabbergue *)
+(* manperjim pabalagon cammonagu chrgencar hugrubsan gleherlop benber
 fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
    "sumaPotenciasDeDosMasUno 0 = 2" |
    "sumaPotenciasDeDosMasUno (Suc n) =
 ^(n+1) + sumaPotenciasDeDosMasUno n"
 (* juacanrod josgomrom4 marfruman1*)
@@ Línea 77: / Línea 85: @@
    "sumaPotenciasDeDosMasUno2 (Suc n) =
 ^(Suc n) + sumaPotenciasDeDosMasUno2 n"
 (* alfmarcua raffergon2 enrparalv alikan giafus1 *)
@@ Línea 82: / Línea 92: @@
    "sumaPotenciasDeDosMasUno3 0 = 2" |
    "sumaPotenciasDeDosMasUno3 n = 2^n + sumaPotenciasDeDosMasUno3 (n-1)"
 text {* ---------------------------------------------------------------
@@ Línea 88: / Línea 100: @@
    ------------------------------------------------------------------- *}
-(* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2 josgomrom4
+(* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
-    hugrubsan enrparalv benber chrgencar gleherlop  giafus1 pabbergue *)
+    josgomrom4 hugrubsan enrparalv benber chrgencar gleherlop  giafus1
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
    apply (induction n)
@@ Línea 111: / Línea 124: @@
    ------------------------------------------------------------------ *}
-(* manperjim pabalagon cammonagu josgomrom4 hugrubsan benber gleherlop pabbergue *)
+(* manperjim pabalagon cammonagu josgomrom4 hugrubsan benber gleherlop
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
    "copia 0 x = []" |
    "copia (Suc n) x = x#copia n x"
 (* juacanrod marfruman1 *)
@@ Línea 120: / Línea 136: @@
    "copia2 0 x = []" |
    "copia2 (Suc n) x = [x] @ copia2 n x"
 (* manperjim alfmarcua raffergon2 enrparalv giafus1 *)
@@ Línea 125: / Línea 143: @@
    "copia3 0 x = []" |
    "copia3 n x = x#(copia (n-1) x)"
 text {* ---------------------------------------------------------------
@@ Línea 136: / Línea 156: @@
    ----------------------------------------------------------------- *}
-(* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2 josgomrom4
+(* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
-    marfruman1 hugrubsan enrparalv benber chrgencar giafus1 gleherlop pabbergue *)
+    josgomrom4 marfruman1 hugrubsan enrparalv benber chrgencar giafus1
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p [] = True" |
    "todos p (x#xs) = (p x ∧ todos p xs)"
 text {* ---------------------------------------------------------------
@@ Línea 147: / Línea 171: @@
    ------------------------------------------------------------------- *}
-(* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2 josgomrom4
+(* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
-    hugrubsan enrparalv benber giafus1 pabbergue *)
+    josgomrom4 hugrubsan enrparalv benber giafus1 pabbergue *)
 lemma "todos (λy. y=x) (copia n x)"
    apply (induction n)
@@ Línea 168: / Línea 192: @@
    ------------------------------------------------------------------ *}
-(* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2 josgomrom4
+(* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
-    marfruman1 hugrubsan enrparalv benber chrgencar gleherlop giafus1 pabbergue *)
+    josgomrom4 marfruman1 hugrubsan enrparalv benber chrgencar gleherlop
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
    "amplia [] y = [y]" |
    "amplia (x#xs) y = x # amplia xs y"
 text {* ---------------------------------------------------------------
@@ Línea 179: / Línea 206: @@
    ------------------------------------------------------------------- *}
-(* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2 josgomrom4 hugrubsan gleherlop enrparalv benber chrgencar giafus1 pabbergue *)
+(* manperjim pabalagon cammonagu juacanrod alfmarcua raffergon2
 lemma "amplia xs y = xs @ [y]"
    apply (induction xs)