% 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

*/