Relación 3 - Historial de revisiones

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

2019-03-06T18:49:15Z

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

Jalonso en 13:04 28 feb 2019

2019-02-28T13:04:09Z

Jalonso en 10:56 28 feb 2019

2019-02-28T10:56:36Z

Antramhur en 11:12 26 ene 2019

2019-01-26T11:12:42Z

Chrgencar en 09:27 24 ene 2019

2019-01-24T09:27:12Z

Alikan en 10:38 13 ene 2019

2019-01-13T10:38:27Z

Jalonso en 11:05 10 ene 2019

2019-01-10T11:05:40Z

Juacanrod en 19:13 9 ene 2019

2019-01-09T19:13:29Z

Giafus1 en 20:45 6 ene 2019

2019-01-06T20:45:28Z

Pabbergue en 17:27 2 ene 2019

2019-01-02T17:27:16Z

@@ Línea 2: / Línea 2: @@
 chapter {* R3: Razonamiento sobre programas *}
-theory R3_Razonamiento_sobre_programas_alu
+theory R3_Razonamiento_sobre_programas
 imports Main
 begin

@@ Línea 65: / Línea 65: @@
 qed
-(* marfruman1 raffergon2 aribatval alfmarcua cammonagu gleherlop chrgencar alikan
+(* marfruman1 raffergon2 aribatval alfmarcua cammonagu gleherlop
-   pabbergue giafus1 antramhur *)
+   chrgencar alikan pabbergue giafus1 antramhur *)
 lemma "sumaImpares n = n*n"
 proof (induct n)
@@ Línea 121: / Línea 121: @@
 qed
-(* marfruman1 alfmarcua hugrubsan enrparalv gleherlop chrgencar juacanrod alikan *)
+(* marfruman1 alfmarcua hugrubsan enrparalv gleherlop chrgencar
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)
@@ Línea 195: / Línea 196: @@
 (* manperjim benber raffergon2 aribatval josgomrom4 hugrubsan cammonagu
-    gleherlop chrgencar marfruman1 pabbergue giafus1 juacanrod antramhur*)
+    gleherlop chrgencar marfruman1 pabbergue giafus1 juacanrod
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)
@@ Línea 320: / Línea 322: @@
 (* manperjim pabalagon raffergon2 aribatval josgomrom4 alfmarcua
-    hugrubsan cammonagu marfruman1 gleherlop chrgencar pabbergue giafus1 juacanrod antramhur*)
+    hugrubsan cammonagu marfruman1 gleherlop chrgencar pabbergue giafus1
 lemma fact2: "factI' n x = x * factR n"
 proof (induction n arbitrary: x)
@@ Línea 357: / Línea 360: @@
 (* manperjim pabalagon raffergon2 josgomrom4 alfmarcua hugrubsan
-    marfruman1 gleherlop chrgencar pabbergue giafus1 juacanrod antramhur *)
+    marfruman1 gleherlop chrgencar pabbergue giafus1 juacanrod
 corollary "factI n = factR n"
 proof -
@@ Línea 398: / Línea 402: @@
 qed
-(* marfruman1 raffergon2 enrparalv alikan gleherlop chrgencar juacanrod *)
+(* marfruman1 raffergon2 enrparalv alikan gleherlop chrgencar
 lemma "amplia xs y = xs @ [y]"
 proof (induct xs)
@@ Línea 413: / Línea 418: @@
 qed
-(* manperjim pabalagon josgomrom4 hugrubsan cammonagu pabbergue antramhur*)
+(* manperjim pabalagon josgomrom4 hugrubsan cammonagu pabbergue
 lemma "amplia xs y = xs @ [y]"
 proof (induction xs)
@@ Línea 421: / Línea 427: @@
    fix a xs
    assume HI: "amplia xs y = xs @ [y]"
-   have "amplia (a#xs) y = a # amplia xs y" by (simp only: amplia.simps(2))
+   have "amplia (a#xs) y = a # amplia xs y"
    also have "... = a # (xs @ [y])" using HI by simp
    finally show "amplia (a#xs) y = (a#xs) @ [y]" by simp

@@ Línea 66: / Línea 66: @@
 (* marfruman1 raffergon2 aribatval alfmarcua cammonagu gleherlop chrgencar alikan
-    pabbergue giafus1 *)
+    pabbergue giafus1 antramhur *)
 lemma "sumaImpares n = n*n"
 proof (induct n)
@@ Línea 121: / Línea 121: @@
 qed
-(* marfruman1 alfmarcua hugrubsan enrparalv gleherlop chrgencar juacanrod alikan*)
+(* marfruman1 alfmarcua hugrubsan enrparalv gleherlop chrgencar juacanrod alikan *)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)
@@ Línea 142: / Línea 142: @@
 (* manperjim pabalagon raffergon2 aribatval cammonagu hugrubsan
-    pabbergue giafus1 *)
+    pabbergue giafus1 antramhur*)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)
@@ Línea 195: / Línea 195: @@
 (* manperjim benber raffergon2 aribatval josgomrom4 hugrubsan cammonagu
-    gleherlop chrgencar marfruman1 pabbergue giafus1 juacanrod *)
+    gleherlop chrgencar marfruman1 pabbergue giafus1 juacanrod antramhur*)
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)
@@ Línea 320: / Línea 320: @@
 (* manperjim pabalagon raffergon2 aribatval josgomrom4 alfmarcua
-    hugrubsan cammonagu marfruman1 gleherlop chrgencar pabbergue giafus1 juacanrod *)
+    hugrubsan cammonagu marfruman1 gleherlop chrgencar pabbergue giafus1 juacanrod antramhur*)
 lemma fact2: "factI' n x = x * factR n"
 proof (induction n arbitrary: x)
@@ Línea 357: / Línea 357: @@
 (* manperjim pabalagon raffergon2 josgomrom4 alfmarcua hugrubsan
-    marfruman1 gleherlop chrgencar pabbergue giafus1 juacanrod *)
+    marfruman1 gleherlop chrgencar pabbergue giafus1 juacanrod antramhur *)
 corollary "factI n = factR n"
 proof -
@@ Línea 413: / Línea 413: @@
 qed
-(* manperjim pabalagon josgomrom4 hugrubsan cammonagu pabbergue *)
+(* manperjim pabalagon josgomrom4 hugrubsan cammonagu pabbergue antramhur*)
 lemma "amplia xs y = xs @ [y]"
 proof (induction xs)

@@ Línea 65: / Línea 65: @@
 qed
-(* marfruman1 raffergon2 aribatval alfmarcua cammonagu gleherlop alikan
+(* marfruman1 raffergon2 aribatval alfmarcua cammonagu gleherlop chrgencar alikan
     pabbergue giafus1 *)
 lemma "sumaImpares n = n*n"
@@ Línea 121: / Línea 121: @@
 qed
-(* marfruman1 alfmarcua hugrubsan enrparalv gleherlop juacanrod alikan*)
+(* marfruman1 alfmarcua hugrubsan enrparalv gleherlop chrgencar juacanrod alikan*)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)
@@ Línea 195: / Línea 195: @@
 (* manperjim benber raffergon2 aribatval josgomrom4 hugrubsan cammonagu
-    gleherlop marfruman1 pabbergue giafus1 juacanrod *)
+    gleherlop chrgencar marfruman1 pabbergue giafus1 juacanrod *)
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)
@@ Línea 320: / Línea 320: @@
 (* manperjim pabalagon raffergon2 aribatval josgomrom4 alfmarcua
-    hugrubsan cammonagu marfruman1 gleherlop pabbergue giafus1 juacanrod *)
+    hugrubsan cammonagu marfruman1 gleherlop chrgencar pabbergue giafus1 juacanrod *)
 lemma fact2: "factI' n x = x * factR n"
 proof (induction n arbitrary: x)
@@ Línea 357: / Línea 357: @@
 (* manperjim pabalagon raffergon2 josgomrom4 alfmarcua hugrubsan
-    marfruman1 gleherlop pabbergue giafus1 juacanrod *)
+    marfruman1 gleherlop chrgencar pabbergue giafus1 juacanrod *)
 corollary "factI n = factR n"
 proof -
@@ Línea 398: / Línea 398: @@
 qed
-(* marfruman1 raffergon2 enrparalv alikan gleherlop juacanrod *)
+(* marfruman1 raffergon2 enrparalv alikan gleherlop chrgencar juacanrod *)
 lemma "amplia xs y = xs @ [y]"
 proof (induct xs)

@@ Línea 121: / Línea 121: @@
 qed
-(* marfruman1 alfmarcua hugrubsan enrparalv gleherlop juacanrod *)
+(* marfruman1 alfmarcua hugrubsan enrparalv gleherlop juacanrod alikan*)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)

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

@@ Línea 2: / Línea 2: @@
 chapter {* R3: Razonamiento sobre programas *}
-theory R3_Razonamiento_sobre_programas
+theory R3_Razonamiento_sobre_programas_alu
 imports Main
 begin
@@ Línea 22: / Línea 22: @@
       sumaImpares n = n*n
    ------------------------------------------------------------------- *}
 (* benber *)
@@ Línea 67: / Línea 65: @@
 qed
-(* marfruman1 raffergon2 aribatval alfmarcua cammonagu gleherlop alikan pabbergue giafus1 *)
+(* marfruman1 raffergon2 aribatval alfmarcua cammonagu gleherlop alikan
 lemma "sumaImpares n = n*n"
 proof (induct n)
@@ Línea 139: / Línea 138: @@
    also have "... = 2^((Suc n)+1)" by simp
    finally show "sumaPotenciasDeDosMasUno (Suc n) = 2^((Suc n)+1)"
-        by simp
+    by simp
 qed
-(* manperjim pabalagon raffergon2 aribatval cammonagu hugrubsan pabbergue giafus1 *)
+(* manperjim pabalagon raffergon2 aribatval cammonagu hugrubsan
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)
@@ Línea 153: / Línea 153: @@
    fix n
    assume HI: "sumaPotenciasDeDosMasUno n = 2^(n+1)"
-   have "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n+1)"
+   have "sumaPotenciasDeDosMasUno (Suc n) =
      by (simp only: sumaPotenciasDeDosMasUno.simps(2))
    also have "... = 2^(n+1) + 2^(n+1)" by (simp only: HI)
@@ Línea 193: / Línea 194: @@
    ------------------------------------------------------------------- *}
-(* manperjim benber raffergon2 aribatval josgomrom4 hugrubsan cammonagu gleherlop marfruman1 pabbergue giafus1 juacanrod *)
+(* manperjim benber raffergon2 aribatval josgomrom4 hugrubsan cammonagu
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)
@@ Línea 301: / Línea 303: @@
      qed
    next
-     show "⋀n. ∀x. factI' n x = x * factR n ⟹ ∀x. factI' (Suc n) x = x * factR (Suc n)"
+     show "⋀n. ∀x. factI' n x = x * factR n ⟹
      proof
        fix x
        fix n
        assume HI: "∀y. factI' n y = y * factR n"
-       have "factI' (Suc n) x =  factI' n (x * Suc n)" by (simp only: factI'.simps(2))
+       have "factI' (Suc n) x =  factI' n (x * Suc n)"
        also have "... = (x * Suc n) * factR n" by (simp only: HI)
        also have "... = x * factR (Suc n)" by (simp only: factR.simps(2))
@@ Línea 315: / Línea 319: @@
 qed
-(* manperjim pabalagon raffergon2 aribatval josgomrom4 alfmarcua hugrubsan cammonagu marfruman1 gleherlop pabbergue giafus1 juacanrod *)
+(* manperjim pabalagon raffergon2 aribatval josgomrom4 alfmarcua
 lemma fact2: "factI' n x = x * factR n"
 proof (induction n arbitrary: x)
@@ Línea 351: / Línea 356: @@
 qed
-(* manperjim pabalagon raffergon2 josgomrom4 alfmarcua hugrubsan marfruman1 gleherlop pabbergue giafus1 juacanrod *)
+(* manperjim pabalagon raffergon2 josgomrom4 alfmarcua hugrubsan
 corollary "factI n = factR n"
 proof -
@@ Línea 392: / Línea 398: @@
 qed
-(*marfruman1 raffergon2 enrparalv alikan gleherlop juacanrod *)
+(* marfruman1 raffergon2 enrparalv alikan gleherlop juacanrod *)
 lemma "amplia xs y = xs @ [y]"
 proof (induct xs)

@@ Línea 67: / Línea 67: @@
 qed
-(* marfruman1 raffergon2 aribatval alfmarcua cammonagu gleherlop alikan *)
+(* marfruman1 raffergon2 aribatval alfmarcua cammonagu gleherlop alikan pabbergue *)
 lemma "sumaImpares n = n*n"
 proof (induct n)
@@ Línea 142: / Línea 142: @@
 qed
-(* manperjim pabalagon raffergon2 aribatval cammonagu hugrubsan *)
+(* manperjim pabalagon raffergon2 aribatval cammonagu hugrubsan pabbergue *)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)
@@ Línea 193: / Línea 193: @@
    ------------------------------------------------------------------- *}
-(* manperjim benber raffergon2 aribatval josgomrom4 hugrubsan cammonagu gleherlop marfruman1*)
+(* manperjim benber raffergon2 aribatval josgomrom4 hugrubsan cammonagu gleherlop marfruman1 pabbergue *)
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)
@@ Línea 315: / Línea 315: @@
 qed
-(* manperjim pabalagon raffergon2 aribatval josgomrom4 alfmarcua hugrubsan cammonagu marfruman1 gleherlop *)
+(* manperjim pabalagon raffergon2 aribatval josgomrom4 alfmarcua hugrubsan cammonagu marfruman1 gleherlop pabbergue *)
 lemma fact2: "factI' n x = x * factR n"
 proof (induction n arbitrary: x)
@@ Línea 351: / Línea 351: @@
 qed
-(* manperjim pabalagon raffergon2 josgomrom4 alfmarcua hugrubsan marfruman1 gleherlop*)
+(* manperjim pabalagon raffergon2 josgomrom4 alfmarcua hugrubsan marfruman1 gleherlop pabbergue *)
 corollary "factI n = factR n"
 proof -
@@ Línea 407: / Línea 407: @@
 qed
-(* manperjim pabalagon josgomrom4 hugrubsan cammonagu*)
+(* manperjim pabalagon josgomrom4 hugrubsan cammonagu pabbergue *)
 lemma "amplia xs y = xs @ [y]"
 proof (induction xs)