X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flists%2Fappend.ma;fp=weblib%2Fbasics%2Flists%2Fappend.ma;h=5b0c403e1b58ab707a31f7223ade3f8e61e1e384;hb=d13c122f5238597ef543eb213eb5ce788c0e9fd9;hp=73fbd36cc5afb91e0021d333522efef89f069383;hpb=adfe42bbd5aaa4130a4133f345930e79444f0f3e;p=helm.git

diff --git a/weblib/basics/lists/append.ma b/weblib/basics/lists/append.ma
index 73fbd36cc..5b0c403e1 100644
--- a/weblib/basics/lists/append.ma
+++ b/weblib/basics/lists/append.ma
@@ -3,37 +3,37 @@
 include "basics/lists/lists.ma".
 include "basics/relations.ma".
 
-img class="anchor" src="icons/tick.png" id="append"let rec append A (l1: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) l2 on l1 ≝ 
+let rec append A (l1: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) l2 on l1 ≝ 
   match l1 with
   [ nil ⇒  l2
   | cons hd tl ⇒  hd :a title="cons" href="cic:/fakeuri.def(1)":/a append A tl l2 ].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
-img class="anchor" src="icons/tick.png" id="append_nil"theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a [a title="nil" href="cic:/fakeuri.def(1)"]/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
+theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a [a title="nil" href="cic:/fakeuri.def(1)"]/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
 #A #l (elim l) normalize // qed.
 
-img class="anchor" src="icons/tick.png" id="associative_append"theorem associative_append: 
- ∀A.font class="Apple-style-span" color="#FF0000"a href="cic:/matita/basics/relations/associative.def(1)"associative/a /font(a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) (a href="cic:/matita/basics/lists/append/append.fix(0,1,1)"append/a A).
+theorem associative_append: 
+ ∀A.font class="Apple-style-span" color="#ff0000"a href="cic:/matita/basics/relations/associative.def(1)"associative/a /font(a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) (a href="cic:/matita/basics/lists/append/append.fix(0,1,1)"append/a A).
 #A #l1 #l2 #l3 (elim l1) normalize // qed.
 
-img class="anchor" src="icons/tick.png" id="append_cons"theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(a:a title="cons" href="cic:/fakeuri.def(1)":/al1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a)a title="append" href="cic:/fakeuri.def(1)"@/al1.
+theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(a:a title="cons" href="cic:/fakeuri.def(1)":/al1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a)a title="append" href="cic:/fakeuri.def(1)"@/al1.
 #A #a #l #l1 >a href="cic:/matita/basics/lists/append/associative_append.def(4)"associative_append/a // qed.
 
-img class="anchor" src="icons/tick.png" id="nil_append_elim"theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.∀P:?→?→Prop. 
+theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.∀P:?→?→Prop. 
   l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a[a title="nil" href="cic:/fakeuri.def(1)"]/a → P (a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"nil/a A) → P l1 l2.
 #A #l1 #l2 #P (cases l1) normalize //
 #a #l3 #heq destruct
 qed.
 
-img class="anchor" src="icons/tick.png" id="nil_to_nil"theorem nil_to_nil:  ∀A.∀l1,l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.
+theorem nil_to_nil:  ∀A.∀l1,l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.
   l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a.
 #A #l1 #l2 #isnil @(a href="cic:/matita/basics/lists/append/nil_append_elim.def(4)"nil_append_elim/a A l1 l2) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
 qed.
 
 (* comparing lists *)
 
-img class="anchor" src="icons/tick.png" id="compare_append"lemma compare_append : ∀A,l1,l2,l3,l4. l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l3a title="append" href="cic:/fakeuri.def(1)"@/al4 → 
+lemma compare_append : ∀A,l1,l2,l3,l4. l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l3a title="append" href="cic:/fakeuri.def(1)"@/al4 → 
 ∃l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a Aa title="exists" href="cic:/fakeuri.def(1)"./a(l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l3a title="append" href="cic:/fakeuri.def(1)"@/al a title="logical and" href="cic:/fakeuri.def(1)"∧/a l4a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ala title="append" href="cic:/fakeuri.def(1)"@/al2) a title="logical or" href="cic:/fakeuri.def(1)"∨/a (l3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l1a title="append" href="cic:/fakeuri.def(1)"@/al a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ala title="append" href="cic:/fakeuri.def(1)"@/al4).
 #A #l1 elim l1
   [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
@@ -48,5 +48,4 @@ qed.
       ]
     ]
   ]
-qed.
-
+qed. 
\ No newline at end of file