| products/sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: zorn.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(zorn
(maximal_upto_subset 0 (maximal_upto_subset-1 nil 3314731234 ("" (skolem!) (("" (typepred "<=") (("" (grind :if-match nil) (("1" (inst -5 "r!1") (("1" (assert) (("1" (skosimp) (("1" (inst - "x!1" "t!1" "r!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst + "r!1") (("2" (inst - "t!1") (("2" (inst - "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= formal-const-decl "(partial_order?[T])" zorn nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil zorn nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (set type-eq-decl nil sets nil) (subset? const-decl "bool" sets nil) (upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (reflexive_closure const-decl "(reflexive?)" closure_ops nil) (maximal? const-decl "bool" minmax_orders nil) (/= const-decl "boolean" notequal nil) (fullset const-decl "set" sets nil) (antisymmetric? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (reflexive? const-decl "bool" relations nil)) shostak)) (bounded_chain_upto 0 (bounded_chain_upto-1 nil 3314731357 ("" (skosimp* t) (("" (inst?) (("" (expand* "bounded_above?" "upper_bound?") (("" (skolem!) (("" (inst? +) (("" (expand* "subset?" "upto" "reflexive_closure" "union" "member") (("" (skosimp) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (reflexive_closure const-decl "(reflexive?)" closure_ops nil) (subset? const-decl "bool" sets nil) (x!1 skolem-const-decl "T" zorn nil) (ch!1 skolem-const-decl "subchain[T, <=]" zorn nil) (bounded_above? const-decl "bool" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders 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 zorn nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (chain? const-decl "bool" chain nil) (subchain nonempty-type-eq-decl nil chain_chain nil)) shostak)) (succ_TCC1 0 (succ_TCC1-1 nil 3314731120 ("" (subtype-tcc) nil nil) ((subchain nonempty-type-eq-decl nil chain_chain nil) (set type-eq-decl nil sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (restrict const-decl "R" restrict nil) (dichotomous? const-decl "bool" orders nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (partial_order? const-decl "bool" orders 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 zorn nil) (chain? const-decl "bool" chain nil) (add_set const-decl "set[T]" zorn nil) (empty? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil)) nil)) (succ_TCC2 0 (succ_TCC2-1 nil 3314731120 ("" (skosimp) (("" (typepred "choose(add_set(ch!1))") (("" (expand "add_set" -1 :occurrence 1) (("" (flatten) nil nil)) nil)) nil)) nil) ((choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (add_set const-decl "set[T]" zorn nil) (subchain nonempty-type-eq-decl nil chain_chain nil) (chain? const-decl "bool" chain nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil zorn nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (empty_succ 0 (empty_succ-1 nil 3314731591 ("" (skolem!) (("" (prop) (("1" (expand "succ") (("1" (assert) nil nil)) nil) ("2" (expand "succ") (("2" (assert) (("2" (decompose-equality) (("2" (expand* "empty?" "member") (("2" (skolem!) (("2" (inst-cp - "x!1") (("2" (iff) (("2" (prop) (("1" (expand* "add_set" "member") (("1" (flatten) nil nil)) nil) ("2" (expand* "add" "member") (("2" (assert) (("2" (typepred "choose(add_set(ch!1))") (("2" (expand "add_set" -1 :occurrence 1) (("2" (expand "member") (("2" (inst - "choose(add_set(ch!1))") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((succ const-decl "subchain" zorn nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (add_set const-decl "set[T]" zorn nil) (choose const-decl "(p)" sets nil) (add const-decl "(nonempty?)" sets nil) (nonempty? const-decl "bool" sets nil) (subchain nonempty-type-eq-decl nil chain_chain nil) (chain? const-decl "bool" chain nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil zorn nil)) shostak)) (maximal_chain_add_set 0 (maximal_chain_add_set-1 nil 3314753251 ("" (skolem!) (("" (expand* "fullset" "maximal?" "chain_incl" "add_set" "difference" "empty?" "member") (("" (prop) (("1" (skosimp :preds? t) (("1" (apply-extensionality :hide? t) (("1" (iff) (("1" (prop) (("1" (expand* "subset?" "member") (("1" (inst -4 "x!1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "x!1") (("2" (assert) (("2" (lemma "subset_chain[T, <=]" ("ch" "r!1" "S" "add(x!1, ch!1)")) (("2" (assert) (("2" (expand* "add" "subset?" "member") (("2" (skosimp) (("2" (inst - "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst + "add(x!1, ch!1)") (("2" (use "subset_add[T]") (("2" (assert) (("2" (decompose-equality) (("2" (inst?) (("2" (expand* "add" "member") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((maximal? const-decl "bool" minmax_orders nil) (add_set const-decl "set[T]" zorn nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (chain_incl const-decl "bool" chain_chain nil) (fullset const-decl "set" sets nil) (subset_add formula-decl nil sets_lemmas nil) (= const-decl "[T, T -> boolean]" equalities nil) (x!1 skolem-const-decl "T" zorn nil) (ch!1 skolem-const-decl "subchain[T, <=]" zorn nil) (TRUE const-decl "bool" booleans nil) (subchain nonempty-type-eq-decl nil chain_chain nil) (chain? const-decl "bool" chain nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil zorn nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (subset_chain formula-decl nil chain nil) (chain nonempty-type-eq-decl nil chain nil) (nonempty? const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (subset? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" zorn nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil)) shostak)) (tower?_TCC1 0 (tower?_TCC1-1 nil 3314731120 ("" (lemma "chain_TCC1[T, <=]") (("" (propax) nil nil)) nil) ((chain_TCC1 subtype-tcc nil chain nil) (T formal-type-decl nil zorn nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (pred type-eq-decl nil defined_types nil) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" zorn nil)) nil)) (tower_intersection 0 (tower_intersection-1 nil 3314753825 ("" (skosimp) (("" (expand "tower?") (("" (split) (("1" (expand* "Intersection" "member") (("1" (skolem!) (("1" (inst?) (("1" (flatten) nil nil)) nil)) nil)) nil) ("2" (skolem-typepred) (("2" (expand* "Intersection" "member") (("2" (skolem!) (("2" (inst - "a!1") (("2" (inst - "a!1") (("2" (flatten) (("2" (inst - "ch!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (expand* "Intersection" "member") (("3" (skolem!) (("3" (inst -2 "a!1") (("3" (flatten) (("3" (inst -4 "CH!1") (("3" (assert) (("3" (skolem!) (("3" (inst - "ch!1") (("3" (inst - "a!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tower? const-decl "bool" zorn nil) (chain_incl const-decl "bool" chain_chain nil) (chain_chain nonempty-type-eq-decl nil chain_chain nil) (NOT const-decl "[bool -> bool]" booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (Tow!1 skolem-const-decl "set[set[subchain]]" zorn nil) (a!1 skolem-const-decl "(Tow!1)" zorn nil) (ch!1 skolem-const-decl "(Intersection[subchain](Tow!1))" zorn nil) (member const-decl "bool" sets nil) (finite_emptyset name-judgement "finite_set[T]" zorn nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (Intersection const-decl "set" sets nil) (T formal-type-decl nil zorn 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) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (chain? const-decl "bool" chain nil) (subchain nonempty-type-eq-decl nil chain_chain nil)) shostak)) (T0_TCC1 0 (T0_TCC1-1 nil 3314731120 ("" (use "tower_intersection") (("" (assert) nil nil)) nil) ((Intersection_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (T formal-type-decl nil zorn 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) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (chain? const-decl "bool" chain nil) (subchain nonempty-type-eq-decl nil chain_chain nil) (tower? const-decl "bool" zorn nil) (tower_intersection formula-decl nil zorn nil)) nil)) (T0_smallest 0 (T0_smallest-1 nil 3314754075 ("" (skolem!) (("" (expand* "T0" "Intersection" "subset?" "member") (("" (skosimp) (("" (inst - "tow!1") nil nil)) nil)) nil)) nil) ((Intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (T0 const-decl "(tower?)" zorn nil) (T formal-type-decl nil zorn 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) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (chain? const-decl "bool" chain nil) (subchain nonempty-type-eq-decl nil chain_chain nil) (tower? const-decl "bool" zorn nil)) shostak)) (make_tower_TCC1 0 (make_tower_TCC1-1 nil 3314731120 ("" (typepred "T0") (("" (skolem-typepred) (("" (expand* "T0_comparable?" "tower?") (("" (prop) (("1" (expand* "emptyset" "subset?" "member") nil nil) ("2" (skosimp :preds? t) (("2" (split) (("1" (case "ch!1 = ch1!1") (("1" (expand "member") (("1" (inst -9 "ch!1") (("1" (assert) (("1" (flatten) (("1" (expand "subset?" 2) (("1" (expand "member") (("1" (skosimp) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (prop) (("1" (inst -8 "ch!1") nil nil) ("2" (inst - "succ(ch!1)") (("1" (assert) (("1" (apply-extensionality 3 :hide? t) (("1" (iff) (("1" (expand* "subset?" "member") (("1" (prop) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil) ("2" (inst -7 "x!1") (("2" (assert) (("2" (expand "succ" -7) (("2" (prop) (("2" (expand* "add" "member") (("2" (skosimp*) (("2" (expand "succ" -3) (("2" (prop) (("2" (expand* "add" "member") (("2" (assert) (("2" (inst - "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "ch!1") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (inst -8 "ch!1") (("2" (prop) (("2" (expand* "subset?" "member") (("2" (skosimp*) (("2" (inst - "x!2") (("2" (assert) (("2" (expand "succ" 2) (("2" (prop) (("2" (expand* "add" "member") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp :preds? t) (("3" (case "EXISTS (D: (CH!1)): subset?(succ(ch1!1), D)") (("1" (skolem!) (("1" (inst -9 "CH!1") (("1" (split) (("1" (expand* "chain_union" "extend" "Union" "subset?" "member") (("1" (prop) (("1" (skosimp*) (("1" (inst - "x!2") (("1" (assert) (("1" (inst + "D!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (inst - "ch!1") (("2" (expand "member") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (prop) (("1" (inst -8 "CH!1") (("1" (assert) (("1" (skolem!) (("1" (inst - "ch!1") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (expand* "subset?" "member") (("2" (skosimp*) (("2" (inst -10 "CH!1") (("2" (split) (("1" (inst -8 "Union(CH!1)") (("1" (inst -10 "chain_union(CH!1)") (("1" (split) (("1" (expand "chain_union") (("1" (expand "Union" -3) (("1" (skolem-typepred) (("1" (expand "extend" -1) (("1" (prop) (("1" (inst -8 "a!1") (("1" (prop) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil) ("2" (inst + "a!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "x!1") (("2" (expand "chain_union") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "chain_union(CH!1)") (("2" (expand "chain_union") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (inst - "ch!1") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T0_comparable? const-decl "bool" zorn nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (emptyset const-decl "set" sets nil) (ch1!1 skolem-const-decl "(T0_comparable?)" zorn nil) (ch!1 skolem-const-decl "({ch2 | T0(ch2) AND (subset?[T](ch2, ch1!1) OR subset?[T](succ(ch1!1), ch2))})" zorn nil) (add const-decl "(nonempty?)" sets nil) (finite_emptyset name-judgement "finite_set[T]" zorn nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" zorn nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (succ const-decl "subchain" zorn nil) (extend const-decl "R" extend nil) (Union const-decl "set" sets nil) (chain_union const-decl "subchain" chain_chain nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (FALSE const-decl "bool" booleans nil) (a!1 skolem-const-decl "(extend[set[T], subchain[T, <=], bool, FALSE](CH!1))" zorn nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (CH!1 skolem-const-decl "chain_chain[T, <=]" zorn nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" zorn nil) (chain_chain nonempty-type-eq-decl nil chain_chain nil) (chain_incl const-decl "bool" chain_chain 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 zorn nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (chain? const-decl "bool" chain nil) (subchain nonempty-type-eq-decl nil chain_chain nil) (tower? const-decl "bool" zorn nil) (T0 const-decl "(tower?)" zorn nil)) nil)) (T0_construct 0 (T0_construct-1 nil 3314757823 ("" (skolem!) (("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (lemma "T0_smallest" ("tow" "make_tower(ch!1)")) (("1" (expand* "subset?" "member") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "make_tower") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil zorn 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) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (chain? const-decl "bool" chain nil) (subchain nonempty-type-eq-decl nil chain_chain nil) (make_tower const-decl "(tower?)" zorn nil) (T0_comparable? const-decl "bool" zorn nil) (T0 const-decl "(tower?)" zorn nil) (tower? const-decl "bool" zorn nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (T0_smallest formula-decl nil zorn nil)) shostak)) (T0_comparable 0 (T0_comparable-1 nil 3314731120 ("" (skolem-typepred) (("" (typepred "T0") (("" (expand "tower?") (("" (flatten) (("" (inst - "ch!1") (("" (expand "member") (("" (assert) (("" (use "T0_construct") (("" (expand "T0_comparable?") (("" (skosimp :preds? t) (("" (replace -3 -2) (("" (expand "make_tower" -2) (("" (assert) (("" (expand* "subset?" "member") (("" (skosimp*) (("" (inst - "x!2") (("" (expand* "succ" "add" "member") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (T0_construct formula-decl nil zorn nil) (make_tower const-decl "(tower?)" zorn nil) (subset? const-decl "bool" sets nil) (succ const-decl "subchain" zorn nil) (add const-decl "(nonempty?)" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" zorn nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" zorn nil) (T0_comparable? const-decl "bool" zorn nil) (T0 const-decl "(tower?)" zorn nil) (tower? const-decl "bool" zorn nil) (subchain nonempty-type-eq-decl nil chain_chain nil) (chain? const-decl "bool" chain nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil zorn nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (T0_all_comparable 0 (T0_all_comparable-1 nil 3314758046 ("" (skolem!) (("" (lemma "T0_smallest") (("" (inst - "{ch: (T0_comparable?) | TRUE}") (("1" (expand* "extend" "subset?" "member") (("1" (inst - "ch!1") (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "T0") (("2" (expand "tower?") (("2" (prop) (("1" (expand* "extend" "member") (("1" (prop) (("1" (expand "T0_comparable?") (("1" (skosimp) (("1" (expand* "emptyset" "subset?" "member") nil nil)) nil)) nil)) nil)) nil) ("2" (skolem-typepred) (("2" (expand* "extend" "member") (("2" (prop) (("1" (inst - "ch!2") nil nil) ("2" (lemma "T0_comparable" ("ch" "ch!2")) (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp :preds? t) (("3" (expand* "extend" "member") (("3" (prop) (("1" (inst -5 "CH!1") (("1" (assert) (("1" (skolem!) (("1" (inst - "ch!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "T0_comparable?" 1) (("2" (skosimp) (("2" (expand* "chain_union" "subset?" "member" "Union") (("2" (skosimp* t) (("2" (expand "extend") (("2" (prop) (("2" (inst - "a!1") (("2" (prop) (("2" (expand "T0_comparable?" -) (("2" (inst - "ch2!1") (("2" (expand* "subset?" "member") (("2" (split) (("1" (inst - "x!1") (("1" (inst + "a!1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "x!2") (("2" (inst + "a!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T0_smallest formula-decl nil zorn nil) (NOT const-decl "[bool -> bool]" booleans nil) (emptyset const-decl "set" sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" zorn nil) (T0_comparable judgement-tcc nil zorn nil) (Union const-decl "set" sets nil) (chain_union const-decl "subchain" chain_chain nil) (CH!1 skolem-const-decl "chain_chain[T, <=]" zorn nil) (a!1 skolem-const-decl "(extend[set[T], subchain[T, <=], bool, FALSE](CH!1))" zorn nil) (chain_chain nonempty-type-eq-decl nil chain_chain nil) (chain_incl const-decl "bool" chain_chain nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (T formal-type-decl nil zorn 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) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (chain? const-decl "bool" chain nil) (subchain nonempty-type-eq-decl nil chain_chain nil) (tower? const-decl "bool" zorn nil) (T0 const-decl "(tower?)" zorn nil) (T0_comparable? const-decl "bool" zorn nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (TRUE const-decl "bool" booleans nil)) shostak)) (T0_chain 0 (T0_chain-1 nil 3314731120 ("" (typepred "chain_incl") (("" (expand* "chain?" "total_order?" "partial_order?" "preorder?" "dichotomous?" "restrict") (("" (skosimp) (("" (lemma "T0_all_comparable" ("ch" "x!1")) (("" (expand* "T0_comparable?" "chain_incl") (("" (inst - "y!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((total_order? const-decl "bool" orders nil) (preorder? const-decl "bool" orders nil) (restrict const-decl "R" restrict nil) (dichotomous? const-decl "bool" orders nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (T0_all_comparable formula-decl nil zorn nil) (tower? const-decl "bool" zorn nil) (T0 const-decl "(tower?)" zorn nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" zorn nil) (T0_comparable? const-decl "bool" zorn nil) (chain_incl_partial_order name-judgement "(partial_order?[subchain])" zorn 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 zorn nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (chain? const-decl "bool" chain nil) (subchain nonempty-type-eq-decl nil chain_chain nil) (chain_incl const-decl "bool" chain_chain nil)) nil)) (zorn 0 (zorn-1 nil 3314758540 ("" (flatten) (("" (lemma "maximal_chain_add_set" ("ch" "chain_union(T0)")) (("" (prop) (("1" (forward-chain "bounded_chain_upto") (("1" (expand* "fullset" "maximal?" "member") (("1" (inst - "chain_union(T0)") (("1" (skolem!) (("1" (use "maximal_upto_subset") (("1" (inst 2 "t!1") (("1" (prop) (("1" (skosimp) (("1" (inst - "r!1") (("1" (assert) (("1" (expand* "upto" "subset?" "member") (("1" (skosimp) (("1" (expand* "fullset" "maximal?" "reflexive_closure" "union" "member") (("1" (inst + "x!1") (("1" (assert) (("1" (typepred "<=") (("1" (expand* "partial_order?" "preorder?" "transitive?") (("1" (flatten) (("1" (inst - "x!1" "t!1" "r!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand* "upto" "chain_incl" "subset?" "member") (("2" (inst + "add(r!1, chain_union(T0))") (("1" (prop) (("1" (skosimp) (("1" (expand* "add" "member") (("1" (flatten) nil nil)) nil)) nil) ("2" (decompose-equality) (("2" (inst - "r!1") (("2" (expand* "add" "reflexive_closure" "union" "member") (("2" (inst - "t!1") (("2" (inst - "r!1") (("2" (typepred "<=") (("2" (expand* "partial_order?" "preorder?" "antisymmetric?") (("2" (flatten) (("2" (inst - "t!1" "r!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "chain_union(T0)") (("2" (typepred "<=") (("2" (expand* "chain?" "total_order?" "partial_order?" "preorder?" "restrict" "dichotomous?") (("2" (skosimp :preds? t) (("2" (expand* "add" "reflexive?" "reflexive_closure" "union" "member") (("2" (ground) (("1" (inst - "r!1") (("1" (assert) nil nil)) nil) ("2" (inst - "y!1") (("2" (inst - "y!1") (("2" (inst - "y!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (inst - "x!1") (("3" (inst - "x!1") (("3" (inst - "x!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (inst - "x!1" "y!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "fullset" "maximal?" "member" "chain_incl") (("2" (skosimp :preds? t) (("2" (lemma "empty_succ" ("ch" "chain_union(T0)")) (("2" (assert) (("2" (apply-extensionality :hide? t) (("2" (expand* "succ" "add" "member") (("2" (iff) (("2" (prop) (("2" (typepred "T0") (("2" (expand* "tower?" "member") (("2" (flatten) (("2" (inst -3 "T0") (("2" (split) (("1" (inst - "chain_union(T0)") (("1" (expand "chain_union" 1) (("1" (expand* "extend" "Union") (("1" (inst + "succ(chain_union(T0))") (("1" (expand* "succ" "add" "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T0 const-decl "(tower?)" zorn nil) (tower? const-decl "bool" zorn nil) (chain_union const-decl "subchain" chain_chain nil) (chain_chain nonempty-type-eq-decl nil chain_chain nil) (chain_incl const-decl "bool" chain_chain nil) (subchain nonempty-type-eq-decl nil chain_chain nil) (chain? const-decl "bool" chain nil) (<= formal-const-decl "(partial_order?[T])" zorn nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types 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 zorn nil) (maximal_chain_add_set formula-decl nil zorn nil) (T0_chain name-judgement "chain_chain" zorn nil) (empty_succ formula-decl nil zorn nil) (succ const-decl "subchain" zorn nil) (FALSE const-decl "bool" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (extend const-decl "R" extend nil) (Union const-decl "set" sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" zorn nil) (bounded_chain_upto formula-decl nil zorn nil) (maximal_upto_subset formula-decl nil zorn nil) (TRUE const-decl "bool" booleans nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset nil) (union const-decl "set" sets nil) (reflexive_closure const-decl "(reflexive?)" closure_ops nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (NOT const-decl "[bool -> bool]" booleans nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" zorn nil) (total_order? const-decl "bool" orders nil) (dichotomous? const-decl "bool" orders nil) (restrict const-decl "R" restrict nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (reflexive? const-decl "bool" relations nil) (antisymmetric? const-decl "bool" relations nil) (= const-decl "[T, T -> boolean]" equalities nil) (r!1 skolem-const-decl "T" zorn nil) (add const-decl "(nonempty?)" sets nil) (nonempty? const-decl "bool" sets nil) (fullset const-decl "set" sets nil) (maximal? const-decl "bool" minmax_orders nil)) shostak))) ¤ Dauer der Verarbeitung: 0.77 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.Bot Zugriff |
