\documentclass[11pt,a4paper]{article}
\usepackage{amsmath}
%\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{latexsym}
\usepackage{vmargin}
   \setpapersize{A4}
   \setmargrb{25mm}{18mm}{35mm}{25mm}

\begin{document}
\begin{verbatim}
% we prove that the 
% composition of relations with injective functions is injective.
use(setrel).
goal
~(
    rel(p,s,t) and rel(q,s,t) and
    func(f,t,b) and injective(f) =>
                 
                 eq(dot(p,f),dot(q,f)) =>  eq(p,q)

).

/*
option(full_cnf(yes))
gives us a case analysis on ~eq(p,q)

Proof:
======

   1 : set(A),set(B) -> eq(A,B)==!C.(contains(A,C)<=>contains(B,C))     [input]
   2 : set(A),set(B) -> subset(A,B)==!C.(contains(A,C)=>contains(B,C))  [input]
   3 : rel(A,B,C) -> set(A)and set(B)and set(C)                         [input]
   4 : rel(A,B,C)==subset(A,product(B,C))                               [input]
   5 : set(A),set(B) -> set(product(A,B))                               [input]
   6 : contains(product(A,B),C)==
                   ?D,E.(C=cons(E,D)and contains(A,E)and contains(B,D)) [input]
   7 : contains(dot(A,B),cons(C,D))==
                    ?E.(contains(A,cons(C,E))and contains(B,cons(E,D))) [input]
   8 : rel(A,B,C),rel(D,C,E) -> rel(dot(A,D),B,E)                       [input]
  11 : total(A,B)==!C.(contains(B,C)=>?D.(contains(A,cons(C,D))))       [input]
  12 : unique(A)==!B,C,D.(contains(A,cons(D,C))and contains(A,cons(D,B))=>C=B)
                                                                        [input]
  13 : pfunc(A,B,C)==(rel(A,B,C)and unique(A))                          [input]
  14 : injective(A)==
           !B,C,D.(contains(A,cons(D,B))and contains(A,cons(C,B))=>D=C) [input]
  15 : func(A,B,C)==(pfunc(A,B,C)and total(A,B))                        [input]
  16 + rel(p,s,t)and rel(q,s,t)and func(f,t,b)and injective(f)=>
                                     eq(dot(p,f),dot(q,f))=>eq(p,q) ->  [input]
  17 : pfunc(A,B,C)==(rel(A,B,C)and
       !D,E,F.(contains(A,cons(F,E))and contains(A,cons(F,D))=>E=D)) 
                                                      [reduction of 13 by [12]]
  18 : func(A,B,C)==(rel(A,B,C)and
       !D,E,F.(contains(A,cons(F,E))and contains(A,cons(F,D))=>E=D) and
       !G.(contains(B,G)=>?H.(contains(A,cons(G,H))))) 
                                                   [reduction of 15 by [11,17]]
  19 + rel(p,s,t)and rel(q,s,t)and(rel(f,t,b)and
       !A,B,C.(contains(f,cons(C,B))and contains(f,cons(C,A))=>B=A) and
       !D.(contains(t,D)=>?E.(contains(f,cons(D,E)))))and
       !F,G,H.(contains(f,cons(H,F))and contains(f,cons(G,F))=>H=G)=>
                eq(dot(p,f),dot(q,f))=>eq(p,q) ->  [reduction of 16 by [14,18]]
  20 : rel(A,B,C) -> set(A)and set(B)                        [expansion from 3]
  21 : rel(A,B,C) -> set(C)                                  [expansion from 3]
  22 + rel(p,s,t)and rel(q,s,t)and(rel(f,t,b)and
      !A,B,C.(contains(f,cons(C,B))and contains(f,cons(C,A))=>B=A) and
      !D.(contains(t,D)=>?E.(contains(f,cons(D,E)))))and
      !F,G,H.(contains(f,cons(H,F))and contains(f,cons(G,F))=>H=G) 
                                                            [expansion from 19]
  23 + eq(dot(p,f),dot(q,f))=>eq(p,q) ->                    [expansion from 19]
  24 : rel(A,B,C) -> set(A)                                 [expansion from 20]
  25 : rel(A,B,C) -> set(B)                                 [expansion from 20]
  26 + rel(p,s,t)and rel(q,s,t)and(rel(f,t,b)and
       !A,B,C.(contains(f,cons(C,B))and contains(f,cons(C,A))=>B=A) and
            !D.(contains(t,D)=>?E.(contains(f,cons(D,E))))) [expansion from 22]
  27 + contains(f,cons(A,B)),contains(f,cons(C,B)) -> A=C   [expansion from 22]
  28 + eq(dot(p,f),dot(q,f))                                [expansion from 23]
  29 + eq(p,q) ->                                           [expansion from 23]
  30 + rel(p,s,t)and rel(q,s,t)                             [expansion from 26]
  31 + rel(f,t,b)and!A,B,C.(contains(f,cons(C,B))and contains(f,cons(C,A))=>
     B=A) and!D.(contains(t,D)=>?E.(contains(f,cons(D,E)))) [expansion from 26]
  32 + rel(p,s,t)                                           [expansion from 30]
  33 + rel(q,s,t)                                           [expansion from 30]
  34 + rel(f,t,b)and!A,B,C.(contains(f,cons(C,B))and contains(f,cons(C,A))=>
                                                       B=A) [expansion from 31]
  35 + contains(t,A) -> ?B.(contains(f,cons(A,B)))          [expansion from 31]
  36 + rel(f,t,b)                                           [expansion from 34]
  38 + contains(t,A) -> contains(f,cons(A,s$9(f,A)))        [expansion from 35]
  39 + set(t)                                 [negative chaining of 32 from 21]
  42 + set(p)                                 [negative chaining of 32 from 24]
  43 + set(q)                                 [negative chaining of 33 from 24]
  45 + set(s)                                 [negative chaining of 32 from 25]
  49 : rel(A,B,C),rel(D,C,E) -> set(dot(A,D))  [negative chaining of 8 from 24]
  51 + !A.(contains(p,A)<=>contains(q,A)),set(p),set(q) ->  
                                               [negative chaining of 1 from 29]
  52 + set(dot(p,f)),set(dot(q,f)) -> 
       !A.(contains(dot(p,f),A)<=>contains(dot(q,f),A)) [chaining of 1 from 28]
  53 : set(A),set(product(B,C)) -> 
!D.(contains(A,D)=>contains(product(B,C),D))==rel(A,B,C) [chaining of 2 from 4]
  56 + rel(A,B,t) -> set(dot(A,f))            [negative chaining of 36 from 49]
  58 + !A.(contains(p,A)<=>contains(q,A)) ->       [reduction of 51 by [42,43]]
  59 + set(dot(p,f)),set(dot(q,f)) -> 
                contains(dot(p,f),A)==contains(dot(q,f),A) [condensement of 52]
  60 : set(A),set(product(B,C)) -> 
       !D.(contains(A,D)=>?E,F.(D=cons(F,E)and contains(B,F)and 
                           contains(C,E)))==rel(A,B,C) [reduction of 53 by [6]]
  61 + contains(p,s$16)==contains(q,s$16) ->                [expansion from 58]
  64 : contains(A,B),rel(A,C,D),set(A),set(product(C,D)) 
    -> ?E,F.(B=cons(F,E)and contains(C,F)and contains(D,E)) [expansion from 60]
  65 + contains(q,s$16)and~contains(p,s$16),
                      ~contains(q,s$16)and contains(p,s$16) [expansion from 61]
  68 + set(dot(p,f))                          [negative chaining of 32 from 56]
  69 + set(dot(q,f))                          [negative chaining of 33 from 56]
  71 : set(product(A,B)),rel(C,A,B),contains(C,D) -> 
 ?E,F.(D=cons(F,E)and contains(A,F)and contains(B,E)) [reduction of 64 by [24]]
  72 + contains(dot(q,f),A)==contains(dot(p,f),A)  [reduction of 59 by [69,68]]
  74 : rel(A,B,C),set(product(B,C)),contains(A,D) -> 
       ?E.(D=cons(E,s$4(B,C,D))and contains(B,E)and 
                                    contains(C,s$4(B,C,D))) [expansion from 71]
  75 + q$499,contains(q,s$16)and~contains(p,s$16)           [expansion from 65]
  76 + q$499 -> ~contains(q,s$16)                           [expansion from 65]
  77 + q$499 -> contains(p,s$16)                            [expansion from 65]
  78 + q$499,contains(q,s$16) ->                       [reduction of 76 by [L]]
  81 : rel(A,B,C),set(product(B,C)),contains(A,D) -> 
       D=cons(s$3(B,C,D),s$4(B,C,D))and contains(B,s$3(B,C,D))and 
                                     contains(C,s$4(B,C,D)) [expansion from 74]
  82 + q$499,contains(q,s$16)                               [expansion from 75]
  83 + q$499,~contains(p,s$16)                              [expansion from 75]
  84 + ?C.(contains(q,cons(A,C))and 
   contains(f,cons(C,B)))==contains(dot(p,f),cons(A,B)) [chaining of 7 from 72]
  85 + contains(p,s$16) -> q$499                       [reduction of 83 by [L]]
  86 + ?C.(contains(q,cons(A,C))and 
           contains(f,cons(C,B)))==
   ?D.(contains(p,cons(A,D))and contains(f,cons(D,B))) [reduction of 84 by [7]]
  87 : rel(A,B,C),set(product(B,C)),contains(A,D) -> 
    D=cons(s$3(B,C,D),s$4(B,C,D))and contains(B,s$3(B,C,D)) [expansion from 81]
  88 : rel(A,B,C),set(product(B,C)),contains(A,D) -> 
                                     contains(C,s$4(B,C,D)) [expansion from 81]
  89 + contains(q,cons(A,B)),contains(f,cons(B,C)) -> 
        ?D.(contains(p,cons(A,D))and contains(f,cons(D,C))) [expansion from 86]
  90 + contains(p,cons(A,B)),contains(f,cons(B,C)) -> 
        ?D.(contains(q,cons(A,D))and contains(f,cons(D,C))) [expansion from 86]
  98 : rel(A,B,C),set(product(B,C)),contains(A,D) -> 
                              D=cons(s$3(B,C,D),s$4(B,C,D)) [expansion from 87]
 100 + contains(q,cons(A,B)),contains(f,cons(B,C)) -> 
       contains(p,cons(A,s$5(p,f,A,C)))and 
                           contains(f,cons(s$5(p,f,A,C),C)) [expansion from 89]
 101 + contains(f,cons(A,B)),contains(p,cons(C,A)) -> 
         contains(q,cons(C,s$5(q,f,C,B)))and 
                           contains(f,cons(s$5(q,f,C,B),B)) [expansion from 90]
 107 + set(product(s,t)),contains(p,A) -> 
                       contains(t,s$4(s,t,A)) [negative chaining of 32 from 88]
 108 + set(product(s,t)),contains(q,A) -> 
                       contains(t,s$4(s,t,A)) [negative chaining of 33 from 88]
 111 + contains(p,A) -> contains(t,s$4(s,t,A))  [reduction of 107 by [5,39,45]]
 112 + contains(q,A) -> contains(t,s$4(s,t,A))  [reduction of 108 by [5,39,45]]
 114 + contains(q,cons(A,B)),contains(f,cons(B,C)) -> 
                          contains(p,cons(A,s$5(p,f,A,C))) [expansion from 100]
 115 + contains(q,cons(A,B)),contains(f,cons(B,C)) -> 
                          contains(f,cons(s$5(p,f,A,C),C)) [expansion from 100]
 116 + contains(f,cons(A,B)),contains(p,cons(C,A)) -> 
                          contains(q,cons(C,s$5(q,f,C,B))) [expansion from 101]
 117 + contains(f,cons(A,B)),contains(p,cons(C,A)) -> 
                          contains(f,cons(s$5(q,f,C,B),B)) [expansion from 101]
 121 + contains(q,A) -> contains(f,cons(s$4(s,t,A),s$9(f,s$4(s,t,A)))) 
                                             [negative chaining of 112 from 38]
 124 + contains(p,A) -> contains(f,cons(s$4(s,t,A),s$9(f,s$4(s,t,A)))) 
                                             [negative chaining of 111 from 38]
 136 + q$499,contains(f,cons(s$4(s,t,s$16),s$9(f,s$4(s,t,s$16)))) 
                                             [negative chaining of 82 from 121]
 138 + q$499 -> contains(f,cons(s$4(s,t,s$16),s$9(f,s$4(s,t,s$16)))) 
                                             [negative chaining of 77 from 124]
 144 + contains(f,cons(s$4(s,t,s$16),s$9(f,s$4(s,t,s$16)))) 
                                                    [reduction of 138 by [136]]
 171 + q$499,rel(p,A,B),set(product(A,B)) -> 
       cons(s$3(A,B,s$16),s$4(A,B,s$16))=s$16 [negative chaining of 77 from 98]
 172 + rel(q,A,B),set(product(A,B)) -> 
 q$499,cons(s$3(A,B,s$16),s$4(A,B,s$16))=s$16 [negative chaining of 82 from 98]
 200 + contains(q,s$16),rel(q,A,B),set(product(A,B)),
              contains(f,cons(s$4(A,B,s$16),C)) -> 
                q$499,contains(p,cons(s$3(A,B,s$16),s$5(p,f,s$3(A,B,s$16),C)))
                                            [negative chaining of 172 from 114]
 201 + contains(q,s$16),rel(q,A,B),set(product(A,B)),
              contains(f,cons(s$4(A,B,s$16),C)) -> 
                q$499,contains(f,cons(s$5(p,f,s$3(A,B,s$16),C),C)) 
                                            [negative chaining of 172 from 115]
 205 + contains(f,cons(s$4(A,B,s$16),C)),set(product(A,B)),rel(q,A,B) -> 
                contains(p,cons(s$3(A,B,s$16),s$5(p,f,s$3(A,B,s$16),C))),q$499 
                                                     [reduction of 200 by [82]]
 206 + contains(f,cons(s$4(A,B,s$16),C)),set(product(A,B)),rel(q,A,B) -> 
                            contains(f,cons(s$5(p,f,s$3(A,B,s$16),C),C)),q$499 
                                                     [reduction of 201 by [82]]
 215 + set(product(A,B)),rel(q,A,B),contains(f,cons(s$4(A,B,s$16),C)),
                     contains(f,cons(D,C)) -> q$499,D=s$5(p,f,s$3(A,B,s$16),C) 
                                             [negative chaining of 206 from 27]
 228 + contains(f,cons(A,s$9(f,s$4(s,t,s$16)))),set(product(s,t)),rel(q,s,t) ->
                            q$499,A=s$5(p,f,s$3(s,t,s$16),s$9(f,s$4(s,t,s$16)))
                                            [negative chaining of 144 from 215]
 233 + contains(f,cons(A,s$9(f,s$4(s,t,s$16)))) -> 
                            A=s$5(p,f,s$3(s,t,s$16),s$9(f,s$4(s,t,s$16))),q$499
                                             [reduction of 228 by [5,39,45,33]]
 239 + s$4(s,t,s$16)=s$5(p,f,s$3(s,t,s$16),s$9(f,s$4(s,t,s$16))),q$499 
                                            [negative chaining of 144 from 233]
 259 + set(product(s,t)),rel(q,s,t),contains(f,cons(s$4(s,t,s$16),
                                             s$9(f,s$4(s,t,s$16)))) -> 
                     contains(p,cons(s$3(s,t,s$16),s$4(s,t,s$16))),q$499,q$499
                                                     [chaining of 239 from 205]
 260 + set(product(s,t)),rel(q,s,t),contains(f,cons(s$4(s,t,s$16),
                                             s$9(f,s$4(s,t,s$16)))) -> 
                           contains(p,cons(s$3(s,t,s$16),s$4(s,t,s$16))),q$499
                                                          [condensement of 259]
 261 + q$499         [reduction of 260 by [5,39,45,33,144,172,5,39,45,33,85,L]]
 262 + contains(q,s$16) ->                           [reduction of 78 by [261]]
 263 + contains(p,s$16)                              [reduction of 77 by [261]]
 264 + rel(p,A,B),set(product(A,B)) -> cons(s$3(A,B,s$16),s$4(A,B,s$16))=s$16 
                                                    [reduction of 171 by [261]]
 273 + contains(p,s$16),rel(p,A,B),set(product(A,B)),
                        contains(f,cons(s$4(A,B,s$16),C)) -> 
                                 contains(f,cons(s$5(q,f,s$3(A,B,s$16),C),C)) 
                                            [negative chaining of 264 from 117]
 277 + contains(f,cons(s$4(A,B,s$16),C)),set(product(A,B)),rel(p,A,B) -> 
       contains(f,cons(s$5(q,f,s$3(A,B,s$16),C),C)) [reduction of 273 by [263]]
 280 + set(product(A,B)),rel(p,A,B),contains(f,cons(s$4(A,B,s$16),C)),
                         contains(f,cons(D,C)) -> D=s$5(q,f,s$3(A,B,s$16),C) 
                                             [negative chaining of 277 from 27]
 293 + contains(f,cons(A,s$9(f,s$4(s,t,s$16)))),set(product(s,t)),
                   rel(p,s,t) -> A=s$5(q,f,s$3(s,t,s$16),s$9(f,s$4(s,t,s$16)))
                                            [negative chaining of 144 from 280]
 298 + contains(f,cons(A,s$9(f,s$4(s,t,s$16)))) -> 
                                 A=s$5(q,f,s$3(s,t,s$16),s$9(f,s$4(s,t,s$16)))
                                             [reduction of 293 by [5,39,45,32]]
 303 + s$4(s,t,s$16)=s$5(q,f,s$3(s,t,s$16),s$9(f,s$4(s,t,s$16))) 
                                            [negative chaining of 144 from 298]
 315 + contains(f,cons(A,s$9(f,s$4(s,t,s$16)))),
       contains(p,cons(s$3(s,t,s$16),A)) -> 
       contains(q,cons(s$3(s,t,s$16),s$4(s,t,s$16))) [chaining of 303 from 116]
 318 + contains(f,cons(A,s$9(f,s$4(s,t,s$16)))),
       contains(p,cons(s$3(s,t,s$16),A)) ->  
                                   [reduction of 315 by [264,5,39,45,32,262,L]]
 322 + contains(p,s$16),rel(p,s,t),set(product(s,t)),
       contains(f,cons(s$4(s,t,s$16),s$9(f,s$4(s,t,s$16)))) ->  
                                            [negative chaining of 264 from 318]
 339 + false                         [reduction of 322 by [263,32,5,39,45,144]]

Length = 111, Depth = 37, Search Depth = 8



Total time: 13010 milliseconds

Number of forward inferences: 189
Number of tableau inferences: 71
Number of generated clauses: 339
Number of kept clauses: 237



*/

\end{verbatim}
\end{document}
%%% Local Variables: 
%%% mode: plain-tex
%%% TeX-master: t
%%% End: 
