]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/esempi/decompose.cic
This commit was manufactured by cvs2svn to create branch 'moogle'.
[helm.git] / helm / gTopLevel / esempi / decompose.cic
diff --git a/helm/gTopLevel/esempi/decompose.cic b/helm/gTopLevel/esempi/decompose.cic
deleted file mode 100644 (file)
index 1a06fcb..0000000
+++ /dev/null
@@ -1,8 +0,0 @@
-!A:Prop.!B:Prop.!C:Prop.(and (sumbool A False) (and (or True B) (or B False))) -> True
-
-!A:Prop.!B:Prop.!C:Prop.(and (sumbool A C) (and (or A B) !D:Prop.(or B D))) -> True
-
-!A:Prop.!B:Prop.!C:Prop.(and (and A C) (and (and A B) (and B C))) -> True
-
-(and True True) -> True
-(and True False) -> True