| products/Sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: minmax_orders.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(minmax_orders
(greatest_TCC1 0 (greatest_TCC1-1 nil 3315155075 ("" (inst + "LAMBDA (lesseq: pred[[T, T]]): LAMBDA (S: (LAMBDA (S): has_greatest?(S, lesseq) (("" (grind :if-match nil) (("" (inst? -3) nil nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (upper_bound? const-decl "bool" bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (greatest? const-decl "bool" minmax_orders nil) (has_greatest? const-decl "bool" minmax_orders nil) (set type-eq-decl nil sets 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 minmax_orders nil)) nil)) (greatest_iff_least_upper_bound 0 (greatest_iff_least_upper_bound-1 nil 3315155267 ("" (grind) nil nil) ((t!1 skolem-const-decl "T" minmax_orders nil) (S!1 skolem-const-decl "set[T]" minmax_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 minmax_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (greatest? const-decl "bool" minmax_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil)) shostak)) (greatest_is_least_upper_bound 0 (greatest_is_least_upper_bound-1 nil 3315155075 ("" (judgement-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (greatest? const-decl "bool" minmax_orders nil) (x!1 skolem-const-decl "(greatest?)" minmax_orders nil) (T formal-type-decl nil minmax_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil)) nil)) (has_greatest_is_least_bounded_above 0 (has_greatest_is_least_bounded_above-1 nil 3315155075 ("" (skolem-typepred) (("" (expand* "least_bounded_above?" "has_greatest?") (("" (skolem!) (("" (inst?) (("" (rewrite "greatest_is_least_upper_bound") nil nil)) nil)) nil)) nil)) nil) ((least_bounded_above? const-decl "bool" bounded_orders nil) (greatest? const-decl "bool" minmax_orders nil) (greatest_is_least_upper_bound judgement-tcc nil minmax_orders nil) (has_greatest? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil minmax_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)) (greatest_equals_lub_TCC1 0 (greatest_equals_lub_TCC1-1 nil 3315155075 ("" (skolem-typepred) (("" (rewrite "has_greatest_is_least_bounded_above") nil nil)) nil) ((has_greatest_is_least_bounded_above judgement-tcc nil minmax_orders nil) (has_greatest? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil minmax_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)) (greatest_equals_lub 0 (greatest_equals_lub-1 nil 3315155331 ("" (skolem-typepred) (("" (use "unique_least_upper_bound") (("" (rewrite "greatest_is_least_upper_bound") nil nil)) nil)) nil) ((unique_least_upper_bound formula-decl nil bounded_orders nil) (ale!1 skolem-const-decl "(antisymmetric?[T])" minmax_orders nil) (S!1 skolem-const-decl "(LAMBDA (S): has_greatest?(S, ale!1))" minmax_orders nil) (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (greatest_is_least_upper_bound judgement-tcc nil minmax_orders nil) (has_greatest? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil minmax_orders 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_unique 0 (greatest_unique-1 nil 3315155424 ("" (skolem-typepred) (("" (rewrite "greatest_iff_least_upper_bound") (("" (rewrite "greatest_iff_least_upper_bound") (("" (flatten) (("" (use "unique_least_upper_bound") nil nil)) nil)) nil)) nil)) nil) ((greatest_iff_least_upper_bound formula-decl nil minmax_orders nil) (unique_least_upper_bound formula-decl nil bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (t!1 skolem-const-decl "(LAMBDA (t): greatest?(t, S!1, lesseqp!1))" minmax_orders nil) (lesseqp!1 skolem-const-decl "(antisymmetric?[T])" minmax_orders nil) (S!1 skolem-const-decl "set[T]" minmax_orders nil) (s!1 skolem-const-decl "(LAMBDA (t): greatest?(t, S!1, lesseqp!1))" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil minmax_orders 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_is_maximal 0 (greatest_is_maximal-1 nil 3315155468 ("" (skosimp :preds? t) (("" (expand* "maximal?" "greatest?" "member" "upper_bound?" "antisymmetric?") (("" (prop) (("" (skosimp) (("" (inst - "r!1") (("" (inst - "t!1" "r!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((greatest? const-decl "bool" minmax_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (maximal? const-decl "bool" minmax_orders 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 minmax_orders nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil)) shostak)) (maximal_is_greatest 0 (maximal_is_greatest-1 nil 3315155503 ("" (skosimp :preds? t) (("" (expand* "maximal?" "greatest?" "member" "upper_bound?" "dichotomous?") (("" (prop) (("" (skolem!) (("" (inst + "r!1") (("" (inst - "t!1" "r!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((greatest? const-decl "bool" minmax_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (maximal? const-decl "bool" minmax_orders 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 minmax_orders nil) (pred type-eq-decl nil defined_types nil) (dichotomous? const-decl "bool" orders nil)) shostak)) (non_empty_finite_has_greatest 0 (non_empty_finite_has_greatest-1 nil 3315156295 ("" (skolem-typepred) (("" (use "max_lem[T, le!1]") (("" (assert) (("" (expand* "has_greatest?" "greatest?" "member" "upper_bound?") (("" (inst? +) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((max_lem formula-decl nil finite_sets_minmax "finite_sets/") (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (greatest? const-decl "bool" minmax_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (has_greatest? const-decl "bool" minmax_orders nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets 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) (T formal-type-decl nil minmax_orders 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_ge 0 (greatest_ge-1 nil 3315156353 ("" (skolem!) (("" (invoke (typepred "%1") (! 1 r)) (("" (expand* "greatest?" "upper_bound?") (("" (flatten) (("" (inst - "m!1") 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 minmax_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (has_greatest? const-decl "bool" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders nil) (upper_bound? const-decl "bool" bounded_orders nil)) shostak)) (greatest_monotone 0 (greatest_monotone-1 nil 3315156389 ("" (skosimp) (("" (invoke (typepred "%1" "%2") (! 1 l) (! 1 r)) (("" (expand "greatest?") (("" (flatten) (("" (hide -2) (("" (expand "upper_bound?") (("" (inst?) (("" (expand* "subset?" "member") (("" (inst?) (("" (assert) nil 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 minmax_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (has_greatest? const-decl "bool" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders nil) (S1!1 skolem-const-decl "(LAMBDA (S): has_greatest?(S, lesseqp!1))" minmax_orders nil) (S2!1 skolem-const-decl "(LAMBDA (S): has_greatest?(S, lesseqp!1))" minmax_orders nil) (lesseqp!1 skolem-const-decl "pred[[T, T]]" minmax_orders nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (upper_bound? const-decl "bool" bounded_orders nil)) shostak)) (greatest_def 0 (greatest_def-1 nil 3315156422 ("" (skolem-typepred) (("" (rewrite "greatest_iff_least_upper_bound") (("" (prop) (("1" (rewrite "greatest_equals_lub") (("1" (rewrite "lub_def") nil nil)) nil) ("2" (use "greatest_member") (("2" (assert) nil nil)) nil) ("3" (rewrite "greatest_equals_lub") (("3" (rewrite "lub_def") nil nil)) nil)) nil)) nil)) nil) ((greatest_iff_least_upper_bound formula-decl nil minmax_orders nil) (greatest_equals_lub formula-decl nil minmax_orders nil) (lub_def formula-decl nil bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (has_greatest? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil minmax_orders 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_upper_bound 0 (greatest_upper_bound-1 nil 3315156724 ("" (skolem-typepred) (("" (invoke (typepred "%1") (! 1 l 1)) (("" (expand "greatest?") (("" (prop) (("1" (expand* "upper_bound?" "partial_order?" "preorder?" "transitive?") (("1" (skosimp :preds? t) (("1" (inst?) (("1" (inst - "r!1" "greatest(lesseqp!1)(S!1)" "t!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "upper_bound?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ((greatest? const-decl "bool" minmax_orders nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (has_greatest? const-decl "bool" minmax_orders nil) (set type-eq-decl nil sets nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil minmax_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (least_TCC1 0 (least_TCC1-1 nil 3315155075 ("" (inst + "LAMBDA (lesseq: pred[[T, T]]): LAMBDA (S: (LAMBDA (S): has_least?(S, lesseq))): (("" (grind :if-match nil) (("" (inst? -3) nil nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (lower_bound? const-decl "bool" bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (least? const-decl "bool" minmax_orders nil) (has_least? const-decl "bool" minmax_orders nil) (set type-eq-decl nil sets 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 minmax_orders nil)) nil)) (least_iff_greatest_lower_bound 0 (least_iff_greatest_lower_bound-1 nil 3315156851 ("" (grind) nil nil) ((t!1 skolem-const-decl "T" minmax_orders nil) (S!1 skolem-const-decl "set[T]" minmax_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 minmax_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (least? const-decl "bool" minmax_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil)) shostak)) (least_is_greatest_lower_bound 0 (least_is_greatest_lower_bound-1 nil 3315155075 ("" (judgement-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (least? const-decl "bool" minmax_orders nil) (x!1 skolem-const-decl "(least?)" minmax_orders nil) (T formal-type-decl nil minmax_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil)) nil)) (has_least_is_greatest_bounded_below 0 (has_least_is_greatest_bounded_below-1 nil 3315155075 ("" (skolem-typepred) (("" (expand* "greatest_bounded_below?" "has_least?") (("" (skolem!) (("" (inst?) (("" (rewrite "least_is_greatest_lower_bound") nil nil)) nil)) nil)) nil)) nil) ((greatest_bounded_below? const-decl "bool" bounded_orders nil) (least? const-decl "bool" minmax_orders nil) (least_is_greatest_lower_bound judgement-tcc nil minmax_orders nil) (has_least? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil minmax_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)) (least_equals_glb_TCC1 0 (least_equals_glb_TCC1-1 nil 3315155075 ("" (skolem-typepred) (("" (rewrite "has_least_is_greatest_bounded_below") nil nil)) nil) ((has_least_is_greatest_bounded_below judgement-tcc nil minmax_orders nil) (has_least? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil minmax_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)) (least_equals_glb 0 (least_equals_glb-1 nil 3315156935 ("" (skolem-typepred) (("" (use "unique_greatest_lower_bound") (("" (rewrite "least_is_greatest_lower_bound") nil nil)) nil)) nil) ((unique_greatest_lower_bound formula-decl nil bounded_orders nil) (ale!1 skolem-const-decl "(antisymmetric?[T])" minmax_orders nil) (S!1 skolem-const-decl "(LAMBDA (S): has_least?(S, ale!1))" minmax_orders nil) (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (least_is_greatest_lower_bound judgement-tcc nil minmax_orders nil) (has_least? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil minmax_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (least_unique 0 (least_unique-1 nil 3315156954 ("" (skolem-typepred) (("" (rewrite "least_iff_greatest_lower_bound") (("" (rewrite "least_iff_greatest_lower_bound") (("" (flatten) (("" (use "unique_greatest_lower_bound") nil nil)) nil)) nil)) nil)) nil) ((least_iff_greatest_lower_bound formula-decl nil minmax_orders nil) (unique_greatest_lower_bound formula-decl nil bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (t!1 skolem-const-decl "(LAMBDA (t): least?(t, S!1, lesseqp!1))" minmax_orders nil) (lesseqp!1 skolem-const-decl "(antisymmetric?[T])" minmax_orders nil) (S!1 skolem-const-decl "set[T]" minmax_orders nil) (s!1 skolem-const-decl "(LAMBDA (t): least?(t, S!1, lesseqp!1))" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil minmax_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (least_is_minimal 0 (least_is_minimal-1 nil 3315156973 ("" (skosimp :preds? t) (("" (expand* "minimal?" "least?" "member" "lower_bound?" "antisymmetric?") (("" (prop) (("" (skosimp) (("" (inst - "r!1") (("" (inst - "t!1" "r!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((least? const-decl "bool" minmax_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (minimal? const-decl "bool" minmax_orders 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 minmax_orders nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil)) shostak)) (minimal_is_least 0 (minimal_is_least-1 nil 3315157008 ("" (skosimp :preds? t) (("" (expand* "minimal?" "least?" "member" "lower_bound?" "dichotomous?") (("" (prop) (("" (skolem!) (("" (inst + "r!1") (("" (inst - "t!1" "r!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((least? const-decl "bool" minmax_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (minimal? const-decl "bool" minmax_orders 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 minmax_orders nil) (pred type-eq-decl nil defined_types nil) (dichotomous? const-decl "bool" orders nil)) shostak)) (non_empty_finite_has_least 0 (non_empty_finite_has_least-1 nil 3315157031 ("" (skolem-typepred) (("" (use "min_lem[T, le!1]") (("" (assert) (("" (expand* "has_least?" "least?" "member" "lower_bound?") (("" (inst? +) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((min_lem formula-decl nil finite_sets_minmax "finite_sets/") (min const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}" finite_sets_minmax "finite_sets/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (least? const-decl "bool" minmax_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (has_least? const-decl "bool" minmax_orders nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets 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) (T formal-type-decl nil minmax_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (least_le 0 (least_le-1 nil 3315157082 ("" (skolem!) (("" (invoke (typepred "%1") (! 1 l)) (("" (expand* "least?" "lower_bound?") (("" (flatten) (("" (inst - "m!1") 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 minmax_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (has_least? const-decl "bool" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil) (lower_bound? const-decl "bool" bounded_orders nil)) shostak)) (least_monotone 0 (least_monotone-1 nil 3315157107 ("" (skosimp) (("" (invoke (typepred "%1" "%2") (! 1 l) (! 1 r)) (("" (expand* "least?" "lower_bound?" "subset?" "member") (("" (flatten) (("" (inst?) (("" (inst? -4) (("" (assert) 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 minmax_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (has_least? const-decl "bool" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil) (lesseqp!1 skolem-const-decl "pred[[T, T]]" minmax_orders nil) (S2!1 skolem-const-decl "(LAMBDA (S): has_least?(S, lesseqp!1))" minmax_orders nil) (S1!1 skolem-const-decl "(LAMBDA (S): has_least?(S, lesseqp!1))" minmax_orders nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (lower_bound? const-decl "bool" bounded_orders nil)) shostak)) (least_def 0 (least_def-1 nil 3315157135 ("" (skolem-typepred) (("" (rewrite "least_iff_greatest_lower_bound") (("" (prop) (("1" (rewrite "least_equals_glb") (("1" (rewrite "glb_def") nil nil)) nil) ("2" (use "least_member") (("2" (assert) nil nil)) nil) ("3" (rewrite "least_equals_glb") (("3" (rewrite "glb_def") nil nil)) nil)) nil)) nil)) nil) ((least_iff_greatest_lower_bound formula-decl nil minmax_orders nil) (least_equals_glb formula-decl nil minmax_orders nil) (glb_def formula-decl nil bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (has_least? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil minmax_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (least_lower_bound 0 (least_lower_bound-1 nil 3315157181 ("" (skolem-typepred) (("" (invoke (typepred "%1") (! 1 l 2)) (("" (expand "least?") (("" (prop) (("1" (expand* "lower_bound?" "partial_order?" "preorder?" "transitive?") (("1" (skosimp :preds? t) (("1" (inst?) (("1" (inst - "t!1" "least(lesseqp!1)(S!1)" "r!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "lower_bound?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ((least? const-decl "bool" minmax_orders nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (has_least? const-decl "bool" minmax_orders nil) (set type-eq-decl nil sets nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil minmax_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (has_extrema_has_greatest 0 (has_extrema_has_greatest-1 nil 3315155075 ("" (judgement-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (has_extrema? const-decl "bool" minmax_orders nil) (has_least? const-decl "bool" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (T formal-type-decl nil minmax_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (greatest? const-decl "bool" minmax_orders nil) (has_greatest? const-decl "bool" minmax_orders nil)) nil)) (has_extrema_has_least 0 (has_extrema_has_least-1 nil 3315155075 ("" (judgement-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (has_extrema? const-decl "bool" minmax_orders nil) (has_greatest? const-decl "bool" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (T formal-type-decl nil minmax_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (least? const-decl "bool" minmax_orders nil) (has_least? const-decl "bool" minmax_orders nil)) nil)) (total_order_is_lattice 0 (total_order_is_lattice-1 nil 3315155075 ("" (skolem-typepred) (("" (expand* "lattice?" "upper_semilattice?" "lower_semilattice?" "total_order?") (("" (prop) (("1" (skolem!) (("1" (use "non_empty_finite_has_greatest") (("1" (rewrite "has_greatest_is_least_bounded_above") nil nil)) nil)) nil) ("2" (skolem!) (("2" (use "non_empty_finite_has_least") (("2" (rewrite "has_least_is_greatest_bounded_below") nil nil)) nil)) nil)) nil)) nil)) nil) ((upper_semilattice? const-decl "bool" bounded_orders nil) (lower_semilattice? const-decl "bool" bounded_orders nil) (lattice? const-decl "bool" bounded_orders nil) (has_least? const-decl "bool" minmax_orders nil) (has_least_is_greatest_bounded_below judgement-tcc nil minmax_orders nil) (non_empty_finite_has_least formula-decl nil minmax_orders nil) (has_greatest? const-decl "bool" minmax_orders nil) (has_greatest_is_least_bounded_above judgement-tcc nil minmax_orders nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets 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) (non_empty_finite_has_greatest formula-decl nil minmax_orders nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil minmax_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.38 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 |
