https://www.glc.us.es/~jalonso/RA2016/index.php?action=history&feed=atom&title=Discusi%C3%B3n%3ARelaci%C3%B3n_5
Discusión:Relación 5 - Historial de revisiones
2026-09-25T08:52:29Z
Historial de revisiones para esta página en el wiki
MediaWiki 1.31.14
https://www.glc.us.es/~jalonso/RA2016/index.php?title=Discusi%C3%B3n:Relaci%C3%B3n_5&diff=848&oldid=prev
Danrodcha en 14:07 1 dic 2016
2016-12-01T14:07:13Z
<p></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="es">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 14:07 1 dic 2016</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l33" >Línea 33:</td>
<td colspan="2" class="diff-lineno">Línea 33:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>     using c1 by simp *)</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>     using c1 by simp *)</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>   finally show "?p (a#xs)" by simp</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>   finally show "?p (a#xs)" by simp</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del style="font-weight: bold; text-decoration: none;">(* ¿Aquí porqué no puedo usar "finally show "?p (a # xs)" using c1 by simp? </del></div></td><td colspan="2"> </td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del style="font-weight: bold; text-decoration: none;">  Y porque no puedo añadir "finally show "?p (a # xs)" by simp al final? *)</del></div></td><td colspan="2"> </td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>qed</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>qed</div></td></tr>
</table>
Danrodcha
https://www.glc.us.es/~jalonso/RA2016/index.php?title=Discusi%C3%B3n:Relaci%C3%B3n_5&diff=847&oldid=prev
Danrodcha en 14:06 1 dic 2016
2016-12-01T14:06:26Z
<p></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="es">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 14:06 1 dic 2016</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l18" >Línea 18:</td>
<td colspan="2" class="diff-lineno">Línea 18:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>(* respuesta : danrodcha *)</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>(* respuesta : danrodcha *)</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>(* mirar en editar xq aqui <del class="diffchange diffchange-inline">nose </del>entiende *)</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>(* mirar en editar xq aqui <ins class="diffchange diffchange-inline">no se </ins>entiende *)</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>lemma length_borraDuplicados_2f:  </div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>lemma length_borraDuplicados_2f:  </div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>   "length (borraDuplicados xs) ≤ length xs" (is "?p xs")</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>   "length (borraDuplicados xs) ≤ length xs" (is "?p xs")</div></td></tr>
</table>
Danrodcha
https://www.glc.us.es/~jalonso/RA2016/index.php?title=Discusi%C3%B3n:Relaci%C3%B3n_5&diff=846&oldid=prev
Danrodcha en 14:06 1 dic 2016
2016-12-01T14:06:11Z
<p></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="es">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 14:06 1 dic 2016</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l18" >Línea 18:</td>
<td colspan="2" class="diff-lineno">Línea 18:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>(* respuesta : danrodcha *)</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>(* respuesta : danrodcha *)</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">(* mirar en editar xq aqui nose entiende *)</ins></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>lemma length_borraDuplicados_2f:  </div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>lemma length_borraDuplicados_2f:  </div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>   "length (borraDuplicados xs) ≤ length xs" (is "?p xs")</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>   "length (borraDuplicados xs) ≤ length xs" (is "?p xs")</div></td></tr>
</table>
Danrodcha
https://www.glc.us.es/~jalonso/RA2016/index.php?title=Discusi%C3%B3n:Relaci%C3%B3n_5&diff=845&oldid=prev
Danrodcha: Página creada con '(* bowma *) lemma length_borraDuplicados_2f: "length (borraDuplicados xs) ≤ length xs" (is "?p xs") proof (induct xs) show "length (borraDuplicados []) ≤ length []" by ...'
2016-12-01T14:04:47Z
<p>Página creada con '(* bowma *) lemma length_borraDuplicados_2f: "length (borraDuplicados xs) ≤ length xs" (is "?p xs") proof (induct xs) show "length (borraDuplicados []) ≤ length []" by ...'</p>
<p><b>Página nueva</b></p><div>(* bowma *)<br />
lemma length_borraDuplicados_2f: <br />
"length (borraDuplicados xs) ≤ length xs" (is "?p xs")<br />
proof (induct xs)<br />
show "length (borraDuplicados []) ≤ length []" by simp<br />
next<br />
fix a xs<br />
assume HI: "?p xs"<br />
have c1: "1+length xs = length (a#xs)" by simp<br />
also have "length(borraDuplicados (a#xs)) ≤ <br />
1 + length(borraDuplicados xs)" by simp<br />
also have "... ≤ 1+length xs" using HI by simp<br />
then show "length(borraDuplicados (a#xs)) ≤ length (a#xs)" <br />
using c1 by simp<br />
(* ¿Aquí porqué no puedo usar "finally show "?p (a # xs)" using c1 by simp? <br />
Y porque no puedo añadir "finally show "?p (a # xs)" by simp al final? *)<br />
qed<br />
<br />
(* respuesta : danrodcha *)<br />
lemma length_borraDuplicados_2f: <br />
"length (borraDuplicados xs) ≤ length xs" (is "?p xs")<br />
proof (induct xs)<br />
show "length (borraDuplicados []) ≤ length []" by simp (* <----yo aprovecharia los patrones "?p []" *)<br />
next<br />
fix a xs<br />
assume HI: "?p xs"<br />
(* have c1: "1+length xs = length (a#xs)" by simp *) (* <------ esto no hace falta *)<br />
(* also *) have "length(borraDuplicados (a#xs)) ≤ <br />
1 + length(borraDuplicados xs)" by simp<br />
also have "... ≤ 1+length xs" using HI by simp<br />
(* then show "length(borraDuplicados (a#xs)) ≤ length (a#xs)" <br />
using c1 by simp *)<br />
finally show "?p (a#xs)" by simp<br />
(* ¿Aquí porqué no puedo usar "finally show "?p (a # xs)" using c1 by simp? <br />
Y porque no puedo añadir "finally show "?p (a # xs)" by simp al final? *)<br />
qed</div>
Danrodcha