Relación 4 - Historial de revisiones

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

2019-03-06T18:49:39Z

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

Jalonso en 13:04 28 feb 2019

2019-02-28T13:04:24Z

Jalonso en 11:04 28 feb 2019

2019-02-28T11:04:31Z

Aribatval en 18:13 8 feb 2019

2019-02-08T18:13:49Z

Aribatval en 18:12 8 feb 2019

2019-02-08T18:12:51Z

Hugrubsan en 18:57 1 feb 2019

2019-02-01T18:57:10Z

Alikan en 12:29 30 ene 2019

2019-01-30T12:29:49Z

Juacanrod en 19:52 29 ene 2019

2019-01-29T19:52:54Z

Antramhur en 22:03 27 ene 2019

2019-01-27T22:03:43Z

Chrgencar en 09:29 24 ene 2019

2019-01-24T09:29:57Z

@@ Línea 2: / Línea 2: @@
 chapter {* R4: Cuantificadores sobre listas *}
-theory R4_Cuantificadores_sobre_listas_alu
+theory R4_Cuantificadores_sobre_listas
 imports Main
 begin

@@ Línea 109: / Línea 109: @@
 qed
-(* manperjim josgomrom4 raffergon2 cammonagu enrparalv gleherlop chrgencar giafus1
+(* manperjim josgomrom4 raffergon2 cammonagu enrparalv gleherlop
-   pabbergue alikan marfruman1 antramhur hugrubsan aribatval *)
+   chrgencar giafus1 pabbergue alikan marfruman1 antramhur hugrubsan
 lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
 proof (induct xs)
@@ Línea 173: / Línea 174: @@
 (* manperjim pabalagon josgomrom4 raffergon2 cammonagu enrparalv
-    gleherlop chrgencar giafus1 pabbergue alikan antramhur juacanrod hugrubsan *)
+    gleherlop chrgencar giafus1 pabbergue alikan antramhur juacanrod
 lemma todos_append:
    "todos P (x @ y) = (todos P x ∧ todos P y)"
@@ Línea 193: / Línea 195: @@
    have "todos P ([] @ y) = todos P y" by (simp only: append_Nil)
    also have "... = (True ∧ todos P y)" by (simp only: simp_thms(22))
-   also have "... = (todos P [] ∧ todos P y)" by (simp only: todos.simps(1))
+   also have "... = (todos P [] ∧ todos P y)"
    finally show "?P []" .
 next
@@ Línea 239: / Línea 242: @@
 (* manperjim pabalagon josgomrom4 alfmarcua aribatval cammonagu
-    raffergon2 giafus1 pabbergue enrparalv alikan antramhur juacanrod hugrubsan *)
+    raffergon2 giafus1 pabbergue enrparalv alikan antramhur juacanrod
 lemma "todos P (rev xs) = todos P xs"
    by (induct xs) (simp_all add: HOL.conj_comms todos_append)
@@ Línea 255: / Línea 259: @@
 (* manperjim pabalagon josgomrom4 raffergon2 cammonagu gleherlop giafus1
-    pabbergue enrparalv marfruman1 alikan chrgencar antramhur juacanrod hugrubsan aribatval *)
+    pabbergue enrparalv marfruman1 alikan chrgencar antramhur juacanrod
 lemma "todos P (rev xs) = todos P xs"
 proof (induct xs)
@@ Línea 331: / Línea 336: @@
    algunos even [1, 2::nat] ∧ algunos odd [1, 2::nat]"
-(* manperjim alfmarcua raffergon2 gleherlop chrgencar cammonagu giafus1 pabbergue
+(* manperjim alfmarcua raffergon2 gleherlop chrgencar cammonagu giafus1
-    marfruman1 alikan antramhur juacanrod hugrubsan aribatval *)
+    pabbergue marfruman1 alikan antramhur juacanrod hugrubsan
 lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
    quickcheck
@@ Línea 372: / Línea 378: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 gleherlop
-    cammonagu benber giafus1 pabbergue enrparalv marfruman1 alikan antramhur juacanrod hugrubsan aribatval *)
+    cammonagu benber giafus1 pabbergue enrparalv marfruman1 alikan
 lemma "algunos P (map f xs) = algunos (P o f) xs"
    by (induct xs) auto
@@ Línea 383: / Línea 390: @@
 *}
-(* manperjim pabalagon cammonagu giafus1 gleherlop chrgencar pabbergue enrparalv
+(* manperjim pabalagon cammonagu giafus1 gleherlop chrgencar pabbergue
-    marfruman1 alikan antramhur juacanrod hugrubsan *)
+    enrparalv marfruman1 alikan antramhur juacanrod hugrubsan *)
 lemma "algunos P (map f xs) = algunos (P o f) xs"
 proof (induct xs)
@@ Línea 548: / Línea 555: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 gleherlop chrgencar
-    cammonagu giafus1 pabbergue enrparalv alikan antramhur juacanrod hugrubsan aribatval *)
+    cammonagu giafus1 pabbergue enrparalv alikan antramhur juacanrod
 lemma "algunos P (rev xs) = algunos P xs"
    by (induct xs) (simp_all add: HOL.disj_comms algunos_append)
@@ Línea 579: / Línea 587: @@
 qed
-(* manperjim josgomrom4 raffergon2 gleherlop chrgencar cammonagu giafus1 pabbergue
+(* manperjim josgomrom4 raffergon2 gleherlop chrgencar cammonagu giafus1
-    enrparalv marfruman1 alikan antramhur hugrubsan *)
+    pabbergue enrparalv marfruman1 alikan antramhur hugrubsan *)
 lemma "algunos P (rev xs) = algunos P xs"
 proof (induct xs)
@@ Línea 649: / Línea 657: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
-    gleherlop chrgencar benber giafus1 enrparalv marfruman1 antramhur alikan hugrubsan aribatval *)
+    gleherlop chrgencar benber giafus1 enrparalv marfruman1 antramhur
 lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
    by (induct xs) auto
-(* pabalagon josgomrom4 cammonagu pabbergue marfruman1 antramhur juacanrod alikan*)
+(* pabalagon josgomrom4 cammonagu pabbergue marfruman1 antramhur
 lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
 proof (induct xs)
@@ Línea 738: / Línea 748: @@
 *}
-(* manperjim pabalagon josgomrom4 cammonagu pabbergue enrparalv marfruman1
+(* manperjim pabalagon josgomrom4 cammonagu pabbergue enrparalv
-    antramhur juacanrod alikan hugrubsan aribatval *)
+    marfruman1 antramhur juacanrod alikan hugrubsan aribatval *)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
 proof (induct xs)
@@ Línea 827: / Línea 837: @@
 *}
-(* manperjim pabalagon josgomrom4 alfmarcua cammonagu gleherlop chrgencar benber
+(* manperjim pabalagon josgomrom4 alfmarcua cammonagu gleherlop
-   giafus1 pabbergue marfruman1 antramhur juacanrod alikan*)
+   chrgencar benber giafus1 pabbergue marfruman1 antramhur juacanrod
 lemma "estaEn x xs = algunos (λa. x=a) xs"
    by (induct xs) auto

@@ Línea 739: / Línea 739: @@
 (* manperjim pabalagon josgomrom4 cammonagu pabbergue enrparalv marfruman1
-    antramhur juacanrod alikan hugrubsan*)
+    antramhur juacanrod alikan hugrubsan aribatval *)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
 proof (induct xs)
@@ Línea 815: / Línea 815: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
     gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1
-    antramhur juacanrod alikan hugrubsan *)
+    antramhur juacanrod alikan hugrubsan aribatval *)
 fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
    "estaEn x [] = False" |

@@ Línea 55: / Línea 55: @@
 (* manperjim pabalagon alfmarcua josgomrom4 cammonagu raffergon2
     enrparalv gleherlop chrgencar benber giafus1 pabbergue alikan
-    marfruman1 antramhur juacanrod hugrubsan *)
+    marfruman1 antramhur juacanrod hugrubsan aribatval *)
 lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
    by (induct xs) auto
@@ Línea 110: / Línea 110: @@
 (* manperjim josgomrom4 raffergon2 cammonagu enrparalv gleherlop chrgencar giafus1
-    pabbergue alikan marfruman1 antramhur hugrubsan*)
+    pabbergue alikan marfruman1 antramhur hugrubsan aribatval *)
 lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
 proof (induct xs)
@@ Línea 161: / Línea 161: @@
 (* manperjim pabalagon alfmarcua josgomrom4 aritbatval cammonagu
     raffergon2 enrparalv benber gleherlop chrgencar giafus1 pabbergue
-    alikan marfruman1 antramhur juacanrod hugrubsan *)
+    alikan marfruman1 antramhur juacanrod hugrubsan aribatval *)
 lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
    by (induct x) auto
@@ Línea 255: / Línea 255: @@
 (* manperjim pabalagon josgomrom4 raffergon2 cammonagu gleherlop giafus1
-    pabbergue enrparalv marfruman1 alikan chrgencar antramhur juacanrod hugrubsan *)
+    pabbergue enrparalv marfruman1 alikan chrgencar antramhur juacanrod hugrubsan aribatval *)
 lemma "todos P (rev xs) = todos P xs"
 proof (induct xs)
@@ Línea 332: / Línea 332: @@
 (* manperjim alfmarcua raffergon2 gleherlop chrgencar cammonagu giafus1 pabbergue
-    marfruman1 alikan antramhur juacanrod hugrubsan *)
+    marfruman1 alikan antramhur juacanrod hugrubsan aribatval *)
 lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
    quickcheck
@@ Línea 372: / Línea 372: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 gleherlop
-    cammonagu benber giafus1 pabbergue enrparalv marfruman1 alikan antramhur juacanrod hugrubsan *)
+    cammonagu benber giafus1 pabbergue enrparalv marfruman1 alikan antramhur juacanrod hugrubsan aribatval *)
 lemma "algunos P (map f xs) = algunos (P o f) xs"
    by (induct xs) auto
@@ Línea 465: / Línea 465: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
     gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1
-    alikan antramhur juacanrod hugrubsan *)
+    alikan antramhur juacanrod hugrubsan aribatval *)
 lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
    by (induct xs) auto
@@ Línea 548: / Línea 548: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 gleherlop chrgencar
-    cammonagu giafus1 pabbergue enrparalv alikan antramhur juacanrod hugrubsan *)
+    cammonagu giafus1 pabbergue enrparalv alikan antramhur juacanrod hugrubsan aribatval *)
 lemma "algunos P (rev xs) = algunos P xs"
    by (induct xs) (simp_all add: HOL.disj_comms algunos_append)
@@ Línea 649: / Línea 649: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
-    gleherlop chrgencar benber giafus1 enrparalv marfruman1 antramhur alikan hugrubsan *)
+    gleherlop chrgencar benber giafus1 enrparalv marfruman1 antramhur alikan hugrubsan aribatval *)
 lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
    by (induct xs) auto
@@ Línea 727: / Línea 727: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
     gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1
-    antramhur juacanrod alikan hugrubsan*)
+    antramhur juacanrod alikan hugrubsan aribatval *)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
    by (induct xs) auto

@@ Línea 21: / Línea 21: @@
 (* manperjim pabalagon alfmarcua josgomrom4 aribatval cammonagu
     raffergon2 enrparalv gleherlop chrgencar benber giafus1 pabbergue
-    alikan marfruman1 antramhur juacanrod*)
+    alikan marfruman1 antramhur juacanrod hugrubsan *)
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p [] = True" |
@@ Línea 41: / Línea 41: @@
 (* manperjim pabalagon alfmarcua josgomrom4 cammonagu aribatval
     raffergon2 enrparalv gleherlop chrgencar benber giafus1 pabbergue
-    alikan marfruman1 antramhur juacanrod *)
+    alikan marfruman1 antramhur juacanrod hugrubsan *)
 fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "algunos p [] = False" |
@@ Línea 55: / Línea 55: @@
 (* manperjim pabalagon alfmarcua josgomrom4 cammonagu raffergon2
     enrparalv gleherlop chrgencar benber giafus1 pabbergue alikan
-    marfruman1 antramhur juacanrod*)
+    marfruman1 antramhur juacanrod hugrubsan *)
 lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
    by (induct xs) auto
@@ Línea 110: / Línea 110: @@
 (* manperjim josgomrom4 raffergon2 cammonagu enrparalv gleherlop chrgencar giafus1
-    pabbergue alikan marfruman1 antramhur*)
+    pabbergue alikan marfruman1 antramhur hugrubsan*)
 lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
 proof (induct xs)
@@ Línea 161: / Línea 161: @@
 (* manperjim pabalagon alfmarcua josgomrom4 aritbatval cammonagu
     raffergon2 enrparalv benber gleherlop chrgencar giafus1 pabbergue
-    alikan marfruman1 antramhur juacanrod *)
+    alikan marfruman1 antramhur juacanrod hugrubsan *)
 lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
    by (induct x) auto
@@ Línea 173: / Línea 173: @@
 (* manperjim pabalagon josgomrom4 raffergon2 cammonagu enrparalv
-    gleherlop chrgencar giafus1 pabbergue alikan antramhur juacanrod *)
+    gleherlop chrgencar giafus1 pabbergue alikan antramhur juacanrod hugrubsan *)
 lemma todos_append:
    "todos P (x @ y) = (todos P x ∧ todos P y)"
@@ Línea 239: / Línea 239: @@
 (* manperjim pabalagon josgomrom4 alfmarcua aribatval cammonagu
-    raffergon2 giafus1 pabbergue enrparalv alikan antramhur juacanrod *)
+    raffergon2 giafus1 pabbergue enrparalv alikan antramhur juacanrod hugrubsan *)
 lemma "todos P (rev xs) = todos P xs"
    by (induct xs) (simp_all add: HOL.conj_comms todos_append)
@@ Línea 255: / Línea 255: @@
 (* manperjim pabalagon josgomrom4 raffergon2 cammonagu gleherlop giafus1
-    pabbergue enrparalv marfruman1 alikan chrgencar antramhur juacanrod *)
+    pabbergue enrparalv marfruman1 alikan chrgencar antramhur juacanrod hugrubsan *)
 lemma "todos P (rev xs) = todos P xs"
 proof (induct xs)
@@ Línea 332: / Línea 332: @@
 (* manperjim alfmarcua raffergon2 gleherlop chrgencar cammonagu giafus1 pabbergue
-    marfruman1 alikan antramhur juacanrod *)
+    marfruman1 alikan antramhur juacanrod hugrubsan *)
 lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
    quickcheck
@@ Línea 372: / Línea 372: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 gleherlop
-    cammonagu benber giafus1 pabbergue enrparalv marfruman1 alikan antramhur juacanrod *)
+    cammonagu benber giafus1 pabbergue enrparalv marfruman1 alikan antramhur juacanrod hugrubsan *)
 lemma "algunos P (map f xs) = algunos (P o f) xs"
    by (induct xs) auto
@@ Línea 384: / Línea 384: @@
 (* manperjim pabalagon cammonagu giafus1 gleherlop chrgencar pabbergue enrparalv
-    marfruman1 alikan antramhur juacanrod *)
+    marfruman1 alikan antramhur juacanrod hugrubsan *)
 lemma "algunos P (map f xs) = algunos (P o f) xs"
 proof (induct xs)
@@ Línea 465: / Línea 465: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
     gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1
-    alikan antramhur juacanrod *)
+    alikan antramhur juacanrod hugrubsan *)
 lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
    by (induct xs) auto
@@ Línea 477: / Línea 477: @@
 (* manperjim pabalagon josgomrom4 raffergon2 gleherlop cammonagu giafus1
-    pabbergue enrparalv marfruman1 alikan antramhur juacanrod *)
+    pabbergue enrparalv marfruman1 alikan antramhur juacanrod hugrubsan *)
 lemma algunos_append:
    "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
@@ Línea 548: / Línea 548: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 gleherlop chrgencar
-    cammonagu giafus1 pabbergue enrparalv alikan antramhur juacanrod *)
+    cammonagu giafus1 pabbergue enrparalv alikan antramhur juacanrod hugrubsan *)
 lemma "algunos P (rev xs) = algunos P xs"
    by (induct xs) (simp_all add: HOL.disj_comms algunos_append)
@@ Línea 580: / Línea 580: @@
 (* manperjim josgomrom4 raffergon2 gleherlop chrgencar cammonagu giafus1 pabbergue
-    enrparalv marfruman1 alikan antramhur *)
+    enrparalv marfruman1 alikan antramhur hugrubsan *)
 lemma "algunos P (rev xs) = algunos P xs"
 proof (induct xs)
@@ Línea 649: / Línea 649: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
-    gleherlop chrgencar benber giafus1 enrparalv marfruman1 antramhur alikan*)
+    gleherlop chrgencar benber giafus1 enrparalv marfruman1 antramhur alikan hugrubsan *)
 lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
    by (induct xs) auto
@@ Línea 726: / Línea 726: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
-    gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1 antramhur juacanrod alikan*)
+    gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
    by (induct xs) auto
@@ Línea 738: / Línea 739: @@
 (* manperjim pabalagon josgomrom4 cammonagu pabbergue enrparalv marfruman1
-    antramhur juacanrod alikan*)
+    antramhur juacanrod alikan hugrubsan*)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
 proof (induct xs)
@@ Línea 813: / Línea 814: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
-    gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1 antramhur juacanrod alikan*)
+    gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1
 fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
    "estaEn x [] = False" |

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

@@ Línea 20: / Línea 20: @@
 (* manperjim pabalagon alfmarcua josgomrom4 aribatval cammonagu
-    raffergon2 enrparalv gleherlop benber giafus1 pabbergue alikan marfruman1*)
+    raffergon2 enrparalv gleherlop chrgencar benber giafus1 pabbergue alikan marfruman1*)
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p [] = True" |
@@ Línea 39: / Línea 39: @@
 (* manperjim pabalagon alfmarcua josgomrom4 cammonagu aribatval
-    raffergon2 enrparalv gleherlop benber giafus1 pabbergue alikan marfruman1*)
+    raffergon2 enrparalv gleherlop chrgencar benber giafus1 pabbergue alikan marfruman1*)
 fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "algunos p [] = False" |
@@ Línea 52: / Línea 52: @@
 (* manperjim pabalagon alfmarcua josgomrom4 cammonagu raffergon2
-    enrparalv gleherlop benber giafus1 pabbergue alikan marfruman1*)
+    enrparalv gleherlop chrgencar benber giafus1 pabbergue alikan marfruman1*)
 lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
    by (induct xs) auto
@@ Línea 106: / Línea 106: @@
 qed
-(* manperjim josgomrom4 raffergon2 cammonagu enrparalv gleherlop giafus1
+(* manperjim josgomrom4 raffergon2 cammonagu enrparalv gleherlop chrgencar giafus1
     pabbergue alikan marfruman1*)
 lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
@@ Línea 157: / Línea 157: @@
 (* manperjim pabalagon alfmarcua josgomrom4 aritbatval cammonagu
-    raffergon2 enrparalv benber gleherlop giafus1 pabbergue alikan marfruman1*)
+    raffergon2 enrparalv benber gleherlop chrgencar giafus1 pabbergue alikan marfruman1*)
 lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
    by (induct x) auto
@@ Línea 169: / Línea 169: @@
 (* manperjim pabalagon josgomrom4 raffergon2 cammonagu enrparalv
-    gleherlop giafus1 pabbergue alikan*)
+    gleherlop chrgencar giafus1 pabbergue alikan*)
 lemma todos_append:
    "todos P (x @ y) = (todos P x ∧ todos P y)"
@@ Línea 251: / Línea 251: @@
 (* manperjim pabalagon josgomrom4 raffergon2 cammonagu gleherlop giafus1
-    pabbergue enrparalv marfruman1 alikan*)
+    pabbergue enrparalv marfruman1 alikan chrgencar *)
 lemma "todos P (rev xs) = todos P xs"
 proof (induct xs)
@@ Línea 327: / Línea 327: @@
    algunos even [1, 2::nat] ∧ algunos odd [1, 2::nat]"
-(* manperjim alfmarcua raffergon2 gleherlop cammonagu giafus1 pabbergue marfruman1 alikan*)
+(* manperjim alfmarcua raffergon2 gleherlop chrgencar cammonagu giafus1 pabbergue
 lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
    quickcheck
@@ Línea 378: / Línea 379: @@
 *}
-(* manperjim pabalagon cammonagu giafus1 gleherlop pabbergue enrparalv marfruman1 alikan*)
+(* manperjim pabalagon cammonagu giafus1 gleherlop chrgencar pabbergue enrparalv
 lemma "algunos P (map f xs) = algunos (P o f) xs"
 proof (induct xs)
@@ Línea 458: / Línea 460: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
-    gleherlop benber giafus1 pabbergue enrparalv marfruman1 alikan*)
+    gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1 alikan*)
 lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
    by (induct xs) auto
@@ Línea 540: / Línea 542: @@
 *}
-(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 gleherlop
+(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 gleherlop chrgencar
     cammonagu giafus1 pabbergue enrparalv alikan*)
 lemma "algunos P (rev xs) = algunos P xs"
@@ Línea 572: / Línea 574: @@
 qed
-(* manperjim josgomrom4 raffergon2 gleherlop cammonagu giafus1 pabbergue enrparalv marfruman1 alikan*)
+(* manperjim josgomrom4 raffergon2 gleherlop chrgencar cammonagu giafus1 pabbergue
 lemma "algunos P (rev xs) = algunos P xs"
 proof (induct xs)
@@ Línea 641: / Línea 644: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
-    gleherlop benber giafus1 enrparalv marfruman1 *)
+    gleherlop chrgencar benber giafus1 enrparalv marfruman1 *)
 lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
    by (induct xs) auto
@@ Línea 718: / Línea 721: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
-    gleherlop benber giafus1 pabbergue enrparalv marfruman1*)
+    gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1*)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
    by (induct xs) auto
@@ Línea 804: / Línea 807: @@
 (* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
-    gleherlop benber giafus1 pabbergue enrparalv marfruman1 *)
+    gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1 *)
 fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
    "estaEn x [] = False" |
@@ Línea 816: / Línea 819: @@
 *}
-(* manperjim pabalagon josgomrom4 alfmarcua cammonagu gleherlop benber
+(* manperjim pabalagon josgomrom4 alfmarcua cammonagu gleherlop chrgencar benber
     giafus1 pabbergue marfruman1 *)
 lemma "estaEn x xs = algunos (λa. x=a) xs"