]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_TPTP/CASC_2008/GRP200-1.ma
a wrong conjecture bypassed!
[helm.git] / matita / matita / contribs / ng_TPTP / CASC_2008 / GRP200-1.ma
1 include "logic/equality.ma".
2
3 (* Inclusion of: GRP200-1.p *)
4
5 (* -------------------------------------------------------------------------- *)
6
7 (*  File     : GRP200-1 : TPTP v3.7.0. Released v2.2.0. *)
8
9 (*  Domain   : Group Theory (Loops) *)
10
11 (*  Problem  : In Loops, Moufang-1 => Moufang-2. *)
12
13 (*  Version  : [MP96] (equality) axioms. *)
14
15 (*  English  :  *)
16
17 (*  Refs     : [McC98] McCune (1998), Email to G. Sutcliffe *)
18
19 (*           : [Wos96] Wos (1996), OTTER and the Moufang Identity Problem *)
20
21 (*           : [MP96]  McCune & Padmanabhan (1996), Automated Deduction in Eq *)
22
23 (*  Source   : [McC98] *)
24
25 (*  Names    : MFL-1 [MP96] *)
26
27 (*           : - [Wos96] *)
28
29 (*  Status   : Unsatisfiable *)
30
31 (*  Rating   : 0.22 v3.4.0, 0.25 v3.3.0, 0.29 v3.1.0, 0.33 v2.7.0, 0.27 v2.6.0, 0.00 v2.2.1 *)
32
33 (*  Syntax   : Number of clauses     :   10 (   0 non-Horn;  10 unit;   1 RR) *)
34
35 (*             Number of atoms       :   10 (  10 equality) *)
36
37 (*             Maximal clause size   :    1 (   1 average) *)
38
39 (*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
40
41 (*             Number of functors    :    9 (   4 constant; 0-2 arity) *)
42
43 (*             Number of variables   :   15 (   0 singleton) *)
44
45 (*             Maximal term depth    :    4 (   2 average) *)
46
47 (*  Comments : *)
48
49 (* -------------------------------------------------------------------------- *)
50
51 (* ----Loop axioms: *)
52
53 (* ----Moufang-1: *)
54
55 (* ----Denial of Moufang-2: *)
56 ntheorem prove_moufang2:
57  (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
58 ∀a:Univ.
59 ∀b:Univ.
60 ∀c:Univ.
61 ∀identity:Univ.
62 ∀left_division:∀_:Univ.∀_:Univ.Univ.
63 ∀left_inverse:∀_:Univ.Univ.
64 ∀multiply:∀_:Univ.∀_:Univ.Univ.
65 ∀right_division:∀_:Univ.∀_:Univ.Univ.
66 ∀right_inverse:∀_:Univ.Univ.
67 ∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X (multiply Y Z)) X) (multiply (multiply X Y) (multiply Z X)).
68 ∀H1:∀X:Univ.eq Univ (multiply (left_inverse X) X) identity.
69 ∀H2:∀X:Univ.eq Univ (multiply X (right_inverse X)) identity.
70 ∀H3:∀X:Univ.∀Y:Univ.eq Univ (right_division (multiply X Y) Y) X.
71 ∀H4:∀X:Univ.∀Y:Univ.eq Univ (multiply (right_division X Y) Y) X.
72 ∀H5:∀X:Univ.∀Y:Univ.eq Univ (left_division X (multiply X Y)) Y.
73 ∀H6:∀X:Univ.∀Y:Univ.eq Univ (multiply X (left_division X Y)) Y.
74 ∀H7:∀X:Univ.eq Univ (multiply X identity) X.
75 ∀H8:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (multiply (multiply (multiply a b) c) b) (multiply a (multiply b (multiply c b))))
76 .
77 #Univ ##.
78 #X ##.
79 #Y ##.
80 #Z ##.
81 #a ##.
82 #b ##.
83 #c ##.
84 #identity ##.
85 #left_division ##.
86 #left_inverse ##.
87 #multiply ##.
88 #right_division ##.
89 #right_inverse ##.
90 #H0 ##.
91 #H1 ##.
92 #H2 ##.
93 #H3 ##.
94 #H4 ##.
95 #H5 ##.
96 #H6 ##.
97 #H7 ##.
98 #H8 ##.
99 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8 ##;
100 ntry (nassumption) ##;
101 nqed.
102
103 (* -------------------------------------------------------------------------- *)