]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/esempi/decompose.cic
ocaml 3.09 transition
[helm.git] / helm / gTopLevel / esempi / decompose.cic
1 !A:Prop.!B:Prop.!C:Prop.(and (sumbool A False) (and (or True B) (or B False))) -> True
2
3 !A:Prop.!B:Prop.!C:Prop.(and (sumbool A C) (and (or A B) !D:Prop.(or B D))) -> True
4
5 !A:Prop.!B:Prop.!C:Prop.(and (and A C) (and (and A B) (and B C))) -> True
6
7 (and True True) -> True
8 (and True False) -> True