X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fesempi%2Fdecompose.cic;h=1a06fcba380e7e0be9ccdc4914a766bdfa42fac3;hb=e974eb6799c994efdee15aa47a34909360dc0aec;hp=f03d410a3242197acf54b2793789fc41d0d3e4c3;hpb=7bf5d654c18fee290e7e402800543fe40223c04b;p=helm.git

diff --git a/helm/gTopLevel/esempi/decompose.cic b/helm/gTopLevel/esempi/decompose.cic
index f03d410a3..1a06fcba3 100644
--- a/helm/gTopLevel/esempi/decompose.cic
+++ b/helm/gTopLevel/esempi/decompose.cic
@@ -1,5 +1,8 @@
-!A:Prop.!B:Prop.!C:Prop.(and (or A C) (and (or A B) (or B C))) -> True
+!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