Experimental: cycles in proofs generated by paramodulation are now detected

[helm.git] / helm / software / matita / contribs / CoRN / algebra / Setoids.ma

diff --git a/helm/software/matita/contribs/CoRN/algebra/Setoids.ma b/helm/software/matita/contribs/CoRN/algebra/Setoids.ma
index 4fcb5a23be061042d8a70235f4dbb6692ced0da5..5fc3725cc31307a560a4d404119a67d5b916cc6d 100644 (file)
--- a/helm/software/matita/contribs/CoRN/algebra/Setoids.ma
+++ b/helm/software/matita/contribs/CoRN/algebra/Setoids.ma
@@ -1227,11 +1227,6 @@ qed.
 
 
 
-axiom proper_caseZ_diff_CS : \forall CS : CSetoid. \forall f : nat \to nat \to CS.
- (\forall m,n,p,q : nat. eq nat (plus m q) (plus n p) \to (f m n) = (f p q)) \to
- \forall m,n : nat. caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = (f m n).
-
-(*
 lemma proper_caseZ_diff_CS : \forall CS : CSetoid. \forall f : nat \to nat \to CS.
  (\forall m,n,p,q : nat. eq nat (plus m q) (plus n p) \to (f m n) = (f p q)) \to
  \forall m,n : nat. caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = (f m n).
@@ -1253,9 +1248,9 @@ apply f. apply n1. apply m1.
 apply eq_symmetric_unfolded.assumption.
 apply eq_symmetric_unfolded.assumption.
 apply H.
-auto.
+auto new timeout=100.
 qed.
-*)
+
 (*
 Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
 *)