Quelle  complementary_lattices.prf

(complementary_lattices
 (dual_dual 0
  (dual_dual-1 nil 3318702826
   ("" (skolem!)
    (("" (decompose-equality)
      (("" (expand* "dual" "o")
        (("" (rewrite "complement_complement")
          (("" (rewrite "complement_complement") nil nil)) nil))
        nil))
      nil))
    nil)
   ((dual const-decl "[T -> T]" complementary_lattices nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (complement? const-decl "bool" complementary_orders nil)
    (lattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lattice?[T])" complementary_lattices nil)
    (T formal-nonempty-type-decl nil complementary_lattices nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (O const-decl "T3" function_props nil))
   shostak))
 (dual_inclusion1 0
  (dual_inclusion1-1 nil 3318704200
   ("" (skolem!)
    (("" (expand* "dual" "o")
      (("" (lemma "le_complement")
        (("" (inst - "<=" "C!1(t!1)" "H!1(C!1(t!1))" "C!1")
          (("" (rewrite "complement_complement") (("" (prop) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (dual const-decl "[T -> T]" complementary_lattices nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (lattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lattice?[T])" complementary_lattices nil)
    (complement? const-decl "bool" complementary_orders nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (le_complement formula-decl nil complementary_orders nil)
    (T formal-nonempty-type-decl nil complementary_lattices nil))
   shostak))
 (dual_inclusion2 0
  (dual_inclusion2-1 nil 3318704371
   ("" (skolem!)
    (("" (expand* "dual" "o")
      (("" (lemma "le_complement")
        (("" (inst - "<=" "H!1(C!1(t!1))" "C!1(t!1)" "C!1")
          (("" (rewrite "complement_complement") (("" (prop) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (dual const-decl "[T -> T]" complementary_lattices nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (lattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lattice?[T])" complementary_lattices nil)
    (complement? const-decl "bool" complementary_orders nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (le_complement formula-decl nil complementary_orders nil)
    (T formal-nonempty-type-decl nil complementary_lattices nil))
   shostak))
 (dual_inclusion3 0
  (dual_inclusion3-1 nil 3318704401
   ("" (skolem!)
    (("" (expand* "dual" "o")
      (("" (lemma "le_complement")
        (("" (inst - "<=" "t!1" "H!1(t!1)" "C!1")
          (("" (rewrite "complement_complement") (("" (prop) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (dual const-decl "[T -> T]" complementary_lattices nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (lattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lattice?[T])" complementary_lattices nil)
    (complement? const-decl "bool" complementary_orders nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (le_complement formula-decl nil complementary_orders nil)
    (T formal-nonempty-type-decl nil complementary_lattices nil))
   shostak))
 (dual_inclusion4 0
  (dual_inclusion4-1 nil 3318704698
   ("" (skolem!)
    (("" (expand* "dual" "o")
      (("" (lemma "le_complement")
        (("" (inst - "<=" "H!1(t!1)" "t!1" "C!1")
          (("" (rewrite "complement_complement") (("" (prop) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (dual const-decl "[T -> T]" complementary_lattices nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (lattice? const-decl "bool" bounded_orders nil)
    (<= formal-const-decl "(lattice?[T])" complementary_lattices nil)
    (complement? const-decl "bool" complementary_orders nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (le_complement formula-decl nil complementary_orders nil)
    (T formal-nonempty-type-decl nil complementary_lattices nil))
   shostak)))