1 include "logic/equality.ma".
3 (* Inclusion of: COL066-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : COL066-1 : TPTP v3.7.0. Released v1.0.0. *)
9 (* Domain : Combinatory Logic *)
11 (* Problem : Find combinator equivalent to P from B, Q and W *)
13 (* Version : [WM88] (equality) axioms. *)
15 (* English : Construct from B, Q and W alone a combinator that behaves as *)
17 (* the combinator P does, where ((Bx)y)z = x(yz), ((Qx)y)z = *)
19 (* y(xz), (Wx)y = (xy)y, (((Px)y)y)z = (xy)((xy)z) *)
21 (* Refs : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq *)
23 (* : [WW+90] Wos et al. (1990), Automated Reasoning Contributes to *)
25 (* Source : [WW+90] *)
27 (* Names : CL-7 [WW+90] *)
29 (* Status : Unsatisfiable *)
31 (* Rating : 0.78 v3.4.0, 0.88 v3.3.0, 0.93 v3.1.0, 0.89 v2.7.0, 0.82 v2.6.0, 0.67 v2.5.0, 0.25 v2.4.0, 0.00 v2.3.0, 0.33 v2.2.1, 0.89 v2.2.0, 0.86 v2.1.0, 1.00 v2.0.0 *)
33 (* Syntax : Number of clauses : 4 ( 0 non-Horn; 4 unit; 1 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 ( 3 constant; 0-2 arity) *)
43 (* Number of variables : 9 ( 0 singleton) *)
45 (* Maximal term depth : 6 ( 4 average) *)
49 (* -------------------------------------------------------------------------- *)
50 ntheorem prove_p_combinator:
51 (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
52 ∀apply:∀_:Univ.∀_:Univ.Univ.
59 ∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply w X) Y) (apply (apply X Y) Y).
60 ∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply q X) Y) Z) (apply Y (apply X Z)).
61 ∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).∃X:Univ.eq Univ (apply (apply (apply (apply X (f X)) (g X)) (g X)) (h X)) (apply (apply (f X) (g X)) (apply (apply (f X) (g X)) (h X))))
77 napply (ex_intro ? ? ? ?) ##[
81 ntry (nassumption) ##;
84 (* -------------------------------------------------------------------------- *)