helm/software/matita/contribs/TPTP/HEQ/HWV002-1.ma

   1 set "baseuri" "cic:/matita/TPTP/HWV002-1".
   2 include "logic/equality.ma".
   3
   4 (* Inclusion of: HWV002-1.p *)
   5
   6 (* -------------------------------------------------------------------------- *)
   7
   8 (*  File     : HWV002-1 : TPTP v3.2.0. Released v1.1.0. *)
   9
  10 (*  Domain   : Hardware Verification *)
  11
  12 (*  Problem  : Invert 3 inputs with 2 not gates *)
  13
  14 (*  Version  : [ANL] axioms : Reduced > Complete. *)
  15
  16 (*  English  : This is made to validate the circuit that inverts 3 inputs  *)
  17
  18 (*             using as many AND and OR gates as you like, but using only  *)
  19
  20 (*             two NOT gates. *)
  21
  22 (*  Refs     : [WO+92] Wos et al. (1992), Automated Reasoning: Introduction a *)
  23
  24 (*  Source   : [ANL] *)
  25
  26 (*  Names    : two.inverter.val.ver1.in [ANL] *)
  27
  28 (*  Status   : Unsatisfiable *)
  29
  30 (*  Rating   : 0.43 v3.1.0, 0.56 v2.7.0, 0.67 v2.6.0, 0.57 v2.5.0, 0.40 v2.4.0, 0.67 v2.2.1, 1.00 v2.0.0 *)
  31
  32 (*  Syntax   : Number of clauses     :   51 (   0 non-Horn;  50 unit;  34 RR) *)
  33
  34 (*             Number of atoms       :   53 (  47 equality) *)
  35
  36 (*             Maximal clause size   :    3 (   1 average) *)
  37
  38 (*             Number of predicates  :    2 (   0 propositional; 1-2 arity) *)
  39
  40 (*             Number of functors    :   39 (  35 constant; 0-2 arity) *)
  41
  42 (*             Number of variables   :   28 (   2 singleton) *)
  43
  44 (*             Maximal term depth    :    3 (   2 average) *)
  45
  46 (*  Comments : Some duplicate clauses have been removed from the [ANL] version. *)
  47
  48 (* -------------------------------------------------------------------------- *)
  49
  50 (* ----Canonicalizing an exclusive-or/and expression  *)
  51
  52 (* ----Associativity and symmetry  *)
  53
  54 (* ----Problem clauses  *)
  55 theorem prove_inversion:
  56  ∀Univ:Set.∀X:Univ.∀Y:Univ.∀Z:Univ.∀a1:Univ.∀myand:∀_:Univ.∀_:Univ.Univ.∀circuit:∀_:Univ.Prop.∀i1:Univ.∀i2:Univ.∀i3:Univ.∀inv1:Univ.∀inv2:Univ.∀n0:Univ.∀n1:Univ.∀n10:Univ.∀n11:Univ.∀n12:Univ.∀n13:Univ.∀n14:Univ.∀n15:Univ.∀n16:Univ.∀n17:Univ.∀n18:Univ.∀n19:Univ.∀n2:Univ.∀n20:Univ.∀n21:Univ.∀n22:Univ.∀n23:Univ.∀n24:Univ.∀n25:Univ.∀n3:Univ.∀n4:Univ.∀n5:Univ.∀n6:Univ.∀n7:Univ.∀n8:Univ.∀n9:Univ.∀not:∀_:Univ.Univ.∀o1:Univ.∀o2:Univ.∀o3:Univ.∀or:∀_:Univ.∀_:Univ.Univ.∀xor:∀_:Univ.∀_:Univ.Univ.∀H0:circuit o3.∀H1:circuit o2.∀H2:circuit o1.∀H3:eq Univ inv2 (not n9).∀H4:eq Univ inv1 (not n20).∀H5:eq Univ n25 (or n2 n24).∀H6:eq Univ n24 (myand i1 inv1).∀H7:eq Univ n23 (myand i1 i3).∀H8:eq Univ n22 (or n23 n6).∀H9:eq Univ n21 (myand inv1 inv2).∀H10:eq Univ n20 (or n22 n14).∀H11:eq Univ n19 (myand n23 inv2).∀H12:eq Univ n18 (or n19 n25).∀H13:eq Univ n17 (or n18 n21).∀H14:eq Univ n16 (myand n14 inv2).∀H15:eq Univ n15 (myand inv2 n6).∀H16:eq Univ n14 (myand i2 i3).∀H17:eq Univ n13 (or n12 n21).∀H18:eq Univ n12 (or n11 n16).∀H19:eq Univ n11 (or a1 n2).∀H20:eq Univ n10 (or n24 n7).∀H21:eq Univ n9 (or n8 n2).∀H22:eq Univ n8 (or a1 n10).∀H23:eq Univ n7 (myand n6 i3).∀H24:eq Univ n6 (myand i1 i2).∀H25:eq Univ n5 (or n4 n21).∀H26:eq Univ n4 (or n15 n3).∀H27:eq Univ n3 (or a1 n24).∀H28:eq Univ n2 (myand inv1 i3).∀H29:eq Univ a1 (myand inv1 i2).∀H30:eq Univ o3 n5.∀H31:eq Univ o2 n17.∀H32:eq Univ o1 n13.∀H33:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (myand Y (myand X Z)) (myand X (myand Y Z)).∀H34:∀X:Univ.∀Y:Univ.eq Univ (myand X Y) (myand Y X).∀H35:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (xor Y (xor X Z)) (xor X (xor Y Z)).∀H36:∀X:Univ.∀Y:Univ.eq Univ (xor X Y) (xor Y X).∀H37:∀X:Univ.∀Y:Univ.eq Univ (or X Y) (xor (myand X Y) (xor X Y)).∀H38:∀X:Univ.eq Univ (not X) (xor n1 X).∀H39:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (myand X (xor Y Z)) (xor (myand X Y) (myand X Z)).∀H40:∀X:Univ.∀Y:Univ.eq Univ (myand X (myand X Y)) (myand X Y).∀H41:∀X:Univ.eq Univ (myand X X) X.∀H42:∀X:Univ.eq Univ (myand X n1) X.∀H43:∀X:Univ.eq Univ (myand n1 X) X.∀H44:∀X:Univ.eq Univ (myand X n0) n0.∀H45:∀X:Univ.eq Univ (myand n0 X) n0.∀H46:∀X:Univ.∀Y:Univ.eq Univ (xor X (xor X Y)) Y.∀H47:∀X:Univ.eq Univ (xor X X) n0.∀H48:∀X:Univ.eq Univ (xor X n0) X.∀H49:∀X:Univ.eq Univ (xor n0 X) X.∀_:circuit (not i3).∀_:circuit (not i2).circuit (not i1)
  57 .
  58 intros.
  59 autobatch depth=5 width=5 size=20 timeout=10;
  60 try assumption.
  61 print proofterm.
  62 qed.
  63
  64 (* -------------------------------------------------------------------------- *)