1 include "logic/equality.ma".
3 (* Inclusion of: COL068-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : COL068-1 : TPTP v3.7.0. Released v1.2.0. *)
9 (* Domain : Combinatory Logic *)
11 (* Problem : Weak fixed point for B and S *)
13 (* Version : [WM88] (equality) axioms. *)
15 (* English : The weak fixed point property holds for the set P consisting *)
17 (* of the combinators B and S, where ((Sx)y)z (xz)(yz), ((Bx)y)z *)
21 (* Refs : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq *)
23 (* : [Wos93] Wos (1993), The Kernel Strategy and Its Use for the St *)
25 (* Source : [Wos93] *)
27 (* Names : Question 11 [Wos93] *)
29 (* Status : Unknown *)
31 (* Rating : 1.00 v2.0.0 *)
33 (* Syntax : Number of clauses : 3 ( 0 non-Horn; 3 unit; 1 RR) *)
35 (* Number of atoms : 3 ( 3 equality) *)
37 (* Maximal clause size : 1 ( 1 average) *)
39 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
41 (* Number of functors : 4 ( 3 constant; 0-2 arity) *)
43 (* Number of variables : 7 ( 0 singleton) *)
45 (* Maximal term depth : 4 ( 3 average) *)
49 (* -------------------------------------------------------------------------- *)
50 ntheorem prove_fixed_point:
51 (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
52 ∀apply:∀_:Univ.∀_:Univ.Univ.
56 ∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).
57 ∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply s X) Y) Z) (apply (apply X Z) (apply Y Z)).∃Y:Univ.eq Univ Y (apply combinator Y))
69 napply (ex_intro ? ? ? ?) ##[
73 ntry (nassumption) ##;
76 (* -------------------------------------------------------------------------- *)