|
(fun_below_props
(cartesian_bijection 0
(cartesian_bijection-1 nil 3308405027
("" (skolem!)
(("" (case "m!1 = 0")
(("1" (inst + "LAMBDA (x: [below[n!1], below[m!1]]): 0")
(("1" (grind :if-match nil)
(("1" (typepred "x1!1`2") (("1" (assert) nil nil)) nil)) nil)
("2" (skolem!)
(("2" (typepred "x!1`2") (("2" (assert) nil nil)) nil)) nil))
nil)
("2"
(inst +
"LAMBDA (x: [below[n!1], below[m!1]]): m!1 * x`1 + x`2")
(("1" (grind :if-match nil)
(("1" (inst + "(ndiv(y!1, m!1), rem(m!1)(y!1))")
(("1" (assert) nil nil)
("2" (assert)
(("2" (typepred "ndiv(y!1, m!1)")
(("2" (case "ndiv(y!1, m!1) <= y!1 / m!1")
(("1" (hide -2 -3)
(("1"
(lemma "both_sides_div_pos_lt1"
("pz" "m!1" "x" "y!1" "y" "n!1 * m!1"))
(("1" (assert) nil nil)) nil))
nil)
("2" (use "ndiv_lt") nil nil))
nil))
nil))
nil))
nil)
("2" (forward-chain "unique_division")
(("2" (apply-extensionality 2) nil nil)) nil))
nil)
("2" (skolem!)
(("2" (assert)
(("2"
(lemma "both_sides_times_pos_le1"
("x" "x!1`1" "y" "n!1 - 1" "pz" "m!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(bijective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(n!1 skolem-const-decl "nat" fun_below_props nil)
(below type-eq-decl nil nat_types nil)
(m!1 skolem-const-decl "nat" fun_below_props nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(both_sides_div_pos_lt1 formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ndiv_lt formula-decl nil modulo_arithmetic nil)
(<= const-decl "bool" reals nil)
(y!1 skolem-const-decl "below[n!1 * m!1]" fun_below_props nil)
(ndiv const-decl "{q: int | x = b * q + rem(b)(x)}"
modulo_arithmetic nil)
(rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}"
modulo_arithmetic nil)
(mod nonempty-type-eq-decl nil euclidean_division nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(nil application-judgement "upto(n)" modulo_arithmetic nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(unique_division formula-decl nil euclidean_division nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil))
shostak))
(empty_domain1 0
(empty_domain1-1 nil 3308405352
("" (skolem!)
(("" (inst + "LAMBDA (x: below[0]): 0")
(("" (skolem-typepred) nil nil)) nil))
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)
(FALSE const-decl "bool" booleans nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(m!1 skolem-const-decl "nat" fun_below_props nil))
shostak))
(empty_domain2 0
(empty_domain2-1 nil 3308405370
("" (skolem!) (("" (apply-extensionality) nil nil)) 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)
(FALSE const-decl "bool" booleans nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil))
shostak))
(empty_range 0
(empty_range-1 nil 3308405383
("" (skosimp*)
(("" (typepred "f!1(0)") (("" (assert) nil nil)) nil)) nil)
((below type-eq-decl nil nat_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(< 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(funset_bijection_TCC1 0
(funset_bijection_TCC1-1 nil 3308404994 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(funset_bijection 0
(funset_bijection-1 nil 3308405401
("" (induct "n")
(("1" (skolem!)
(("1" (inst + "LAMBDA (x: [below[0] -> below[m!1]]): 0")
(("1" (grind)
(("1" (rewrite "empty_domain1") nil nil)
("2" (rewrite "empty_domain2") nil nil))
nil)
("2" (grind) nil nil))
nil))
nil)
("2" (skosimp*)
(("2" (case "m!1 = 0")
(("1" (delete -2)
(("1" (assert)
(("1" (lemma "empty_range" ("m" "m!1" "p" "1 + j!1"))
(("1" (assert)
(("1"
(inst +
"LAMBDA (h: [below[1 + j!1] -> below[m!1]]): 0")
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (inst - "m!1")
(("2" (skolem!)
(("2"
(inst +
"LAMBDA (h: [below[1 + j!1] -> below[m!1]]): m!1 * f!1(LAMBDA (x: below[j!1]): h(x)) + h(j!1)")
(("1" (expand "bijective?")
(("1" (prop)
(("1" (delete -2)
(("1" (expand "injective?")
(("1" (skosimp)
(("1"
(name-replace "h1"
"LAMBDA (x: below[j!1]): x1!1(x)" :hide?
nil)
(("1"
(name-replace "h2"
"LAMBDA (x: below[j!1]): x2!1(x)" :hide?
nil)
(("1"
(lemma
"unique_division"
("b"
"m!1"
"q1"
"f!1(h1)"
"q2"
"f!1(h2)"
"r1"
"x1!1(j!1)"
"r2"
"x2!1(j!1)"))
(("1"
(smash)
(("1"
(inst - "h1" "h2")
(("1"
(assert)
(("1"
(apply-extensionality :hide? t)
(("1"
(case "h1(x!1) = h2(x!1)")
(("1"
(replace -4 -1 rl)
(("1"
(replace -5 -1 rl)
(("1" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (delete -1)
(("2" (expand "surjective?")
(("2" (skolem!)
(("2" (inst - "ndiv(y!1, m!1)")
(("1" (skolem!)
(("1"
(inst
+
"LAMBDA (x: below[1 + j!1]): IF x = j!1 THEN rem(m!1)(y!1) ELSE x!1(x) ENDIF")
(("1"
(assert)
(("1"
(replace-eta "x!1")
(("1"
(typepred "ndiv(y!1, m!1)")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2" (assert) nil nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(typepred "y!1")
(("2"
(expand "^")
(("2"
(expand "expt" -)
(("2"
(use "ndiv_lt")
(("2"
(assert)
(("2"
(lemma
"both_sides_div_pos_lt1"
("pz"
"m!1"
"x"
"y!1"
"y"
"m!1 * expt(m!1, j!1)"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skolem!)
(("2" (assert)
(("2"
(name-replace "u"
"f!1(LAMBDA (x: below[j!1]): h!1(x))")
(("2" (typepred "u")
(("2" (auto-rewrite "expt_plus" "expt_x1")
(("2" (assert)
(("2" (name-replace "v" "m!1 ^ j!1")
(("2"
(lemma
"both_sides_times_pos_le2"
("x" "u" "y" "v - 1" "pz" "m!1"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(both_sides_times_pos_le2 formula-decl nil real_props nil)
(expt_plus formula-decl nil exponentiation nil)
(expt_x1 formula-decl nil exponentiation nil)
(ndiv_lt formula-decl nil modulo_arithmetic nil)
(both_sides_div_pos_lt1 formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(<= const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(y!1 skolem-const-decl "below[m!1 ^ (1 + j!1)]" fun_below_props
nil)
(ndiv const-decl "{q: int | x = b * q + rem(b)(x)}"
modulo_arithmetic nil)
(rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}"
modulo_arithmetic nil)
(nil application-judgement "upto(n)" modulo_arithmetic nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(mod nonempty-type-eq-decl nil euclidean_division nil)
(unique_division formula-decl nil euclidean_division nil)
(f!1 skolem-const-decl
"[[below[j!1] -> below[m!1]] -> below[m!1 ^ j!1]]" fun_below_props
nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(empty_range formula-decl nil fun_below_props nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(j!1 skolem-const-decl "nat" fun_below_props nil)
(m!1 skolem-const-decl "nat" fun_below_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(surjective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(expt def-decl "real" exponentiation nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat_expt application-judgement "nat" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(empty_domain1 formula-decl nil fun_below_props nil)
(empty_domain2 formula-decl nil fun_below_props nil)
(m!1 skolem-const-decl "nat" fun_below_props nil)
(FALSE const-decl "bool" booleans nil)
(nat_induction formula-decl nil naturalnumbers nil)
(bijective? const-decl "bool" functions nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals 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)
(nat_exp application-judgement "nat" exponentiation nil))
shostak)))
¤ Dauer der Verarbeitung: 0.30 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.
|
