X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtopLevel%2Fesempi.cic;fp=helm%2FgTopLevel%2FtopLevel%2Fesempi.cic;h=0000000000000000000000000000000000000000;hb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;hp=38e5f33331b787daf533ee700c5620556b772f1b;hpb=2dc0733271cd251aaa3edaece8a883fe691775ab;p=helm.git

diff --git a/helm/gTopLevel/topLevel/esempi.cic b/helm/gTopLevel/topLevel/esempi.cic
deleted file mode 100644
index 38e5f3333..000000000
--- a/helm/gTopLevel/topLevel/esempi.cic
+++ /dev/null
@@ -1,125 +0,0 @@
-alias BV                 /Sophia-Antipolis/HARDWARE/GENE/BV/BV.con
-alias BV_increment       /Sophia-Antipolis/HARDWARE/ADDER/IncrDecr/BV_increment.con
-alias BV_increment_carry /Sophia-Antipolis/HARDWARE/ADDER/IncrDecr/BV_increment_carry.con
-alias BV_to_nat          /Sophia-Antipolis/HARDWARE/GENE/BV/BV_to_nat.con
-alias Exp                /Eindhoven/POCKLINGTON/exp/Exp.con
-alias IZR                /Coq/Reals/Raxioms/IZR.con
-alias Int_part           /Coq/Reals/R_Ifp/Int_part.con
-alias Mod                /Eindhoven/POCKLINGTON/mod/Mod.con
-alias NEG                /Coq/ZArith/fast_integer/fast_integers/Z.ind#1/1/3
-alias O                  /Coq/Init/Datatypes/nat.ind#1/1/1
-alias POS                /Coq/ZArith/fast_integer/fast_integers/Z.ind#1/1/2
-alias Prime              /Eindhoven/POCKLINGTON/prime/Prime.con
-alias R                  /Coq/Reals/Rdefinitions/R.con
-alias R0                 /Coq/Reals/Rdefinitions/R0.con
-alias R1                 /Coq/Reals/Rdefinitions/R1.con
-alias Rgt                /Coq/Reals/Rdefinitions/Rgt.con
-alias Rinv               /Coq/Reals/Rdefinitions/Rinv.con
-alias Rle                /Coq/Reals/Rdefinitions/Rle.con
-alias Rlt                /Coq/Reals/Rdefinitions/Rlt.con
-alias Rminus             /Coq/Reals/Rdefinitions/Rminus.con
-alias Rmult              /Coq/Reals/Rdefinitions/Rmult.con
-alias Ropp               /Coq/Reals/Rdefinitions/Ropp.con
-alias Rplus              /Coq/Reals/Rdefinitions/Rplus.con
-alias S                  /Coq/Init/Datatypes/nat.ind#1/1/2
-alias Z                  /Coq/ZArith/fast_integer/fast_integers/Z.ind#1/1
-alias ZERO               /Coq/ZArith/fast_integer/fast_integers/Z.ind#1/1/1
-alias ZExp               /Eindhoven/POCKLINGTON/exp/ZExp.con
-alias Zdiv2              /Coq/ZArith/Zmisc/arith/Zdiv2.con
-alias Zge                /Coq/ZArith/zarith_aux/Zge.con
-alias Zle                /Coq/ZArith/zarith_aux/Zle.con
-alias Zlt                /Coq/ZArith/zarith_aux/Zlt.con
-alias Zminus             /Coq/ZArith/zarith_aux/Zminus.con
-alias Zmult              /Coq/ZArith/fast_integer/fast_integers/Zmult.con
-alias Zodd               /Coq/ZArith/Zmisc/arith/Zodd.con
-alias Zplus              /Coq/ZArith/fast_integer/fast_integers/Zplus.con
-alias Zpower_nat         /Coq/omega/Zpower/section1/Zpower_nat.con
-alias Zpower_pos         /Coq/omega/Zpower/section1/Zpower_pos.con
-alias Zpred              /Coq/ZArith/zarith_aux/Zpred.con
-alias Zs                 /Coq/ZArith/zarith_aux/Zs.con
-alias ad                 /Coq/IntMap/Addr/ad.ind#1/1
-alias ad_bit             /Coq/IntMap/Addr/ad_bit.con
-alias ad_double_plus_un  /Coq/IntMap/Addr/ad_double_plus_un.con
-alias ad_x               /Coq/IntMap/Addr/ad.ind#1/1/2
-alias ad_xor             /Coq/IntMap/Addr/ad_xor.con
-alias allex              /Eindhoven/POCKLINGTON/fermat/allex.con
-alias and                /Coq/Init/Logic/Conjunction/and.ind#1/1
-alias appbv              /Sophia-Antipolis/HARDWARE/GENE/BV/appbv.con
-alias bool               /Coq/Init/Datatypes/bool.ind#1/1
-alias consbv             /Sophia-Antipolis/HARDWARE/GENE/BV/consbv.con
-alias convert            /Coq/ZArith/fast_integer/fast_integers/convert.con
-alias div2               /Coq/Arith/Div2/div2.con
-alias double             /Coq/Arith/Div2/double.con
-alias eq                 /Coq/Init/Logic/Equality/eq.ind#1/1
-alias eq_ind             /Coq/Init/Logic/Equality/eq_ind.con
-alias eq_ind_r           /Coq/Init/Logic/Logic_lemmas/eq_ind_r.con
-alias eqT                /Coq/Init/Logic_Type/eqT.ind#1/1
-alias even               /Coq/Arith/Even/even.ind#1/1
-alias ex                 /Coq/Init/Logic/First_order_quantifiers/ex.ind#1/1
-alias f_equal            /Coq/Init/Logic/Logic_lemmas/equality/f_equal.con
-alias iff                /Coq/Init/Logic/Equivalence/iff.con
-alias le                 /Coq/Init/Peano/le.ind#1/1
-alias lengthbv           /Sophia-Antipolis/HARDWARE/GENE/BV/lengthbv.con
-alias lift_rec_r         /Rocq/LAMBDA/Substitution/lift_rec_r.con
-alias log_inf            /Coq/omega/Zlogarithm/Log_pos/log_inf.con
-alias log_sup            /Coq/omega/Zlogarithm/Log_pos/log_sup.con
-alias lt                 /Coq/Init/Peano/lt.con
-alias mapmult            /Eindhoven/POCKLINGTON/list/mapmult.con
-alias minus              /Coq/Arith/Minus/minus.con
-alias mult               /Coq/Init/Peano/mult.con
-alias nat                /Coq/Init/Datatypes/nat.ind#1/1
-alias nat_of_ad          /Coq/IntMap/Adalloc/AdAlloc/nat_of_ad.con 
-alias negb               /Coq/Bool/Bool/negb.con
-alias nilbv              /Sophia-Antipolis/HARDWARE/GENE/BV/nilbv.con
-alias not                /Coq/Init/Logic/not.con
-alias odd                /Coq/Arith/Even/even.ind#1/2
-alias or                 /Coq/Init/Logic/Disjunction/or.ind#1/1
-alias permmod            /Eindhoven/POCKLINGTON/fermat/permmod.con
-alias plus               /Coq/Init/Peano/plus.con
-alias positive           /Coq/ZArith/fast_integer/fast_integers/positive.ind#1/1
-alias power2             /Sophia-Antipolis/HARDWARE/GENE/Arith_compl/power2.con
-alias pred               /Coq/Init/Peano/pred.con
-alias redexes            /Rocq/LAMBDA/Redexes/redexes.ind#1/1
-alias shift_nat          /Coq/omega/Zpower/Powers_of_2/shift_nat.con
-alias shift_pos          /Coq/omega/Zpower/Powers_of_2/shift_pos.con
-alias subst_rec_r        /Rocq/LAMBDA/Substitution/subst_rec_r.con
-alias two_p              /Coq/omega/Zpower/Powers_of_2/two_p.con
-alias until              /Eindhoven/POCKLINGTON/fermat/until.con
-alias xH                 /Coq/ZArith/fast_integer/fast_integers/positive.ind#1/1/3
-alias xI                 /Coq/ZArith/fast_integer/fast_integers/positive.ind#1/1/1
-alias xO                 /Coq/ZArith/fast_integer/fast_integers/positive.ind#1/1/2
-alias zproduct           /Eindhoven/POCKLINGTON/list/zproduct.con
-
-!n:nat.(eq nat (mult (S (S O)) n) O);
-!n:nat.(eq nat (plus O n) (plus n O));
-!n:nat.!m:nat.(le (mult (S (S O)) n) (mult (S (S O)) m));
-!p:nat.(eq nat p p)->(eq nat p p);
-!p:nat.!q:nat.(le p q)->(or (le (S p) q) (eq nat p q));
-!n:nat.(eq nat (double (S n)) (S (S (double n))));
-!n:nat.(and (iff (even n) (eq nat (div2 n) (div2 (S n)))) (iff (odd n) (eq nat (S (div2 n)) (div2 (S n)))));
-!n:nat.!m:nat.!p:nat.(eq nat (minus n m) (minus (plus p n) (plus p m)));
-!a:Z.!n:nat.(eq Z (Exp a (pred (S n))) (Exp a n));
-!a:Z.!x:Z.(eq Z (ZExp a (Zminus (Zplus x (POS xH)) (POS xH))) (ZExp a x));
-!p:nat.!a:Z.(Prime p)->(not (Mod a ZERO p))->(allex p (until (pred p)) (mapmult a (until (pred p))));
-!a:Z.!n:nat.(eq Z (zproduct (mapmult a (until n))) (Zmult (Exp a n) (zproduct (until n))));
-!p:nat.!a:Z.(Prime p)->(not (Mod a ZERO p))->(permmod p (until (pred p)) (mapmult a (until (pred p))));
-!p:nat.(Prime p)->(not (Mod (zproduct (until (pred p))) ZERO p));
-!p:nat.!n:nat.(lt O n)->(lt n p)->(Prime p)->(not (Mod (zproduct (until n)) ZERO p));
-!p:positive.(eq nat (convert (xI p)) (S (mult (S (S O)) (convert p))));
-!a:ad.(eq nat (nat_of_ad (ad_double_plus_un a)) (S (mult (S (S O)) (nat_of_ad a))));
-!p:positive.!a:ad.(eq bool (ad_bit (ad_xor (ad_x (xI p)) a) O) (negb (ad_bit a O)));
-!r:R.(and (Rle (IZR (Int_part r)) r) (Rgt (Rminus (IZR (Int_part r)) r) (Ropp R1)));
-!eps:R.(Rgt eps R0)->(Rlt (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))) eps);
-!x:Z.(Zge x ZERO)->(Zodd x)->(eq Z x (Zplus (Zmult (POS (xO xH)) (Zdiv2 x)) (POS xH)));
-!v:Z.!l1:Z.!l2:Z.!x:positive.(eq Z (Zplus (Zplus (Zmult v (POS x)) l1) (Zplus (Zmult v (NEG x)) l2)) (Zplus l1 l2));
-!v:Z.!l1:Z.!l2:Z.!x:positive.(eq Z (Zplus (Zplus (Zmult v (NEG x)) l1) (Zplus (Zmult v (POS x)) l2)) (Zplus l1 l2));
-!p:positive.(and (Zle (two_p (log_inf p)) (POS p)) (Zlt (POS p) (two_p (Zs (log_inf p)))));
-!x:positive.(and (Zlt (two_p (Zpred (log_sup x))) (POS x)) (Zle (POS x) (two_p (log_sup x))));
-!n:nat.!x:positive.(eq Z (POS (shift_nat n x)) (Zmult (Zpower_nat (POS (xO xH)) n) (POS x)));
-!p:positive.!x:positive.(eq Z (POS (shift_pos p x)) (Zmult (Zpower_pos (POS (xO xH)) p) (POS x)));
-!U:redexes.!V:redexes.!k:nat.!p:nat.!n:nat.(eq redexes (lift_rec_r (subst_rec_r V U p) (plus p n) k) (subst_rec_r (lift_rec_r V (S (plus p n)) k) (lift_rec_r U n k) p));
-!U:redexes.!V:redexes.!W:redexes.!n:nat.!p:nat.(eq redexes (subst_rec_r (subst_rec_r V U p) W (plus p n)) (subst_rec_r (subst_rec_r V W (S (plus p n))) (subst_rec_r U W n) p));
-!v:BV.(eq nat (BV_to_nat (appbv (BV_increment v) (consbv (BV_increment_carry v) nilbv))) (S (BV_to_nat v)));
-!l:BV.!n:BV.(eq nat (BV_to_nat (appbv l n)) (plus (BV_to_nat l) (mult (power2 (lengthbv l)) (BV_to_nat n))));
-!x:Z.(Zle ZERO x)->(eq Z (Zdiv2 (Zplus (Zmult (POS (xO xH)) x) (POS xH))) x);
-!n:Z.(Zle (POS xH) n)->(Zle ZERO (Zplus (Zdiv2 (Zminus n (POS (xO xH)))) (POS xH)));