Relación 3 - Historial de revisiones

Jalonso en 18:40 14 jul 2018

2018-07-14T18:40:05Z

Cesgongut en 16:58 13 feb 2018

2018-02-13T16:58:53Z

Davperriv en 11:49 8 ene 2018

2018-01-08T11:49:13Z

Jospermon1 en 07:23 30 nov 2017

2017-11-30T07:23:05Z

Cesgongut en 06:30 30 nov 2017

2017-11-30T06:30:33Z

Cesgongut en 06:28 30 nov 2017

2017-11-30T06:28:48Z

Jalonso en 06:24 30 nov 2017

2017-11-30T06:24:05Z

Rafferrod en 02:52 30 nov 2017

2017-11-30T02:52:32Z

Rafferrod en 02:42 30 nov 2017

2017-11-30T02:42:29Z

Rafferrod en 02:38 30 nov 2017

2017-11-30T02:38:21Z

← Revisión anterior		Revisión del 18:40 14 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	chapter {* R3: Razonamiento sobre programas *}		chapter {* R3: Razonamiento sobre programas *}

@@ Línea 116: / Línea 116: @@
    ------------------------------------------------------------------- *}
-(* anddonram edupalhid rafcabgon luicedval macmerflo jescudero diwu2 jospermon1 davperriv *)
+(* anddonram edupalhid rafcabgon luicedval macmerflo jescudero diwu2 jospermon1 davperriv cesgongut *)
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)
@@ Línea 244: / Línea 244: @@
-(* anddonram rafcabgon luicedval macmerflo diwu2 jescudero rafferrod jospermon1 davperriv  *)
+(* anddonram rafcabgon luicedval macmerflo diwu2 jescudero rafferrod jospermon1 davperriv cesgongut *)
 lemma "amplia xs y = xs @ [y]"
 proof (induct xs)

@@ Línea 25: / Línea 25: @@
 -- "La demostración detallada es"
 (* anddonram edupalhid rafcabgon luicedval jescudero macmerflo diwu2
-    rafferrod cesgongut jospermon1 *)
+    rafferrod cesgongut jospermon1 davperriv *)
 lemma "sumaImpares n = n*n"
 proof (induct n)
@@ Línea 56: / Línea 56: @@
    ------------------------------------------------------------------- *}
-(* anddonram edupalhid luicedval macmerflo jescudero diwu2 rafferrod jospermon1 *)
+(* anddonram edupalhid luicedval macmerflo jescudero diwu2 rafferrod jospermon1 davperriv *)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)
@@ Línea 116: / Línea 116: @@
    ------------------------------------------------------------------- *}
-(* anddonram edupalhid rafcabgon luicedval macmerflo jescudero diwu2 jospermon1 *)
+(* anddonram edupalhid rafcabgon luicedval macmerflo jescudero diwu2 jospermon1 davperriv *)
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)
@@ Línea 193: / Línea 193: @@
 qed
-(* edupalhid rafcabgon luicedval macmerflo diwu2 jescudero jospermon1 *)
+(* edupalhid rafcabgon luicedval macmerflo diwu2 jescudero jospermon1 davperriv  *)
 lemma fact': "factI' n x = x * factR n"
 proof (induct n arbitrary: x)
@@ Línea 217: / Línea 217: @@
 (* anddonram edupalhid rafcabgon luicedval macmerflo diwu2 jescudero
-    rafferrod jospermon1 *)
+    rafferrod jospermon1 davperriv *)
 corollary "factI n = factR n"
 proof -
@@ Línea 244: / Línea 244: @@
-(* anddonram rafcabgon luicedval macmerflo diwu2 jescudero rafferrod jospermon1 *)
+(* anddonram rafcabgon luicedval macmerflo diwu2 jescudero rafferrod jospermon1 davperriv  *)
 lemma "amplia xs y = xs @ [y]"
 proof (induct xs)

@@ Línea 25: / Línea 25: @@
 -- "La demostración detallada es"
 (* anddonram edupalhid rafcabgon luicedval jescudero macmerflo diwu2
-    rafferrod cesgongut *)
+    rafferrod cesgongut jospermon1 *)
 lemma "sumaImpares n = n*n"
 proof (induct n)
@@ Línea 56: / Línea 56: @@
    ------------------------------------------------------------------- *}
-(* anddonram edupalhid luicedval macmerflo jescudero diwu2 rafferrod *)
+(* anddonram edupalhid luicedval macmerflo jescudero diwu2 rafferrod jospermon1 *)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)
@@ Línea 116: / Línea 116: @@
    ------------------------------------------------------------------- *}
-(* anddonram edupalhid rafcabgon luicedval macmerflo jescudero diwu2 *)
+(* anddonram edupalhid rafcabgon luicedval macmerflo jescudero diwu2 jospermon1 *)
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)
@@ Línea 193: / Línea 193: @@
 qed
-(* edupalhid rafcabgon luicedval macmerflo diwu2 jescudero*)
+(* edupalhid rafcabgon luicedval macmerflo diwu2 jescudero jospermon1 *)
 lemma fact': "factI' n x = x * factR n"
 proof (induct n arbitrary: x)
@@ Línea 217: / Línea 217: @@
 (* anddonram edupalhid rafcabgon luicedval macmerflo diwu2 jescudero
-    rafferrod*)
+    rafferrod jospermon1 *)
 corollary "factI n = factR n"
 proof -
@@ Línea 244: / Línea 244: @@
-(* anddonram rafcabgon luicedval macmerflo diwu2 jescudero rafferrod *)
+(* anddonram rafcabgon luicedval macmerflo diwu2 jescudero rafferrod jospermon1 *)
 lemma "amplia xs y = xs @ [y]"
 proof (induct xs)

@@ Línea 56: / Línea 56: @@
    ------------------------------------------------------------------- *}
-(* anddonram edupalhid luicedval macmerflo jescudero diwu2 rafferrod cesgongut *)
+(* anddonram edupalhid luicedval macmerflo jescudero diwu2 rafferrod *)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)
@@ Línea 71: / Línea 71: @@
    qed
-(*rafcabgon*)
+(* rafcabgon cesgongut *)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)

@@ Línea 24: / Línea 24: @@
 -- "La demostración detallada es"
-(*anddonram edupalhid rafcabgon luicedval jescudero macmerflo diwu2 rafferrod*)
+(* anddonram edupalhid rafcabgon luicedval jescudero macmerflo diwu2
 lemma "sumaImpares n = n*n"
 proof (induct n)
@@ Línea 31: / Línea 32: @@
    fix n
    assume HI: "sumaImpares n=n*n"
-   have "sumaImpares (Suc n) =sumaImpares n + (2*n+1)" by simp
+   have "sumaImpares (Suc n) = sumaImpares n + (2*n+1)" by simp
    also have "... = n*n + (2*n+1)" using HI by simp
    finally show "sumaImpares (Suc n) =(Suc n) *(Suc n)" by simp
 qed
 text {* ---------------------------------------------------------------
@@ Línea 55: / Línea 55: @@
       sumaPotenciasDeDosMasUno n = 2^(n+1)
    ------------------------------------------------------------------- *}
 (*anddonram edupalhid luicedval macmerflo jescudero diwu2 rafferrod*)
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
 proof (induct n)
@@ Línea 62: / Línea 63: @@
    fix n
    assume HI: "sumaPotenciasDeDosMasUno n = 2^(n+1)"
-   have "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n+1)" by simp
+   have "sumaPotenciasDeDosMasUno (Suc n) =
    also have "... = 2^(n+1) +  2^(n+1)" using HI by simp
    also have "... = 2^((n+1)+1)" by simp
-   finally show "sumaPotenciasDeDosMasUno (Suc n) = 2^(Suc n + 1)" by simp
+   finally show "sumaPotenciasDeDosMasUno (Suc n) = 2^(Suc n + 1)"
    qed
@@ Línea 75: / Línea 78: @@
    fix n
    assume HI: "sumaPotenciasDeDosMasUno n = 2^(n+1)"
-   have "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n+1)" by simp
+   have "sumaPotenciasDeDosMasUno (Suc n) =
    also have "... = 2^(n+1) + 2^(n+1)" using HI by simp
    also have "... = 2^((Suc n) + 1)" by simp
-   finally show "sumaPotenciasDeDosMasUno (Suc n) = 2 ^ (Suc n + 1)" by simp
+   finally show "sumaPotenciasDeDosMasUno (Suc n) = 2 ^ (Suc n + 1)"
 qed
@@ Línea 111: / Línea 116: @@
    ------------------------------------------------------------------- *}
-(*anddonram edupalhid rafcabgon luicedval macmerflo jescudero diwu2*)
+(* anddonram edupalhid rafcabgon luicedval macmerflo jescudero diwu2 *)
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)
@@ Línea 118: / Línea 123: @@
    fix n
    assume HI: "todos (λy. y=x) (copia n x)"
-   have "todos (λy. y=x) (copia (Suc n) x) =todos (λy. y=x) (x#(copia n x)) " by simp
+   have "todos (λy. y=x) (copia (Suc n) x) =
    also have "... =  todos (λy. y=x) (copia n x) " by simp
    show "todos (λy. y=x) (copia (Suc n) x)"  using HI by simp
 qed
-(*rafferrod*)
+(* rafferrod *)
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)
@@ Línea 130: / Línea 136: @@
    fix n
    assume HI: "todos (λy. y=x) (copia n x)"
-   have "todos (λy. y=x) (copia (Suc n) x) = todos (λy. y=x) (x#(copia n x))" by simp
+   have "todos (λy. y=x) (copia (Suc n) x) =
-   also have "... = (((λy. y=x) x) ∧ (todos (λy. y=x) (copia n x)))" by simp
+        todos (λy. y=x) (x#(copia n x))" by simp
    also have "... = True" using HI by simp
    finally show "todos (λy. y=x) (copia (Suc n) x)" by simp
@@ Línea 171: / Línea 179: @@
    "factI n = factI' n 1"
-(*anddonram rafferrod*)
+(* anddonram rafferrod *)
 lemma fact: "factI' n x = x * factR n"
 proof (induct n arbitrary: x)
@@ Línea 179: / Línea 187: @@
    assume HI: "⋀x. factI' n x = x * factR n"
    fix x
-   have "factI' (Suc n) x = factI' n (x*Suc n)" by simp
+   have "factI' (Suc n) x = factI' n (x * Suc n)" by simp
    also have "... = (x * Suc n) * factR n" using HI by simp
    also have "... = x * (Suc n * factR n)" by (simp del:mult_Suc)
@@ Línea 207: / Línea 215: @@
       factI n = factR n
    ------------------------------------------------------------------- *}
 (*anddonram edupalhid rafcabgon luicedval macmerflo diwu2 jescudero rafferrod*)
 corollary "factI n = factR n"
 proof -
@@ Línea 234: / Línea 244: @@
-(*anddonram rafcabgon luicedval macmerflo diwu2 jescudero rafferrod*)
+(* anddonram rafcabgon luicedval macmerflo diwu2 jescudero rafferrod *)
 lemma "amplia xs y = xs @ [y]"
 proof (induct xs)