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

   1 set "baseuri" "cic:/matita/TPTP/SWV251-2".
   2 include "logic/equality.ma".
   3
   4 (* Inclusion of: SWV251-2.p *)
   5
   6 (* ------------------------------------------------------------------------------ *)
   7
   8 (*  File     : SWV251-2 : TPTP v3.2.0. Released v3.2.0. *)
   9
  10 (*  Domain   : Software Verification *)
  11
  12 (*  Problem  : Cryptographic protocol problem for messages *)
  13
  14 (*  Version  : [Pau06] axioms : Reduced > Especial. *)
  15
  16 (*  English  : *)
  17
  18 (*  Refs     : [Pau06] Paulson (2006), Email to G. Sutcliffe *)
  19
  20 (*  Source   : [Pau06] *)
  21
  22 (*  Names    :  *)
  23
  24 (*  Status   : Unsatisfiable *)
  25
  26 (*  Rating   : 0.43 v3.2.0 *)
  27
  28 (*  Syntax   : Number of clauses     :   13 (   0 non-Horn;   6 unit;   9 RR) *)
  29
  30 (*             Number of atoms       :   23 (   4 equality) *)
  31
  32 (*             Maximal clause size   :    3 (   2 average) *)
  33
  34 (*             Number of predicates  :    3 (   0 propositional; 2-3 arity) *)
  35
  36 (*             Number of functors    :   11 (   5 constant; 0-3 arity) *)
  37
  38 (*             Number of variables   :   60 (  47 singleton) *)
  39
  40 (*             Maximal term depth    :    5 (   2 average) *)
  41
  42 (*  Comments : The problems in the [Pau06] collection each have very many axioms, *)
  43
  44 (*             of which only a small selection are required for the refutation. *)
  45
  46 (*             The mission is to find those few axioms, after which a refutation *)
  47
  48 (*             can be quite easily found. This version has only the necessary *)
  49
  50 (*             axioms. *)
  51
  52 (* ------------------------------------------------------------------------------ *)
  53 theorem cls_conjecture_2:
  54  ∀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
  55 .
  56 intros.
  57 autobatch depth=5 width=5 size=20 timeout=10;
  58 try assumption.
  59 print proofterm.
  60 qed.
  61
  62 (* ------------------------------------------------------------------------------ *)