This commit was manufactured by cvs2svn to create branch 'init'.

[helm.git] / helm / gTopLevel / esempi / fourier.cic

diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic
deleted file mode 100644 (file)
index 09caea7..0000000
--- a/helm/gTopLevel/esempi/fourier.cic
+++ /dev/null
@@ -1,35 +0,0 @@
-alias Rge       /Coq/Reals/Rdefinitions/Rge.con
-alias Rle       /Coq/Reals/Rdefinitions/Rle.con
-alias Rgt       /Coq/Reals/Rdefinitions/Rgt.con
-alias Rlt       /Coq/Reals/Rdefinitions/Rlt.con
-alias Ropp     /Coq/Reals/Rdefinitions/Ropp.con
-alias Rinv     /Coq/Reals/Rdefinitions/Rinv.con
-alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
-alias Rminus    /Coq/Reals/Rdefinitions/Rminus.con
-alias R1        /Coq/Reals/Rdefinitions/R1.con
-alias R0        /Coq/Reals/Rdefinitions/R0.con
-alias R        /Coq/Reals/Rdefinitions/R.con
-alias Eq       /Coq/Init/Logic_Type/eqT.ind#1/1
-
-//test base1 ok
-!x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
-
-//test base2 ok
-!x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1))
-
-//test base3 (unification fails)
-!x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1)))
-
-//test base4 ok
-!x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1))
-
-//test base5 ok
-!x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0))
-
-//test base6 (unification fails)
-!x:R.!y:R.(Eq R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
-
-//test base7 (should fail) ok
-!x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1))
-
-