]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/ng_TPTP/COL056-1.ma
New management of justifications.
[helm.git] / matitaB / matita / contribs / ng_TPTP / COL056-1.ma
1 include "logic/equality.ma".
2
3 (* Inclusion of: COL056-1.p *)
4
5 (* -------------------------------------------------------------------------- *)
6
7 (*  File     : COL056-1 : TPTP v3.7.0. Released v1.0.0. *)
8
9 (*  Domain   : Combinatory Logic *)
10
11 (*  Problem  : Normal Birds *)
12
13 (*  Version  : Especial. *)
14
15 (*  English  : For all birds x and y, there exists a bird z that composes  *)
16
17 (*             x with y for all birds w. Prove that if there exists a happy  *)
18
19 (*             bird then there exists a normal bird. *)
20
21 (*  Refs     : [Smu85] Smullyan (1978), To Mock a Mocking Bird and Other Logi *)
22
23 (*  Source   : [ANL] *)
24
25 (*  Names    : bird8.ver1.in [ANL] *)
26
27 (*  Status   : Unsatisfiable *)
28
29 (*  Rating   : 0.11 v3.4.0, 0.12 v3.3.0, 0.07 v3.1.0, 0.00 v2.7.0, 0.09 v2.6.0, 0.17 v2.5.0, 0.00 v2.0.0 *)
30
31 (*  Syntax   : Number of clauses     :    4 (   0 non-Horn;   4 unit;   3 RR) *)
32
33 (*             Number of atoms       :    4 (   4 equality) *)
34
35 (*             Maximal clause size   :    1 (   1 average) *)
36
37 (*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
38
39 (*             Number of functors    :    5 (   3 constant; 0-2 arity) *)
40
41 (*             Number of variables   :    5 (   1 singleton) *)
42
43 (*             Maximal term depth    :    3 (   2 average) *)
44
45 (*  Comments :  *)
46
47 (* -------------------------------------------------------------------------- *)
48
49 (* ----For all birds x and y, there exists a bird z that composes x with  *)
50
51 (* ----y for all birds w. *)
52
53 (* ----   FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))]. *)
54
55 (* ----   response(comp(x,y),w) = response(x,response(y,w)).  *)
56
57 (* ----Hypothesis: If there exists a happy bird then there exists a normal  *)
58
59 (* ----bird. *)
60
61 (* ----Finding clause (using xy to replace response(x,y)): *)
62
63 (* ----   -[ If TEx TEy TEz (xy = z) and (xz = y) *)
64
65 (* ----      then TEw TEv (wv = v) ]. *)
66
67 (* ----   -[ FAx FAy FAz -((xy = z) and (xz = y)) | TEw TEv (wv = v) ] *)
68
69 (* ----   TEx TEy TEz [(xy = z) and (xz = y)] and FAw FAv -(wv = v). *)
70
71 (* ----   (AB = C) and (AC = B) and -(wv = v). *)
72 ntheorem prove_there_exists_a_happy_bird:
73  (∀Univ:Type.∀V:Univ.∀W:Univ.∀X:Univ.∀Y:Univ.
74 ∀a:Univ.
75 ∀b:Univ.
76 ∀c:Univ.
77 ∀compose:∀_:Univ.∀_:Univ.Univ.
78 ∀response:∀_:Univ.∀_:Univ.Univ.
79 ∀H0:eq Univ (response a c) b.
80 ∀H1:eq Univ (response a b) c.
81 ∀H2:∀W:Univ.∀X:Univ.∀Y:Univ.eq Univ (response (compose X Y) W) (response X (response Y W)).∃V:Univ.∃W:Univ.eq Univ (response W V) V)
82 .
83 #Univ ##.
84 #V ##.
85 #W ##.
86 #X ##.
87 #Y ##.
88 #a ##.
89 #b ##.
90 #c ##.
91 #compose ##.
92 #response ##.
93 #H0 ##.
94 #H1 ##.
95 #H2 ##.
96 napply (ex_intro ? ? ? ?) ##[
97 ##2:
98 napply (ex_intro ? ? ? ?) ##[
99 ##2:
100 nauto by H0,H1,H2 ##;
101 ##| ##skip ##]
102 ##| ##skip ##]
103 ntry (nassumption) ##;
104 nqed.
105
106 (* -------------------------------------------------------------------------- *)