regenerated

[helm.git] / helm / software / matita / contribs / TPTP / HEQ / ANA032-2.ma

diff --git a/helm/software/matita/contribs/TPTP/HEQ/ANA032-2.ma b/helm/software/matita/contribs/TPTP/HEQ/ANA032-2.ma
index 4a0a754746caed7ad04506fe91aa6827d12d3bd0..b041269eb977ac969a410f267e651e8073f7f6a3 100644 (file)
--- a/helm/software/matita/contribs/TPTP/HEQ/ANA032-2.ma
+++ b/helm/software/matita/contribs/TPTP/HEQ/ANA032-2.ma
@@ -51,7 +51,7 @@ include "logic/equality.ma".
 
 (* ------------------------------------------------------------------------------ *)
 theorem cls_conjecture_1:
- ∀Univ:Set.∀T_a:Univ.∀V_a:Univ.∀V_b:Univ.∀V_c:Univ.∀c_0:Univ.∀c_HOL_Oabs:∀_:Univ.∀_:Univ.Univ.∀c_lessequals:∀_:Univ.∀_:Univ.∀_:Univ.Prop.∀c_times:∀_:Univ.∀_:Univ.∀_:Univ.Univ.∀class_OrderedGroup_Oab__semigroup__mult:∀_:Univ.Prop.∀class_OrderedGroup_Olordered__ab__group__abs:∀_:Univ.Prop.∀class_OrderedGroup_Osemigroup__mult:∀_:Univ.Prop.∀class_Ring__and__Field_Opordered__semiring:∀_:Univ.Prop.∀t_b:Univ.∀v_b:∀_:Univ.Univ.∀v_c:Univ.∀v_f:∀_:Univ.Univ.∀v_g:∀_:Univ.Univ.∀v_x:Univ.∀H0:c_lessequals (c_HOL_Oabs (v_b v_x) t_b) (c_times v_c (c_HOL_Oabs (v_g v_x) t_b) t_b) t_b.∀H1:∀T_a:Univ.∀V_a:Univ.∀V_b:Univ.∀V_c:Univ.∀_:class_Ring__and__Field_Opordered__semiring T_a.∀_:c_lessequals V_a V_b T_a.∀_:c_lessequals c_0 V_c T_a.c_lessequals (c_times V_c V_a T_a) (c_times V_c V_b T_a) T_a.∀H2:∀T_a:Univ.∀V_a:Univ.∀V_b:Univ.∀_:class_OrderedGroup_Oab__semigroup__mult T_a.eq Univ (c_times V_a V_b T_a) (c_times V_b V_a T_a).∀H3:∀T_a:Univ.∀V_a:Univ.∀V_b:Univ.∀V_c:Univ.∀_:class_OrderedGroup_Osemigroup__mult T_a.eq Univ (c_times (c_times V_a V_b T_a) V_c T_a) (c_times V_a (c_times V_b V_c T_a) T_a).∀H4:∀T_a:Univ.∀V_a:Univ.∀_:class_OrderedGroup_Olordered__ab__group__abs T_a.c_lessequals c_0 (c_HOL_Oabs V_a T_a) T_a.c_lessequals (c_times (c_HOL_Oabs (v_b v_x) t_b) (c_HOL_Oabs (v_f v_x) t_b) t_b) (c_times v_c (c_times (c_HOL_Oabs (v_f v_x) t_b) (c_HOL_Oabs (v_g v_x) t_b) t_b) t_b) t_b
+ ∀Univ:Set.∀T_a:Univ.∀V_a:Univ.∀V_b:Univ.∀V_c:Univ.∀c_0:Univ.∀c_HOL_Oabs:∀_:Univ.∀_:Univ.Univ.∀c_lessequals:∀_:Univ.∀_:Univ.∀_:Univ.Prop.∀c_times:∀_:Univ.∀_:Univ.∀_:Univ.Univ.∀class_OrderedGroup_Oab__semigroup__mult:∀_:Univ.Prop.∀class_OrderedGroup_Olordered__ab__group__abs:∀_:Univ.Prop.∀class_OrderedGroup_Osemigroup__mult:∀_:Univ.Prop.∀class_Ring__and__Field_Opordered__semiring:∀_:Univ.Prop.∀t_b:Univ.∀v_b:∀_:Univ.Univ.∀v_c:Univ.∀v_f:∀_:Univ.Univ.∀v_g:∀_:Univ.Univ.∀v_x:Univ.∀H0:c_lessequals (c_HOL_Oabs (v_b v_x) t_b) (c_times v_c (c_HOL_Oabs (v_g v_x) t_b) t_b) t_b.∀H1:∀T_a:Univ.∀V_a:Univ.∀V_b:Univ.∀V_c:Univ.∀_:c_lessequals c_0 V_c T_a.∀_:c_lessequals V_a V_b T_a.∀_:class_Ring__and__Field_Opordered__semiring T_a.c_lessequals (c_times V_c V_a T_a) (c_times V_c V_b T_a) T_a.∀H2:∀T_a:Univ.∀V_a:Univ.∀V_b:Univ.∀_:class_OrderedGroup_Oab__semigroup__mult T_a.eq Univ (c_times V_a V_b T_a) (c_times V_b V_a T_a).∀H3:∀T_a:Univ.∀V_a:Univ.∀V_b:Univ.∀V_c:Univ.∀_:class_OrderedGroup_Osemigroup__mult T_a.eq Univ (c_times (c_times V_a V_b T_a) V_c T_a) (c_times V_a (c_times V_b V_c T_a) T_a).∀H4:∀T_a:Univ.∀V_a:Univ.∀_:class_OrderedGroup_Olordered__ab__group__abs T_a.c_lessequals c_0 (c_HOL_Oabs V_a T_a) T_a.c_lessequals (c_times (c_HOL_Oabs (v_b v_x) t_b) (c_HOL_Oabs (v_f v_x) t_b) t_b) (c_times v_c (c_times (c_HOL_Oabs (v_f v_x) t_b) (c_HOL_Oabs (v_g v_x) t_b) t_b) t_b) t_b
 .
 intros.
 autobatch depth=5 width=5 size=20 timeout=10;