regenerated

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

diff --git a/helm/software/matita/contribs/TPTP/HEQ/SWV251-2.ma b/helm/software/matita/contribs/TPTP/HEQ/SWV251-2.ma
index ec68d0dc70ad55eb761620563d4f3035c4fde05d..99d6fe4aad99147f7d369ed23908b124a13b94a7 100644 (file)
--- a/helm/software/matita/contribs/TPTP/HEQ/SWV251-2.ma
+++ b/helm/software/matita/contribs/TPTP/HEQ/SWV251-2.ma
@@ -51,7 +51,7 @@ include "logic/equality.ma".
 
 (* ------------------------------------------------------------------------------ *)
 theorem cls_conjecture_2:
- ∀Univ:Set.∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀V_C:Univ.∀V_G:Univ.∀V_H:Univ.∀V_c:Univ.∀V_x:Univ.∀c_Message_Oanalz:∀_:Univ.Univ.∀c_Message_Osynth:∀_:Univ.Univ.∀c_in:∀_:Univ.∀_:Univ.∀_:Univ.Prop.∀c_insert:∀_:Univ.∀_:Univ.∀_:Univ.Univ.∀c_lessequals:∀_:Univ.∀_:Univ.∀_:Univ.Prop.∀c_minus:∀_:Univ.∀_:Univ.∀_:Univ.Univ.∀c_union:∀_:Univ.∀_:Univ.∀_:Univ.Univ.∀tc_Message_Omsg:Univ.∀tc_set:∀_:Univ.Univ.∀v_G:Univ.∀v_H:Univ.∀v_X:Univ.∀v_x:Univ.∀H0:c_in v_x (c_Message_Oanalz (c_insert v_X v_H tc_Message_Omsg)) tc_Message_Omsg.∀H1:c_in v_X (c_Message_Osynth (c_Message_Oanalz v_G)) tc_Message_Omsg.∀H2:∀T_a:Univ.∀V_A:Univ.c_lessequals V_A V_A (tc_set T_a).∀H3:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀_:c_lessequals V_B V_A (tc_set T_a).∀_:c_lessequals V_A V_B (tc_set T_a).eq Univ V_A V_B.∀H4:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀V_c:Univ.∀_:c_in V_c V_A T_a.∀_:c_lessequals V_A V_B (tc_set T_a).c_in V_c V_B T_a.∀H5:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀V_x:Univ.∀_:c_in V_x V_B T_a.eq Univ (c_minus (c_insert V_x V_A T_a) V_B (tc_set T_a)) (c_minus V_A V_B (tc_set T_a)).∀H6:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀V_C:Univ.∀_:c_lessequals V_B V_C (tc_set T_a).∀_:c_lessequals V_A V_C (tc_set T_a).c_lessequals (c_union V_A V_B T_a) V_C (tc_set T_a).∀H7:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀V_C:Univ.∀_:c_lessequals (c_union V_A V_B T_a) V_C (tc_set T_a).c_lessequals V_B V_C (tc_set T_a).∀H8:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀V_C:Univ.∀_:c_lessequals (c_union V_A V_B T_a) V_C (tc_set T_a).c_lessequals V_A V_C (tc_set T_a).∀H9:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.eq Univ (c_union V_A (c_minus V_B V_A (tc_set T_a)) T_a) (c_union V_A V_B T_a).∀H10:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.eq Univ (c_union (c_minus V_B V_A (tc_set T_a)) V_A T_a) (c_union V_B V_A T_a).∀H11:∀V_G:Univ.∀V_H:Univ.∀_:c_lessequals V_G V_H (tc_set tc_Message_Omsg).c_lessequals (c_Message_Oanalz V_G) (c_Message_Oanalz V_H) (tc_set tc_Message_Omsg).c_in v_x (c_Message_Oanalz (c_union (c_Message_Osynth (c_Message_Oanalz v_G)) v_H tc_Message_Omsg)) tc_Message_Omsg
+ ∀Univ:Set.∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀V_C:Univ.∀V_G:Univ.∀V_H:Univ.∀V_c:Univ.∀V_x:Univ.∀c_Message_Oanalz:∀_:Univ.Univ.∀c_Message_Osynth:∀_:Univ.Univ.∀c_in:∀_:Univ.∀_:Univ.∀_:Univ.Prop.∀c_insert:∀_:Univ.∀_:Univ.∀_:Univ.Univ.∀c_lessequals:∀_:Univ.∀_:Univ.∀_:Univ.Prop.∀c_minus:∀_:Univ.∀_:Univ.∀_:Univ.Univ.∀c_union:∀_:Univ.∀_:Univ.∀_:Univ.Univ.∀tc_Message_Omsg:Univ.∀tc_set:∀_:Univ.Univ.∀v_G:Univ.∀v_H:Univ.∀v_X:Univ.∀v_x:Univ.∀H0:c_in v_x (c_Message_Oanalz (c_insert v_X v_H tc_Message_Omsg)) tc_Message_Omsg.∀H1:c_in v_X (c_Message_Osynth (c_Message_Oanalz v_G)) tc_Message_Omsg.∀H2:∀T_a:Univ.∀V_A:Univ.c_lessequals V_A V_A (tc_set T_a).∀H3:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀_:c_lessequals V_A V_B (tc_set T_a).∀_:c_lessequals V_B V_A (tc_set T_a).eq Univ V_A V_B.∀H4:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀V_c:Univ.∀_:c_lessequals V_A V_B (tc_set T_a).∀_:c_in V_c V_A T_a.c_in V_c V_B T_a.∀H5:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀V_x:Univ.∀_:c_in V_x V_B T_a.eq Univ (c_minus (c_insert V_x V_A T_a) V_B (tc_set T_a)) (c_minus V_A V_B (tc_set T_a)).∀H6:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀V_C:Univ.∀_:c_lessequals V_A V_C (tc_set T_a).∀_:c_lessequals V_B V_C (tc_set T_a).c_lessequals (c_union V_A V_B T_a) V_C (tc_set T_a).∀H7:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀V_C:Univ.∀_:c_lessequals (c_union V_A V_B T_a) V_C (tc_set T_a).c_lessequals V_B V_C (tc_set T_a).∀H8:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.∀V_C:Univ.∀_:c_lessequals (c_union V_A V_B T_a) V_C (tc_set T_a).c_lessequals V_A V_C (tc_set T_a).∀H9:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.eq Univ (c_union V_A (c_minus V_B V_A (tc_set T_a)) T_a) (c_union V_A V_B T_a).∀H10:∀T_a:Univ.∀V_A:Univ.∀V_B:Univ.eq Univ (c_union (c_minus V_B V_A (tc_set T_a)) V_A T_a) (c_union V_B V_A T_a).∀H11:∀V_G:Univ.∀V_H:Univ.∀_:c_lessequals V_G V_H (tc_set tc_Message_Omsg).c_lessequals (c_Message_Oanalz V_G) (c_Message_Oanalz V_H) (tc_set tc_Message_Omsg).c_in v_x (c_Message_Oanalz (c_union (c_Message_Osynth (c_Message_Oanalz v_G)) v_H tc_Message_Omsg)) tc_Message_Omsg
 .
 intros.
 autobatch depth=5 width=5 size=20 timeout=10;