1 include "logic/equality.ma".
3 (* Inclusion of: COL053-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : COL053-1 : TPTP v3.2.0. Released v1.0.0. *)
9 (* Domain : Combinatory Logic *)
11 (* Problem : An Exercise in Composition *)
13 (* Version : Especial. *)
15 (* English : For all birds x and y, there exists a bird z that composes *)
17 (* x with y for all birds w. Prove that for all birds x, y, and *)
19 (* z, there exists a bird u such that for all w, uw = x(y(zw)). *)
21 (* Refs : [Smu85] Smullyan (1978), To Mock a Mocking Bird and Other Logi *)
25 (* Names : bird5.ver1.in [ANL] *)
27 (* Status : Unsatisfiable *)
29 (* Rating : 0.00 v2.0.0 *)
31 (* Syntax : Number of clauses : 2 ( 0 non-Horn; 2 unit; 1 RR) *)
33 (* Number of atoms : 2 ( 2 equality) *)
35 (* Maximal clause size : 1 ( 1 average) *)
37 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
39 (* Number of functors : 6 ( 3 constant; 0-2 arity) *)
41 (* Number of variables : 4 ( 0 singleton) *)
43 (* Maximal term depth : 5 ( 4 average) *)
47 (* -------------------------------------------------------------------------- *)
49 (* ----For all birds x and y, there exists a bird z that composes x with *)
51 (* ----y for all birds w. *)
53 (* ---- FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))]. *)
55 (* ---- response(comp(x,y),w) = response(x,response(y,w)). *)
57 (* ----Hypothesis: For all birds x, y, and z, there exists a bird u such *)
59 (* ----that for all w, uw = x(y(zw)). *)
61 (* ----Finding clause (using xy to replace response(x,y)): *)
63 (* ---- - (FAx FAy FAz TEu FAw (uw = x(y(zw)))). *)
65 (* ---- TEx TEy TEz FAu TEw -(uw = x(y(zw))). *)
67 (* ---- Letting w = f(u), x = A, y = B, and z = C, *)
69 (* ---- -[(u)f(u) = A(B((C)f(u)))]. *)
70 ntheorem prove_bird_exists:
71 ∀Univ:Type.∀U:Univ.∀W:Univ.∀X:Univ.∀Y:Univ.
75 ∀compose:∀_:Univ.∀_:Univ.Univ.
77 ∀response:∀_:Univ.∀_:Univ.Univ.
78 ∀H0:∀W:Univ.∀X:Univ.∀Y:Univ.eq Univ (response (compose X Y) W) (response X (response Y W)).∃U:Univ.eq Univ (response U (f U)) (response a (response b (response c (f U))))
99 (* -------------------------------------------------------------------------- *)