1 files changed, 29 insertions, 0 deletions
diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio-normalizado.acl2 b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio-normalizado.acl2
new file mode 100644
index 0000000..d70e8aa
--- /dev/null
+++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio-normalizado.acl2
@@ -0,0 +1,29 @@
+(in-package "ACL2")
+
+(defconst *import-symbols*
+  (set-difference-eq
+   (union-eq *acl2-exports*
+	     *common-lisp-symbols-from-main-lisp-package*)
+     '(null + * - < = / commutativity-of-* associativity-of-* 
+	    commutativity-of-+ associativity-of-+ distributivity)))
+
+(defpkg "FLD"
+  *import-symbols*)
+
+(defpkg "FUTER"
+  *import-symbols*)
+
+(defpkg "FUMON"
+  (union-eq *import-symbols*
+	    '(FLD::fdp FUTER::terminop)))
+
+(defpkg "FUPOL"
+  (union-eq *import-symbols*
+	    '(FUTER::naturalp FUTER::terminop FUMON::monomio FUMON::coeficiente
+			    FUMON::termino FUMON::monomiop)))
+
+(defpkg "FUNPOL"
+  (set-difference-eq *import-symbols*
+		     '(rem)))
+
+(certify-book "fupolinomio-normalizado" ? t)