| products/Sources/formale Sprachen/PVS/trig/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sincos_def.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(fixpoints
(unique_bottom 0 (unique_bottom-1 nil 3330266163 ("" (skosimp) (("" (lemma "least_unique" ("<=" "<=" "S" "fullset[T]" "s" "x!1" "t" "y!1")) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (typepred "<=") (("4" (expand "pointed_directed_complete_partial_order?") (("4" (expand "directed_complete_partial_order?") (("4" (expand "partial_order?") (("4" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-type-decl nil fixpoints nil) (least? const-decl "bool" minmax_orders "orders/") (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (pred type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (least_unique formula-decl nil minmax_orders "orders/")) shostak)) (bottom_TCC1 0 (bottom_TCC1-1 nil 3330266277 ("" (typepred "<=") (("" (expand "pointed_directed_complete_partial_order?") (("" (flatten) (("" (expand "has_least?") (("" (skosimp) (("" (inst + "t!1") nil nil)) nil)) nil)) nil)) nil)) nil) ((has_least? const-decl "bool" minmax_orders "orders/") (set type-eq-decl nil sets nil) (least? const-decl "bool" minmax_orders "orders/") (fullset const-decl "set" sets nil) (t!1 skolem-const-decl "T" fixpoints 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-nonempty-type-decl nil fixpoints nil) (pred type-eq-decl nil defined_types nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil)) shostak)) (bottom_le 0 (bottom_le-1 nil 3330266367 ("" (skosimp) (("" (typepred "bottom") (("" (expand "least?") (("" (flatten) (("" (expand "lower_bound?") (("" (inst - "x!1") (("" (expand "fullset") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bottom const-decl "(LAMBDA (t: T): least?(t, fullset[T], <=))" fixpoints nil) (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (fullset const-decl "set" sets nil) (least? const-decl "bool" minmax_orders "orders/") (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil fixpoints nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (x!1 skolem-const-decl "T" fixpoints nil) (lower_bound? const-decl "bool" bounded_orders "orders/")) shostak)) (le_bottom 0 (le_bottom-1 nil 3330266441 ("" (skosimp) (("" (typepred "bottom") (("" (expand "least?") (("" (flatten) (("" (expand "lower_bound?") (("" (inst - "x!1") (("1" (typepred "<=") (("1" (expand "pointed_directed_complete_partial_order?") (("1" (expand "directed_complete_partial_order?") (("1" (expand "partial_order?") (("1" (flatten) (("1" (expand "antisymmetric?") (("1" (inst - "bottom" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bottom const-decl "(LAMBDA (t: T): least?(t, fullset[T], <=))" fixpoints nil) (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (fullset const-decl "set" sets nil) (least? const-decl "bool" minmax_orders "orders/") (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil fixpoints nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (x!1 skolem-const-decl "T" fixpoints nil) (partial_order? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (partial_order_antisymmetric formula-decl nil partial_order_props "orders/") (directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (lower_bound? const-decl "bool" bounded_orders "orders/")) shostak)) (nonempty_T 0 (nonempty_T-1 nil 3330306835 ("" (typepred "<=") (("" (expand "pointed_directed_complete_partial_order?") (("" (flatten) (("" (expand "has_bottom?") (("" (skosimp) (("" (expand "nonempty?") (("" (expand "empty?") (("" (inst - "x!1") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (has_least? const-decl "bool" minmax_orders "orders/") (least? const-decl "bool" minmax_orders "orders/") (lower_bound? const-decl "bool" bounded_orders "orders/") (fullset const-decl "set" sets nil) (directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (directed_complete? const-decl "bool" directed_orders "orders/") (least_bounded_above? const-decl "bool" bounded_orders "orders/") (least_upper_bound? const-decl "bool" bounded_orders "orders/") (upper_bound? const-decl "bool" bounded_orders "orders/") (partial_order? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (partial_order_transitive formula-decl nil partial_order_props "orders/") (reflexive? const-decl "bool" relations nil) (partial_order_reflexive formula-decl nil partial_order_props "orders/") (empty? const-decl "bool" 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-nonempty-type-decl nil fixpoints nil) (pred type-eq-decl nil defined_types nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil)) shostak)) (IMP_monoid_TCC1 0 (IMP_monoid_TCC1-1 nil 3330308000 ("" (expand "monoid?") (("" (expand "monad?") (("" (expand "groupoid?") (("" (expand "star_closed?") (("" (split) (("1" (expand "fullset") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "fullset") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil) ("3" (expand "identity?") (("3" (expand "restrict") (("3" (skosimp) (("3" (split) (("1" (apply-extensionality :hide? t) (("1" (expand "o") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "o") (("2" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "associative?") (("4" (skosimp) (("4" (expand "restrict") (("4" (apply-extensionality :hide? t) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((monad? const-decl "bool" monad_def "algebra/") (member const-decl "bool" sets nil) (fullset const-decl "set" sets nil) (restrict const-decl "R" restrict nil) (O const-decl "T3" function_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil fixpoints nil) (identity? const-decl "bool" operator_defs nil) (associative? const-decl "bool" operator_defs nil) (star_closed? const-decl "bool" groupoid_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/")) shostak)) (lub_add_bottom_TCC1 0 (lub_add_bottom_TCC1-2 nil 3407241824 ("" (skosimp) (("" (typepred "D!1") (("" (expand "lub_set?") (("" (typepred "<=") (("" (expand "pointed_directed_complete_partial_order?") (("" (expand "directed_complete_partial_order?") (("" (flatten) (("" (expand "directed_complete?") (("" (inst - "D!1") (("1" (expand "least_bounded_above?") (("1" (skosimp) (("1" (inst + "t!1") (("1" (hide -5) (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (split) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "r!1") (("1" (expand "add") (("1" (split) (("1" (lemma "bottom_le" ("x" "t!1")) (("1" (assert) nil nil)) nil) ("2" (expand "member") (("2" (inst -3 "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -4 "r!1") (("2" (assert) (("2" (expand "upper_bound?" (2 -1)) (("2" (skosimp) (("2" (typepred "r!2") (("2" (inst - "r!2") (("2" (expand "add") (("2" (flatten) (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (expand "directed?") (("2" (expand "directed?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((directed type-eq-decl nil directed_order_props "orders/") (directed? const-decl "bool" directed_order_props "orders/") (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (pred type-eq-decl nil defined_types nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil fixpoints nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (directed_complete? const-decl "bool" directed_orders "orders/") (least_bounded_above? const-decl "bool" bounded_orders "orders/") (least_upper_bound? const-decl "bool" bounded_orders "orders/") (member const-decl "bool" sets nil) (r!1 skolem-const-decl "(add[T](bottom, D!1))" fixpoints nil) (bottom_le formula-decl nil fixpoints nil) (bottom const-decl "(LAMBDA (t: T): least?(t, fullset[T], <=))" fixpoints nil) (fullset const-decl "set" sets nil) (least? const-decl "bool" minmax_orders "orders/") (add const-decl "(nonempty?)" sets nil) (upper_bound? const-decl "bool" bounded_orders "orders/") (r!2 skolem-const-decl "(D!1)" fixpoints nil) (fullset_is_clopen name-judgement "clopen[T, scott_open_sets]" fixpoints nil) (D!1 skolem-const-decl "directed[T, <=]" fixpoints nil) (directed? const-decl "bool" directed_orders "orders/") (partial_order? const-decl "bool" orders nil) (lub_set? const-decl "bool" bounded_order_props "orders/")) nil) (lub_add_bottom_TCC1-1 nil 3352752603 ("" (skosimp) (("" (typepred "D!1") (("" (typepred "<=") (("" (expand "pointed_directed_complete_partial_order?") (("" (expand "directed_complete_partial_order?") (("" (flatten) (("" (expand "lub_set?") (("" (expand "directed_complete?") (("" (inst - "add[T](bottom, D!1)") (("" (hide 2 -2 -3) (("" (expand "directed?") (("" (skosimp) (("" (expand "add") (("" (expand "member") (("" (expand "directed?") (("" (split -1) (("1" (inst + "y!1") (("1" (rewrite "partial_order_reflexive" 1) (("1" (replace -1 1 rl) (("1" (rewrite "bottom_le") nil nil)) nil)) nil) ("2" (expand "add") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (split -2) (("1" (inst + "x!1") (("1" (rewrite "partial_order_reflexive" 1) (("1" (replace -1 1 rl) (("1" (rewrite "bottom_le") nil nil)) nil)) nil) ("2" (expand "add") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (inst - "x!1" "y!1") (("2" (assert) (("2" (skosimp) (("2" (inst + "z!1") (("1" (assert) nil nil) ("2" (expand "add") (("2" (expand "member") (("2" (propax) 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) ((directed type-eq-decl nil directed_order_props "orders/") (directed? const-decl "bool" directed_order_props "orders/") (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (directed_complete? const-decl "bool" directed_orders "orders/") (member const-decl "bool" sets nil) (partial_order_reflexive formula-decl nil partial_order_props "orders/") (fullset const-decl "set" sets nil) (least? const-decl "bool" minmax_orders "orders/") (add const-decl "(nonempty?)" sets nil) (directed? const-decl "bool" directed_orders "orders/") (partial_order? const-decl "bool" orders nil) (lub_set? const-decl "bool" bounded_order_props "orders/") (directed_complete_partial_order? const-decl "bool" directed_orders "orders/")) nil)) (lub_add_bottom 0 (lub_add_bottom-1 nil 3352753179 ("" (skosimp) (("" (typepred "lub(D!1)") (("1" (typepred "lub(add(bottom,D!1))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (inst -2 "lub(D!1)") (("1" (split -2) (("1" (inst -4 "lub(add(bottom, D!1))") (("1" (split -4) (("1" (lemma "partial_order_antisymmetric" ("x" "lub(D!1)" "y" "lub(add(bottom, D!1))")) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "r!1") (("2" (inst -3 "r!1") (("2" (expand "add") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "<=") (("2" (expand "pointed_directed_complete_partial_order?") (("2" (expand "directed_complete_partial_order?") (("2" (expand "partial_order?") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "r!1") (("2" (expand "add") (("2" (split -1) (("1" (replace -1 * rl) (("1" (rewrite "bottom_le") nil nil)) nil) ("2" (expand "member") (("2" (inst -3 "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "<=") (("2" (expand "pointed_directed_complete_partial_order?") (("2" (expand "directed_complete_partial_order?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "<=") (("2" (expand "pointed_directed_complete_partial_order?") (("2" (flatten) (("2" (expand "directed_complete_partial_order?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((directed type-eq-decl nil directed_order_props "orders/") (directed? const-decl "bool" directed_order_props "orders/") (nonempty? const-decl "bool" sets nil) (lub const-decl "{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" bounded_order_props "orders/") (lub_set? const-decl "bool" bounded_order_props "orders/") (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (least_upper_bound? const-decl "bool" bounded_orders "orders/") (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil fixpoints nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (upper_bound? const-decl "bool" bounded_orders "orders/") (partial_order_antisymmetric formula-decl nil partial_order_props "orders/") (D!1 skolem-const-decl "directed[T, <=]" fixpoints nil) (r!1 skolem-const-decl "(D!1)" fixpoints nil) (member const-decl "bool" sets nil) (bottom_le formula-decl nil fixpoints nil) (r!1 skolem-const-decl "(add(bottom, D!1))" fixpoints nil) (add const-decl "(nonempty?)" sets nil) (least? const-decl "bool" minmax_orders "orders/") (fullset const-decl "set" sets nil) (bottom const-decl "(LAMBDA (t: T): least?(t, fullset[T], <=))" fixpoints nil)) shostak)) (increasing_phi_n 0 (increasing_phi_n-1 nil 3330313672 ("" (induct "n") (("1" (expand "power") (("1" (skosimp) (("1" (expand "increasing?") (("1" (skosimp*) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "power" 1) (("2" (expand "o") (("2" (inst - "phi!1") (("2" (typepred "phi!1") (("2" (expand "increasing?") (("2" (skosimp*) (("2" (inst - "power(phi!1, j!1)(x!1)" "power(phi!1, j!1)(y!1)") (("2" (inst - "x!1" "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (typepred "<=") (("3" (expand "pointed_directed_complete_partial_order?") (("3" (expand "directed_complete_partial_order?") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (nat_induction formula-decl nil naturalnumbers nil) (power def-decl "T" monoid_def "algebra/") (O const-decl "T3" function_props nil) (increasing? const-decl "bool" fun_preds_partial nil) (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (T formal-nonempty-type-decl nil fixpoints nil) (pred type-eq-decl nil defined_types 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)) shostak)) (increasing_power 0 (increasing_power-1 nil 3330311141 ("" (skosimp) (("" (typepred "phi!1") (("" (expand "increasing?") (("" (skosimp*) (("" (lemma "increasing_phi_n" ("phi" "phi!1" "n" "x!1")) (("" (lemma "bottom_le" ("x" "power(phi!1, y!1-x!1)(bottom)")) (("1" (hide -3) (("1" (expand "increasing?") (("1" (inst - "bottom" "power(phi!1, y!1 - x!1)(bottom)") (("1" (assert) (("1" (lemma "power_mult" ("a" "phi!1" "n" "x!1" "m" "y!1-x!1")) (("1" (expand "o") (("1" (replace -1 1 rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((increasing? const-decl "bool" fun_preds_partial nil) (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (pred type-eq-decl nil defined_types nil) (T formal-nonempty-type-decl nil fixpoints nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (bottom const-decl "(LAMBDA (t: T): least?(t, fullset[T], <=))" fixpoints nil) (fullset const-decl "set" sets nil) (least? const-decl "bool" minmax_orders "orders/") (set type-eq-decl nil sets nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (power def-decl "T" monoid_def "algebra/") (O const-decl "T3" function_props nil) (bottom_le formula-decl nil fixpoints nil) (int_minus_int_is_int application-judgement "int" integers 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) (power_mult formula-decl nil monoid "algebra/") (x!1 skolem-const-decl "nat" fixpoints nil) (y!1 skolem-const-decl "nat" fixpoints nil) (increasing_phi_n formula-decl nil fixpoints nil) (number nonempty-type-decl nil numbers 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (fix_approx_nonempty 0 (fix_approx_nonempty-1 nil 3330310179 ("" (skosimp) (("" (expand "nonempty?") (("" (expand "empty?") (("" (inst - "bottom") (("" (expand "FIX_APPROX") (("" (grind) (("" (inst + "0") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (T formal-nonempty-type-decl nil fixpoints 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) (least? const-decl "bool" minmax_orders "orders/") (fullset const-decl "set" sets nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (bottom const-decl "(LAMBDA (t: T): least?(t, fullset[T], <=))" fixpoints nil) (member const-decl "bool" sets nil) (image const-decl "set[R]" function_image nil) (O const-decl "T3" function_props nil) (power def-decl "T" monoid_def "algebra/") (nat nonempty-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) (FIX_APPROX const-decl "set[T]" fixpoints nil) (empty? const-decl "bool" sets nil)) shostak)) (fix_approx_chain 0 (fix_approx_chain-1 nil 3330310223 ("" (skosimp) (("" (expand "FIX_APPROX") (("" (expand "fullset") (("" (expand "image") (("" (expand "chain?") (("" (expand "total_order?") (("" (expand "dichotomous?") (("" (expand "restrict") (("" (typepred "<=") (("" (expand "pointed_directed_complete_partial_order?") (("" (flatten) (("" (expand "directed_complete_partial_order?") (("" (flatten) (("" (hide -2 -3) (("" (expand "partial_order?") (("" (prop) (("" (expand "preorder?") (("" (flatten) (("" (skosimp) (("" (typepred "x!1") (("" (skosimp) (("" (typepred "y!1") (("" (skosimp) (("" (lemma "trich_lt" ("x" "x!2" "y" "x!3")) (("" (case "forall (i,j:nat): i <= j => power(phi!1, i)(bottom) <= power(phi!1, j)(bottom)") (("1" (split -2) (("1" (inst - "x!2" "x!3") (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (replace -3 * rl) (("2" (replace -4 * rl) (("2" (hide-all-but (1 -5)) (("2" (expand "reflexive?") (("2" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst - "x!3" "x!2") (("3" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (-4 -5 -6 1)) (("2" (skosimp) (("2" (lemma "increasing_power" ("phi" "phi!1")) (("2" (expand "increasing?") (("2" (inst - "i!1" "j!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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((FIX_APPROX const-decl "set[T]" fixpoints nil) (image const-decl "set[R]" function_image nil) (total_order? const-decl "bool" orders nil) (restrict const-decl "R" restrict nil) (directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (bottom const-decl "(LAMBDA (t: T): least?(t, fullset[T], <=))" fixpoints nil) (least? const-decl "bool" minmax_orders "orders/") (set type-eq-decl nil sets nil) (increasing? const-decl "bool" fun_preds_partial nil) (power def-decl "T" monoid_def "algebra/") (O const-decl "T3" function_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (TRUE const-decl "bool" booleans nil) (nat nonempty-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) (trich_lt formula-decl nil real_props nil) (increasing_power formula-decl nil fixpoints nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (reflexive? const-decl "bool" relations nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (preorder? const-decl "bool" orders nil) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (pred type-eq-decl nil defined_types nil) (T formal-nonempty-type-decl nil fixpoints nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (dichotomous? const-decl "bool" orders nil) (chain? const-decl "bool" chain "orders/") (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) (fullset const-decl "set" sets nil)) shostak)) (ne_chain_is_directed 0 (ne_chain_is_directed-1 nil 3330315762 ("" (skosimp) (("" (typepred "X!1") (("" (expand "directed?") (("" (skosimp) (("" (expand "chain?") (("" (expand "total_order?") (("" (expand "restrict") (("" (expand "dichotomous?") (("" (inst - "x!1" "y!1") (("" (split) (("1" (inst + "y!1") (("1" (assert) nil nil)) nil) ("2" (inst + "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil fixpoints nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans 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) (total_order? const-decl "bool" orders nil) (dichotomous? const-decl "bool" orders nil) (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (pred type-eq-decl nil defined_types nil) (partial_order_reflexive formula-decl nil partial_order_props "orders/") (y!1 skolem-const-decl "T" fixpoints nil) (x!1 skolem-const-decl "T" fixpoints nil) (X!1 skolem-const-decl "(nonempty?[T])" fixpoints nil) (restrict const-decl "R" restrict nil) (chain? const-decl "bool" chain "orders/") (directed? const-decl "bool" directed_orders "orders/")) shostak)) (lub_emptyset_TCC1 0 (lub_emptyset_TCC1-1 nil 3352752603 ("" (expand "lub_set?") (("" (expand "least_bounded_above?") (("" (inst + "bottom") (("" (expand "least_upper_bound?") (("" (expand "upper_bound?") (("" (split) (("1" (skosimp) (("1" (typepred "r!1") (("1" (expand "emptyset") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "bottom_le") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((least_bounded_above? const-decl "bool" bounded_orders "orders/") (least_upper_bound? const-decl "bool" bounded_orders "orders/") (NOT const-decl "[bool -> bool]" booleans nil) (emptyset const-decl "set" sets nil) (bottom_le formula-decl nil fixpoints nil) (upper_bound? const-decl "bool" bounded_orders "orders/") (bottom const-decl "(LAMBDA (t: T): least?(t, fullset[T], <=))" fixpoints nil) (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (fullset const-decl "set" sets nil) (least? const-decl "bool" minmax_orders "orders/") (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-nonempty-type-decl nil fixpoints nil) (lub_set? const-decl "bool" bounded_order_props "orders/")) nil)) (lub_emptyset 0 (lub_emptyset-1 nil 3352753432 ("" (typepred "lub(emptyset[T])") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (inst -2 "bottom") (("1" (split -2) (("1" (lemma "le_bottom" ("x" "lub(emptyset[T])")) (("1" (assert) nil nil)) nil) ("2" (skosimp) (("2" (typepred "r!1") (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "<=") (("2" (expand "pointed_directed_complete_partial_order?") (("2" (flatten) (("2" (expand "directed_complete_partial_order?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ((upper_bound? const-decl "bool" bounded_orders "orders/") (le_bottom formula-decl nil fixpoints nil) (least? const-decl "bool" minmax_orders "orders/") (fullset const-decl "set" sets nil) (bottom const-decl "(LAMBDA (t: T): least?(t, fullset[T], <=))" fixpoints nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (emptyset_is_clopen name-judgement "clopen[T, scott_open_sets]" fixpoints nil) (finite_emptyset name-judgement "finite_set[T]" fixpoints 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-nonempty-type-decl nil fixpoints nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (least_upper_bound? const-decl "bool" bounded_orders "orders/") (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (lub_set? const-decl "bool" bounded_order_props "orders/") (lub const-decl "{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" bounded_order_props "orders/") (emptyset const-decl "set" sets nil)) shostak)) (fix_TCC1 0 (fix_TCC1-1 nil 3330308687 ("" (skosimp) (("" (lemma "fix_approx_chain" ("phi" "phi!1")) (("" (lemma "fix_approx_nonempty" ("phi" "phi!1")) (("" (lemma "ne_chain_is_directed" ("X" "FIX_APPROX(phi!1)")) (("1" (assert) (("1" (assert) (("1" (lemma "directed_is_lub_set" ("x" "FIX_APPROX(phi!1)")) (("1" (propax) nil nil) ("2" (expand "directed?" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((increasing? const-decl "bool" fun_preds_partial nil) (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (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-nonempty-type-decl nil fixpoints nil) (fix_approx_chain formula-decl nil fixpoints nil) (FIX_APPROX const-decl "set[T]" fixpoints nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (ne_chain_is_directed formula-decl nil fixpoints nil) (directed_is_lub_set judgement-tcc nil directed_order_props "orders/") (directed? const-decl "bool" directed_order_props "orders/") (directed type-eq-decl nil directed_order_props "orders/") (fix_approx_nonempty formula-decl nil fixpoints nil)) shostak)) (member_FIX 0 (member_FIX-1 nil 3330321661 ("" (skosimp) (("" (expand "member") (("" (expand "FIX") (("" (propax) nil nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (FIX const-decl "set[T]" fixpoints nil)) shostak)) (fix_is_least 0 (fix_is_least-1 nil 3330321980 ("" (skosimp) (("" (expand "fix") (("" (expand "FIX") (("" (expand "member") (("" (case "forall n: power(phi!1,n)(x!1) = x!1") (("1" (lemma "bottom_le" ("x" "x!1")) (("1" (lemma "increasing_phi_n" ("phi" "phi!1")) (("1" (case "forall n: power(phi!1, n)(bottom) <= x!1") (("1" (lemma "fix_approx_nonempty" ("phi" "phi!1")) (("1" (lemma "fix_approx_chain" ("phi" "phi!1")) (("1" (case "lub_set?(FIX_APPROX(phi!1))") (("1" (typepred "lub[T, <=](FIX_APPROX(phi!1))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst - "x!1") (("1" (replace 1 -2) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "r!1") (("1" (expand "FIX_APPROX") (("1" (hide -2) (("1" (expand "image") (("1" (skosimp) (("1" (inst -5 "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "fix_TCC1" ("phi" "phi!1")) (("2" (propax) nil nil)) nil) ("3" (typepred "<=") (("3" (expand "pointed_directed_complete_partial_order?") (("3" (expand "directed_complete_partial_order?") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "n!1") (("2" (expand "increasing?") (("2" (inst - "bottom" "x!1") (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (induct "n") (("1" (expand "power") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (expand "power" 1) (("2" (expand "o") (("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fix const-decl "T" fixpoints nil) (member const-decl "bool" sets nil) (nat_induction formula-decl nil naturalnumbers nil) (bottom_le formula-decl nil fixpoints nil) (set type-eq-decl nil sets nil) (least? const-decl "bool" minmax_orders "orders/") (fullset const-decl "set" sets nil) (bottom const-decl "(LAMBDA (t: T): least?(t, fullset[T], <=))" fixpoints nil) (fix_approx_chain formula-decl nil fixpoints nil) (fix_TCC1 subtype-tcc nil fixpoints nil) (NOT const-decl "[bool -> bool]" booleans nil) (least_upper_bound? const-decl "bool" bounded_orders "orders/") (lub const-decl "{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" bounded_order_props "orders/") (image const-decl "set[R]" function_image nil) (upper_bound? const-decl "bool" bounded_orders "orders/") (FIX_APPROX const-decl "set[T]" fixpoints nil) (lub_set? const-decl "bool" bounded_order_props "orders/") (fix_approx_nonempty formula-decl nil fixpoints nil) (increasing_phi_n formula-decl nil fixpoints 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil fixpoints nil) (= const-decl "[T, T -> boolean]" equalities nil) (O const-decl "T3" function_props nil) (power def-decl "T" monoid_def "algebra/") (pred type-eq-decl nil defined_types nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (<= formal-const-decl "(pointed_directed_complete_partial_order?[T])" fixpoints nil) (increasing? const-decl "bool" fun_preds_partial nil) (FIX const-decl "set[T]" fixpoints nil)) shostak)) (fix_le 0 (fix_le-1 nil 3352796666 ("" (skosimp) (("" (typepred "phi!1") (("" (expand "fix") (("" (lemma "fix_approx_chain" ("phi" "phi!1")) (("" (case "lub_set?(FIX_APPROX(phi!1))") (("1" (typepred "lub(FIX_APPROX(phi!1))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst - "phi!1(lub[T, <=](FIX_APPROX(phi!1)))") (("1" (split -2) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "r!1") (("2" (name-replace "LUB" "lub[T, <=](FIX_APPROX(phi!1))") (("2" (expand "FIX_APPROX") (("2" (expand "fullset") (("2" (expand "image") (("2" (skosimp) (("2" (case-replace "x!1=0") (("1" (expand "power") (("1" (replace -2) (("1" (rewrite "bottom_le") nil nil)) nil)) nil) ("2" (inst - "power(phi!1,x!1-1)(bottom)") (("1" (expand "increasing?") (("1" (inst - "power(phi!1, x!1 - 1)(bottom)" "LUB") (("1" (assert) (("1" (expand "power" -1) (("1" (expand "o") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "FIX_APPROX") (("2" (expand "image") (("2" (inst + "x!1-1") (("2" (assert) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "<=") (("2" (expand "pointed_directed_complete_partial_order?") (("2" (expand "directed_complete_partial_order?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.96 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 |
