1 include "logic/equality.ma".
3 (* Inclusion of: COL002-5.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : COL002-5 : TPTP v3.7.0. Bugfixed v3.1.0. *)
9 (* Domain : Combinatory Logic *)
11 (* Problem : Weak fixed point for S, B, C, and I *)
13 (* Version : [WM88] (equality) axioms. *)
15 (* Theorem formulation : The fixed point is provided and checked. *)
17 (* English : The weak fixed point property holds for the set P consisting *)
19 (* of the combinators S, B, C, and I, where ((Sx)y)z = (xz)(yz), *)
21 (* ((Bx)y)z = x(yz), ((Cx)y)z = (xz)y, and Ix = x. *)
23 (* Refs : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq *)
29 (* Status : Unsatisfiable *)
31 (* Rating : 0.11 v3.4.0, 0.12 v3.3.0, 0.43 v3.1.0 *)
33 (* Syntax : Number of clauses : 6 ( 0 non-Horn; 6 unit; 1 RR) *)
35 (* Number of atoms : 6 ( 6 equality) *)
37 (* Maximal clause size : 1 ( 1 average) *)
39 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
41 (* Number of functors : 7 ( 5 constant; 0-2 arity) *)
43 (* Number of variables : 11 ( 0 singleton) *)
45 (* Maximal term depth : 6 ( 3 average) *)
47 (* Comments : This is the one found in proof 3 of C1.1 in [WM88]. *)
49 (* Bugfixes : Fixed clauses weak_fixed_point and prove_weak_fixed_point. *)
51 (* -------------------------------------------------------------------------- *)
52 ntheorem prove_weak_fixed_point:
53 (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
54 ∀apply:∀_:Univ.∀_:Univ.Univ.
60 ∀weak_fixed_point:∀_:Univ.Univ.
61 ∀H0:∀X:Univ.eq Univ (weak_fixed_point X) (apply (apply (apply s (apply c (apply b X))) (apply s (apply c (apply b X)))) (apply s (apply c (apply b X)))).
62 ∀H1:∀X:Univ.eq Univ (apply i X) X.
63 ∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply c X) Y) Z) (apply (apply X Z) Y).
64 ∀H3:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).
65 ∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply s X) Y) Z) (apply (apply X Z) (apply Y Z)).eq Univ (weak_fixed_point fixed_pt) (apply fixed_pt (weak_fixed_point fixed_pt)))
83 nauto by H0,H1,H2,H3,H4 ##;
84 ntry (nassumption) ##;
87 (* -------------------------------------------------------------------------- *)