Quelle mucalculus_prop.prf Sprache: Lisp

(mucalculus_prop
(antisymmetry 0
  (antisymmetry-2 nil 3324308681 ("" (grind-with-ext) nil nil)
   ((bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil)
    (<= const-decl "bool" mucalculus nil))
   nil)
  (antisymmetry-1 nil 3324295090
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   nil nil))
(reflexivity 0
  (reflexivity-2 nil 3324308681 ("" (grind) nil nil)
   ((<= const-decl "bool" mucalculus nil)) nil)
  (reflexivity-1 nil 3324295090 ("" (grind) nil nil) nil nil))
(glb_lower_bound 0
  (glb_lower_bound-2 nil 3324308681 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
    (glb const-decl "pred[T]" mucalculus nil)
    (<= const-decl "bool" mucalculus nil))
   nil)
  (glb_lower_bound-1 nil 3324295090 ("" (grind) nil nil) nil nil))
(glb_greatest_lower_bound 0
  (glb_greatest_lower_bound-2 nil 3324308681
   ("" (grind :polarity? t) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
    (glb const-decl "pred[T]" mucalculus nil)
    (<= const-decl "bool" mucalculus nil))
   nil)
  (glb_greatest_lower_bound-1 nil 3324295090
   ("" (grind :polarity? t) nil nil) nil nil))
(lub_upper_bound 0
  (lub_upper_bound-2 nil 3324308681 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
    (lub const-decl "pred[T]" mucalculus nil)
    (<= const-decl "bool" mucalculus nil))
   nil)
  (lub_upper_bound-1 nil 3324295090 ("" (grind) nil nil) nil nil))
(lub_least_upper_bound 0
  (lub_least_upper_bound-2 nil 3324308681
   ("" (grind :polarity? t) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
    (lub const-decl "pred[T]" mucalculus nil)
    (<= const-decl "bool" mucalculus nil))
   nil)
  (lub_least_upper_bound-1 nil 3324295090
   ("" (grind :polarity? t) nil nil) nil nil))
(closure_mu 0
  (closure_mu-2 nil 3324308681
   (""
    (auto-rewrite "glb_lower_bound" "glb_greatest_lower_bound" "mu"
                  "lfp" "monotonic?")
    (("" (reduce :if-match nil)
      (("" (inst - "mu(F!1)" "q!1")
        (("" (assert) (("" (grind :exclude ("glb")) nil nil)) nil))
        nil))
      nil))
    nil)
   ((lfp const-decl "pred[T]" mucalculus nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (glb_greatest_lower_bound formula-decl nil mucalculus_prop nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (<= const-decl "bool" mucalculus nil)
    (glb_lower_bound formula-decl nil mucalculus_prop nil))
   nil)
  (closure_mu-1 nil 3324295090
   (""
    (auto-rewrite "glb_lower_bound" "glb_greatest_lower_bound" "mu"
                  "lfp" "monotonic?")
    (("" (reduce :if-match nil)
      (("" (inst - "mu(F!1)" "q!1")
        (("" (assert) (("" (grind :exclude ("glb")) nil nil)) nil))
        nil))
      nil))
    nil)
   nil nil))
(smallest_closed 0
  (smallest_closed-2 nil 3324308681
   ("" (auto-rewrite "mu" "lfp" "glb_lower_bound")
    (("" (skosimp) (("" (assert) nil nil)) nil)) nil)
   ((lfp const-decl "pred[T]" mucalculus nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (glb_lower_bound formula-decl nil mucalculus_prop nil))
   nil)
  (smallest_closed-1 nil 3324295090
   ("" (auto-rewrite "mu" "lfp" "glb_lower_bound")
    (("" (skosimp) (("" (assert) nil nil)) nil)) nil)
   nil nil))
(fixpoint_mu1 0
  (fixpoint_mu1-2 nil 3324308681
   ("" (auto-rewrite "closure_mu" "monotonic?" "lfp")
    (("" (skolem-typepred)
      (("" (rewrite "antisymmetry")
        (("" (delete 2)
          (("" (expand "mu" 1 1)
            (("" (assert)
              (("" (rewrite "glb_lower_bound")
                (("" (inst?) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (pred type-eq-decl nil defined_types nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (lfp const-decl "pred[T]" mucalculus nil)
    (glb_lower_bound formula-decl nil mucalculus_prop nil)
    (set type-eq-decl nil sets nil)
    (<= const-decl "bool" mucalculus nil)
    (closure_mu formula-decl nil mucalculus_prop nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (antisymmetry formula-decl nil mucalculus_prop nil))
   nil)
  (fixpoint_mu1-1 nil 3324295090
   ("" (auto-rewrite "closure_mu" "monotonic?" "lfp")
    (("" (skolem-typepred)
      (("" (rewrite "antisymmetry")
        (("" (delete 2)
          (("" (expand "mu" 1 1)
            (("" (assert)
              (("" (rewrite "glb_lower_bound")
                (("" (inst?) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
(fixpoint_mu2 0
  (fixpoint_mu2-2 nil 3324308681
   ("" (lemma "fixpoint_mu1")
    (("" (expand* "fixpoint?" "fixpoint?") nil nil)) nil)
   ((fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint_mu1 formula-decl nil mucalculus_prop nil))
   nil)
  (fixpoint_mu2-1 nil 3324295090
   ("" (auto-rewrite "fixpoint?")
    (("" (skolem!)
      (("" (assert) (("" (rewrite "fixpoint_mu1") nil nil)) nil)) nil))
    nil)
   nil nil))
(least_fixpoint1 0
  (least_fixpoint1-2 nil 3324308681
   ("" (skosimp)
    (("" (rewrite "smallest_closed")
      (("" (replace*) (("" (rewrite "reflexivity") nil nil)) nil))
      nil))
    nil)
   ((smallest_closed formula-decl nil mucalculus_prop nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (reflexivity formula-decl nil mucalculus_prop nil))
   nil)
  (least_fixpoint1-1 nil 3324295090
   ("" (skosimp)
    (("" (rewrite "smallest_closed")
      (("" (replace*) (("" (rewrite "reflexivity") nil nil)) nil))
      nil))
    nil)
   nil nil))
(least_fixpoint2 0
  (least_fixpoint2-2 nil 3324308681
   ("" (lemma "least_fixpoint1")
    (("" (expand* "fixpoint?" "fixpoint?") nil nil)) nil)
   ((fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (least_fixpoint1 formula-decl nil mucalculus_prop nil))
   nil)
  (least_fixpoint2-1 nil 3324295090
   ("" (expand* "fixpoint?" "fixpoint?")
    (("" (lemma "least_fixpoint1") (("" (propax) nil nil)) nil)) nil)
   nil nil))
(mu_lfp 0
  (mu_lfp-2 nil 3324308681
   ("" (skolem!)
    (("" (expand* "lfp?" "lfp?" "fixpoint?")
      (("" (reduce)
        (("1" (forward-chain "least_fixpoint1") nil nil)
         ("2" (rewrite "fixpoint_mu1") nil nil))
        nil))
      nil))
    nil)
   ((lfp? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (lfp? const-decl "bool" mucalculus nil)
    (fixpoint_mu1 formula-decl nil mucalculus_prop nil)
    (least_fixpoint1 formula-decl nil mucalculus_prop nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil))
   nil)
  (mu_lfp-1 nil 3324295090
   ("" (skolem!)
    (("" (expand* "lfp?" "lfp?" "fixpoint?")
      (("" (reduce)
        (("1" (forward-chain "least_fixpoint1") nil nil)
         ("2" (rewrite "fixpoint_mu1") nil nil))
        nil))
      nil))
    nil)
   nil nil))
(closure_nu 0
  (closure_nu-2 nil 3324308681
   (""
    (auto-rewrite "lub_upper_bound" "lub_least_upper_bound" "nu" "gfp"
                  "monotonic?")
    (("" (reduce :if-match nil)
      (("" (inst - "q!1" "nu(F!1)")
        (("" (assert) (("" (grind :exclude ("lub")) nil nil)) nil))
        nil))
      nil))
    nil)
   ((gfp const-decl "pred[T]" mucalculus nil)
    (nu const-decl "pred[T]" mucalculus nil)
    (lub_least_upper_bound formula-decl nil mucalculus_prop nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (<= const-decl "bool" mucalculus nil)
    (lub_upper_bound formula-decl nil mucalculus_prop nil))
   nil)
  (closure_nu-1 nil 3324295090
   (""
    (auto-rewrite "lub_upper_bound" "lub_least_upper_bound" "nu" "gfp"
                  "monotonic?")
    (("" (reduce :if-match nil)
      (("" (inst - "q!1" "nu(F!1)")
        (("" (assert) (("" (grind :exclude ("lub")) nil nil)) nil))
        nil))
      nil))
    nil)
   nil nil))
(largest_closed 0
  (largest_closed-2 nil 3324308681
   ("" (auto-rewrite "nu" "gfp" "lub_upper_bound")
    (("" (skosimp) (("" (assert) nil nil)) nil)) nil)
   ((gfp const-decl "pred[T]" mucalculus nil)
    (nu const-decl "pred[T]" mucalculus nil)
    (lub_upper_bound formula-decl nil mucalculus_prop nil))
   nil)
  (largest_closed-1 nil 3324295090
   ("" (auto-rewrite "nu" "gfp" "lub_upper_bound")
    (("" (skosimp) (("" (assert) nil nil)) nil)) nil)
   nil nil))
(fixpoint_nu1 0
  (fixpoint_nu1-2 nil 3324308681
   ("" (auto-rewrite "closure_nu" "monotonic?" "gfp")
    (("" (skolem-typepred)
      (("" (rewrite "antisymmetry")
        (("" (delete 2)
          (("" (expand "nu" 1 2)
            (("" (assert)
              (("" (rewrite "lub_upper_bound")
                (("" (inst?) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (pred type-eq-decl nil defined_types nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (gfp const-decl "pred[T]" mucalculus nil)
    (lub_upper_bound formula-decl nil mucalculus_prop nil)
    (set type-eq-decl nil sets nil)
    (<= const-decl "bool" mucalculus nil)
    (closure_nu formula-decl nil mucalculus_prop nil)
    (nu const-decl "pred[T]" mucalculus nil)
    (antisymmetry formula-decl nil mucalculus_prop nil))
   nil)
  (fixpoint_nu1-1 nil 3324295090
   ("" (auto-rewrite "closure_nu" "monotonic?" "gfp")
    (("" (skolem-typepred)
      (("" (rewrite "antisymmetry")
        (("" (delete 2)
          (("" (expand "nu" 1 2)
            (("" (assert)
              (("" (rewrite "lub_upper_bound")
                (("" (inst?) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
(fixpoint_nu2 0
  (fixpoint_nu2-2 nil 3324308681
   ("" (lemma "fixpoint_nu1")
    (("" (expand* "fixpoint?" "fixpoint?") nil nil)) nil)
   ((fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint_nu1 formula-decl nil mucalculus_prop nil))
   nil)
  (fixpoint_nu2-1 nil 3324295090
   ("" (expand* "fixpoint?" "fixpoint?")
    (("" (lemma "fixpoint_nu1") (("" (propax) nil nil)) nil)) nil)
   nil nil))
(greatest_fixpoint1 0
  (greatest_fixpoint1-2 nil 3324308681
   ("" (skosimp)
    (("" (rewrite "largest_closed")
      (("" (replace*) (("" (rewrite "reflexivity") nil nil)) nil))
      nil))
    nil)
   ((largest_closed formula-decl nil mucalculus_prop nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (reflexivity formula-decl nil mucalculus_prop nil))
   nil)
  (greatest_fixpoint1-1 nil 3324295090
   ("" (skosimp)
    (("" (rewrite "largest_closed")
      (("" (replace*) (("" (rewrite "reflexivity") nil nil)) nil))
      nil))
    nil)
   nil nil))
(greatest_fixpoint2 0
  (greatest_fixpoint2-2 nil 3324308681
   ("" (lemma "greatest_fixpoint1")
    (("" (expand* "fixpoint?" "fixpoint?") nil nil)) nil)
   ((fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (greatest_fixpoint1 formula-decl nil mucalculus_prop nil))
   nil)
  (greatest_fixpoint2-1 nil 3324295090
   ("" (expand* "fixpoint?" "fixpoint?")
    (("" (lemma "greatest_fixpoint1") (("" (propax) nil nil)) nil))
    nil)
   nil nil))
(nu_gfp 0
  (nu_gfp-2 nil 3324308681
   ("" (skolem!)
    (("" (expand* "gfp?" "gfp?" "fixpoint?")
      (("" (reduce)
        (("1" (forward-chain "greatest_fixpoint1") nil nil)
         ("2" (rewrite "fixpoint_nu1") nil nil))
        nil))
      nil))
    nil)
   ((gfp? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (gfp? const-decl "bool" mucalculus nil)
    (fixpoint_nu1 formula-decl nil mucalculus_prop nil)
    (greatest_fixpoint1 formula-decl nil mucalculus_prop nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil))
   nil)
  (nu_gfp-1 nil 3324295090
   ("" (skolem!)
    (("" (expand* "gfp?" "gfp?" "fixpoint?")
      (("" (reduce)
        (("1" (forward-chain "greatest_fixpoint1") nil nil)
         ("2" (rewrite "fixpoint_nu1") nil nil))
        nil))
      nil))
    nil)
   nil nil))
(dual_dual 0
  (dual_dual-2 nil 3324308681
   ("" (grind-with-ext :rewrites ("complement_complement[T]")) nil nil)
   ((dual const-decl "[pred[T] -> pred[T]]" mucalculus_prop nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (O const-decl "T3" function_props nil)
    (complement const-decl "set" sets nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)
  (dual_dual-1 nil 3324295090
   ("" (skolem!)
    (("" (apply-extensionality :hide? t)
      (("" (grind :rewrites ("complement_complement[T]")) nil nil))
      nil))
    nil)
   nil nil))
(dual_inclusion1 0
  (dual_inclusion1-2 nil 3324308681 ("" (grind) nil nil)
   ((T formal-type-decl nil mucalculus_prop nil)
    (member const-decl "bool" sets nil)
    (complement const-decl "set" sets nil)
    (<= const-decl "bool" mucalculus nil)
    (dual const-decl "[pred[T] -> pred[T]]" mucalculus_prop nil)
    (O const-decl "T3" function_props nil))
   nil)
  (dual_inclusion1-1 nil 3324295090 ("" (grind) nil nil) nil nil))
(dual_inclusion2 0
  (dual_inclusion2-2 nil 3324308681 ("" (grind) nil nil)
   ((T formal-type-decl nil mucalculus_prop nil)
    (member const-decl "bool" sets nil)
    (complement const-decl "set" sets nil)
    (<= const-decl "bool" mucalculus nil)
    (dual const-decl "[pred[T] -> pred[T]]" mucalculus_prop nil)
    (O const-decl "T3" function_props nil))
   nil)
  (dual_inclusion2-1 nil 3324295090 ("" (grind) nil nil) nil nil))
(dual_inclusion3 0
  (dual_inclusion3-2 nil 3324308681
   ("" (grind :rewrites ("complement_complement[T]")) nil nil)
   ((complement const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (O const-decl "T3" function_props nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (dual const-decl "[pred[T] -> pred[T]]" mucalculus_prop nil)
    (<= const-decl "bool" mucalculus nil))
   nil)
  (dual_inclusion3-1 nil 3324295090
   ("" (grind :rewrites ("complement_complement[T]")) nil nil) nil
   nil))
(dual_inclusion4 0
  (dual_inclusion4-2 nil 3324308681
   ("" (grind :rewrites ("complement_complement[T]")) nil nil)
   ((complement const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (O const-decl "T3" function_props nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (dual const-decl "[pred[T] -> pred[T]]" mucalculus_prop nil)
    (<= const-decl "bool" mucalculus nil))
   nil)
  (dual_inclusion4-1 nil 3324295090
   ("" (grind :rewrites ("complement_complement[T]")) nil nil) nil
   nil))
(monotonic_dual_monotonic 0
  (monotonic_dual_monotonic-2 nil 3324308681
   ("" (grind :if-match nil)
    (("" (inst - "complement(p2!1)" "complement(p1!1)")
      (("" (reduce :polarity? t) nil nil)) nil))
    nil)
   ((set type-eq-decl nil sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (pred type-eq-decl nil defined_types nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (complement const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (O const-decl "T3" function_props nil)
    (<= const-decl "bool" mucalculus nil)
    (dual const-decl "[pred[T] -> pred[T]]" mucalculus_prop nil))
   nil)
  (monotonic_dual_monotonic-1 nil 3324295090
   ("" (grind :if-match nil)
    (("" (inst - "complement(p2!1)" "complement(p1!1)")
      (("" (reduce :polarity? t) nil nil)) nil))
    nil)
   nil nil))
(least_fixpoint_dual 0
  (least_fixpoint_dual-2 nil 3324308681
   ("" (skolem!)
    ((""
      (case "mu(dual(F!1)) <= complement(nu(F!1)) AND complement(mu(dual(F!1))) <= nu(F!1)")
      (("1" (grind-with-ext :exclude ("mu" "nu" "dual")) nil nil)
       ("2"
        (auto-rewrite "dual_inclusion1" "dual_inclusion2" "dual_dual"
                      "smallest_closed" "largest_closed" "closure_nu"
                      "closure_mu")
        (("2" (ground) nil nil)) nil))
      nil))
    nil)
   ((nu const-decl "pred[T]" mucalculus nil)
    (complement const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (dual const-decl "[pred[T] -> pred[T]]" mucalculus_prop nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (<= const-decl "bool" mucalculus nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (mu_lfp application-judgement "(lfp?(F))" mucalculus_prop nil)
    (nu_gfp application-judgement "(gfp?(F))" mucalculus_prop nil)
    (monotonic_dual_monotonic application-judgement "(monotonic?[T])"
     mucalculus_prop nil)
    (member const-decl "bool" sets nil)
    (closure_mu formula-decl nil mucalculus_prop nil)
    (dual_inclusion2 formula-decl nil mucalculus_prop nil)
    (largest_closed formula-decl nil mucalculus_prop nil)
    (dual_dual formula-decl nil mucalculus_prop nil)
    (closure_nu formula-decl nil mucalculus_prop nil)
    (dual_inclusion1 formula-decl nil mucalculus_prop nil)
    (smallest_closed formula-decl nil mucalculus_prop nil))
   nil)
  (least_fixpoint_dual-1 nil 3324295090
   ("" (skolem!)
    ((""
      (case "mu(dual(F!1)) <= complement(nu(F!1)) AND complement(mu(dual(F!1))) <= nu(F!1)")
      (("1" (apply-extensionality :hide? t)
        (("1" (grind :exclude ("mu" "nu" "dual")) nil nil)) nil)
       ("2"
        (auto-rewrite "dual_inclusion1" "dual_inclusion2" "dual_dual"
                      "smallest_closed" "largest_closed" "closure_nu"
                      "closure_mu")
        (("2" (ground) nil nil)) nil))
      nil))
    nil)
   nil nil))
(greatest_fixpoint_dual 0
  (greatest_fixpoint_dual-2 nil 3324308681
   ("" (skolem!)
    ((""
      (case "complement(mu(F!1)) <= nu(dual(F!1)) AND mu(F!1) <= complement(nu(dual(F!1)))")
      (("1" (grind-with-ext :exclude ("mu" "nu" "dual")) nil nil)
       ("2"
        (auto-rewrite "dual_inclusion1" "dual_inclusion2" "dual_dual"
                      "smallest_closed" "largest_closed" "closure_nu"
                      "closure_mu")
        (("2" (ground) nil nil)) nil))
      nil))
    nil)
   ((dual const-decl "[pred[T] -> pred[T]]" mucalculus_prop nil)
    (nu const-decl "pred[T]" mucalculus nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (complement const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (<= const-decl "bool" mucalculus nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil mucalculus_prop nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nu_gfp application-judgement "(gfp?(F))" mucalculus_prop nil)
    (monotonic_dual_monotonic application-judgement "(monotonic?[T])"
     mucalculus_prop nil)
    (mu_lfp application-judgement "(lfp?(F))" mucalculus_prop nil)
    (member const-decl "bool" sets nil)
    (closure_nu formula-decl nil mucalculus_prop nil)
    (dual_inclusion1 formula-decl nil mucalculus_prop nil)
    (smallest_closed formula-decl nil mucalculus_prop nil)
    (dual_dual formula-decl nil mucalculus_prop nil)
    (closure_mu formula-decl nil mucalculus_prop nil)
    (dual_inclusion2 formula-decl nil mucalculus_prop nil)
    (largest_closed formula-decl nil mucalculus_prop nil))
   nil)
  (greatest_fixpoint_dual-1 nil 3324295090
   ("" (skolem!)
    ((""
      (case "complement(mu(F!1)) <= nu(dual(F!1)) AND mu(F!1) <= complement(nu(dual(F!1)))")
      (("1" (apply-extensionality :hide? t)
        (("1" (grind :exclude ("mu" "nu" "dual")) nil nil)) nil)
       ("2"
        (auto-rewrite "dual_inclusion1" "dual_inclusion2" "dual_dual"
                      "smallest_closed" "largest_closed" "closure_nu"
                      "closure_mu")
        (("2" (ground) nil nil)) nil))
      nil))
    nil)
   nil nil)))

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.