Relación 8 - Historial de revisiones

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

2019-03-06T18:51:05Z

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

2019-03-06T10:54:42Z

2019-03-05T17:55:49Z

2019-03-04T21:33:29Z

2019-03-04T18:35:09Z

2019-03-04T14:27:15Z

2019-03-04T09:34:52Z

2019-03-01T20:42:02Z

2019-03-01T17:28:35Z

2019-03-01T13:16:01Z

@@ Línea 86: / Línea 86: @@
 qed
-(* pabalagon marfruman1 *)
+(* pabalagon marfruman1 pabbergue *)
 lemma T_en_S2:
    assumes "w ∈ T"
@@ Línea 176: / Línea 176: @@
 qed
-(* pabalagon giafus1 marfruman1 *)
+(* pabalagon giafus1 marfruman1 pabbergue *)
 lemma S_en_T3:
    "w ∈ S ⟹ w ∈ T"
@@ Línea 202: / Línea 202: @@
    ------------------------------------------------------------------ *}
-(* benber cammonagu antramhur josgomrom4 *)
+(* benber cammonagu antramhur josgomrom4 pabbergue *)
 lemma S_igual_T:
    "S = T"
@@ Línea 237: / Línea 237: @@
    ------------------------------------------------------------------ *}
-(* benber alfmarcua antramhur josgomrom4 pabalagon gleherlop giafus1 marfruman1*)
+(* benber alfmarcua antramhur josgomrom4 pabalagon gleherlop giafus1 marfruman1 pabbergue *)
 (* balanceada_aux w n = True si y solo si ([A]*n) @ w es balanceada *)
 fun balanceada_aux :: "alfabeto list ⇒ nat ⇒ bool" where
@@ Línea 355: / Línea 355: @@
 qed
-(* alfmarcua antramhur josgomrom4 giafus1 *)
+(* alfmarcua antramhur josgomrom4 giafus1 pabbergue *)
 lemma balanceada_correcto_aux3:
    shows "balanceada_aux v m ⟹
@@ Línea 518: / Línea 518: @@
    ------------------------------------------------------------------ *}
-(* benber antramhur pabalagon *)
+(* benber antramhur pabalagon pabbergue *)
 lemma balanceada_aux_unico:
    "⟦balanceada_aux w k; balanceada_aux w l⟧ ⟹ k = l" for w k l

@@ Línea 518: / Línea 518: @@
    ------------------------------------------------------------------ *}
-(* benber antramhur *)
+(* benber antramhur pabalagon *)
 lemma balanceada_aux_unico:
    "⟦balanceada_aux w k; balanceada_aux w l⟧ ⟹ k = l" for w k l

@@ Línea 518: / Línea 518: @@
    ------------------------------------------------------------------ *}
-(* benber *)
+(* benber antramhur *)
 lemma balanceada_aux_unico:
    "⟦balanceada_aux w k; balanceada_aux w l⟧ ⟹ k = l" for w k l

@@ Línea 86: / Línea 86: @@
 qed
-(* pabalagon *)
+(* pabalagon marfruman1 *)
 lemma T_en_S2:
    assumes "w ∈ T"
@@ Línea 176: / Línea 176: @@
 qed
-(* pabalagon giafus1 *)
+(* pabalagon giafus1 marfruman1 *)
 lemma S_en_T3:
    "w ∈ S ⟹ w ∈ T"
@@ Línea 207: / Línea 207: @@
    using T_en_S S_en_T by auto
-(* alfmarcua pabalagon giafus1 gleherlop *)
+(* alfmarcua pabalagon giafus1 gleherlop marfruman1*)
 lemma S_igual_T_2:
    "S = T"
@@ Línea 237: / Línea 237: @@
    ------------------------------------------------------------------ *}
-(* benber alfmarcua antramhur josgomrom4 pabalagon gleherlop giafus1 *)
+(* benber alfmarcua antramhur josgomrom4 pabalagon gleherlop giafus1 marfruman1*)
 (* balanceada_aux w n = True si y solo si ([A]*n) @ w es balanceada *)
 fun balanceada_aux :: "alfabeto list ⇒ nat ⇒ bool" where

@@ Línea 46: / Línea 46: @@
    ------------------------------------------------------------------ *}
-(* benber alfmarcua antramhur josgomrom4 juacanrod giafus1 *)
+(* benber alfmarcua antramhur josgomrom4 juacanrod giafus1 gleherlop *)
 lemma T_en_S:
    assumes "w ∈ T"
@@ Línea 150: / Línea 150: @@
 qed
-(* alfmarcua antramhur josgomrom4 juacanrod *)
+(* alfmarcua antramhur josgomrom4 juacanrod gleherlop *)
 lemma S_en_T_2:
    "w ∈ S ⟹ w ∈ T"
@@ Línea 207: / Línea 207: @@
    using T_en_S S_en_T by auto
-(* alfmarcua pabalagon giafus1 *)
+(* alfmarcua pabalagon giafus1 gleherlop *)
 lemma S_igual_T_2:
    "S = T"
@@ Línea 237: / Línea 237: @@
    ------------------------------------------------------------------ *}
-(* benber alfmarcua antramhur josgomrom4 pabalagon giafus1 *)
+(* benber alfmarcua antramhur josgomrom4 pabalagon gleherlop giafus1 *)
 (* balanceada_aux w n = True si y solo si ([A]*n) @ w es balanceada *)
 fun balanceada_aux :: "alfabeto list ⇒ nat ⇒ bool" where

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

@@ Línea 84: / Línea 84: @@
    have "w ∈ T ⟹ w ∈ S" using assms by (rule T2ImpS)
    thus ?thesis using assms .
 qed
@@ Línea 162: / Línea 173: @@
      then show "v @ va ∈ T ⟹ w ∈ T ⟹ v @ va @ [A] @ w @ [B] ∈ T "
        by (simp only: List.append_assoc)
    qed
 qed
@@ Línea 175: / Línea 207: @@
    using T_en_S S_en_T by auto
-(* alfmarcua *)
+(* alfmarcua pabalagon *)
 lemma S_igual_T_2:
    "S = T"
@@ Línea 205: / Línea 237: @@
    ------------------------------------------------------------------ *}
-(* benber alfmarcua antramhur josgomrom4 *)
+(* benber alfmarcua antramhur josgomrom4 pabalagon *)
 (* balanceada_aux w n = True si y solo si ([A]*n) @ w es balanceada *)
 fun balanceada_aux :: "alfabeto list ⇒ nat ⇒ bool" where
@@ Línea 417: / Línea 449: @@
      by (simp only:Groups.monoid_add_class.add.right_neutral)
    then show ?case by (simp only: balanceada.simps)
 qed

@@ Línea 139: / Línea 139: @@
 qed
-(* alfmarcua antramhur *)
+(* alfmarcua antramhur josgomrom4 *)
 lemma S_en_T_2:
    "w ∈ S ⟹ w ∈ T"