Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: T6394563.empty.out Sprache: Lisp

Original von: PVS^©

(new_mucalculus_prop
(leq_equals_subset 0
  (leq_equals_subset-1 nil 3318705433
   ("" (expand* "<=" "subset?" "member") nil nil)
   ((member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (<= const-decl "bool" mucalculus nil))
   shostak))
(monotonic_is_monotone 0
  (monotonic_is_monotone-1 nil 3318705390 ("" (judgement-tcc) nil nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (<= const-decl "bool" mucalculus nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (monotone? const-decl "bool" fixed_points nil))
   nil))
(leq_is_complete_lattice 0
  (leq_is_complete_lattice-1 nil 3318705390
   ("" (rewrite "leq_equals_subset") (("" (assert) nil nil)) nil)
   ((subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (leq_equals_subset formula-decl nil new_mucalculus_prop nil))
   nil))
(fixpoint_equals_fixed_point 0
  (fixpoint_equals_fixed_point-1 nil 3318705472
   ("" (skolem!)
    (("" (expand* "fixpoint?" "fixpoint?" "fixed_point?") nil nil))
    nil)
   ((fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (fixed_point? const-decl "bool" fixed_points nil))
   shostak))
(fixpoint2_equals_fixed_point 0
  (fixpoint2_equals_fixed_point-1 nil 3318705503
   ("" (skolem!) (("" (expand* "fixpoint?" "fixed_point?") nil nil))
    nil)
   ((fixpoint? const-decl "bool" mucalculus nil)
    (fixed_point? const-decl "bool" fixed_points nil))
   shostak))
(antisymmetry 0
  (antisymmetry-1 nil 3318705539 ("" (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 new_mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil)
    (<= const-decl "bool" mucalculus nil))
   shostak))
(reflexivity 0
  (reflexivity-1 nil 3318705554 ("" (grind) nil nil)
   ((<= const-decl "bool" mucalculus nil)) shostak))
(glb_equals_glb 0
  (glb_equals_glb-1 nil 3318705716
   ("" (decompose-equality)
    (("" (decompose-equality)
      (("" (rewrite "subset_equals_pointwise_implies")
        (("" (expand "restrict")
          (("" (rewrite "glb_pointwise_def")
            (("1" (assert)
              (("1"
                (invoke (case "greatest_lower_bound?(%1, %2, IMPLIES)")
                 (! 1 l) (! 1 r 1))
                (("1" (use "glb_def[bool]")
                  (("1" (assert) nil nil)
                   ("2" (expand "greatest_bounded_below?")
                    (("2" (inst?) nil nil)) nil))
                  nil)
                 ("2" (hide 2)
                  (("2"
                    (expand* "glb" "member" "greatest_lower_bound?")
                    (("2" (split)
                      (("1" (expand "lower_bound?")
                        (("1" (skosimp* t)
                          (("1" (inst?) (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (skosimp* t)
                        (("2" (expand "lower_bound?")
                          (("2" (inst - "p!1(x!2)")
                            (("1" (assert) nil nil)
                             ("2" (inst?) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (skolem!)
              (("2" (rewrite "all_greatest_bounded[bool]") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((all_greatest_bounded formula-decl nil bounded_orders nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (p!1 skolem-const-decl "pred[T]" new_mucalculus_prop nil)
    (member const-decl "bool" sets nil)
    (glb_def formula-decl nil bounded_orders nil)
    (x!2 skolem-const-decl "T" new_mucalculus_prop nil)
    (x!1 skolem-const-decl "[[T -> boolean] -> boolean]"
     new_mucalculus_prop nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (glb_pointwise_def formula-decl nil pointwise_orders nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pointwise_preserves_complete_lattices application-judgement
     "(complete_lattice?[[T -> bool]])" new_mucalculus_prop nil)
    (implies_is_total_order name-judgement "(total_order?[bool])"
     booleans_are_finite nil)
    (subset_equals_pointwise_implies formula-decl nil
     sets_complete_lattices nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil)
    (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
     bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (restrict const-decl "R" restrict nil)
    (subset? const-decl "bool" sets nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (set type-eq-decl nil sets nil)
    (glb const-decl "pred[T]" mucalculus nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil))
   shostak))
(glb_lower_bound 0
  (glb_lower_bound-1 nil 3318705901
   ("" (skolem!)
    (("" (rewrite "glb_equals_glb")
      (("" (expand "restrict")
        (("" (rewrite "leq_equals_subset")
          (("" (use "glb_le[set[T]]") nil nil)) nil))
        nil))
      nil))
    nil)
   ((glb_equals_glb formula-decl nil new_mucalculus_prop nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (leq_equals_subset formula-decl nil new_mucalculus_prop nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (glb_le formula-decl nil bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (subset? const-decl "bool" sets nil)
    (pred type-eq-decl nil defined_types nil)
    (restrict const-decl "R" restrict nil))
   shostak))
(glb_greatest_lower_bound 0
  (glb_greatest_lower_bound-1 nil 3318706358
   ("" (skolem!)
    (("" (rewrite "leq_equals_subset")
      (("" (rewrite "glb_equals_glb")
        (("" (expand "restrict")
          (("" (rewrite "glb_ge")
            (("" (expand "lower_bound?") (("" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((leq_equals_subset formula-decl nil new_mucalculus_prop nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (restrict const-decl "R" restrict nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (subset? const-decl "bool" sets nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (pred type-eq-decl nil defined_types nil)
    (glb_ge formula-decl nil bounded_orders nil)
    (glb_equals_glb formula-decl nil new_mucalculus_prop nil))
   shostak))
(lub_equals_lub 0
  (lub_equals_lub-1 nil 3318706402
   ("" (decompose-equality)
    (("" (decompose-equality)
      (("" (expand "restrict")
        (("" (rewrite "subset_equals_pointwise_implies")
          (("" (rewrite "lub_pointwise_def")
            (("1" (assert)
              (("1"
                (invoke (case "least_upper_bound?(%1, %2, IMPLIES)")
                 (! 1 l) (! 1 r 1))
                (("1" (use "lub_def[bool]")
                  (("1" (assert) nil nil)
                   ("2" (expand "least_bounded_above?")
                    (("2" (inst?) nil nil)) nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (expand* "lub" "member" "least_upper_bound?")
                    (("2" (split)
                      (("1" (expand "upper_bound?")
                        (("1" (skosimp* t)
                          (("1" (inst?) (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (skosimp*)
                        (("2" (expand "upper_bound?")
                          (("2" (inst - "p!1(x!2)")
                            (("1" (assert) nil nil)
                             ("2" (inst?) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (skolem!)
              (("2" (rewrite "all_least_bounded") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subset_equals_pointwise_implies formula-decl nil
     sets_complete_lattices nil)
    (implies_is_total_order name-judgement "(total_order?[bool])"
     booleans_are_finite nil)
    (pointwise_preserves_complete_lattices application-judgement
     "(complete_lattice?[[T -> bool]])" new_mucalculus_prop nil)
    (all_least_bounded formula-decl nil bounded_orders nil)
    (complete_upper_semilattice? const-decl "bool" bounded_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (p!1 skolem-const-decl "pred[T]" new_mucalculus_prop nil)
    (member const-decl "bool" sets nil)
    (lub_def formula-decl nil bounded_orders nil)
    (x!2 skolem-const-decl "T" new_mucalculus_prop nil)
    (x!1 skolem-const-decl "[[T -> boolean] -> boolean]"
     new_mucalculus_prop nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (lub_pointwise_def formula-decl nil pointwise_orders nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil)
    (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
     bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (restrict const-decl "R" restrict nil)
    (subset? const-decl "bool" sets nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (set type-eq-decl nil sets nil)
    (lub const-decl "pred[T]" mucalculus nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil))
   shostak))
(lub_upper_bound 0
  (lub_upper_bound-1 nil 3318706647
   ("" (skolem!)
    (("" (rewrite "lub_equals_lub")
      (("" (expand "restrict")
        (("" (rewrite "leq_equals_subset")
          (("" (use "lub_ge[set[T]]") nil nil)) nil))
        nil))
      nil))
    nil)
   ((lub_equals_lub formula-decl nil new_mucalculus_prop nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (leq_equals_subset formula-decl nil new_mucalculus_prop nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (lub_ge formula-decl nil bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (subset? const-decl "bool" sets nil)
    (pred type-eq-decl nil defined_types nil)
    (restrict const-decl "R" restrict nil))
   shostak))
(lub_least_upper_bound 0
  (lub_least_upper_bound-1 nil 3318706676
   ("" (skolem!)
    (("" (rewrite "leq_equals_subset")
      (("" (rewrite "lub_equals_lub")
        (("" (expand "restrict")
          (("" (rewrite "lub_le")
            (("" (expand "upper_bound?") (("" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((leq_equals_subset formula-decl nil new_mucalculus_prop nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (restrict const-decl "R" restrict nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (subset? const-decl "bool" sets nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (pred type-eq-decl nil defined_types nil)
    (lub_le formula-decl nil bounded_orders nil)
    (lub_equals_lub formula-decl nil new_mucalculus_prop nil))
   shostak))
(mu_equals_least_prefixed_point_TCC1 0
  (mu_equals_least_prefixed_point_TCC1-1 nil 3318705390
   ("" (skolem!) (("" (rewrite "all_greatest_bounded") nil nil)) nil)
   ((leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (all_greatest_bounded formula-decl nil bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (prefixed_point? const-decl "bool" fixed_points nil)
    (<= const-decl "bool" mucalculus nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil))
   nil))
(mu_equals_least_prefixed_point 0
  (mu_equals_least_prefixed_point-1 nil 3318706756
   ("" (skolem!)
    (("" (expand* "mu" "lfp" "prefixed_point?")
      (("" (rewrite "glb_equals_glb")
        (("" (expand "restrict")
          (("" (rewrite "leq_equals_subset") nil nil)) nil))
        nil))
      nil))
    nil)
   ((lfp const-decl "pred[T]" mucalculus nil)
    (prefixed_point? const-decl "bool" fixed_points nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (restrict const-decl "R" restrict nil)
    (leq_equals_subset formula-decl nil new_mucalculus_prop nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (glb_equals_glb formula-decl nil new_mucalculus_prop nil))
   shostak))
(smallest_closed 0
  (smallest_closed-1 nil 3318706785
   ("" (skosimp :preds? t)
    (("" (rewrite "mu_equals_least_prefixed_point")
      (("" (rewrite "leq_equals_subset")
        (("" (rewrite "glb_le")
          (("" (expand "prefixed_point?") (("" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((mu_equals_least_prefixed_point formula-decl nil
     new_mucalculus_prop nil)
    (leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (set type-eq-decl nil sets nil)
    (prefixed_point? const-decl "bool" fixed_points nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (subset? const-decl "bool" sets nil)
    (glb_le formula-decl nil bounded_orders nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (leq_equals_subset formula-decl nil new_mucalculus_prop 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 new_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))
   shostak))
(fixpoint_mu2 0
  (fixpoint_mu2-1 nil 3318706824
   ("" (skolem!)
    (("" (use "monotonic_is_monotone")
      (("" (rewrite "fixpoint_equals_fixed_point")
        (("" (rewrite "mu_equals_least_prefixed_point")
          (("" (rewrite "leq_equals_subset")
            (("" (use "least_prefixed_point_is_fixed_point")
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((monotonic_is_monotone judgement-tcc nil new_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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (mu_equals_least_prefixed_point formula-decl nil
     new_mucalculus_prop nil)
    (leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (set type-eq-decl nil sets nil)
    (least_prefixed_point_is_fixed_point formula-decl nil fixed_points
     nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (subset? const-decl "bool" sets nil)
    (monotone? const-decl "bool" fixed_points nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
     bounded_orders nil)
    (prefixed_point? const-decl "bool" fixed_points nil)
    (implies_is_total_order name-judgement "(total_order?[bool])"
     booleans_are_finite nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (leq_equals_subset formula-decl nil new_mucalculus_prop nil)
    (fixpoint_equals_fixed_point formula-decl nil new_mucalculus_prop
     nil))
   shostak))
(fixpoint_mu1 0
  (fixpoint_mu1-1 nil 3318706885
   ("" (lemma "fixpoint_mu2")
    (("" (expand* "fixpoint?" "fixpoint?") nil nil)) nil)
   ((fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint_mu2 formula-decl nil new_mucalculus_prop nil))
   shostak))
(closure_mu 0
  (closure_mu-1 nil 3318706909
   ("" (skolem!)
    (("" (rewrite "leq_equals_subset")
      (("" (use "subset_reflexive[T]")
        (("" (rewrite "fixpoint_mu1") nil nil)) nil))
      nil))
    nil)
   ((leq_equals_subset formula-decl nil new_mucalculus_prop nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (fixpoint_mu1 formula-decl nil new_mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (subset_reflexive formula-decl nil sets_lemmas nil)
    (T formal-type-decl nil new_mucalculus_prop nil))
   shostak))
(least_fixpoint2 0
  (least_fixpoint2-1 nil 3318707381
   ("" (skosimp)
    (("" (rewrite "mu_equals_least_prefixed_point")
      (("" (rewrite "leq_equals_subset")
        (("" (rewrite "glb_le")
          (("" (hide 2)
            (("" (expand* "prefixed_point?" "fixpoint?" "fixpoint?")
              (("" (use "reflexivity[set[T]]")
                (("" (rewrite "leq_equals_subset")
                  (("" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((mu_equals_least_prefixed_point formula-decl nil
     new_mucalculus_prop nil)
    (T formal-type-decl nil new_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)
    (leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (glb_le formula-decl nil bounded_orders nil)
    (subset? const-decl "bool" sets nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (prefixed_point? const-decl "bool" fixed_points nil)
    (set type-eq-decl nil sets nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (reflexivity formula-decl nil new_mucalculus_prop nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (leq_equals_subset formula-decl nil new_mucalculus_prop nil))
   shostak))
(least_fixpoint1 0
  (least_fixpoint1-1 nil 3318707450
   ("" (lemma "least_fixpoint2")
    (("" (expand* "fixpoint?" "fixpoint?") nil nil)) nil)
   ((fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (least_fixpoint2 formula-decl nil new_mucalculus_prop nil))
   shostak))
(lfp_equals_lfp 0
  (lfp_equals_lfp-1 nil 3318707470
   ("" (skolem!)
    (("" (decompose-equality)
      (("" (iff)
        (("" (expand* "lfp?" "lfp?" "least?" "lower_bound?")
          (("" (auto-rewrite "fixpoint2_equals_fixed_point")
            (("" (assert)
              (("" (prop)
                (("1" (skolem-typepred)
                  (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
                 ("2" (skosimp) (("2" (inst?) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop 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)
    (lfp? const-decl "bool" mucalculus nil)
    (set type-eq-decl nil sets nil)
    (lfp? const-decl "bool" fixed_points nil)
    (<= const-decl "bool" mucalculus nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (lfp? const-decl "bool" mucalculus nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (least? const-decl "bool" minmax_orders nil)
    (fixpoint2_equals_fixed_point formula-decl nil new_mucalculus_prop
     nil)
    (F!1 skolem-const-decl "(monotonic?[T])" new_mucalculus_prop nil)
    (p2!1 skolem-const-decl "pred[T]" new_mucalculus_prop nil)
    (fixed_point? const-decl "bool" fixed_points nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (implies_is_total_order name-judgement "(total_order?[bool])"
     booleans_are_finite nil))
   shostak))
(mu_lfp 0
  (mu_lfp-1 nil 3318705390
   ("" (skolem!)
    (("" (rewrite "lfp_equals_lfp")
      (("" (rewrite "mu_equals_least_prefixed_point")
        (("" (rewrite "leq_equals_subset")
          (("" (rewrite "least_prefixed_point") (("" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lfp_equals_lfp formula-decl nil new_mucalculus_prop nil)
    (T formal-type-decl nil new_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)
    (leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (leq_equals_subset formula-decl nil new_mucalculus_prop nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (set type-eq-decl nil sets nil)
    (monotone? const-decl "bool" fixed_points nil)
    (prefixed_point? const-decl "bool" fixed_points nil)
    (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
     bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (subset? const-decl "bool" sets nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (least_prefixed_point formula-decl nil fixed_points nil)
    (mu_equals_least_prefixed_point formula-decl nil
     new_mucalculus_prop nil))
   nil))
(monotonic_dual_monotonic 0
  (monotonic_dual_monotonic-1 nil 3318705390
   ("" (skolem-typepred)
    (("" (expand* "monotonic?" "dual" "o")
      (("" (skosimp)
        (("" (inst - "C!1(p2!1)" "C!1(p1!1)")
          (("" (rewrite "le_complement")
            (("" (assert)
              (("" (use "le_complement") (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dual const-decl "[T -> T]" complementary_lattices nil)
    (O const-decl "T3" function_props nil)
    (implies_is_total_order name-judgement "(total_order?[bool])"
     booleans_are_finite nil)
    (leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (le_complement formula-decl nil complementary_orders nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (<= const-decl "bool" mucalculus nil)
    (complement? const-decl "bool" complementary_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil new_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))
   nil))
(least_fixpoint_dual 0
  (least_fixpoint_dual-1 nil 3318724423
   ("" (skolem-typepred)
    (("" (expand* "mu" "lfp" "nu" "gfp")
      (("" (rewrite "leq_equals_subset")
        (("" (rewrite "glb_equals_glb")
          (("" (expand "restrict")
            (("" (rewrite "lub_equals_lub")
              (("" (use "glb_complement")
                ((""
                  (invoke (then (case-replace "%1 = %2") (assert))
                   (! -1 r 1 1) (! 1 r 1 1))
                  (("1" (expand "restrict") (("1" (propax) nil nil))
                    nil)
                   ("2" (hide-all-but 1)
                    (("2" (decompose-equality)
                      (("2" (expand "image")
                        (("2" (iff)
                          (("2" (prop)
                            (("1" (skolem-typepred)
                              (("1"
                                (use "dual_inclusion3")
                                (("1"
                                  (rewrite "leq_equals_subset")
                                  (("1"
                                    (rewrite "dual_dual")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (inst + "C!1(x!1)")
                              (("1"
                                (rewrite "complement_complement")
                                nil
                                nil)
                               ("2"
                                (use "dual_inclusion4")
                                (("2"
                                  (rewrite "leq_equals_subset")
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lfp const-decl "pred[T]" mucalculus nil)
    (gfp const-decl "pred[T]" mucalculus nil)
    (nu const-decl "pred[T]" mucalculus nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (glb_equals_glb formula-decl nil new_mucalculus_prop nil)
    (lub_equals_lub formula-decl nil new_mucalculus_prop nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (image const-decl "set[R]" function_image nil)
    (F!1 skolem-const-decl "(monotonic?[T])" new_mucalculus_prop nil)
    (x!1 skolem-const-decl "[T -> boolean]" new_mucalculus_prop nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (dual_inclusion4 formula-decl nil complementary_lattices nil)
    (dual_dual formula-decl nil complementary_lattices nil)
    (dual_inclusion3 formula-decl nil complementary_lattices nil)
    (monotonic_dual_monotonic application-judgement "(monotonic?[T])"
     new_mucalculus_prop nil)
    (C!1 skolem-const-decl "(complement?(<=))" new_mucalculus_prop nil)
    (leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (dual const-decl "[T -> T]" complementary_lattices nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (subset? const-decl "bool" sets nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (glb_complement formula-decl nil complementary_orders nil)
    (restrict const-decl "R" restrict nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset_is_a_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (leq_equals_subset formula-decl nil new_mucalculus_prop nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (<= const-decl "bool" mucalculus nil)
    (complement? const-decl "bool" complementary_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil new_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))
   shostak))
(greatest_fixpoint_dual 0
  (greatest_fixpoint_dual-1 nil 3318724891
   ("" (skolem!)
    ((""
      (case-replace
       "C!1(mu(F!1)) = C!1(mu(dual(C!1)(dual(C!1)(F!1))))")
      (("1" (hide -1)
        (("1" (rewrite "least_fixpoint_dual")
          (("1" (rewrite "complement_complement") nil nil)) nil))
        nil)
       ("2" (rewrite "dual_dual") nil nil))
      nil))
    nil)
   ((monotonic_dual_monotonic application-judgement "(monotonic?[T])"
     new_mucalculus_prop nil)
    (leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pred type-eq-decl nil defined_types nil)
    (complement? const-decl "bool" complementary_orders nil)
    (<= const-decl "bool" mucalculus nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (dual const-decl "[T -> T]" complementary_lattices nil)
    (least_fixpoint_dual formula-decl nil new_mucalculus_prop nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (nu const-decl "pred[T]" mucalculus nil)
    (dual_dual formula-decl nil complementary_lattices nil))
   shostak))
(complement_is_complement 0
  (complement_is_complement-1 nil 3318705390
   ("" (judgement-tcc)
    (("" (decompose-equality) (("" (decompose-equality) nil nil)) nil))
    nil)
   ((id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (O const-decl "T3" function_props nil)
    (reflexive_converse application-judgement "(reflexive?[T])"
     relation_converse_props nil)
    (antisymmetric_converse application-judgement "(antisymmetric?[T])"
     relation_converse_props nil)
    (transitive_converse application-judgement "(transitive?[T])"
     relation_converse_props nil)
    (preorder_converse application-judgement "(preorder?[T])"
     relation_converse_props nil)
    (partial_order_converse application-judgement "(partial_order?[T])"
     relation_converse_props nil)
    (leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (complement? const-decl "bool" complementary_orders nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (preserves const-decl "bool" functions nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (complement const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (<= const-decl "bool" mucalculus nil))
   nil))
(closure_nu 0
  (closure_nu-1 nil 3318724967
   ("" (skolem!)
    ((""
      (case-replace
       "nu(F!1) = nu(dual(complement)(dual(complement)(F!1)))")
      (("1" (rewrite "greatest_fixpoint_dual")
        (("1" (use "closure_mu")
          (("1" (use "dual_inclusion2") (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (rewrite "dual_dual") nil nil))
      nil))
    nil)
   ((complement_is_complement name-judgement "(complement?(<=))"
     new_mucalculus_prop nil)
    (monotonic_dual_monotonic application-judgement "(monotonic?[T])"
     new_mucalculus_prop nil)
    (leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (T formal-type-decl nil new_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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (nu const-decl "pred[T]" mucalculus nil)
    (set type-eq-decl nil sets nil)
    (<= const-decl "bool" mucalculus nil)
    (dual const-decl "[T -> T]" complementary_lattices nil)
    (complement const-decl "set" sets nil)
    (closure_mu formula-decl nil new_mucalculus_prop nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (dual_inclusion2 formula-decl nil complementary_lattices nil)
    (mu_lfp application-judgement "(lfp?(F))" new_mucalculus_prop nil)
    (greatest_fixpoint_dual formula-decl nil new_mucalculus_prop nil)
    (complement? const-decl "bool" complementary_orders nil)
    (dual_dual formula-decl nil complementary_lattices nil))
   shostak))
(largest_closed 0
  (largest_closed-1 nil 3318725016
   ("" (skosimp)
    ((""
      (case-replace
       "nu(F!1) = nu(dual(complement)(dual(complement)(F!1)))")
      (("1" (rewrite "greatest_fixpoint_dual")
        (("1" (lemma "le_complement")
          (("1"
            (inst - "<=" "complement(p!1)" "mu(dual(complement)(F!1))"
             "complement")
            (("1" (use "complement_complement")
              (("1" (assert)
                (("1" (rewrite "smallest_closed")
                  (("1" (use "dual_inclusion4")
                    (("1" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (rewrite "dual_dual") nil nil))
      nil))
    nil)
   ((complement_is_complement name-judgement "(complement?(<=))"
     new_mucalculus_prop nil)
    (monotonic_dual_monotonic application-judgement "(monotonic?[T])"
     new_mucalculus_prop nil)
    (leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (T formal-type-decl nil new_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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (nu const-decl "pred[T]" mucalculus nil)
    (set type-eq-decl nil sets nil)
    (<= const-decl "bool" mucalculus nil)
    (dual const-decl "[T -> T]" complementary_lattices nil)
    (complement const-decl "set" sets nil)
    (le_complement formula-decl nil complementary_orders nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (smallest_closed formula-decl nil new_mucalculus_prop nil)
    (dual_inclusion4 formula-decl nil complementary_lattices nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (mu_lfp application-judgement "(lfp?(F))" new_mucalculus_prop nil)
    (greatest_fixpoint_dual formula-decl nil new_mucalculus_prop nil)
    (complement? const-decl "bool" complementary_orders nil)
    (dual_dual formula-decl nil complementary_lattices nil))
   shostak))
(fixpoint_nu1 0
  (fixpoint_nu1-1 nil 3318725241
   ("" (skolem!)
    ((""
      (case-replace
       "nu(F!1) = nu(dual(complement)(dual(complement)(F!1)))")
      (("1" (rewrite "greatest_fixpoint_dual")
        (("1" (use "fixpoint_mu1")
          (("1" (expand "dual" -1 1)
            (("1" (expand "o")
              (("1" (lemma "complement_complement")
                (("1" (invoke (inst - "<=" "%1" "complement") (! 1 l))
                  (("1" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (rewrite "dual_dual") nil nil))
      nil))
    nil)
   ((complement_is_complement name-judgement "(complement?(<=))"
     new_mucalculus_prop nil)
    (monotonic_dual_monotonic application-judgement "(monotonic?[T])"
     new_mucalculus_prop nil)
    (leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (T formal-type-decl nil new_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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (nu const-decl "pred[T]" mucalculus nil)
    (set type-eq-decl nil sets nil)
    (<= const-decl "bool" mucalculus nil)
    (dual const-decl "[T -> T]" complementary_lattices nil)
    (complement const-decl "set" sets nil)
    (fixpoint_mu1 formula-decl nil new_mucalculus_prop nil)
    (O const-decl "T3" function_props nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (mu_lfp application-judgement "(lfp?(F))" new_mucalculus_prop nil)
    (greatest_fixpoint_dual formula-decl nil new_mucalculus_prop nil)
    (complement? const-decl "bool" complementary_orders nil)
    (dual_dual formula-decl nil complementary_lattices nil))
   shostak))
(fixpoint_nu2 0
  (fixpoint_nu2-1 nil 3318725319
   ("" (skolem!)
    (("" (expand* "fixpoint?" "fixpoint?")
      (("" (use "fixpoint_nu1") nil nil)) nil))
    nil)
   ((fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint_nu1 formula-decl nil new_mucalculus_prop nil)
    (T formal-type-decl nil new_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))
   shostak))
(greatest_fixpoint1 0
  (greatest_fixpoint1-1 nil 3318725348
   ("" (skosimp)
    ((""
      (case-replace
       "nu(F!1) = nu(dual(complement)(dual(complement)(F!1)))")
      (("1" (rewrite "greatest_fixpoint_dual")
        (("1" (lemma "least_fixpoint1")
          (("1" (inst - "dual(complement)(F!1)" "complement(p!1)")
            (("1" (expand "dual" -1 1)
              (("1" (expand "o")
                (("1" (lemma "complement_complement")
                  (("1" (inst - "<=" _ _)
                    (("1" (inst?)
                      (("1" (assert)
                        (("1" (lemma "le_complement")
                          (("1"
                            (inst - "<=" "complement(p!1)"
                             "mu(dual(complement)(F!1))" "complement")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (rewrite "dual_dual") nil nil))
      nil))
    nil)
   ((complement_is_complement name-judgement "(complement?(<=))"
     new_mucalculus_prop nil)
    (monotonic_dual_monotonic application-judgement "(monotonic?[T])"
     new_mucalculus_prop nil)
    (leq_is_complete_lattice name-judgement
     "(complete_lattice?[set[T]])" new_mucalculus_prop nil)
    (T formal-type-decl nil new_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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (nu const-decl "pred[T]" mucalculus nil)
    (set type-eq-decl nil sets nil)
    (<= const-decl "bool" mucalculus nil)
    (dual const-decl "[T -> T]" complementary_lattices nil)
    (complement const-decl "set" sets nil)
    (least_fixpoint1 formula-decl nil new_mucalculus_prop nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (le_complement formula-decl nil complementary_orders nil)
    (mu const-decl "pred[T]" mucalculus nil)
    (implies_is_total_order name-judgement "(total_order?[bool])"
     booleans_are_finite nil)
    (O const-decl "T3" function_props nil)
    (mu_lfp application-judgement "(lfp?(F))" new_mucalculus_prop nil)
    (greatest_fixpoint_dual formula-decl nil new_mucalculus_prop nil)
    (complement? const-decl "bool" complementary_orders nil)
    (dual_dual formula-decl nil complementary_lattices nil))
   shostak))
(greatest_fixpoint2 0
  (greatest_fixpoint2-1 nil 3318725433
   ("" (skosimp)
    (("" (expand* "fixpoint?" "fixpoint?")
      (("" (forward-chain "greatest_fixpoint1") nil nil)) nil))
    nil)
   ((fixpoint? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (monotonic? const-decl "bool" mucalculus nil)
    (predicate_transformer type-eq-decl nil mucalculus nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil new_mucalculus_prop nil)
    (greatest_fixpoint1 formula-decl nil new_mucalculus_prop nil))
   shostak))
(nu_gfp 0
  (nu_gfp-1 nil 3318705390
   ("" (skolem!)
    (("" (expand* "gfp?" "gfp?" "fixpoint?")
      (("" (prop)
        (("1" (rewrite "fixpoint_nu1") nil nil)
         ("2" (skosimp) (("2" (rewrite "greatest_fixpoint1") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((gfp? const-decl "bool" mucalculus nil)
    (fixpoint? const-decl "bool" mucalculus nil)
    (gfp? const-decl "bool" mucalculus nil)
    (greatest_fixpoint1 formula-decl nil new_mucalculus_prop nil)
    (fixpoint_nu1 formula-decl nil new_mucalculus_prop nil)
    (T formal-type-decl nil new_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)))

¤ Dauer der Verarbeitung: 0.94 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.