1%
2% This is Stage 1 of the Kernel Method.
3% Wos & McCune, "Searching for Fixed Point Combinators ...", ANL-88-10.
4%
5% Stage 1 searches for kernels (reducible fixed points of an
6% arbitrary combinator).
7% Stage 2 attempts to expand a kernel into a fixed point combinator.
8%
9
10set(para_into).
11clear(para_from_left).
12clear(para_into_left).
13set(para_ones_rule).
14
15clear(back_sub).
16clear(print_proofs).
17
18assign(max_proofs, -1).
19assign(max_given, 30).
20
21% set(para_into_vars).
22% set(para_from_vars).
23
24list(usable).
25x = x.
26
27% regular isolators (including replicators)
28
29 a(a(a(B,x),y),z) = a(x,a(y,z)).
30% a(a(L,x),y) = a(x,a(y,y)).
31% a(I,x) = x.
32% a(a(K,x),y) = x.
33% a(a(a(Q1,x),y),z) = a(x,a(z,y)).
34
35% irregular isolators (including replicators)
36
37% a(M,x) = a(x,x).
38% a(a(O,x),y) = a(y,a(x,y)).
39% a(a(T,x),y) = a(y,x).
40% a(a(a(Q,x),y),z) = a(y,a(x,z)).
41
42% regular replicators (non-isolating)
43
44 a(a(W,x),y) = a(a(x,y),y).
45% a(a(a(N,x),y),z) = a(a(a(x,z),y),z).
46% a(a(a(H,x),y),z) = a(a(a(x,y),z),y).
47% a(a(a(S,x),y),z) = a(a(x,z),a(y,z)).
48
49% irregular replicators (non-isolating)
50
51% a(a(W1,x),y) = a(a(y,x),x).
52
53% others (non-isolating non-replicating)
54
55% a(a(a(C,x),y),z) = a(a(x,z),y).
56% a(a(a(R,x),y),z) = a(a(y,z),x).
57
58end_of_list.
59
60list(sos).
61y != a(f,y) | $Ans(y).  % denial of the weak fixed point property
62end_of_list.
63
64% The following discards ground clauses.
65
66assign(max_weight, 1).
67
68weight_list(purge_gen).
69weight(x, -1000).
70end_of_list.
71