Relación 12 - Historial de revisiones

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

2018-07-16T15:46:13Z

Texto reemplazado: «isar» por «isabelle»

Domlloriv en 17:56 10 mar 2014

2014-03-10T17:56:22Z

Zoiruicha en 01:14 10 mar 2014

2014-03-10T01:14:56Z

Marescpla en 22:26 9 mar 2014

2014-03-09T22:26:10Z

Maresccas4 en 20:22 9 mar 2014

2014-03-09T20:22:59Z

Irealetei en 19:25 9 mar 2014

2014-03-09T19:25:00Z

Irealetei en 19:22 9 mar 2014

2014-03-09T19:22:06Z

Irealetei en 19:12 9 mar 2014

2014-03-09T19:12:35Z

Irealetei en 18:33 9 mar 2014

2014-03-09T18:33:38Z

Jaisalmen en 16:53 9 mar 2014

2014-03-09T16:53:59Z

@@ Línea 1: / Línea 1: @@
-<source lang="isar">
+<source lang="isabelle">
 header {* R12: Representación de fórmulas proposicionales mediante
    polinomios *}

@@ Línea 59: / Línea 59: @@
    ------------------------------------------------------------------ *}
---"diecabmen1 irealetei pabflomar jaisalmen zoiruicha maresccas4 marescpla"
+--"diecabmen1 irealetei pabflomar jaisalmen zoiruicha maresccas4 marescpla domlloriv"
 -- "jaisalmen: http://es.wikipedia.org/wiki/Disyunci%C3%B3n_exclusiva"
 -- "jaisalmen: de la definicion de xor: p xor q  =  (   p∧¬  q) or (¬ p ∧ q)"
@@ Línea 106: / Línea 106: @@
    --------------------------------------------------------------------- *}
---"diecabmen1 irealetei maresccas4 marescpla jaisalmen zoiruicha"
+--"diecabmen1 irealetei maresccas4 marescpla jaisalmen zoiruicha domlloriv"
 fun valorF :: "(nat ⇒ bool) ⇒ form ⇒ bool" where
    "valorF i T = True"
@@ Línea 127: / Línea 127: @@
    --------------------------------------------------------------------- *}
---"diecabmen1 irealetei maresccas4 marescpla jaisalmen zoiruicha"
+--"diecabmen1 irealetei maresccas4 marescpla jaisalmen zoiruicha domlloriv"
 fun formM :: "nat list ⇒ form" where
    "formM [] = T"
@@ Línea 155: / Línea 155: @@
 value "valorM (int1(0:=True,1:=True,2:=True)) [0,2,1]"
---"diecabmen1 irealetei"
+--"diecabmen1 irealetei domlloriv"
 lemma correccion_valorM:
    "valorM i m = valorF i (formM m)"
@@ Línea 200: / Línea 200: @@
    --------------------------------------------------------------------- *}
---"diecabmen1 irealetei maresccas4 marescpla"
+--"diecabmen1 irealetei maresccas4 marescpla domlloriv"
 fun formP :: "nat list list ⇒ form" where
    "formP [] = Xor T T"

@@ Línea 106: / Línea 106: @@
    --------------------------------------------------------------------- *}
---"diecabmen1 irealetei maresccas4 marescpla"
+--"diecabmen1 irealetei maresccas4 marescpla jaisalmen zoiruicha"
 fun valorF :: "(nat ⇒ bool) ⇒ form ⇒ bool" where
    "valorF i T = True"
@@ Línea 127: / Línea 127: @@
    --------------------------------------------------------------------- *}
---"diecabmen1 irealetei maresccas4 marescpla"
+--"diecabmen1 irealetei maresccas4 marescpla jaisalmen zoiruicha"
 fun formM :: "nat list ⇒ form" where
    "formM [] = T"

@@ Línea 59: / Línea 59: @@
    ------------------------------------------------------------------ *}
---"diecabmen1 irealetei pabflomar jaisalmen zoiruicha maresccas4"
+--"diecabmen1 irealetei pabflomar jaisalmen zoiruicha maresccas4 marescpla"
 -- "jaisalmen: http://es.wikipedia.org/wiki/Disyunci%C3%B3n_exclusiva"
 -- "jaisalmen: de la definicion de xor: p xor q  =  (   p∧¬  q) or (¬ p ∧ q)"
@@ Línea 106: / Línea 106: @@
    --------------------------------------------------------------------- *}
---"diecabmen1 irealetei maresccas4"
+--"diecabmen1 irealetei maresccas4 marescpla"
 fun valorF :: "(nat ⇒ bool) ⇒ form ⇒ bool" where
    "valorF i T = True"
@@ Línea 127: / Línea 127: @@
    --------------------------------------------------------------------- *}
---"diecabmen1 irealetei maresccas4"
+--"diecabmen1 irealetei maresccas4 marescpla"
 fun formM :: "nat list ⇒ form" where
    "formM [] = T"
@@ Línea 147: / Línea 147: @@
    --------------------------------------------------------------------- *}
---"diecabmen1 irealetei maresccas4"
+--"diecabmen1 irealetei maresccas4 marescpla"
 fun valorM :: "(nat ⇒ bool) ⇒ nat list ⇒ bool" where
    "valorM i [] = True"
@@ Línea 171: / Línea 171: @@
 qed
---"irealetei maresccas4"
+--"irealetei maresccas4 marescpla"
 lemma correccion_valorM_detalle:
    "valorM i m = valorF i (formM m)"
@@ Línea 200: / Línea 200: @@
    --------------------------------------------------------------------- *}
---"diecabmen1 irealetei maresccas4"
+--"diecabmen1 irealetei maresccas4 marescpla"
 fun formP :: "nat list list ⇒ form" where
    "formP [] = Xor T T"

@@ Línea 59: / Línea 59: @@
    ------------------------------------------------------------------ *}
---"diecabmen1 irealetei pabflomar jaisalmen zoiruicha"
+--"diecabmen1 irealetei pabflomar jaisalmen zoiruicha maresccas4"
 -- "jaisalmen: http://es.wikipedia.org/wiki/Disyunci%C3%B3n_exclusiva"
 -- "jaisalmen: de la definicion de xor: p xor q  =  (   p∧¬  q) or (¬ p ∧ q)"
@@ Línea 428: / Línea 428: @@
 lemma lema2: "xor a (xor b c) = xor (xor a b) c"
 by (auto simp add: xor_def)
 lemma valorP_conc:

@@ Línea 402: / Línea 402: @@
    --------------------------------------------------------------------- *}
---"irealetei"
+--"irealetei: tenía una de más que no valía para nada, se me queda igual que maresccas4"
 fun producto :: "nat list list ⇒ nat list list ⇒ nat list list" where
-   "producto p [] = []"
+   "producto [] q = []"
 | "producto (a1 # p) (q) = (productoM a1 q)@(producto p q)"

@@ Línea 425: / Línea 425: @@
 -- "maresccas4 irealetei"
--- "Si me da tiempo, intentaré probar este lema"
+-- "Si me da tiempo, intentaré probar este lema. Irealetei: lo estoy intentando pero me he quedado en: '((a ∧ (¬b ∨ c) ∧ (b∨¬c))  ∨ (¬a ∧ ((b∧¬c) ∨ (¬b∧c ))))' y me va a petar el cerebro..."
 lemma lema2: "xor a (xor b c) = xor (xor a b) c"
 by (auto simp add: xor_def)

@@ Línea 507: / Línea 507: @@
    --------------------------------------------------------------------- *}
--- "maresccas4"
+-- "maresccas4 irealetei"
 theorem correccion_polinomio: