|
(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)))
¤ Dauer der Verarbeitung: 0.36 Sekunden
(vorverarbeitet)
¤
|
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.
|
