X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fesempi%2Ffourier.cic;h=09caea79be6c9617500e850bb255e7c9b15ca5ee;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=cae3925a7102fc58a1539f7c2a72e6994ff76374;hpb=273ed08112cf9470644498dc495d9e60519e5eaa;p=helm.git

diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic
index cae3925a7..09caea79b 100644
--- a/helm/gTopLevel/esempi/fourier.cic
+++ b/helm/gTopLevel/esempi/fourier.cic
@@ -1,8 +1,35 @@
 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))
+
+