Added examples.

[helm.git] / helm / gTopLevel / esempi / ring / caso3.1bis.cic

diff --git a/helm/gTopLevel/esempi/ring/caso3.1bis.cic b/helm/gTopLevel/esempi/ring/caso3.1bis.cic
new file mode 100644 (file)
index 0000000..ec85c07
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/caso3.1bis.cic
@@ -0,0 +1,25 @@
+(* ok *)
+alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R             /Coq/Reals/Rdefinitions/R.con
+alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
+alias R1            /Coq/Reals/Rdefinitions/R1.con
+alias R0            /Coq/Reals/Rdefinitions/R0.con
+alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
+alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
+alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
+alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
+alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
+alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
+alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
+alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
+alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
+alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
+alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
+alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
+alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
+alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3
+(eqT R
+  (Rplus R1 R1)
+  (Rmult R1 R1))