matitaB/matita/contribs/TPTP/HEQ/HWV003-1.ma

   1 set "baseuri" "cic:/matita/TPTP/HWV003-1".
   2 include "logic/equality.ma".
   3
   4 (* Inclusion of: HWV003-1.p *)
   5
   6 (* -------------------------------------------------------------------------- *)
   7
   8 (*  File     : HWV003-1 : TPTP v3.2.0. Released v1.1.0. *)
   9
  10 (*  Domain   : Hardware Verification *)
  11
  12 (*  Problem  : One bit Full Adder *)
  13
  14 (*  Version  : [WO+92] axioms. *)
  15
  16 (*  English  :  *)
  17
  18 (*  Refs     : [WO+92] Wos et al. (1992), Automated Reasoning: Introduction a *)
  19
  20 (*  Source   : [WO+92] *)
  21
  22 (*  Names    : - [WO+92] *)
  23
  24 (*  Status   : Unsatisfiable *)
  25
  26 (*  Rating   : 0.29 v3.1.0, 0.67 v2.7.0, 0.50 v2.6.0, 0.86 v2.5.0, 0.80 v2.4.0, 0.83 v2.3.0, 1.00 v2.2.1, 0.89 v2.2.0, 0.86 v2.1.0, 1.00 v2.0.0 *)
  27
  28 (*  Syntax   : Number of clauses     :   47 (   0 non-Horn;  47 unit;  13 RR) *)
  29
  30 (*             Number of atoms       :   47 (  45 equality) *)
  31
  32 (*             Maximal clause size   :    1 (   1 average) *)
  33
  34 (*             Number of predicates  :    2 (   0 propositional; 2-2 arity) *)
  35
  36 (*             Number of functors    :   20 (  14 constant; 0-3 arity) *)
  37
  38 (*             Number of variables   :   69 (  14 singleton) *)
  39
  40 (*             Maximal term depth    :    4 (   2 average) *)
  41
  42 (*  Comments :  *)
  43
  44 (* -------------------------------------------------------------------------- *)
  45
  46 (* ----Include definitions of AND, OR and NOT  *)
  47
  48 (* Inclusion of: Axioms/HWC002-0.ax *)
  49
  50 (* -------------------------------------------------------------------------- *)
  51
  52 (*  File     : HWC002-0 : TPTP v3.2.0. Released v1.0.0. *)
  53
  54 (*  Domain   : Hardware Creation *)
  55
  56 (*  Axioms   : Definitions of AND, OR and NOT *)
  57
  58 (*  Version  : [WO+92] axioms. *)
  59
  60 (*             Axiom formulation : Non-ground axioms. *)
  61
  62 (*  English  :  *)
  63
  64 (*  Refs     : [WO+92] Wos et al. (1992), Automated Reasoning: Introduction a *)
  65
  66 (*  Source   : [ANL] *)
  67
  68 (*  Names    :  *)
  69
  70 (*  Status   :  *)
  71
  72 (*  Syntax   : Number of clauses    :    6 (   0 non-Horn;   6 unit;   2 RR) *)
  73
  74 (*             Number of literals   :    6 (   6 equality) *)
  75
  76 (*             Maximal clause size  :    1 (   1 average) *)
  77
  78 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
  79
  80 (*             Number of functors   :    5 (   2 constant; 0-2 arity) *)
  81
  82 (*             Number of variables  :    4 (   2 singleton) *)
  83
  84 (*             Maximal term depth   :    2 (   2 average) *)
  85
  86 (*  Comments :  *)
  87
  88 (* -------------------------------------------------------------------------- *)
  89
  90 (* -------------------------------------------------------------------------- *)
  91
  92 (* -------------------------------------------------------------------------- *)
  93
  94 (* ----Simplifiers  *)
  95
  96 (* ----Evaluators  *)
  97
  98 (* ----Evaluators of lists of 3 terms  *)
  99
 100 (* ----Simplifiers for products of 4 terms  *)
 101
 102 (* ----Subsumption type demodulators  *)
 103
 104 (* ----Karnaugh map technique  *)
 105
 106 (* ----Karnaugh simplifier of inside product  *)
 107
 108 (* ----Circuit description  *)
 109 theorem prove_circuit:
 110  ∀Univ:Set.∀X:Univ.∀X1:Univ.∀X2:Univ.∀X3:Univ.∀Y:Univ.∀Z:Univ.∀a:Univ.∀a11:Univ.∀a12:Univ.∀a13:Univ.∀a14:Univ.∀a15:Univ.∀a16:Univ.∀a17:Univ.∀myand:∀_:Univ.∀_:Univ.Univ.∀b:Univ.∀c1:Univ.∀carryin:Univ.∀carryout:∀_:Univ.∀_:Univ.∀_:Univ.Univ.∀circuit:∀_:Univ.∀_:Univ.Prop.∀n0:Univ.∀n1:Univ.∀not:∀_:Univ.Univ.∀or:∀_:Univ.∀_:Univ.Univ.∀s1:Univ.∀sum:∀_:Univ.∀_:Univ.∀_:Univ.Univ.∀xor:∀_:Univ.∀_:Univ.Univ.∀H0:circuit s1 c1.∀H1:eq Univ c1 (not (myand a11 a15)).∀H2:eq Univ s1 (not (myand a16 a17)).∀H3:eq Univ a17 (not (myand a15 carryin)).∀H4:eq Univ a16 (not (myand a14 a15)).∀H5:eq Univ a15 (not (myand a14 carryin)).∀H6:eq Univ a14 (not (myand a12 a13)).∀H7:eq Univ a13 (not (myand a11 b)).∀H8:eq Univ a12 (not (myand a11 a)).∀H9:eq Univ a11 (not (myand a b)).∀H10:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (sum X Y Z) (xor (xor X Y) Z).∀H11:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (carryout X Y Z) (or (myand X (or Y Z)) (myand (not X) (myand Y Z))).∀H12:∀X:Univ.∀Y:Univ.eq Univ (xor X Y) (or (myand X (not Y)) (myand Y (not X))).∀H13:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (or (myand (myand X Y) (not Z)) (myand X Z)) (or (myand X Y) (myand X Z)).∀H14:∀X:Univ.∀Y:Univ.eq Univ (or (myand (not X) (not Y)) Y) (or Y (not X)).∀H15:∀X:Univ.∀Y:Univ.eq Univ (or (myand X (not Y)) Y) (or X Y).∀H16:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (or (or X (myand Y Z)) Z) (or X Z).∀H17:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (or (or (myand X Y) Z) Y) (or Z Y).∀H18:∀X:Univ.∀Y:Univ.eq Univ (or (myand X Y) X) X.∀H19:∀X:Univ.∀Y:Univ.eq Univ (or (myand X Y) Y) Y.∀H20:∀X1:Univ.∀X2:Univ.∀X3:Univ.eq Univ (myand (myand (myand X1 X2) X3) (not X2)) n0.∀H21:∀X1:Univ.∀X2:Univ.∀X3:Univ.eq Univ (myand (myand (myand X1 X2) X3) (not X1)) n0.∀H22:∀X:Univ.∀Y:Univ.eq Univ (or (or X Y) Y) (or X Y).∀H23:∀X:Univ.∀Y:Univ.eq Univ (myand (myand X Y) Y) (myand X Y).∀H24:∀X:Univ.∀Y:Univ.eq Univ (or (or X Y) (not X)) n1.∀H25:∀X:Univ.∀Y:Univ.eq Univ (or (or X Y) (not Y)) n1.∀H26:∀X:Univ.∀Y:Univ.eq Univ (myand (myand X Y) (not X)) n0.∀H27:∀X:Univ.∀Y:Univ.eq Univ (myand (myand X Y) (not Y)) n0.∀H28:∀X:Univ.eq Univ (or X X) X.∀H29:∀X:Univ.eq Univ (myand X X) X.∀H30:∀X:Univ.eq Univ (or X (not X)) n1.∀H31:∀X:Univ.eq Univ (myand X (not X)) n0.∀H32:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (or (or X Y) Z) (or (or X Z) Y).∀H33:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (myand (myand X Y) Z) (myand (myand X Z) Y).∀H34:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (myand (or X Y) Z) (or (myand X Z) (myand Y Z)).∀H35:∀X:Univ.∀Y:Univ.eq Univ (or X Y) (or Y X).∀H36:∀X:Univ.∀Y:Univ.eq Univ (myand X Y) (myand Y X).∀H37:∀X:Univ.eq Univ (not (not X)) X.∀H38:∀X:Univ.∀Y:Univ.eq Univ (not (or X Y)) (myand (not X) (not Y)).∀H39:∀X:Univ.∀Y:Univ.eq Univ (not (myand X Y)) (or (not X) (not Y)).∀H40:eq Univ (not n1) n0.∀H41:eq Univ (not n0) n1.∀H42:∀X:Univ.eq Univ (or X n1) n1.∀H43:∀X:Univ.eq Univ (or X n0) X.∀H44:∀X:Univ.eq Univ (myand X n1) X.∀H45:∀X:Univ.eq Univ (myand X n0) n0.circuit (sum a b carryin) (carryout a b carryin)
 111 .
 112 intros.
 113 autobatch depth=5 width=5 size=20 timeout=10;
 114 try assumption.
 115 print proofterm.
 116 qed.
 117
 118 (* -------------------------------------------------------------------------- *)