X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fautomath%2FOmega.aut;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fautomath%2FOmega.aut;h=2466a606e0bde14fb594e8f2d1130c646e04ac89;hb=ab13cfa248f0ee58d239ceeddfb50ec49a6b5c6d;hp=0000000000000000000000000000000000000000;hpb=514017fb6545009bdc62dcaf294f4317beb251b2;p=helm.git

diff --git a/helm/software/lambda-delta/src/automath/Omega.aut b/helm/software/lambda-delta/src/automath/Omega.aut
new file mode 100644
index 000000000..2466a606e
--- /dev/null
+++ b/helm/software/lambda-delta/src/automath/Omega.aut
@@ -0,0 +1,10 @@
+# The lambda-term \Omega
+# This book is not accepted in AUT-QE because [y:'type'] is not allowed
+# This book is accepted in lambda-delta with sort inclusion but Omega is not
+#    valid if sort inclusion is allowed on the term backbone only
+# This book is valid in lambda-delta with unrestricted sort inclusion 
+
++l 
+@ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
+  Omega := <Delta>Delta             : 'type'
+-l