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

   1 set "baseuri" "cic:/matita/TPTP/NUM017-2".
   2 include "logic/equality.ma".
   3
   4 (* Inclusion of: NUM017-2.p *)
   5
   6 (* -------------------------------------------------------------------------- *)
   7
   8 (*  File     : NUM017-2 : TPTP v3.2.0. Bugfixed v1.2.1. *)
   9
  10 (*  Domain   : Number Theory *)
  11
  12 (*  Problem  : Square root of this prime is irrational *)
  13
  14 (*  Version  : [Rob63] axioms : Incomplete > Augmented > Complete. *)
  15
  16 (*  English  : If a is prime, and a is not b^2/c^2, then the square root  *)
  17
  18 (*             of a is irrational. *)
  19
  20 (*  Refs     : [Rob63] Robinson (1963), Theorem Proving on the Computer *)
  21
  22 (*  Source   : [TPTP] *)
  23
  24 (*  Names    :  *)
  25
  26 (*  Status   : Unsatisfiable *)
  27
  28 (*  Rating   : 0.00 v3.1.0, 0.22 v2.7.0, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.2.1, 0.38 v2.2.0, 0.50 v2.1.0, 0.33 v2.0.0 *)
  29
  30 (*  Syntax   : Number of clauses     :   15 (   0 non-Horn;   5 unit;  14 RR) *)
  31
  32 (*             Number of atoms       :   34 (   2 equality) *)
  33
  34 (*             Maximal clause size   :    4 (   2 average) *)
  35
  36 (*             Number of predicates  :    4 (   0 propositional; 1-3 arity) *)
  37
  38 (*             Number of functors    :    7 (   5 constant; 0-2 arity) *)
  39
  40 (*             Number of variables   :   37 (   1 singleton) *)
  41
  42 (*             Maximal term depth    :    2 (   1 average) *)
  43
  44 (*  Comments :  *)
  45
  46 (*  Bugfixes : v1.2.1 - Clause primes_lemma1 fixed. *)
  47
  48 (* -------------------------------------------------------------------------- *)
  49 theorem prove_there_is_no_common_divisor:
  50  ∀Univ:Set.∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀a:Univ.∀b:Univ.∀c:Univ.∀d:Univ.∀divides:∀_:Univ.∀_:Univ.Prop.∀e:Univ.∀multiply:∀_:Univ.∀_:Univ.Univ.∀prime:∀_:Univ.Prop.∀product:∀_:Univ.∀_:Univ.∀_:Univ.Prop.∀second_divided_by_1st:∀_:Univ.∀_:Univ.Univ.∀H0:product a e d.∀H1:product c c e.∀H2:product b b d.∀H3:prime a.∀H4:∀A:Univ.∀B:Univ.∀C:Univ.∀_:prime A.∀_:product C C B.∀_:divides A B.divides A C.∀H5:∀A:Univ.∀B:Univ.∀C:Univ.∀_:product A B C.divides A C.∀H6:∀A:Univ.∀B:Univ.∀_:divides A B.product A (second_divided_by_1st A B) B.∀H7:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀_:product A B D.∀_:product A B C.eq Univ D C.∀H8:∀A:Univ.∀B:Univ.∀C:Univ.∀_:divides C A.∀_:divides A B.divides C B.∀H9:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀_:product A D C.∀_:product A B C.eq Univ B D.∀H10:∀A:Univ.∀B:Univ.∀C:Univ.∀_:product A B C.product B A C.∀H11:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀_:product F D A.∀_:product D B E.∀_:product A B C.product F E C.∀H12:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀_:product A D F.∀_:product D E B.∀_:product A B C.product F E C.∀H13:∀A:Univ.∀B:Univ.product A B (multiply A B).∃A:Univ.And (divides A b) (divides A c)
  51 .
  52 intros.
  53 exists[
  54 2:
  55 autobatch depth=5 width=5 size=20 timeout=10;
  56 try assumption.
  57 |
  58 skip]
  59 print proofterm.
  60 qed.
  61
  62 (* -------------------------------------------------------------------------- *)