| products/sources/formale sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: digraph_ops.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(compactness
(IMP_metric_spaces_TCC1 0 (IMP_metric_spaces_TCC1-1 nil 3514557102 ("" (lemma "fullset_metric_space") (("" (propax) nil nil)) nil) ((fullset_metric_space formula-decl nil compactness nil)) nil)) (nBalls_open_cover 0 (nBalls_open_cover-1 nil 3459609819 ("" (skosimp*) (("" (expand "open_cover?") (("" (expand "extend") (("" (split +) (("1" (expand "subset?") (("1" (skosimp*) (("1" (assert) (("1" (expand "Union") (("1" (case "EXISTS (n: posnat): n > d(p!1,x!1)") (("1" (skosimp*) (("1" (inst + "ball(p!1,n!1)") (("1" (expand "ball") (("1" (assert) nil nil)) nil) ("2" (ground) (("1" (expand "nBalls") (("1" (expand "restrict") (("1" (inst?) nil nil)) nil)) nil) ("2" (lemma "ball_open") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "axiom_of_archimedes") (("2" (inst?) (("2" (skosimp*) (("2" (inst + "i!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((open_cover? const-decl "bool" compactness nil) (Union const-decl "set" sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (i!1 skolem-const-decl "int" compactness nil) (axiom_of_archimedes formula-decl nil real_props nil) (restrict const-decl "R" restrict nil) (ball_open formula-decl nil metric_spaces nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (set type-eq-decl nil sets nil) (open? const-decl "bool" metric_spaces nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (ball const-decl "set[T]" metric_spaces nil) (p!1 skolem-const-decl "T" compactness nil) (n!1 skolem-const-decl "posnat" compactness nil) (nBalls const-decl "set[(open?)]" compactness nil) (FALSE const-decl "bool" booleans nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (T formal-nonempty-type-decl nil compactness nil) (nnreal type-eq-decl nil real_types nil) (d formal-const-decl "[T, T -> nnreal]" compactness nil) (member const-decl "bool" sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (extend const-decl "R" extend nil)) shostak)) (reverse_ball_TCC1 0 (reverse_ball_TCC1-1 nil 3459866641 ("" (inst + "(LAMBDA (H: set[[T, posreal]], a: {s: (nonempty?[T]) | ball_covering(H)(s)}): choose({h: (H) | ball[T, d](h`1, h`2) = a}))" (("1" (skosimp*) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (typepred "a!1") (("1" (expand "ball_covering") (("1" (skosimp*) (("1" (inst - "h!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "fullset_metric_space") nil nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (ball const-decl "set[T]" metric_spaces nil) (d formal-const-decl "[T, T -> nnreal]" compactness nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (ball_covering const-decl "set[set[T]]" compactness nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T formal-nonempty-type-decl nil compactness nil)) nil)) (set_compact 0 (set_compact-1 nil 3459849180 ("" (skosimp*) (("" (expand "compact?") (("" (inst - "ball_covering(H!1)") (("" (prop) (("" (skosimp*) (("" (expand "finite_cover?") (("" (prop) (("" (lemma "is_finite_surj[set[T]]") (("" (inst - "YS!1") (("" (skosimp*) (("" (prop) (("" (skosimp*) (("" (expand "surjective?") (("" (inst + "N!1" "(LAMBDA (n: below[N!1]): reverse_ball(H!1,f!1(n)))") (("1" (expand "open_cover?" +) (("1" (expand "subset?") (("1" (expand "member") (("1" (expand "Union") (("1" (expand "ball_covering" +) (("1" (prop) (("1" (skosimp*) (("1" (expand "open_cover?") (("1" (prop) (("1" (expand "subset?") (("1" (expand "member") (("1" (expand "Union") (("1" (case "FORALL (x: T): S!1(x) => (EXISTS (a: (YS!1)): a(x))") (("1" (inst - "x!1") (("1" (prop) (("1" (skosimp*) (("1" (typepred "a!1") (("1" (inst + "ball(reverse_ball(H!1,a!1)`1,reverse_ball(H!1,a!1)`2)") (("1" (typepred "reverse_ball(H!1,a!1)") (("1" (assert) nil nil)) nil) ("2" (expand "ball_covering") (("2" (inst + "reverse_ball(H!1,a!1)") (("1" (inst - "a!1") (("1" (skosimp*) (("1" (inst + "x!2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (x: set[T]): YS!1(x) => (EXISTS (h: (H!1)): x = ball(h`1, h`2))") (("1" (inst - "a!1") (("1" (prop) (("1" (expand "ball_covering") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "ball_covering") (("2" (case "FORALL (x: set[T]): YS!1(x) => (EXISTS (h: (H!1)): x = ball(h`1, h`2))") (("1" (inst - "a!1") (("1" (prop) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "ball_open") (("2" (inst - "h!1`2" "h!1`1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "n!1") (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (typepred "f!1(n!1)") (("1" (expand "subset?") (("1" (case "FORALL (x: set[T]): member(x, YS!1) => member(x, ball_covering(H!1))") (("1" (inst - "f!1(n!1)") (("1" (expand "member") (("1" (expand "ball_covering") (("1" (skosimp*) (("1" (inst - "h!1`1") (("1" (expand "ball") (("1" (assert) (("1" (decompose-equality) (("1" (inst - "h!1`1") (("1" (lemma "fullset_metric_space") (("1" (expand "metric_space?") (("1" (prop) (("1" (expand "space_zero?") (("1" (inst - "h!1`1" "h!1`1") (("1" (prop) (("1" (assert) nil nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "f!1(n!1)") (("2" (expand "subset?") (("2" (case "FORALL (x: set[T]): member(x, YS!1) => member(x, ball_covering(H!1))") (("1" (inst - "f!1(n!1)") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((compact? const-decl "bool" compactness nil) (finite_cover? const-decl "bool" compactness nil) (is_finite_surj formula-decl nil finite_sets nil) (H!1 skolem-const-decl "set[[T, posreal]]" compactness nil) (f!1 skolem-const-decl "[below[N!1] -> (YS!1)]" compactness nil) (YS!1 skolem-const-decl "set[set[T]]" compactness nil) (nonempty? const-decl "bool" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (N!1 skolem-const-decl "nat" compactness nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (d formal-const-decl "[T, T -> nnreal]" compactness nil) (ball const-decl "set[T]" metric_spaces nil) (reverse_ball const-decl "{h: (H) | ball(h`1, h`2) = A}" compactness nil) (subset? const-decl "bool" sets nil) (Union const-decl "set" sets nil) (a!1 skolem-const-decl "(YS!1)" compactness nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (ball_open formula-decl nil metric_spaces nil) (member const-decl "bool" sets nil) (open_cover? const-decl "bool" compactness nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (metric_space? const-decl "bool" metric_spaces_def nil) (space_zero? const-decl "bool" metric_spaces_def nil) (h!1 skolem-const-decl "(H!1)" compactness nil) (fullset const-decl "set" sets nil) (fullset_metric_space formula-decl nil compactness nil) (surjective? const-decl "bool" functions nil) (ball_covering const-decl "set[set[T]]" compactness nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (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 compactness nil)) shostak)) (idxCover_TCC1 0 (idxCover_TCC1-1 nil 3459871403 ("" (skosimp*) (("" (expand "nonempty?") (("" (expand "empty?") (("" (assert) (("" (lemma "set_compact") (("" (inst?) (("" (inst - "S!1") (("" (assert) (("" (skosimp*) (("" (inst - "(N!1,seq!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (T formal-nonempty-type-decl nil compactness nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (set type-eq-decl nil sets nil) (open_cover? const-decl "bool" compactness nil) (ball_covering const-decl "set[set[T]]" compactness nil) (compact? const-decl "bool" compactness nil) (Htype type-eq-decl nil compactness nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (set_compact formula-decl nil compactness nil) (empty? const-decl "bool" sets nil)) nil)) (idxCover_def 0 (idxCover_def-1 nil 3460202946 ("" (skolem!) (("" (assert) (("" (flatten) (("" (typepred "idxCover(S!1, H!1)") (("1" (expand "ball_covering") (("1" (expand "open_cover?") (("1" (flatten) (("1" (hide -2) (("1" (expand "subset?") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (expand "Union") (("1" (skosimp*) (("1" (typepred "a!1") (("1" (skosimp*) (("1" (typepred "h!1") (("1" (skosimp*) (("1" (inst + "n!1") (("1" (assert) (("1" (inst + "h!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((idxCover const-decl "{pair: [N: nat, seq: [below[N] -> (H)]] | open_cover?(ball_covering({h: [T, posreal] | H(h) AND (EXISTS (n: below[pair`1]): h = pair`2(n))}), S)}" compactness nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (Htype type-eq-decl nil compactness nil) (compact? const-decl "bool" compactness nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (ball_covering const-decl "set[set[T]]" compactness nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (open_cover? const-decl "bool" compactness nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil compactness nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (nnreal type-eq-decl nil real_types nil) (d formal-const-decl "[T, T -> nnreal]" compactness nil) (ball const-decl "set[T]" metric_spaces nil) (Union const-decl "set" sets nil) (subset? const-decl "bool" sets nil)) nil)) (set_compact_alt 0 (set_compact_alt-1 nil 3459871447 ("" (skosimp*) (("" (assert) (("" (lemma "set_compact") (("" (inst?) (("" (assert) (("" (skosimp*) (("" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (max_min_finite_scaf 0 (max_min_finite_scaf-5 nil 3460115843 ("" (skosimp*) (("" (case "FORALL (n: below(N!1)): nonempty?[nat]({M: nat| FORALL (m: above(M)): P!1( (("1" (case "is_finite[nat]({x: nat | EXISTS (n: below(N!1)): x = min_nat[nat].min({M: (("1" (name "f" "(LAMBDA (n:below(N!1)): min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, (("1" (swap-rel -1) (("1" (inst + "max({K: nat | EXISTS (n1: below(N!1)): K = f(n1)})") (("1" (skosimp*) (("1" (typepred "m!1") (("1" (typepred "n!1") (("1" (replace -3) (("1" (typepred "max({K: nat | EXISTS (n1: below(N!1)): K = (LAMBDA (n: below(N!1)): min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n)})) (n1)})") (("1" (skosimp*) (("1" (inst - "min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst - "n!1") (("1" (prop) (("1" (swap-rel -1) (("1" (add-formulas -1 -4) (("1" (assert) (("1" (both-sides "-" "max({K: nat | EXISTS (n1: below(N!1)): K = min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n1)})})" -1) (("1" (assert) (("1" (typepred "min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst - "m!1") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (prop) (("2" (inst - "min_nat[nat].min ({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil) ("3" (prop) (("3" (expand "empty?") (("3" (expand "nonempty?") (("3" (expand "empty?") (("3" (expand "member") (("3" (inst - "min_nat[nat].min ({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst + "n!1") nil nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "min_nat[nat].min ({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst + "n!1") nil nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "n!1") nil nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (case "FORALL (n: below(N!1)): EXISTS (M: nat): FORALL (m: above(M)): P!1(m, n)") (("1" (inst - "n!1") (("1" (skosimp*) (("1" (inst -2 "M!1") nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "min_nat[nat].min ({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst + "n!1") nil nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (case "FORALL (n: below(N!1)): EXISTS (M: nat): FORALL (m: above(M)): P!1(m, n)") (("1" (inst - "n!1") (("1" (skosimp*) (("1" (inst -2 "M!1") nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst-cp - "n!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "f(0)") (("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "is_finite_surj[nat]") (("2" (inst - "{x: nat | EXISTS (n: below(N!1)): x = min_nat[nat].min ({M: nat | FORALL (m: above(M)): P!1(m, n)})}") (("2" (prop) (("2" (inst + "N!1" "(LAMBDA (n: below(N!1)): min_nat[nat].min ({M: nat | FORALL (m: above(M)): P!1(m, n)}))") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (skosimp*) (("1" (inst + "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst -2 "n!1") (("2" (skosimp*) (("2" (inst - "M!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((above nonempty-type-eq-decl nil integers nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (posint nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (is_finite_surj formula-decl nil finite_sets nil) (surjective? const-decl "bool" functions nil) (below type-eq-decl nil nat_types nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (N!1 skolem-const-decl "posint" compactness nil) (P!1 skolem-const-decl "[[nat, below(N!1)] -> bool]" compactness nil) (f skolem-const-decl "[n: below(N!1) -> {a | (FORALL (m: above(a)): P!1(m, n)) AND (FORALL (x: nat): (FORALL (m: above(x)): P!1(m, n)) IMPLIES a <= x)}]" compactness nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (restrict const-decl "R" restrict nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_plus_gt2 formula-decl nil real_props nil) (both_sides_plus_ge2 formula-decl nil real_props nil) (both_sides_minus_gt1 formula-decl nil real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (member const-decl "bool" sets nil) (n!1 skolem-const-decl "below(N!1)" compactness nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (is_finite const-decl "bool" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil)) nil) (max_min_finite_scaf-4 nil 3460115556 (";;; Proof max_min_finite_scaf-3 for formula compactness.max_min_finite_scaf" (skosimp*) ((";;; Proof max_min_finite_scaf-3 for formula compactness.max_min_finite_scaf" (name "f" "(LAMBDA (n:below(N!1)): min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, (("1" (swap-rel -1) (("1" (inst-cp + "max({K: nat | EXISTS (n1: below(N!1)): K = f(n1)})") (("1" (skosimp*) (("1" (typepred "m!1") (("1" (typepred "n!1") (("1" (replace -3) (("1" (typepred "max({K: nat | EXISTS (n1: below(N!1)): K = (LAMBDA (n: below(N!1)): min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n)})) (n1)})") (("1" (skosimp*) (("1" (inst-cp - "min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst-cp - "n!1") (("1" (prop) (("1" (swap-rel -1) (("1" (add-formulas -1 -4) (("1" (assert) (("1" (both-sides "-" "max({K: nat | EXISTS (n1: below(N!1)): K = min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n1)})})" -1) (("1" (assert) (("1" (typepred "min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst-cp - "m!1") nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst-cp - "M!1") nil))))))))))))) ("2" (expand "nonempty?") (("2" (skosimp*) (("2" (expand "empty?") (("2" (expand "member") (("2" (inst-cp - "M!1") nil))))))))))))) ("2" (postpone) nil) ("3" (postpone) nil) ("4" (postpone) nil))) ("2" (postpone) nil) ("3" (postpone) nil))) ("2" (postpone) nil))))) ("2" (postpone) nil))))) ("2" (postpone) nil) ("3" (postpone) nil))))))))))) ("2" (postpone) nil))))) ("2" (postpone) nil)))) ";;; developed with shostak decision procedures") nil nil) (max_min_finite_scaf-3 nil 3460114454 ("" (skosimp*) (("" (name "f" "(LAMBDA (n:below(N!1)): min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, (("1" (swap-rel -1) (("1" (inst + "max({K: nat | EXISTS (n1: below(N!1)): K = f(n1)})") (("1" (skosimp*) (("1" (typepred "m!1") (("1" (typepred "n!1") (("1" (replace -3) (("1" (typepred "max({K: nat | EXISTS (n1: below(N!1)): K = (LAMBDA (n: below(N!1)): min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n)})) (n1)})") (("1" (skosimp*) (("1" (inst - "min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst - "n!1") (("1" (prop) (("1" (swap-rel -1) (("1" (add-formulas -1 -4) (("1" (assert) (("1" (both-sides "-" "max({K: nat | EXISTS (n1: below(N!1)): K = min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n1)})})" -1) (("1" (assert) (("1" (typepred "min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst - "m!1") nil nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst - "M!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (skosimp*) (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "M!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 1.80 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 |
