Relación 4 - Historial de revisiones

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

2018-07-16T11:05:41Z

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

Pabrodmac en 09:06 31 ene 2017

2017-01-31T09:06:56Z

Fracorjim1 en 12:37 5 ene 2017

2017-01-05T12:37:04Z

Antsancab1 en 19:38 22 dic 2016

2016-12-22T19:38:52Z

Mostrar los cambios

Jeamacpov en 19:36 13 dic 2016

2016-12-13T19:36:52Z

Jalonso: Desprotegió «Relación 4»

2016-12-08T17:47:10Z

Desprotegió «Relación 4»

Jalonso: Protegió «Relación 4» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2016-11-25T07:05:09Z

Protegió «Relación 4» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Wilmorort en 22:10 24 nov 2016

2016-11-24T22:10:12Z

Wilmorort en 21:53 24 nov 2016

2016-11-24T21:53:45Z

Rubgonmar en 08:41 24 nov 2016

2016-11-24T08:41:00Z

← Revisión anterior		Revisión del 11:05 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	chapter {* R4: Cuantificadores sobre listas *}		chapter {* R4: Cuantificadores sobre listas *}

@@ Línea 620: / Línea 620: @@
 (* migtermor ivamenjim ferrenseg paupeddeg crigomgom serrodcal wilmorort
     juacabsou rubgonmar anaprarod marpoldia1 fraortmoy josgarsan
-    danrodcha pablucoto lucnovdos marcarmor13 jeamacpov antsancab1 fracorjim1 *)
+    danrodcha pablucoto lucnovdos marcarmor13 jeamacpov antsancab1 fracorjim1 pabrodmac *)
 lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
 quickcheck
@@ Línea 655: / Línea 655: @@
 (* ivamenjim migtermor marpoldia1 crigomgom rubgonmar wilmorort anaprarod
     fraortmoy juacabsou paupeddeg josgarsan danrodcha pablucoto lucnovdos
-    marcarmor13 jeamacpov antsancab1 *)
+    marcarmor13 jeamacpov antsancab1 pabrodmac *)
 lemma "algunos P (map f xs) = algunos (P o f) xs"
 by (induct xs) auto
@@ Línea 755: / Línea 755: @@
 (* crigomgom rubgonmar anaprarod marpoldia1 juacabsou danrodcha
-    paupeddeg josgarsan lucnovdos *)
+    paupeddeg josgarsan lucnovdos pabrodmac *)
 lemma "algunos P (map f xs) = algunos (P o f) xs"
 proof (induct xs)
@@ Línea 854: / Línea 854: @@
 (* ivamenjim marpoldia1 paupeddeg crigomgom rubgonmar  wilmorort
     fraortmoy danrodcha pablucoto dancorgar josgarsan anaprarod juacabsou
-    lucnovdos marcarmor13 jeamacpov antsancab1 *)
+    lucnovdos marcarmor13 jeamacpov antsancab1 pabrodmac *)
 lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
 by (induct xs) auto
@@ Línea 944: / Línea 944: @@
 qed
-(* danrodcha pablucoto anaprarod marcarmor13 jeamacpov *)
+(* danrodcha pablucoto anaprarod marcarmor13 jeamacpov pabrodmac *)
 lemma algunos_append5:
    "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)" (is "?Q xs")
@@ Línea 1074: / Línea 1074: @@
 qed
-(* crigomgom pablucoto anaprarod rubgonmar juacabsou marcarmor13 jeamacpov *)
+(* crigomgom pablucoto anaprarod rubgonmar juacabsou marcarmor13 jeamacpov pabrodmac *)
 lemma "algunos P (rev xs) = algunos P xs"
 proof (induct xs)
@@ Línea 1223: / Línea 1223: @@
 (* Comentario: Uso de auto *)
-(* wilmorort danrodcha anaprarod juacabsou rubgonmar *)
+(* wilmorort danrodcha anaprarod juacabsou rubgonmar*)
 lemma "algunos (λx. P x ∨ Q x) xs =
         (¬todos(λx. ¬P x)xs ∨ ¬todos(λx. ¬Q x)xs)"
@@ Línea 1296: / Línea 1296: @@
 qed
-(* pablucoto crigomgom serrodcal marcarmor13 jeamacpov *)
+(* pablucoto crigomgom serrodcal marcarmor13 jeamacpov pabrodmac *)
 -- "Automatica"
 lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
@@ Línea 1361: / Línea 1361: @@
 (* ivamenjim wilmorort migtermor marpoldia1 crigomgom rubgonmar
     paupeddeg danrodcha pablucoto dancorgar josgarsan anaprarod juacabsou
-    lucnovdos serrodcal marcarmor13 jeamacpov antsancab1 *)
+    lucnovdos serrodcal marcarmor13 jeamacpov antsancab1 pabrodmac *)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
 by (induct xs) auto
@@ Línea 1414: / Línea 1414: @@
 qed
-(* danrodcha pablucoto anaprarod rubgonmar marcarmor13 jeamacpov*)
+(* danrodcha pablucoto anaprarod rubgonmar marcarmor13 jeamacpov pabrodmac *)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)" (is "?Q xs")
 proof (induct xs)
@@ Línea 1483: / Línea 1483: @@
 (* ivamenjim ferrenseg migtermor serrodcal crigomgom rubgonmar
     marpoldia1 paupeddeg danrodcha dancorgar pablucoto anaprarod
-    juacabsou lucnovdos marcarmor13 wilmorort jeamacpov fracorjim1 *)
+    juacabsou lucnovdos marcarmor13 wilmorort jeamacpov fracorjim1 pabrodmac *)
 fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
    "estaEn x []     = False"
@@ Línea 1611: / Línea 1611: @@
 qed
-(* pablucoto marcarmor13 jeamacpov*)
+(* pablucoto marcarmor13 jeamacpov pabrodmac *)
 -- "Automatica"
 lemma " estaEn y xs = algunos (λx. x=y) xs"

@@ Línea 367: / Línea 367: @@
 (* Comentario: Uso de auto. *)
-(* danrodcha *)
+(* danrodcha fracorjim1 *)
 lemma todos_append6:
    "todos P (x @ y) = (todos P x ∧ todos P y)" (is "?Q x")
@@ Línea 403: / Línea 403: @@
 (* migtermor ivamenjim marpoldia1 serrodcal anaprarod paupeddeg
-    dancorgar antsancab1 *)
+    dancorgar antsancab1 fracorjim1 *)
 lemma "todos P (rev xs) = todos P xs"
 apply (induct xs)
@@ Línea 559: / Línea 559: @@
 (* Comentario: Uso de HOL.conj_commute *)
-(* anaprarod *)
+(* anaprarod fracorjim1 *)
 (* es igual que las anteriores pero con el final también con patrones *)
 lemma "todos P (rev xs) = todos P xs" (is "?P xs")
@@ Línea 620: / Línea 620: @@
 (* migtermor ivamenjim ferrenseg paupeddeg crigomgom serrodcal wilmorort
     juacabsou rubgonmar anaprarod marpoldia1 fraortmoy josgarsan
-    danrodcha pablucoto lucnovdos marcarmor13 jeamacpov antsancab1 *)
+    danrodcha pablucoto lucnovdos marcarmor13 jeamacpov antsancab1 fracorjim1 *)
 lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
 quickcheck
@@ Línea 663: / Línea 663: @@
 by (induct xs) simp_all
-(* anaprarod dancorgar serrodcal *)
+(* anaprarod dancorgar serrodcal fracorjim1 *)
 lemma "algunos P (map f xs) = algunos (P o f) xs"
 apply (induct xs)
@@ Línea 802: / Línea 802: @@
 qed
-(* danrodcha *)
+(* danrodcha fracorjim1 *)
 lemma "algunos P (map f xs) = algunos (P o f) xs" (is "?Q xs")
 proof (induct xs)
@@ Línea 862: / Línea 862: @@
 by (induct xs) simp_all
-(* anaprarod *)
+(* anaprarod fracorjim1 *)
 lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
 apply (induct  xs)
@@ Línea 980: / Línea 980: @@
 (* ivamenjim migtermor marpoldia1 rubgonmar paupeddeg dancorgar
-    anaprarod serrodcal antsancab1 *)
+    anaprarod serrodcal antsancab1 fracorjim1 *)
 lemma "algunos P (rev xs) = algunos P xs"
 apply (induct xs)
@@ Línea 1483: / Línea 1483: @@
 (* ivamenjim ferrenseg migtermor serrodcal crigomgom rubgonmar
     marpoldia1 paupeddeg danrodcha dancorgar pablucoto anaprarod
-    juacabsou lucnovdos marcarmor13 wilmorort jeamacpov *)
+    juacabsou lucnovdos marcarmor13 wilmorort jeamacpov fracorjim1 *)
 fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
    "estaEn x []     = False"
@@ Línea 1676: / Línea 1676: @@
 end
 </source>

@@ Línea 22: / Línea 22: @@
     ferrenseg paupeddeg pablucoto crigomgom anaprarod serrodcal juacabsou
     rubgonmar josgarsan fraortmoy lucnovdos pabrodmac fracorjim1
-    marcarmor13 *)
+    marcarmor13 jeamacpov *)
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p []     = True"
@@ Línea 42: / Línea 42: @@
 (* danrodcha ivamenjim migtermor dancorgar marpoldia1 ferrenseg
     wilmorort paupeddeg pablucoto crigomgom anaprarod serrodcal juacabsou
-    rubgonmar josgarsan fraortmoy lucnovdos pabrodmac marcarmor13 *)
+    rubgonmar josgarsan fraortmoy lucnovdos pabrodmac marcarmor13 jeamacpov *)
 fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "algunos p []     = False"
@@ Línea 62: / Línea 62: @@
 (* danrodcha ivamenjim migtermor dancorgar marpoldia1 ferrenseg
     wilmorort paupeddeg pablucoto anaprarod serrodcal juacabsou rubgonmar
-    josgarsan fraortmoy lucnovdos pabrodmac marcarmor13 *)
+    josgarsan fraortmoy lucnovdos pabrodmac marcarmor13 jeamacpov *)
 lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
 by (induct xs) auto
@@ Línea 204: / Línea 204: @@
 (* wilmorort pablucoto crigomgom anaprarod juacabsou rubgonmar fraortmoy
-    marcarmor13 *)
+    marcarmor13 jeamacpov *)
 lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
 proof (induct xs)
@@ Línea 247: / Línea 247: @@
 (* danrodcha ivamenjim marpoldia1 migtermor ferrenseg wilmorort
     paupeddeg crigomgom anaprarod serrodcal juacabsou rubgonmar pablucoto
-    fraortmoy josgarsan lucnovdos pabrodmac marcarmor13 *)
+    fraortmoy josgarsan lucnovdos pabrodmac marcarmor13 jeamacpov *)
 lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
 by (induct x) auto
@@ Línea 338: / Línea 338: @@
 qed
-(* pablucoto marcarmor13 *)
+(* pablucoto marcarmor13 jeamacpov *)
 lemma todos_append5:
    "todos P (x @ y) = (todos P x ∧ todos P y)"
@@ Línea 417: / Línea 417: @@
 (* Comentario: Pasos dentro de apply *)
-(* pablucoto marcarmor13 *)
+(* pablucoto marcarmor13 jeamacpov *)
 lemma "todos P (rev xs) = todos P xs"
 by (induct xs) (auto, simp_all add: todos_append)
@@ Línea 466: / Línea 466: @@
 (* marpoldia1 ferrenseg crigomgom serrodcal juacabsou rubgonmar
-    josgarsan pablucoto pabrodmac lucnovdos marcarmor13 *)
+    josgarsan pablucoto pabrodmac lucnovdos marcarmor13 jeamacpov *)
 lemma "todos P (rev xs) = todos P xs"
 proof (induct xs)
@@ Línea 592: / Línea 592: @@
 (* migtermor ivamenjim ferrenseg paupeddeg crigomgom serrodcal wilmorort
     juacabsou rubgonmar anaprarod marpoldia1 fraortmoy josgarsan
-    danrodcha pablucoto lucnovdos marcarmor13 *)
+    danrodcha pablucoto lucnovdos marcarmor13 jeamacpov *)
 lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
 quickcheck
@@ Línea 627: / Línea 627: @@
 (* ivamenjim migtermor marpoldia1 crigomgom rubgonmar wilmorort anaprarod
     fraortmoy juacabsou paupeddeg josgarsan danrodcha pablucoto lucnovdos
-    marcarmor13*)
+    marcarmor13 jeamacpov *)
 lemma "algunos P (map f xs) = algunos (P o f) xs"
 by (induct xs) auto
@@ Línea 743: / Línea 743: @@
 qed
-(* wilmorort pablucoto marcarmor13*)
+(* wilmorort pablucoto marcarmor13 jeamacpov *)
 lemma "algunos P (map f xs) = algunos (P o f) xs" (is "?P xs" )
 proof (induct xs)
@@ Línea 812: / Línea 812: @@
 (* ivamenjim marpoldia1 paupeddeg crigomgom rubgonmar  wilmorort
     fraortmoy danrodcha pablucoto dancorgar josgarsan anaprarod juacabsou
-    lucnovdos marcarmor13 *)
+    lucnovdos marcarmor13 jeamacpov *)
 lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
 by (induct xs) auto
@@ Línea 902: / Línea 902: @@
 qed
-(* danrodcha pablucoto anaprarod marcarmor13 *)
+(* danrodcha pablucoto anaprarod marcarmor13 jeamacpov *)
 lemma algunos_append5:
    "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)" (is "?Q xs")
@@ Línea 934: / Línea 934: @@
 (* ferrenseg crigomgom danrodcha pablucoto josgarsan pabrodmac lucnovdos
-    marcarmor13 *)
+    marcarmor13 jeamacpov *)
 lemma "algunos P (rev xs) = algunos P xs"
 by (induct xs) (auto simp add: algunos_append)
@@ Línea 1019: / Línea 1019: @@
 qed
-(* crigomgom pablucoto anaprarod rubgonmar juacabsou marcarmor13 *)
+(* crigomgom pablucoto anaprarod rubgonmar juacabsou marcarmor13 jeamacpov *)
 lemma "algunos P (rev xs) = algunos P xs"
 proof (induct xs)
@@ Línea 1226: / Línea 1226: @@
 qed
-(* pablucoto crigomgom serrodcal marcarmor13 *)
+(* pablucoto crigomgom serrodcal marcarmor13 jeamacpov *)
 -- "Automatica"
 lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
@@ Línea 1275: / Línea 1275: @@
 (* ivamenjim wilmorort migtermor marpoldia1 crigomgom rubgonmar
     paupeddeg danrodcha pablucoto dancorgar josgarsan anaprarod juacabsou
-    lucnovdos serrodcal marcarmor13 *)
+    lucnovdos serrodcal marcarmor13 jeamacpov *)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
 by (induct xs) auto
@@ Línea 1328: / Línea 1328: @@
 qed
-(* danrodcha pablucoto anaprarod rubgonmar marcarmor13 *)
+(* danrodcha pablucoto anaprarod rubgonmar marcarmor13 jeamacpov*)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)" (is "?Q xs")
 proof (induct xs)
@@ Línea 1384: / Línea 1384: @@
 (* ivamenjim ferrenseg migtermor serrodcal crigomgom rubgonmar
     marpoldia1 paupeddeg danrodcha dancorgar pablucoto anaprarod
-    juacabsou lucnovdos marcarmor13 wilmorort *)
+    juacabsou lucnovdos marcarmor13 wilmorort jeamacpov *)
 fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
    "estaEn x []     = False"
@@ Línea 1504: / Línea 1504: @@
 qed
-(* pablucoto marcarmor13*)
+(* pablucoto marcarmor13 jeamacpov*)
 -- "Automatica"
 lemma " estaEn y xs = algunos (λx. x=y) xs"

@@ Línea 1384: / Línea 1384: @@
 (* ivamenjim ferrenseg migtermor serrodcal crigomgom rubgonmar
     marpoldia1 paupeddeg danrodcha dancorgar pablucoto anaprarod
-    juacabsou lucnovdos marcarmor13 *)
+    juacabsou lucnovdos marcarmor13 wilmorort *)
 fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
    "estaEn x []     = False"
@@ Línea 1449: / Línea 1449: @@
 (* Comentario: Uso de auto *)
-(* crigomgom paupeddeg dancorgar juacabsou serrodcal lucnovdos *)
+(* crigomgom paupeddeg dancorgar juacabsou serrodcal lucnovdos wilmorort *)
 lemma "estaEn a xs = algunos (λx. x = a) xs"
 by (induct xs) auto

← Revisión anterior	Revisión del 17:47 8 dic 2016
(Sin diferencias)

← Revisión anterior	Revisión del 07:05 25 nov 2016
(Sin diferencias)

@@ Línea 1298: / Línea 1298: @@
 (* ivamenjim migtermor marpoldia1 crigomgom paupeddeg josgarsan
-    juacabsou serrodcal *)
+    juacabsou serrodcal wilmorort *)
 lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
 proof (induct xs)