Quelle  similarity.prf

(similarity
 (similarity_is_isomorphism 0
  (similarity_is_isomorphism-1 nil 3324309296
   ("" (expand* "similarity?" "isomorphism?" "preserves")
    (("" (skosimp* t)
      (("" (inst-cp - "d1!1" "d2!1")
        (("" (smash)
          (("" (expand* "total_order?" "dichotomous?")
            (("" (flatten)
              (("" (inst - "d1!1" "d2!1")
                (("" (inst -6 "d2!1" "d1!1")
                  (("" (assert)
                    (("" (expand "partial_order?" -3)
                      (("" (expand "antisymmetric?")
                        (("" (flatten)
                          (("" (inst - "f!1(d1!1)" "f!1(d2!1)")
                            (("" (assert)
                              ((""
                                (expand* "bijective?" "injective?")
                                ((""
                                  (flatten)
                                  ((""
                                    (inst -6 "d1!1" "d2!1")
                                    (("" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (R formal-type-decl nil similarity nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (D formal-type-decl nil similarity nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (partial_order? const-decl "bool" orders nil)
    (injective? const-decl "bool" functions nil)
    (antisymmetric? const-decl "bool" relations nil)
    (dichotomous? const-decl "bool" orders nil)
    (similarity? const-decl "bool" similarity nil)
    (preserves const-decl "bool" functions nil)
    (isomorphism? const-decl "bool" isomorphism nil))
   shostak))
 (similar_is_isomorphic 0
  (similar_is_isomorphic-1 nil 3324309680
   ("" (skosimp)
    (("" (expand* "similar?" "isomorphic?")
      (("" (skolem!)
        (("" (inst?)
          (("" (forward-chain "similarity_is_isomorphism") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((isomorphic? const-decl "bool" isomorphism nil)
    (similar? const-decl "bool" similarity nil)
    (D formal-type-decl nil similarity nil)
    (R formal-type-decl nil similarity nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (similarity_is_isomorphism formula-decl nil similarity nil))
   shostak)))