X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2FCerco%2FASM%2FUtils.ma;h=bcb583a95f6c4b0daaa2525e19a4a47d08df0add;hb=93768d9ebc0e3c8e3bcd69571d7a635cb1a16b29;hp=a7eeaad705fc2a1c7473e335402b197a0b32cdcf;hpb=b5f54d2815f446a999736abd0ffe80641596a5f6;p=helm.git

diff --git a/weblib/Cerco/ASM/Utils.ma b/weblib/Cerco/ASM/Utils.ma
index a7eeaad70..bcb583a95 100644
--- a/weblib/Cerco/ASM/Utils.ma
+++ b/weblib/Cerco/ASM/Utils.ma
@@ -1,70 +1,70 @@
-include "basics/list.ma".
+include "basics/list2.ma".
 include "basics/types.ma".
 include "arithmetics/nat.ma".
 
-include "utilities/pair.ma".
-include "ASM/JMCoercions.ma".
+include "Cerco/utilities/pair.ma".
+include "Cerco/ASM/JMCoercions.ma".
 
 (* let's implement a daemon not used by automation *)
 inductive DAEMONXXX: Type[0] ≝ K1DAEMONXXX: DAEMONXXX | K2DAEMONXXX: DAEMONXXX.
-axiom IMPOSSIBLE: K1DAEMONXXX = K2DAEMONXXX.
-example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
-example not_implemented: False. cases daemon qed.
+axiom IMPOSSIBLE: a href="cic:/matita/Cerco/ASM/Utils/DAEMONXXX.con(0,1,0)"K1DAEMONXXX/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/Cerco/ASM/Utils/DAEMONXXX.con(0,2,0)"K2DAEMONXXX/a.
+example daemon: a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. generalize in match a href="cic:/matita/Cerco/ASM/Utils/IMPOSSIBLE.dec"IMPOSSIBLE/a; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
+example not_implemented: a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. cases a href="cic:/matita/Cerco/ASM/Utils/daemon.def(2)" title="null"daemon/a qed.
 
 notation "⊥" with precedence 90
   for @{ match ? in False with [ ] }.
 
 definition ltb ≝
-  λm, n: nat.
-    leb (S m) n.
+  λm, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+    a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) n.
     
 definition geb ≝
-  λm, n: nat.
-    ltb n m.
+  λm, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+    a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"ltb/a n m.
 
 definition gtb ≝
-  λm, n: nat.
-    ltb n m.
+  λm, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+    a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"ltb/a n m.
 
 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
-let rec eq_nat (n: nat) (m: nat) on n: bool ≝
+let rec eq_nat (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (m: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) on n: a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
   match n with
-  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
-  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
+  [ O ⇒ match m with [ O ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | _ ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a ]
+  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a ]
   ].
 
 let rec forall
-  (A: Type[0]) (f: A → bool) (l: list A)
+  (A: Type[0]) (f: A → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A)
     on l ≝
   match l with
-  [ nil        ⇒ true
-  | cons hd tl ⇒ f hd ∧ forall A f tl
+  [ nil        ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a
+  | cons hd tl ⇒ f hd a title="boolean and" href="cic:/fakeuri.def(1)"∧/a forall A f tl
   ].
 
 let rec prefix
-  (A: Type[0]) (k: nat) (l: list A)
+  (A: Type[0]) (k: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A)
     on l ≝
   match l with
-  [ nil ⇒ [ ]
+  [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ]
   | cons hd tl ⇒
     match k with
-    [ O ⇒ [ ]
-    | S k' ⇒ hd :: prefix A k' tl
+    [ O ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ]
+    | S k' ⇒ hd a title="cons" href="cic:/fakeuri.def(1)":/a: prefix A k' tl
     ]
   ].
-  
+
 let rec fold_left2
   (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → A) (accu: A)
-  (left: list B) (right: list C) (proof: |left| = |right|)
+  (left: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) (right: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a C) (proof: a title="norm" href="cic:/fakeuri.def(1)"|/aleft| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/aright|)
     on left: A ≝
-  match left return λx. |x| = |right| → A with
+  match left return λx. a title="norm" href="cic:/fakeuri.def(1)"|/ax| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/aright| → A with
   [ nil ⇒ λnil_prf.
-    match right return λx. |[ ]| = |x| → A with
+    match right return λx. a title="norm" href="cic:/fakeuri.def(1)"|/aa title="nil" href="cic:/fakeuri.def(1)"[/a ]| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/ax| → A with
     [ nil ⇒ λnil_nil_prf. accu
     | cons hd tl ⇒ λcons_nil_absrd. ?
     ] nil_prf
   | cons hd tl ⇒ λcons_prf.
-    match right return λx. |hd::tl| = |x| → A with
+    match right return λx. a title="norm" href="cic:/fakeuri.def(1)"|/ahda title="cons" href="cic:/fakeuri.def(1)":/a:tl| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/ax| → A with
     [ nil ⇒ λcons_nil_absrd. ?
     | cons hd' tl' ⇒ λcons_cons_prf.
         fold_left2 …  f (f accu hd hd') tl tl' ?
@@ -75,49 +75,43 @@ let rec fold_left2
   | 2: normalize in cons_nil_absrd;
        destruct(cons_nil_absrd)
   | 3: normalize in cons_cons_prf;
-       @injective_S
+       @a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a
        assumption
   ]
-qed.
+qed. 
 
 let rec remove_n_first_internal
-  (i: nat) (A: Type[0]) (l: list A) (n: nat)
+  (i: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (A: Type[0]) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a)
     on l ≝
   match l with
-  [ nil ⇒ [ ]
+  [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ]
   | cons hd tl ⇒
-    match eq_nat i n with
+    match a href="cic:/matita/Cerco/ASM/Utils/eq_nat.fix(0,0,1)"eq_nat/a i n with
     [ true ⇒ l
-    | _ ⇒ remove_n_first_internal (S i) A tl n
+    | _ ⇒ remove_n_first_internal (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i) A tl n
     ]
   ].
 
 definition remove_n_first ≝
   λA: Type[0].
-  λn: nat.
-  λl: list A.
-    remove_n_first_internal 0 A l n.
+  λn: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+  λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
+    a href="cic:/matita/Cerco/ASM/Utils/remove_n_first_internal.fix(0,2,2)"remove_n_first_internal/a a title="natural number" href="cic:/fakeuri.def(1)"0/a A l n.
     
 let rec foldi_from_until_internal
-  (A: Type[0]) (i: nat) (res: ?) (rem: list A) (m: nat) (f: nat → list A → A → list A)
+  (A: Type[0]) (i: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (res: ?) (rem: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (m: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (f: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A → A → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A)
     on rem ≝
   match rem with
   [ nil ⇒ res
   | cons e tl ⇒
-    match geb i m with
+    match a href="cic:/matita/Cerco/ASM/Utils/geb.def(3)"geb/a i m with
     [ true ⇒ res
-    | _ ⇒ foldi_from_until_internal A (S i) (f i res e) tl m f
+    | _ ⇒ foldi_from_until_internal A (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i) (f i res e) tl m f
     ]
   ].
 
 definition foldi_from_until ≝
-  λA: Type[0].
-  λn: nat.
-  λm: nat.
-  λf: ?.
-  λa: ?.
-  λl: ?.
-    foldi_from_until_internal A 0 a (remove_n_first A n l) m f.
+  λA,n,m,f,a,l. a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until_internal.fix(0,3,4)"foldi_from_until_internal/a A a title="natural number" href="cic:/fakeuri.def(1)"0/a a (a href="cic:/matita/Cerco/ASM/Utils/remove_n_first.def(3)"remove_n_first/a A n l) m f.
 
 definition foldi_from ≝
   λA: Type[0].
@@ -125,7 +119,7 @@ definition foldi_from ≝
   λf.
   λa.
   λl.
-    foldi_from_until A n (|l|) f a l.
+    a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until.def(5)"foldi_from_until/a A n (a title="norm" href="cic:/fakeuri.def(1)"|/al|) f a l. 
 
 definition foldi_until ≝
   λA: Type[0].
@@ -133,117 +127,117 @@ definition foldi_until ≝
   λf.
   λa.
   λl.
-    foldi_from_until A 0 m f a l.
+    a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until.def(5)"foldi_from_until/a A a title="natural number" href="cic:/fakeuri.def(1)"0/a m f a l.
 
 definition foldi ≝
   λA: Type[0].
   λf.
   λa.
   λl.
-    foldi_from_until A 0 (|l|) f a l.
+    a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until.def(5)"foldi_from_until/a A a title="natural number" href="cic:/fakeuri.def(1)"0/a (a title="norm" href="cic:/fakeuri.def(1)"|/al|) f a l.
 
 definition hd_safe ≝
   λA: Type[0].
-  λl: list A.
-  λproof: 0 < |l|.
-  match l return λx. 0 < |x| → A with
+  λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
+  λproof: a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/al|.
+  match l return λx. a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/ax| → A with
   [ nil ⇒ λnil_absrd. ?
   | cons hd tl ⇒ λcons_prf. hd
   ] proof.
   normalize in nil_absrd;
-  cases(not_le_Sn_O 0)
+  cases(a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"not_le_Sn_O/a a title="natural number" href="cic:/fakeuri.def(1)"0/a)
   #HYP
   cases(HYP nil_absrd)
 qed.
 
 definition tail_safe ≝
   λA: Type[0].
-  λl: list A.
-  λproof: 0 < |l|.
-  match l return λx. 0 < |x| → list A with
+  λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
+  λproof: a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/al|.
+  match l return λx. a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/ax| → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A with
   [ nil ⇒ λnil_absrd. ?
   | cons hd tl ⇒ λcons_prf. tl
   ] proof.
   normalize in nil_absrd;
-  cases(not_le_Sn_O 0)
+  cases(a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"not_le_Sn_O/a a title="natural number" href="cic:/fakeuri.def(1)"0/a)
   #HYP
   cases(HYP nil_absrd)
 qed.
 
 let rec split
-  (A: Type[0]) (l: list A) (index: nat) (proof: index ≤ |l|)
+  (A: Type[0]) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (index: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (proof: index a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a title="norm" href="cic:/fakeuri.def(1)"|/al|)
     on index ≝
-  match index return λx. x ≤ |l| → (list A) × (list A) with
-  [ O ⇒ λzero_prf. 〈[], l〉
+  match index return λx. x a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a title="norm" href="cic:/fakeuri.def(1)"|/al| → (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) a title="Product" href="cic:/fakeuri.def(1)"×/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) with
+  [ O ⇒ λzero_prf. a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="nil" href="cic:/fakeuri.def(1)"[/a], l〉
   | S index' ⇒ λsucc_prf.
-    match l return λx. S index' ≤ |x| → (list A) × (list A) with
+    match l return λx. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a index' a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a title="norm" href="cic:/fakeuri.def(1)"|/ax| → (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) a title="Product" href="cic:/fakeuri.def(1)"×/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) with
     [ nil ⇒ λnil_absrd. ?
     | cons hd tl ⇒ λcons_prf.
       let 〈l1, l2〉 ≝ split A tl index' ? in
-        〈hd :: l1, l2〉
+        a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ahd a title="cons" href="cic:/fakeuri.def(1)":/a: l1, l2〉
     ] succ_prf
   ] proof.
   [1: normalize in nil_absrd;
-      cases(not_le_Sn_O index')
+      cases(a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"not_le_Sn_O/a index')
       #HYP
       cases(HYP nil_absrd)
   |2: normalize in cons_prf;
-      @le_S_S_to_le
+      @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a
       assumption
   ]
 qed.
 
 let rec nth_safe
-  (elt_type: Type[0]) (index: nat) (the_list: list elt_type)
-  (proof: index < | the_list |)
+  (elt_type: Type[0]) (index: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (the_list: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a elt_type)
+  (proof: index a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/a the_list |)
     on index ≝
-  match index return λs. s < | the_list | → elt_type with
+  match index return λs. s a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/a the_list | → elt_type with
   [ O ⇒
-    match the_list return λt. 0 < | t | → elt_type with
+    match the_list return λt. a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/a t | → elt_type with
     [ nil        ⇒ λnil_absurd. ?
     | cons hd tl ⇒ λcons_proof. hd
     ]
   | S index' ⇒
-    match the_list return λt. S index' < | t | → elt_type with
+    match the_list return λt. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a index' a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/a t | → elt_type with
     [ nil ⇒ λnil_absurd. ?
     | cons hd tl ⇒
       λcons_proof. nth_safe elt_type index' tl ?
     ]
   ] proof.
   [ normalize in nil_absurd;
-    cases (not_le_Sn_O 0)
+    cases (a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"not_le_Sn_O/a a title="natural number" href="cic:/fakeuri.def(1)"0/a)
     #ABSURD
     elim (ABSURD nil_absurd)
   | normalize in nil_absurd;
-    cases (not_le_Sn_O (S index'))
+    cases (a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"not_le_Sn_O/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a index'))
     #ABSURD
     elim (ABSURD nil_absurd)
   | normalize in cons_proof
-    @le_S_S_to_le
+    @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a
     assumption
   ]
 qed.
 
 definition last_safe ≝
   λelt_type: Type[0].
-  λthe_list: list elt_type.
-  λproof   : 0 < | the_list |.
-    nth_safe elt_type (|the_list| - 1) the_list ?.
-  normalize /2/
-qed.
+  λthe_list: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a elt_type.
+  λproof   : a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/a the_list |.
+    a href="cic:/matita/Cerco/ASM/Utils/nth_safe.fix(0,1,6)"nth_safe/a elt_type (a title="norm" href="cic:/fakeuri.def(1)"|/athe_list| a title="natural minus" href="cic:/fakeuri.def(1)"-/a a title="natural number" href="cic:/fakeuri.def(1)"1/a) the_list ?.
+  normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_plus_to_minus.def(12)"lt_plus_to_minus/a/span/span/
+qed. 
 
 let rec reduce 
-  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) on left ≝
+  (A: Type[0]) (B: Type[0]) (left: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (right: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) on left ≝
   match left with
-  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
+  [ nil ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="nil" href="cic:/fakeuri.def(1)"[/a ], a title="nil" href="cic:/fakeuri.def(1)"[/a ]〉, a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="nil" href="cic:/fakeuri.def(1)"[/a ], right〉〉
   | cons hd tl ⇒
     match right with
-    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
+    [ nil ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="nil" href="cic:/fakeuri.def(1)"[/a ], left〉, a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="nil" href="cic:/fakeuri.def(1)"[/a ], a title="nil" href="cic:/fakeuri.def(1)"[/a ]〉〉
     | cons hd' tl' ⇒
       let 〈cleft, cright〉 ≝ reduce A B tl tl' in
       let 〈commonl, restl〉 ≝ cleft in
       let 〈commonr, restr〉 ≝ cright in
-        〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉
+        a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ahd a title="cons" href="cic:/fakeuri.def(1)":/a: commonl, restl〉, a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ahd' a title="cons" href="cic:/fakeuri.def(1)":/a: commonr, restr〉〉
     ]
   ].
 
@@ -255,6 +249,7 @@ axiom reduce_strong:
     Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |.
 *)
 
+(*
 let rec reduce_strong
   (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
     on left : Σret: ((list A) × (list A)) × ((list B) × (list B)). |\fst (\fst ret)| = |\fst (\snd ret)|  ≝
@@ -277,41 +272,41 @@ let rec reduce_strong
        >p2 >p3 >p4 normalize in ⊢ (% → ?)
        #HYP //
   ]
-qed. 
+qed.*)
     
 let rec map2_opt
   (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
-  (left: list A) (right: list B) on left ≝
+  (left: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (right: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) on left ≝
   match left with
   [ nil ⇒
     match right with
-    [ nil ⇒ Some ? (nil C)
-    | _ ⇒ None ?
+    [ nil ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a C)
+    | _ ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
     ]
   | cons hd tl ⇒
     match right with
-    [ nil ⇒ None ?
+    [ nil ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
     | cons hd' tl' ⇒
       match map2_opt A B C f tl tl' with
-      [ None ⇒ None ?
-      | Some tail ⇒ Some ? (f hd hd' :: tail)
+      [ None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
+      | Some tail ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (f hd hd' a title="cons" href="cic:/fakeuri.def(1)":/a: tail)
       ]
     ]
   ].
 
 let rec map2
   (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
-  (left: list A) (right: list B) (proof: | left | = | right |) on left ≝
-  match left return λx. | x | = | right | → list C with
+  (left: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (right: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) (proof: a title="norm" href="cic:/fakeuri.def(1)"|/a left | a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/a right |) on left ≝
+  match left return λx. a title="norm" href="cic:/fakeuri.def(1)"|/a x | a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/a right | → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a C with
   [ nil ⇒
-    match right return λy. | [] | = | y | → list C with
-    [ nil ⇒ λnil_prf. nil C
+    match right return λy. a title="norm" 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 a title="norm" href="cic:/fakeuri.def(1)"|/a y | → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a C with
+    [ nil ⇒ λnil_prf. a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a C
     | _ ⇒ λcons_absrd. ?
     ]
   | cons hd tl ⇒
-    match right return λy. | hd::tl | = | y | → list C with
+    match right return λy. a title="norm" href="cic:/fakeuri.def(1)"|/a hda title="cons" href="cic:/fakeuri.def(1)":/a:tl | a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/a y | → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a C with
     [ nil ⇒ λnil_absrd. ?
-    | cons hd' tl' ⇒ λcons_prf. (f hd hd') :: map2 A B C f tl tl' ?
+    | cons hd' tl' ⇒ λcons_prf. (f hd hd') a title="cons" href="cic:/fakeuri.def(1)":/a: map2 A B C f tl tl' ?
     ]
   ] proof.
   [1: normalize in cons_absrd;
@@ -323,146 +318,86 @@ let rec map2
       assumption
   ]
 qed.
-
-let rec map3
-  (A: Type[0]) (B: Type[0]) (C: Type[0]) (D: Type[0]) (f: A → B → C → D)
-  (left: list A) (centre: list B) (right: list C)
-  (prflc: |left| = |centre|) (prfcr: |centre| = |right|) on left ≝
-  match left return λx. |x| = |centre| → list D with
-  [ nil ⇒ λnil_prf.
-    match centre return λx. |x| = |right| → list D with
-    [ nil ⇒ λnil_nil_prf.
-      match right return λx. |nil ?| = |x| → list D with
-      [ nil        ⇒ λnil_nil_nil_prf. nil D
-      | cons hd tl ⇒ λcons_nil_nil_absrd. ?
-      ] nil_nil_prf
-    | cons hd tl ⇒ λnil_cons_absrd. ?
-    ] prfcr
-  | cons hd tl ⇒ λcons_prf.
-    match centre return λx. |x| = |right| → list D with
-    [ nil ⇒ λcons_nil_absrd. ?
-    | cons hd' tl' ⇒ λcons_cons_prf.
-      match right return λx. |right| = |x| → |cons ? hd' tl'| = |x| → list D with
-      [ nil ⇒ λrefl_prf. λcons_cons_nil_absrd. ?
-      | cons hd'' tl'' ⇒ λrefl_prf. λcons_cons_cons_prf.
-        (f hd hd' hd'') :: (map3 A B C D f tl tl' tl'' ? ?)
-      ] (refl ? (|right|)) cons_cons_prf
-    ] prfcr
-  ] prflc.
-  [ 1: normalize in cons_nil_nil_absrd;
-       destruct(cons_nil_nil_absrd)
-  | 2: generalize in match nil_cons_absrd;
-       prfcrnil_prf #hyp="" normalize="" hyp;="" destruct(hyp)="" |="" 3:="" generalize="" in="" match="" cons_nil_absrd;=""prfcrcons_prf #hyp="" hyp;="" destruct(hyp)="" 4:="" cons_cons_nil_absrd;="" destruct(cons_cons_nil_absrd)="" 5:="" normalize="" destruct(cons_cons_cons_prf)="" assumption="" |="" 6:="" generalize="" in="" match="" cons_cons_cons_prf;=""refl_prfprfcrcons_prf #hyp="" normalize="" hyp;="" destruct(hyp)="" @sym_eq="" assumption="" ]="" lemma="" eq_rect_type0_r="" :="" ∀a:="" ∀a:a.="" ∀p:="" ∀x:a.="" eq="" type[0].="" (refl="" a="" →="" ∀x:="" a.∀p:eq="" ?="" a.="" x="" p.="" #a="" #h="" #x="" #p="" h="" generalize="" in="" match="" cases="" p="" qed.="" let="" rec="" safe_nth="" (a:="" type[0])="" (n:="" nat)="" (l:="" list="" a)="" (p:="" n=""< length A l) on n: A ≝
-  match n return λo. o < length A l → A with
-  [ O ⇒
-    match l return λm. 0 < length A m → A with
-    [ nil ⇒ λabsd1. ?
-    | cons hd tl ⇒ λprf1. hd
-    ]
-  | S n' ⇒
-    match l return λm. S n' < length A m → A with
-    [ nil ⇒ λabsd2. ?
-    | cons hd tl ⇒ λprf2. safe_nth A n' tl ?
-    ]
-  ] ?.
-  [ 1:
-    @ p
-  | 4:
-    normalize in prf2
-    normalize
-    @ le_S_S_to_le
-    assumption
-  | 2:
-    normalize in absd1;
-    cases (not_le_Sn_O O)
-    # H
-    elim (H absd1)
-  | 3:
-    normalize in absd2;
-    cases (not_le_Sn_O (S n'))
-    # H
-    elim (H absd2)
-  ]
-qed.
   
-let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝
+let rec nub_by_internal (A: Type[0]) (f: A → A → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) on n ≝
   match n with
   [ O ⇒
     match l with
-    [ nil ⇒ [ ]
+    [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ]
     | cons hd tl ⇒ l
     ]
   | S n ⇒
     match l with
-    [ nil ⇒ [ ]
+    [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ]
     | cons hd tl ⇒
-      hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n
+      hd a title="cons" href="cic:/fakeuri.def(1)":/a: nub_by_internal A f (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? (λy. a href="cic:/matita/basics/bool/notb.def(1)"notb/a (f y hd)) tl) n
     ]
   ].
   
 definition nub_by ≝
   λA: Type[0].
-  λf: A → A → bool.
-  λl: list A.
-    nub_by_internal A f l (length ? l).
+  λf: A → A → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.
+  λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
+    a href="cic:/matita/Cerco/ASM/Utils/nub_by_internal.fix(0,3,3)"nub_by_internal/a A f l (a href="cic:/matita/basics/list2/length.fix(0,1,1)"length/a ? l).
   
-let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝
+let rec member (A: Type[0]) (eq: A → A → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (a: A) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝
   match l with
-  [ nil ⇒ false
-  | cons hd tl ⇒ orb (eq a hd) (member A eq a tl)
+  [ nil ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a
+  | cons hd tl ⇒ a href="cic:/matita/basics/bool/orb.def(1)"orb/a (eq a hd) (member A eq a tl)
   ].
   
-let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝
+let rec take (A: Type[0]) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on n: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A ≝
   match n with
-  [ O ⇒ [ ]
+  [ O ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ]
   | S n ⇒
     match l with
-    [ nil ⇒ [ ]
-    | cons hd tl ⇒ hd :: take A n tl
+    [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ]
+    | cons hd tl ⇒ hd a title="cons" href="cic:/fakeuri.def(1)":/a: take A n tl
     ]
   ].
   
-let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝
+let rec drop (A: Type[0]) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on n ≝
   match n with
   [ O ⇒ l
   | S n ⇒
     match l with
-    [ nil ⇒ [ ]
+    [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ]
     | cons hd tl ⇒ drop A n tl
     ]
   ].
   
 definition list_split ≝
   λA: Type[0].
-  λn: nat.
-  λl: list A.
-    〈take A n l, drop A n l〉.
+  λn: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+  λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
+    a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/Cerco/ASM/Utils/take.fix(0,1,1)"take/a A n l, a href="cic:/matita/Cerco/ASM/Utils/drop.fix(0,1,1)"drop/a A n l〉.
   
-let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B)
-                      (l: list A) on l: list B ≝
+let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (f: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → A → B)
+                      (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B ≝
   match l with
-  [ nil ⇒ nil ?
-  | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl)
+  [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ?
+  | cons hd tl ⇒ (f n hd) a title="cons" href="cic:/fakeuri.def(1)":/a: (mapi_internal A B (n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a title="natural number" href="cic:/fakeuri.def(1)"1/a) f tl)
   ].  
 
 definition mapi ≝
   λA, B: Type[0].
-  λf: nat → A → B.
-  λl: list A.
-    mapi_internal A B 0 f l.
+  λf: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → A → B.
+  λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
+    a href="cic:/matita/Cerco/ASM/Utils/mapi_internal.fix(0,4,2)"mapi_internal/a A B a title="natural number" href="cic:/fakeuri.def(1)"0/a f l.
 
 let rec zip_pottier
-  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
+  (A: Type[0]) (B: Type[0]) (left: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (right: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B)
     on left ≝
   match left with
-  [ nil ⇒ [ ]
+  [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ]
   | cons hd tl ⇒
     match right with
-    [ nil ⇒ [ ]
-    | cons hd' tl' ⇒ 〈hd, hd'〉 :: zip_pottier A B tl tl'
+    [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ]
+    | cons hd' tl' ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ahd, hd'〉 a title="cons" href="cic:/fakeuri.def(1)":/a: zip_pottier A B tl tl'
     ]
   ].
 
+(*
 let rec zip_safe
   (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) (prf: |left| = |right|)
     on left ≝
@@ -486,23 +421,23 @@ let rec zip_safe
        @injective_S
        assumption
   ]
-qed.
+qed. *)
 
-let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝
+let rec zip (A: Type[0]) (B: Type[0]) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (r: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) on l: a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (A a title="Product" href="cic:/fakeuri.def(1)"×/a B)) ≝
   match l with
-  [ nil ⇒ Some ? (nil (A × B))
+  [ nil ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a (A a title="Product" href="cic:/fakeuri.def(1)"×/a B))
   | cons hd tl ⇒
     match r with
-    [ nil ⇒ None ?
+    [ nil ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
     | cons hd' tl' ⇒
       match zip ? ? tl tl' with
-      [ None ⇒ None ?
-      | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail)
+      [ None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
+      | Some tail ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ahd, hd'〉 a title="cons" href="cic:/fakeuri.def(1)":/a: tail)
       ]
     ]
   ].
 
-let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝
+let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) on l ≝
   match l with
   [ nil ⇒ a
   | cons hd tl ⇒ foldl A B f (f a hd) tl
@@ -513,9 +448,9 @@ lemma foldl_step:
   ∀B: Type[0].
    ∀H: A → B → A.
     ∀acc: A.
-     ∀pre: list B.
+     ∀pre: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B.
       ∀hd:B.
-       foldl A B H acc (pre@[hd]) = (H (foldl A B H acc pre) hd).
+       a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"foldl/a A B H acc (prea title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/ahd]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (H (a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"foldl/a A B H acc pre) hd).
  #A #B #H #acc #pre generalize in match acc; -acc; elim pre
   [ normalize; //
   | #hd #tl #IH #acc #X normalize; @IH ]
@@ -526,24 +461,25 @@ lemma foldl_append:
   ∀B: Type[0].
    ∀H: A → B → A.
     ∀acc: A.
-     ∀suff,pre: list B.
-      foldl A B H acc (pre@suff) = (foldl A B H (foldl A B H acc pre) suff).
+     ∀suff,pre: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B.
+      a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"foldl/a A B H acc (prea title="append" href="cic:/fakeuri.def(1)"@/asuff) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"foldl/a A B H (a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"foldl/a A B H acc pre) suff).
  #A #B #H #acc #suff elim suff
-  [ #pre >append_nil %
-  | #hd #tl #IH #pre whd in ⊢ (???%) <(foldl_step … H ??) applyS (IH (pre@[hd])) ] 
+  [ #pre >a href="cic:/matita/basics/list/append_nil.def(4)"append_nil/a %
+  | #hd #tl #IH #pre whd in ⊢ (???%) <(a href="cic:/matita/Cerco/ASM/Utils/foldl_step.def(2)"foldl_step/a … H ??) applyS (IH (prea title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/ahd])) ] 
 qed.
 
 definition flatten ≝
   λA: Type[0].
-  λl: list (list A).
-    foldr ? ? (append ?) [ ] l.
+  λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A).
+    a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ? ? (a href="cic:/matita/basics/list/append.fix(0,1,1)"append/a ?) a title="nil" href="cic:/fakeuri.def(1)"[/a ] l.
 
-let rec rev (A: Type[0]) (l: list A) on l ≝ 
+let rec rev (A: Type[0]) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ 
   match l with
-  [ nil ⇒ nil A
-  | cons hd tl ⇒ (rev A tl) @ [ hd ]
+  [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A
+  | cons hd tl ⇒ (rev A tl) a title="append" href="cic:/fakeuri.def(1)"@/a a title="cons" href="cic:/fakeuri.def(1)"[/a hd ]
   ].
 
+(*
 lemma append_length:
   ∀A: Type[0].
   ∀l, r: list A.
@@ -618,7 +554,7 @@ lemma nth_append_second:
    | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
    ] 
  ]
-qed.
+qed.*)
 
     
 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
@@ -627,17 +563,17 @@ notation < "hvbox('if' \nbsp term 19 e \nbsp break 'then' \nbsp term 19 t \nbsp
  for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
 
 let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
-                        (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
+                        (f: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → A → B → A) (x: A) (i: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) on l ≝
   match l with
     [ nil ⇒ x
-    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
+    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i) tl
     ].
 
-definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
+definition fold_left_i ≝ λA,B,f,x. a href="cic:/matita/Cerco/ASM/Utils/fold_left_i_aux.fix(0,5,1)"fold_left_i_aux/a A B f x a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
 
-notation "hvbox(t⌈o ↦ h⌉)"
+(* notation "hvbox(t\lceil o \mapsto h\rceil )"
   with precedence 45
-  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
+  for @{ match (? : $o=$h) with [ refl \Rightarrow $t ] }. *)
 
 definition function_apply ≝
   λA, B: Type[0].
@@ -650,8 +586,14 @@ notation "f break $ x"
   for @{ 'function_apply $f $x }.
   
 interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
+    
+notation "f break $ x"
+  left associative with precedence 99
+  for @{ 'function_apply $f $x }.
+  
+interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
 
-let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
+let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) on n ≝
   match n with
     [ O ⇒ a
     | S o ⇒ f (iterate A f a o)
@@ -682,8 +624,8 @@ axiom pair_elim':
   ∀A,B,C: Type[0].
   ∀T: A → B → C.
   ∀p.
-  ∀P: A×B → C → Prop.
-    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
+  ∀P: Aa title="Product" href="cic:/fakeuri.def(1)"×/aB → C → Prop.
+    (∀lft, rgt. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/alft,rgt〉 → P a title="Pair construction" href="cic:/fakeuri.def(1)"〈/alft,rgt〉 (T lft rgt)) →
       P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
 
 axiom pair_elim'':
@@ -691,32 +633,32 @@ axiom pair_elim'':
   ∀T: A → B → C.
   ∀T': A → B → C'.
   ∀p.
-  ∀P: A×B → C → C' → Prop.
-    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
+  ∀P: Aa title="Product" href="cic:/fakeuri.def(1)"×/aB → C → C' → Prop.
+    (∀lft, rgt. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/alft,rgt〉 → P a title="Pair construction" href="cic:/fakeuri.def(1)"〈/alft,rgt〉 (T lft rgt) (T' lft rgt)) →
       P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
 
 lemma pair_destruct_1:
- ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
- #A #B #a #b *; /2/
+ ∀A,B.∀a:A.∀b:B.∀c. a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa,b〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a c → a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a c.
+ #A #B #a #b *; /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/trans_eq.def(4)"trans_eq/a/span/span/
 qed.
 
 lemma pair_destruct_2:
- ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
- #A #B #a #b *; /2/
+ ∀A,B.∀a:A.∀b:B.∀c. a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa,b〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a c → b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a c.
+ #A #B #a #b *; /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/trans_eq.def(4)"trans_eq/a/span/span/
 qed.
 
 
-let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
+let rec exclusive_disjunction (b: a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (c: a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) on b ≝
   match b with
     [ true ⇒
       match c with
-        [ false ⇒ true
-        | true ⇒ false
+        [ false ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a
+        | true ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a
         ]
     | false ⇒
       match c with
-        [ false ⇒ false
-        | true ⇒ true
+        [ false ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a
+        | true ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a
         ]
     ].
 
@@ -726,21 +668,21 @@ interpretation "Nat greater than" 'gt m n = (gtb m n).
 interpretation "Nat greater than eq" 'geq m n = (geb m n).
 *)
 
-let rec division_aux (m: nat) (n : nat) (p: nat) ≝
-  match ltb n (S p) with
-    [ true ⇒ O
+let rec division_aux (m: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (n : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (p: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) ≝
+  match a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"ltb/a n (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a p) with
+    [ true ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a
     | false ⇒
       match m with
-        [ O ⇒ O
-        | (S q) ⇒ S (division_aux q (n - (S p)) p)
+        [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a
+        | (S q) ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (division_aux q (n a title="natural minus" href="cic:/fakeuri.def(1)"-/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a p)) p)
         ]
     ].
     
 definition division ≝
-  λm, n: nat.
+  λm, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
     match n with
-      [ O ⇒ S m
-      | S o ⇒ division_aux m m o
+      [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m
+      | S o ⇒ a href="cic:/matita/Cerco/ASM/Utils/division_aux.fix(0,0,3)"division_aux/a m m o
       ].
       
 notation "hvbox(n break ÷ m)"
@@ -749,21 +691,21 @@ notation "hvbox(n break ÷ m)"
   
 interpretation "Nat division" 'division n m = (division n m).
 
-let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
-  match leb n p with
+let rec modulus_aux (m: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (p: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) ≝
+  match a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n p with
     [ true ⇒ n
     | false ⇒
       match m with
         [ O ⇒ n
-        | S o ⇒ modulus_aux o (n - (S p)) p
+        | S o ⇒ modulus_aux o (n a title="natural minus" href="cic:/fakeuri.def(1)"-/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a p)) p
         ]
     ].
     
 definition modulus ≝
-  λm, n: nat.
+  λm, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
     match n with
       [ O ⇒ m
-      | S o ⇒ modulus_aux m m o
+      | S o ⇒ a href="cic:/matita/Cerco/ASM/Utils/modulus_aux.fix(0,0,2)"modulus_aux/a m m o
       ].
     
 notation "hvbox(n break 'mod' m)"
@@ -773,13 +715,13 @@ notation "hvbox(n break 'mod' m)"
 interpretation "Nat modulus" 'modulus m n = (modulus m n).
 
 definition divide_with_remainder ≝
-  λm, n: nat.
-    pair ? ? (m ÷ n) (modulus m n).
+  λm, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+    a href="cic:/matita/basics/types/Prod.con(0,1,2)"pair/a ? ? (m a title="Nat division" href="cic:/fakeuri.def(1)"÷/a n) (a href="cic:/matita/Cerco/ASM/Utils/modulus.def(3)"modulus/a m n).
     
-let rec exponential (m: nat) (n: nat) on n ≝
+let rec exponential (m: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) on n ≝
   match n with
-    [ O ⇒ S O
-    | S o ⇒ m * exponential m o
+    [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a
+    | S o ⇒ m a title="natural times" href="cic:/fakeuri.def(1)"*/a exponential m o
     ].
 
 interpretation "Nat exponential" 'exp n m = (exponential n m).
@@ -790,16 +732,16 @@ for @{ 'disjoint_union $a $b }.
 interpretation "sum" 'disjoint_union A B = (Sum A B).
 
 theorem less_than_or_equal_monotone:
-  ∀m, n: nat.
-    m ≤ n → (S m) ≤ (S n).
+  ∀m, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+    m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n).
  #m #n #H
  elim H
- /2/
+ /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/
 qed.
 
 theorem less_than_or_equal_b_complete:
-  ∀m, n: nat.
-    leb m n = false → ¬(m ≤ n).
+  ∀m, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+    a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a m n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="logical not" href="cic:/fakeuri.def(1)"¬/a(m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n).
  #m;
  elim m;
  normalize
@@ -809,15 +751,15 @@ theorem less_than_or_equal_b_complete:
    cases z
    normalize
    [ #H
-     /2/
-   | /3/
+     /span class="autotactic"2span class="autotrace" trace {}/span/span/
+   | /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_le_to_not_le_S_S.def(5)"not_le_to_not_le_S_S/a/span/span/    
    ]
  ]
 qed.
 
 theorem less_than_or_equal_b_correct:
-  ∀m, n: nat.
-    leb m n = true → m ≤ n.
+  ∀m, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+    a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a m n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
  #m
  elim m
  //
@@ -826,72 +768,65 @@ theorem less_than_or_equal_b_correct:
  normalize
  [ #H
    destruct
- | #n #H lapply (H1 … H) /2/
+ | #n #H lapply (H1 … H) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/Cerco/ASM/Utils/less_than_or_equal_monotone.def(2)"less_than_or_equal_monotone/a/span/span/
  ]
 qed.
 
 definition less_than_or_equal_b_elim:
- ∀m, n: nat.
- ∀P: bool → Type[0].
-   (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n).
+ ∀m, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+ ∀P: a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Type[0].
+   (m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → (a title="logical not" href="cic:/fakeuri.def(1)"¬/a(m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n) → P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → P (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a m n).
  #m #n #P #H1 #H2;
- lapply (less_than_or_equal_b_correct m n)
- lapply (less_than_or_equal_b_complete m n)
- cases (leb m n)
- /3/
+ lapply (a href="cic:/matita/Cerco/ASM/Utils/less_than_or_equal_b_correct.def(3)"less_than_or_equal_b_correct/a m n)
+ lapply (a href="cic:/matita/Cerco/ASM/Utils/less_than_or_equal_b_complete.def(6)"less_than_or_equal_b_complete/a m n)
+ cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a m n)
+ /span class="autotactic"3span class="autotrace" trace {}/span/span/
 qed.
 
 lemma inclusive_disjunction_true:
-  ∀b, c: bool.
-    (orb b c) = true → b = true ∨ c = true.
+  ∀b, c: a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.
+    (a href="cic:/matita/basics/bool/orb.def(1)"orb/a b c) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical or" href="cic:/fakeuri.def(1)"∨/a c a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
   # b
   # c
   elim b
   [ normalize
     # H
-    @ or_introl
+    @ a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a
     %
   | normalize
-    /2/
+    /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/
   ]
 qed.
 
 lemma conjunction_true:
-  ∀b, c: bool.
-    andb b c = true → b = true ∧ c = true.
+  ∀b, c: a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.
+    a href="cic:/matita/basics/bool/andb.def(1)"andb/a b c a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a c a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
   # b
   # c
   elim b
   normalize
-  [ /2/
+  [ /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
   | # K
     destruct
   ]
 qed.
 
-lemma eq_true_false: false=true → False.
+lemma eq_true_false: a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a.
  # K
  destruct
 qed.
 
-lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
+lemma inclusive_disjunction_b_true: ∀b. a href="cic:/matita/basics/bool/orb.def(1)"orb/a b a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
  # b
  cases b
  %
 qed.
 
 definition bool_to_Prop ≝
- λb. match b with [ true ⇒ True | false ⇒ False ].
+ λb. match b with [ true ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | false ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a ].
 
-coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 
-
-lemma eq_false_to_notb: ∀b. b = false → ¬ b.
- *; /2/
-qed.
+coercion bool_to_Prop: ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. Prop ≝ a href="cic:/matita/Cerco/ASM/Utils/bool_to_Prop.def(1)"bool_to_Prop/a on _b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a to Type[0]. 
 
-lemma length_append:
- ∀A.∀l1,l2:list A.
-  |l1 @ l2| = |l1| + |l2|.
- #A #l1 elim l1
-  [ //
-  | #hd #tl #IH #l2 normalize ih ]="" qed.=""/ih/cons_prf/prfcr/refl_prf/cons_prf/prfcr/nil_prf/prfcr
\ No newline at end of file
+lemma eq_false_to_notb: ∀b. b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="boolean not" href="cic:/fakeuri.def(1)"¬/a b.
+ *; /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/True.con(0,1,0)"I/a/span/span/
+qed.
\ No newline at end of file