【演習問題１０：組合せ論理``不動点'' (TPTP/COL012-1)】

dom(A),dom(B)-->
   equal(apply(apply(u,A),B),
         apply(B,apply(apply(A,A),B))).

equal(A,apply(combinator,A))-->false.

dom(A)-->equal(A,A).
equal(A,B)-->equal(B,A).
equal(A,B),equal(B,C)-->equal(A,C).

equal(A,B),dom(C)-->equal(apply(A,C),apply(B,C)).
equal(A,B),dom(C)-->equal(apply(C,A),apply(C,B)).

true-->dom(u),dom(combinator).
dom(A),dom(B)-->dom(apply(A,B)).