Relación 3 - Historial de revisiones

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

2018-07-16T15:46:14Z

Texto reemplazado: «isar» por «isabelle»

Jaisalmen en 23:57 2 mar 2014

2014-03-02T23:57:05Z

Jaisalmen en 23:44 2 mar 2014

2014-03-02T23:44:55Z

Jaisalmen en 22:58 2 mar 2014

2014-03-02T22:58:05Z

Jaisalmen en 22:54 2 mar 2014

2014-03-02T22:54:14Z

Jaisalmen en 22:50 2 mar 2014

2014-03-02T22:50:25Z

Jaisalmen en 22:48 2 mar 2014

2014-03-02T22:48:47Z

Jaisalmen en 20:33 2 mar 2014

2014-03-02T20:33:09Z

Jaisalmen en 20:31 2 mar 2014

2014-03-02T20:31:49Z

Jaisalmen en 20:29 2 mar 2014

2014-03-02T20:29:22Z

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

@@ Línea 403: / Línea 403: @@
 qed
 -- "irealetei" (*Éste ha sido la muerte a pellizcos, aún leyéndome todo el tema.*)
 lemma fact2: "factI' n x = x * factR n"
@@ Línea 500: / Línea 502: @@
 qed
--- "irealetei diecabmen1 domlloriv pabflomar juaruipav"
+-- "irealetei diecabmen1 domlloriv pabflomar juaruipav jaisalmen zoiruicha"
 corollary "factI n = factR n"
 by (simp add: fact)

@@ Línea 548: / Línea 548: @@
 qed
---"irealetei diecabmen1 domlloriv pabflomar juaruipav"
+--"irealetei diecabmen1 domlloriv pabflomar juaruipav jaisalmen zoiruicha"
 lemma "amplia xs y = xs @ [y]"
 proof (induct xs)

@@ Línea 276: / Línea 276: @@
 qed
--- "irealetei diecabmen1 pabflomar"
+-- "irealetei diecabmen1 pabflomar jaisalmen zoiruicha"
 lemma "todos (λy. y=x) (copia n x)"
 proof (induct n)

@@ Línea 125: / Línea 125: @@
    ------------------------------------------------------------------- *}
--- "maresccas4 pabflomar juaruipav"
+-- "maresccas4 pabflomar juaruipav jaisalmen zoiruicha"
 lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"

@@ Línea 39: / Línea 39: @@
    ------------------------------------------------------------------- *}
--- "maresccas4 pabflomar juaruipav marescpla jaisalmen"
+-- "maresccas4 pabflomar juaruipav marescpla jaisalmen zoiruicha"
 -- "jaisalmen: con la definición sumaImpares3 me da algunos errores al tratar de probar por inducción"
@@ Línea 112: / Línea 112: @@
 value "sumaPotenciasDeDosMasUno 3" -- "= 16"
--- "ElyIvan jaisalmen"
+-- "ElyIvan jaisalmen zoiruicha"
 fun sumaPotenciasDeDosMasUno2 :: "nat ⇒ nat" where
@@ Línea 217: / Línea 217: @@
    ------------------------------------------------------------------ *}
--- "maresccas4 irealetei diecabmen1 domlloriv pabflomar julrobrel marescpla jaisalmen"
+-- "maresccas4 irealetei diecabmen1 domlloriv pabflomar julrobrel marescpla jaisalmen zoiruicha"
 fun copia :: "nat ⇒ 'a ⇒ 'a list" where
@@ Línea 252: / Línea 252: @@
 value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p [] = True"
@@ Línea 355: / Línea 355: @@
    ------------------------------------------------------------------ *}
--- "maresccas4 irealetei diecabmen1 domlloriv pabflomar julrobrel marescpla jaisalmen"
+-- "maresccas4 irealetei diecabmen1 domlloriv pabflomar julrobrel marescpla jaisalmen zoiruicha"
 fun factR :: "nat ⇒ nat" where
@@ Línea 522: / Línea 522: @@
    ------------------------------------------------------------------ *}
--- "maresccas4 irealetei diecabmen1 domlloriv julrobrel marescpla jaisalmen"
+-- "maresccas4 irealetei diecabmen1 domlloriv julrobrel marescpla jaisalmen zoiruicha"
 fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where

@@ Línea 29: / Línea 29: @@
 value "sumaImpares2 5" -- "= 25"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun sumaImpares3 :: "nat ⇒ nat" where
    "sumaImpares3 0 = 0"

@@ Línea 251: / Línea 251: @@
 value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True"
 value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False"
 text {* ---------------------------------------------------------------