bug in hypotesis parsing solved

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

diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic
index ba51e64ad80b3a8ee7dab716b0b34e6b93fe4f3f..d2f9e4983b456c06c95231b3481a8a159e36614c 100644 (file)
--- a/helm/gTopLevel/esempi/fourier.cic
+++ b/helm/gTopLevel/esempi/fourier.cic
@@ -14,7 +14,13 @@ alias eqT    /Coq/Init/Logic_Type/eqT.ind#1/1
 alias not      /Coq/Init/Logic/not.con
 alias or /Coq/Init/Logic/or.ind#1/1
 
-(*test real*)
+//baco
+!x:R.
+(Rlt (Rmult(Ropp x)R1)
+R0)
+->(Rlt R0 x)
+
+// test 3x4 -> 35''
 !x:R.!y:R.!z:R.
 (Rge
 (Rplus
@@ -44,6 +50,39 @@ alias or /Coq/Init/Logic/or.ind#1/1
 
 -> (Rlt z R1)
 
+// test 6x6 -> 
+
+!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.
+(Rgt
+(Rplus (Ropp x) (Rplus y (Rplus z (Rplus t (Rplus u (Rplus v (Rplus R1 R1)))))))
+  R0)
+->
+(Rgt
+(Rplus x (Rplus (Ropp y) (Rplus (Ropp z) (Rplus (Ropp t) (Rplus (Ropp u) (Rplus R1 R1))))))
+  R0)
+->
+(Rgt
+(Rplus y (Rplus (Ropp z) (Rplus t (Rplus u (Rplus R1 R1)))))
+  R0)
+->
+(Rgt
+(Rplus y (Rplus z (Rplus (Ropp t) (Rplus (Ropp (Rmult (Rplus R1 R1)v)) (Rplus R1 R1)))))
+  R0)
+->
+(Rgt
+(Rplus y (Rplus z (Rplus t (Rplus (Ropp u) (Rplus R1 R1)))))
+  R0)
+->
+(Rlt
+(Rplus (Rmult (Rplus R1 R1) x) (Rplus v y))
+  R0)
+-> (Rlt (Rmult (Rplus R1 R1) x) R0)
+
+
+
+
+
+
 //test base1 ok
 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))