|
(finite_orders
(IMP_finite_types_TCC1 0
(IMP_finite_types_TCC1-1 nil 3315153951
("" (rewrite "finite_type") nil nil)
((finite_type formula-decl nil finite_orders nil)) nil))
(finite_lower_semilattice_is_complete 0
(finite_lower_semilattice_is_complete-1 nil 3315153982
("" (skosimp)
(("" (expand* "complete_lower_semilattice?" "lower_semilattice?")
(("" (prop)
(("" (skolem!)
(("" (case-replace "S!1 = emptyset")
(("" (inst?) (("" (rewrite "emptyset_is_empty?") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((lower_semilattice? const-decl "bool" bounded_orders nil)
(complete_lower_semilattice? const-decl "bool" bounded_orders nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(empty? const-decl "bool" sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(S!1 skolem-const-decl "set[T]" finite_orders nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(emptyset const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities 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-nonempty-type-decl nil finite_orders nil))
shostak))
(finite_upper_semilattice_is_complete 0
(finite_upper_semilattice_is_complete-1 nil 3315154016
("" (skosimp)
(("" (expand* "complete_upper_semilattice?" "upper_semilattice?")
(("" (prop)
(("" (skolem!)
(("" (case-replace "S!1 = emptyset")
(("" (inst?) (("" (rewrite "emptyset_is_empty?") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((upper_semilattice? const-decl "bool" bounded_orders nil)
(complete_upper_semilattice? const-decl "bool" bounded_orders nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(empty? const-decl "bool" sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(S!1 skolem-const-decl "set[T]" finite_orders nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(emptyset const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities 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-nonempty-type-decl nil finite_orders nil))
shostak))
(finite_lattice_is_complete 0
(finite_lattice_is_complete-1 nil 3315153951
("" (skolem-typepred)
(("" (expand* "complete_lattice?" "lattice?")
(("" (prop)
(("1" (rewrite "finite_upper_semilattice_is_complete")
(("1" (rewrite "least_bounded_above_emptyset")
(("1" (rewrite "all_finite_greatest_bounded") nil nil))
nil))
nil)
("2" (rewrite "finite_lower_semilattice_is_complete")
(("2" (rewrite "greatest_bounded_below_emptyset")
(("2" (rewrite "all_finite_least_bounded") nil nil)) nil))
nil))
nil))
nil))
nil)
((complete_lattice? const-decl "bool" bounded_orders nil)
(finite_lower_semilattice_is_complete formula-decl nil
finite_orders nil)
(all_finite_least_bounded formula-decl nil bounded_orders nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(greatest_bounded_below_emptyset formula-decl nil bounded_orders
nil)
(finite_upper_semilattice_is_complete formula-decl nil
finite_orders nil)
(all_finite_greatest_bounded formula-decl nil bounded_orders nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(fullset const-decl "set" sets nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(fullset_is_nonempty_finite name-judgement
"non_empty_finite_set[T]" finite_orders nil)
(least_bounded_above_emptyset formula-decl nil bounded_orders nil)
(lattice? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-nonempty-type-decl nil finite_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(finite_strict_order_is_well_founded 0
(finite_strict_order_is_well_founded-1 nil 3315153951
("" (skolem-typepred)
(("" (expand "well_founded?")
(("" (measure-induct+ "card(p)" ("p"))
(("" (skolem!)
(("" (inst - "remove(y!1, x!2)")
(("" (prop)
(("1" (inst-cp + "y!1")
(("1" (skosimp* t)
(("1" (inst + "y!2")
(("1" (skolem-typepred)
(("1" (inst-cp - "x!3")
(("1" (inst - "x!4")
(("1" (expand* "remove" "member" "/=")
(("1" (lemma "transitive")
(("1"
(inst - "x!1" "x!3" "y!1" "y!2")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand* "remove" "member" "/=")
(("2" (use "irreflexive")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (expand* "remove" "member")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (inst 2 "y!1")
(("2" (skolem-typepred)
(("2" (inst + "x!3")
(("2" (expand* "remove" "member" "/=")
(("2" (use "irreflexive")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (rewrite "card_remove") (("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((well_founded? const-decl "bool" orders nil)
(irreflexive? const-decl "bool" relations nil)
(irreflexive formula-decl nil relations_extra nil)
(x!4 skolem-const-decl "(x!2)" finite_orders nil)
(transitive formula-decl nil relations_extra nil)
(PRED type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(/= const-decl "boolean" notequal nil)
(member const-decl "bool" sets nil)
(x!3 skolem-const-decl "(x!2)" finite_orders nil)
(finite_remove application-judgement "finite_set[T]" finite_orders
nil)
(y!2 skolem-const-decl "(remove(y!1, x!2))" finite_orders nil)
(y!1 skolem-const-decl "T" finite_orders nil)
(x!2 skolem-const-decl "pred[T]" finite_orders nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(card_remove formula-decl nil finite_sets nil)
(remove const-decl "set" sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(naturalnumber type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(measure_induction formula-decl nil measure_induction nil)
(strict_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-nonempty-type-decl nil finite_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(finite_strict_total_order_is_well_ordered 0
(finite_strict_total_order_is_well_ordered-1 nil 3315153951
("" (skolem-typepred)
(("" (expand "well_ordered?")
(("" (rewrite "finite_strict_order_is_well_founded") nil nil))
nil))
nil)
((well_ordered? const-decl "bool" orders nil)
(strict_order? const-decl "bool" orders nil)
(finite_strict_order_is_well_founded judgement-tcc nil
finite_orders nil)
(strict_total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-nonempty-type-decl nil finite_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil)))
¤ Dauer der Verarbeitung: 0.33 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.
|
