1 include "logic/equality.ma".
3 (* Inclusion of: COL052-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : COL052-1 : TPTP v3.7.0. Released v1.0.0. *)
9 (* Domain : Combinatory Logic *)
11 (* Problem : A Question on Agreeable Birds *)
13 (* Version : Especial. *)
15 (* Theorem formulation : Implicit definition of agreeable. *)
17 (* English : For all birds x and y, there exists a bird z that composes *)
19 (* x with y for all birds w. Prove that if C is agreeable then *)
23 (* Refs : [Smu85] Smullyan (1978), To Mock a Mocking Bird and Other Logi *)
27 (* Names : bird4.ver1.in [ANL] *)
29 (* Status : Unsatisfiable *)
31 (* Rating : 0.00 v2.0.0 *)
33 (* Syntax : Number of clauses : 4 ( 0 non-Horn; 4 unit; 2 RR) *)
35 (* Number of atoms : 4 ( 4 equality) *)
37 (* Maximal clause size : 1 ( 1 average) *)
39 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
41 (* Number of functors : 7 ( 4 constant; 0-2 arity) *)
43 (* Number of variables : 5 ( 0 singleton) *)
45 (* Maximal term depth : 3 ( 2 average) *)
49 (* -------------------------------------------------------------------------- *)
51 (* ----For all birds x and y, there exists a bird z that composes x with *)
53 (* ----y for all birds w. *)
55 (* ---- FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))]. *)
57 (* ---- response(comp(x,y),w) = response(x,response(y,w)). *)
59 (* ----Hypothesis: If C is agreeable then A is agreeable. *)
61 (* ---- -[ If FAx TEy (response(C,y) = response(x,y)), *)
63 (* ---- then FAw TEv (response(A,v) = response(w,v)) ]. *)
65 (* ---- -[ TEx FAy -(response(C,y) = response(x,y)) | *)
67 (* ---- FAw TEv (response(A,v) = response(w,v)) ]. *)
69 (* ---- FAx TEy (response(C,y) = response(x,y)) and *)
71 (* ---- TEw FAv -(response(A,v) = response(w,v). *)
73 (* ---- response(C,commom_bird(x)) = response(x,common_bird(x)) and *)
75 (* ---- -(response(A,v) = response(odd_bird,v)). *)
76 ntheorem prove_a_is_agreeable:
77 (∀Univ:Type.∀V:Univ.∀W:Univ.∀X:Univ.∀Y:Univ.
80 ∀common_bird:∀_:Univ.Univ.
81 ∀compose:∀_:Univ.∀_:Univ.Univ.
83 ∀response:∀_:Univ.∀_:Univ.Univ.
84 ∀H0:∀X:Univ.eq Univ (response c (common_bird X)) (response X (common_bird X)).
85 ∀H1:∀W:Univ.∀X:Univ.∀Y:Univ.eq Univ (response (compose X Y) W) (response X (response Y W)).∃V:Univ.eq Univ (response a V) (response odd_bird V))
100 napply (ex_intro ? ? ? ?) ##[
104 ntry (nassumption) ##;
107 (* ----C composes A with B. WHY is this here? *)
109 (* -------------------------------------------------------------------------- *)