|
(euclidean
(sigma_nnreal_eq_0_TCC1 0
(sigma_nnreal_eq_0_TCC1-1 nil 3508674642 ("" (subtype-tcc) nil nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(sigma_nnreal_eq_0 0
(sigma_nnreal_eq_0-1 nil 3508674648
("" (skosimp)
((""
(lemma "sigma_nonneg_eq_0" ("low" "0" "high" "n-1" "Fnnr" "f!1"))
(("" (split 1)
(("1" (flatten)
(("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)
("2" (flatten)
(("2" (hide -2)
(("2" (lemma "sigma_zero" ("low" "0" "high" "n-1"))
(("2"
(lemma "sigma_eq"
("low" "0" "high" "n-1" "F" "LAMBDA (i: below(n)): 0"
"G" "f!1"))
(("2" (split -1)
(("1" (assert) nil nil)
("2" (hide -1 2)
(("2" (skosimp)
(("2" (inst - "n1!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((below type-eq-decl nil naturalnumbers nil)
(n formal-const-decl "posnat" euclidean nil)
(posnat 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)
(T_low type-eq-decl nil sigma "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(T_high type-eq-decl nil sigma "reals/")
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(below type-eq-decl nil nat_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sigma_nonneg_eq_0 formula-decl nil sigma "reals/")
(int_minus_int_is_int application-judgement "int" integers nil)
(sigma_zero formula-decl nil sigma "reals/")
(sigma_nat application-judgement "nat" euclidean nil)
(subrange type-eq-decl nil integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sigma_eq formula-decl nil sigma "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sigma_nnreal application-judgement "nnreal" euclidean nil))
nil))
(d1_TCC1 0
(d1_TCC1-2 nil 3508674747
("" (expand "metric?")
(("" (split)
(("1" (expand "metric_zero?")
(("1" (skosimp*)
(("1" (split)
(("1" (flatten)
(("1" (apply-extensionality 1 :hide? t)
(("1" (rewrite "sigma_nnreal_eq_0" -1)
(("1" (inst - "x!2") (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1)
(("2" (lemma "sigma_zero" ("low" "0" "high" "n-1"))
(("2"
(lemma "extensionality_postulate"
("f" "LAMBDA (i: below(n)): 0" "g"
"LAMBDA i: abs(y!1(i) - y!1(i))"))
(("2" (flatten)
(("2" (hide -2)
(("2" (split)
(("1" (assert) nil nil)
("2" (hide -1 2)
(("2" (skosimp) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "metric_symmetric?")
(("2" (skosimp*)
(("2" (lemma "extensionality_postulate[below[n],nnreal]")
(("2"
(inst - "LAMBDA i: abs(x!1(i) - y!1(i))"
"LAMBDA i: abs(y!1(i) - x!1(i))")
(("2" (flatten)
(("2" (hide -2)
(("2" (split)
(("1" (assert) nil nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "metric_triangle?")
(("3" (skosimp*)
(("3" (rewrite "sigma_sum" 1)
(("3"
(lemma "sigma_le"
("low" "0" "high" "n-1" "F"
"LAMBDA (i_1: below[n]): abs(x!1(i_1) - z!1(i_1))" "G"
"LAMBDA (i_1: below(n)):
abs(x!1(i_1) - y!1(i_1)) + abs(y!1(i_1) - z!1(i_1))"))
(("3" (split -1)
(("1" (propax) nil nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((below type-eq-decl nil naturalnumbers nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(<= const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(sigma_zero formula-decl nil sigma "reals/")
(sigma_nat application-judgement "nat" euclidean nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(extensionality_postulate formula-decl nil functions nil)
(sigma_nnreal_eq_0 formula-decl nil euclidean nil)
(below type-eq-decl nil nat_types nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(n formal-const-decl "posnat" euclidean nil)
(posnat 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)
(metric_zero? const-decl "bool" metric_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(metric_symmetric? const-decl "bool" metric_def nil)
(sigma_le formula-decl nil sigma "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(subrange type-eq-decl nil integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sigma_sum formula-decl nil sigma "reals/")
(metric_triangle? const-decl "bool" metric_def nil)
(metric? const-decl "bool" metric_def nil)
(sigma_nnreal application-judgement "nnreal" euclidean nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil)
(d1_TCC1-1 nil 3382851446
("" (expand "metric?")
(("" (split)
(("1" (expand "metric_zero?")
(("1" (skosimp*)
(("1" (split)
(("1" (flatten)
(("1" (apply-extensionality 1 :hide? t)
(("1" (rewrite "sigma_nnreal" -1)
(("1" (inst - "x!2") (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1)
(("2" (lemma "sigma_zero" ("low" "0" "high" "n-1"))
(("2"
(lemma "extensionality_postulate"
("f" "LAMBDA (i: below(n)): 0" "g"
"LAMBDA i: abs(y!1(i) - y!1(i))"))
(("2" (flatten)
(("2" (hide -2)
(("2" (split)
(("1" (assert) nil nil)
("2" (hide -1 2)
(("2" (skosimp) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "metric_symmetric?")
(("2" (skosimp*)
(("2" (lemma "extensionality_postulate[below[n],nnreal]")
(("2"
(inst - "LAMBDA i: abs(x!1(i) - y!1(i))"
"LAMBDA i: abs(y!1(i) - x!1(i))")
(("2" (flatten)
(("2" (hide -2)
(("2" (split)
(("1" (assert) nil nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "metric_triangle?")
(("3" (skosimp*)
(("3" (rewrite "sigma_sum" 1)
(("3"
(lemma "sigma_le"
("low" "0" "high" "n-1" "F"
"LAMBDA (i_1: below[n]): abs(x!1(i_1) - z!1(i_1))" "G"
"LAMBDA (i_1: below(n)):
abs(x!1(i_1) - y!1(i_1)) + abs(y!1(i_1) - z!1(i_1))"))
(("3" (split -1)
(("1" (propax) nil nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(sigma_zero formula-decl nil sigma "reals/")
(extensionality_postulate formula-decl nil functions nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(metric_zero? const-decl "bool" metric_def nil)
(metric_symmetric? const-decl "bool" metric_def nil)
(sigma_le formula-decl nil sigma "reals/")
(sigma_sum formula-decl nil sigma "reals/")
(metric_triangle? const-decl "bool" metric_def nil)
(metric? const-decl "bool" metric_def nil))
nil))
(d2_TCC1 0
(d2_TCC1-1 nil 3382851446
("" (expand "metric?")
(("" (split)
(("1" (expand "metric_zero?")
(("1" (skosimp)
(("1" (split)
(("1" (flatten)
(("1"
(lemma "sqrt_eq_0"
("nnx"
"sigma[below(n)](0, n - 1, LAMBDA i: sq(x!1(i) - y!1(i)))"))
(("1" (replace -2 -1)
(("1" (hide -2)
(("1"
(lemma "sigma_nonneg_eq_0[below(n)]"
("Fnnr"
"LAMBDA (i_1: below[n]): sq(x!1(i_1) - y!1(i_1))"
"low" "0" "high" "n-1"))
(("1" (replace -2 -1)
(("1" (assert)
(("1" (hide -2)
(("1"
(lemma "sub_eq_zero[n]"
("u" "x!1" "v" "y!1"))
(("1"
(replace -1 1 rl)
(("1"
(hide -1)
(("1"
(expand "-" 1)
(("1"
(apply-extensionality 1 :hide? t)
(("1"
(inst - "x!2")
(("1"
(rewrite "sq_eq_0")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (replace -1 * rl)
(("2" (hide -1)
(("2"
(lemma "extensionality"
("f" "LAMBDA (i:below(n)): sq(x!1(i) - x!1(i))"
"g" "lambda (i:below(n)): 0"))
(("2" (split -1)
(("1" (replace -1)
(("1" (rewrite "sigma_zero")
(("1" (assert) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (skosimp) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "metric_symmetric?")
(("2" (skosimp)
(("2"
(lemma "extensionality"
("f" "lambda (i:below(n)): sq(x!1(i) - y!1(i))" "g"
"lambda (i:below(n)): sq(y!1(i) - x!1(i))"))
(("2" (split -1)
(("1" (replace -1) (("1" (propax) nil nil)) nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (assert)
(("2" (rewrite "sq_neg_minus") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "metric_triangle?")
(("3" (skosimp*)
(("3" (lemma "norm_add_le" ("u" "x!1-y!1" "v" "y!1-z!1"))
(("3" (expand "norm")
(("3" (expand "-")
(("3" (expand "sqv")
(("3" (assert)
(("3" (expand "*")
(("3" (expand "sq")
(("3"
(name-replace "DRL1" "LAMBDA (i_1: Index[n]):
y!1(i_1) * y!1(i_1) - y!1(i_1) * z!1(i_1) +
(z!1(i_1) * z!1(i_1) - y!1(i_1) * z!1(i_1))")
(("3"
(name-replace "DRL2"
"LAMBDA (i_2: Index[n]):
x!1(i_2) * x!1(i_2) - x!1(i_2) * y!1(i_2) +
(y!1(i_2) * y!1(i_2) - x!1(i_2) * y!1(i_2))")
(("3"
(lemma "extensionality"
("f"
" LAMBDA (i_1: Index[n]):
((LAMBDA (i: Index[n]): x!1(i) - y!1(i)) +
(LAMBDA (i: Index[n]): y!1(i) - z!1(i)))
(i_1)
*
((LAMBDA (i: Index[n]): x!1(i) - y!1(i)) +
(LAMBDA (i: Index[n]): y!1(i) - z!1(i)))
(i_1)"
"g"
"LAMBDA i:
x!1(i) * x!1(i) - x!1(i) * z!1(i) +
(z!1(i) * z!1(i) - x!1(i) * z!1(i))"))
(("3"
(split -1)
(("1"
(replace -1)
(("1" (propax) nil nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skosimp)
(("2"
(expand "+")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sigma_zero formula-decl nil sigma "reals/")
(sqrt_0 formula-decl nil sqrt "reals/")
(sq_0 formula-decl nil sq "reals/")
(extensionality formula-decl nil functions nil)
(sigma_nonneg_eq_0 formula-decl nil sigma "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sub_eq_zero formula-decl nil vectors "vectors/")
(zero const-decl "Vector" vectors "vectors/")
(comp_zero formula-decl nil vectors "vectors/")
(sq_eq_0 formula-decl nil sq "reals/")
(- const-decl "real" vectors "vectors/")
(int_minus_int_is_int application-judgement "int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sigma_nnreal application-judgement "nnreal" euclidean nil)
(sqrt_eq_0 formula-decl nil sqrt "reals/")
(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)
(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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" 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)
(n formal-const-decl "posnat" euclidean nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(sigma def-decl "real" sigma "reals/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil nat_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(metric_zero? const-decl "bool" metric_def nil)
(sq_neg_minus formula-decl nil sq "reals/")
(metric_symmetric? const-decl "bool" metric_def nil)
(norm const-decl "nnreal" vectors "vectors/")
(sqv const-decl "nnreal" vectors "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors "vectors/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "real" vectors "vectors/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(norm_add_le formula-decl nil vectors "vectors/")
(metric_triangle? const-decl "bool" metric_def nil)
(metric? const-decl "bool" metric_def nil))
nil))
(dinf_TCC1 0
(dinf_TCC1-1 nil 3293695864
("" (skosimp*)
((""
(case "EXISTS (K:below[n]): FORALL (i:below[n]): abs(x!1(i)-y!1(i)) <= abs(x!1(K)-y!1(K))")
(("1"
(case-replace
"nonempty?[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})")
(("1"
(case-replace "above_bounded[nnreal]
({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})")
(("1" (expand "in_set")
(("1"
(case-replace
"sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z}) >= 0")
(("1" (skolem!)
(("1" (inst + "K!1")
(("1"
(typepred
"sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})")
(("1"
(name-replace "NNS"
"{z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z}")
(("1" (expand "least_upper_bound")
(("1" (flatten)
(("1" (inst -2 "abs(x!1(K!1) - y!1(K!1))")
(("1" (split -2)
(("1"
(expand "upper_bound")
(("1"
(inst -2 "abs(x!1(K!1) - y!1(K!1))")
(("1" (assert) nil nil)
("2"
(expand "NNS")
(("2" (inst + "K!1") nil nil))
nil))
nil))
nil)
("2" (assert) nil nil)
("3"
(hide 2)
(("3"
(expand "upper_bound")
(("3"
(skosimp*)
(("3"
(typepred "z!1")
(("3"
(expand "NNS" -2)
(("3"
(skolem!)
(("3"
(inst -7 "i!1")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(typepred
"sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})")
(("1"
(name-replace "NNS"
"{z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z}")
(("1" (expand "least_upper_bound")
(("1" (flatten)
(("1" (expand "upper_bound")
(("1" (inst -1 "abs(x!1(0)-y!1(0))")
(("1" (assert) nil nil)
("2" (hide 2)
(("2"
(expand "NNS")
(("2"
(inst + "0")
(("2" (assert) nil nil))
nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "above_bounded")
(("2" (skolem!)
(("2" (inst + "abs(x!1(K!1) - y!1(K!1))")
(("2" (expand "upper_bound")
(("2" (skosimp*)
(("2" (typepred "z!1")
(("2" (skolem!)
(("2" (inst - "i!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (inst - "abs(x!1(0)-y!1(0))")
(("1" (expand "member")
(("1" (inst + "0") (("1" (assert) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(case "FORALL (f: [below[n] -> nnreal], m: below[n]):
EXISTS (K: below[m+1]): FORALL (i: below[m+1]): f(i) <= f(K)")
(("1"
(inst - "lambda (i:below[n]): abs(x!1(i)-y!1(i))" "n-1")
(("1" (typepred "n") (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (induct "m")
(("1" (typepred "n")
(("1" (replace -1)
(("1" (skosimp*)
(("1" (inst + "0") (("1" (grind) nil nil)) nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst - "f!1")
(("2" (skolem!)
(("2" (case "f!1(K!1) <= f!1(jb!1+1)")
(("1" (inst + "jb!1+1")
(("1" (skosimp*)
(("1" (inst - "i!1")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (inst + "K!1")
(("2" (skosimp*)
(("2" (case "i!1<=jb!1")
(("1" (inst - "i!1")
(("1" (assert) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(n formal-const-decl "posnat" euclidean nil)
(posnat 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)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(above_bounded const-decl "bool" bounded_reals "reals/")
(setof type-eq-decl nil defined_types nil)
(sup_set type-eq-decl nil bounded_reals "reals/")
(pred type-eq-decl nil defined_types nil)
(least_upper_bound const-decl "bool" bound_defs "reals/")
(sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
"reals/")
(NNS skolem-const-decl "[nnreal -> boolean]" euclidean nil)
(x!1 skolem-const-decl "Vector[n]" euclidean nil)
(K!1 skolem-const-decl "below[n]" euclidean nil)
(y!1 skolem-const-decl "Vector[n]" euclidean nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(NNS skolem-const-decl "[nnreal -> boolean]" euclidean nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(in_set const-decl "bool" bounded_reals "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(nnreal type-eq-decl nil real_types nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(below type-eq-decl nil naturalnumbers nil)
(below_induction formula-decl nil bounded_nat_inductions nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(i!1 skolem-const-decl "below[2 + jb!1]" euclidean nil)
(jb!1 skolem-const-decl "below(n)" euclidean nil)
(i!1 skolem-const-decl "below[2 + jb!1]" euclidean nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(dinf_TCC2 0
(dinf_TCC2-1 nil 3382851446
("" (expand "metric?")
(("" (split)
(("1" (expand "metric_zero?")
(("1" (skosimp)
(("1" (split)
(("1" (flatten)
(("1"
(case "nonempty?[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})")
(("1"
(case "above_bounded[nnreal]
({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})")
(("1" (expand "max")
(("1"
(typepred
"sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})")
(("1" (expand "least_upper_bound")
(("1" (flatten)
(("1" (replace -5)
(("1"
(name-replace "XX"
"{z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z}")
(("1"
(hide -5)
(("1"
(expand "upper_bound")
(("1"
(apply-extensionality 1 :hide? t)
(("1"
(inst - "abs(x!1(x!2)-y!1(x!2))")
(("1"
(typepred
"abs(x!1(x!2)-y!1(x!2))")
(("1" (assert) nil nil))
nil)
("2"
(expand "XX")
(("2" (inst + "x!2") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (expand "above_bounded")
(("2" (expand "upper_bound")
(("2"
(inst +
"sigma(0,n-1,lambda (i:below(n)): abs(x!1(i) - y!1(i)))")
(("1" (skosimp)
(("1" (typepred "z!1")
(("1" (skosimp)
(("1"
(replace -2 1 rl)
(("1"
(hide -1 -2 -3 -4 2)
(("1"
(typepred "i!1")
(("1"
(lemma
"sigma_split[below(n)]"
("low"
"0"
"high"
"n-1"
"F"
"LAMBDA (i: below(n)): abs(x!1(i) - y!1(i))"))
(("1"
(inst - "i!1-1")
(("1"
(assert)
(("1"
(replace -1 1)
(("1"
(hide -1)
(("1"
(lemma
"sigma_nonneg"
("low"
"0"
"high"
"i!1-1"
"F"
" LAMBDA (i: below(n)): abs(x!1(i) - y!1(i))"))
(("1"
(split -1)
(("1"
(name-replace
"DRL1"
"sigma(0, i!1 - 1, LAMBDA (i: below(n)): abs(x!1(i) - y!1(i)))")
(("1"
(lemma
"sigma_first"
("low"
"i!1"
"high"
"n-1"
"F"
"LAMBDA (i_1: below(n)): abs(x!1(i_1) - y!1(i_1))"))
(("1"
(assert)
(("1"
(replace
-1
1)
(("1"
(hide -1)
(("1"
(lemma
"sigma_nonneg"
("low"
"1+i!1"
"high"
"n-1"
"F"
"LAMBDA (i_1: below(n)): abs(x!1(i_1) - y!1(i_1))"))
(("1"
(split
-1)
(("1"
(assert)
nil
nil)
("2"
(skosimp)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) (("2" (assert) nil nil)) nil)
("3" (assert) (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "member")
(("2" (inst - "abs(x!1(0)-y!1(0))")
(("1" (inst + "0") (("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1 * rl)
(("2" (assert)
(("2" (expand "abs")
(("2" (expand "max")
(("2"
(typepred
"sup[nnreal]({z: nnreal | EXISTS i: 0 = z})")
(("1" (expand "least_upper_bound")
(("1" (flatten)
(("1" (expand "upper_bound")
(("1"
(inst - "0")
(("1"
(assert)
(("1"
(inst - "0")
(("1"
(split)
(("1" (assert) nil nil)
("2" (propax) nil nil)
("3"
(skosimp)
(("3"
(typepred "z!1")
(("3"
(skosimp)
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst + "0")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (split)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1"
(expand "member")
(("1"
(inst - "0")
(("1"
(inst + "0")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "above_bounded")
(("2" (inst + "0")
(("2"
(expand "upper_bound")
(("2"
(skosimp)
(("2"
(typepred "z!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "metric_symmetric?")
(("2" (skosimp)
(("2"
(lemma "extensionality"
("a" "{z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z}"
"b" "{z: nnreal | EXISTS i: abs(y!1(i) - x!1(i)) = z}"))
(("2" (split -1)
(("1" (replace -1) (("1" (propax) nil nil)) nil)
("2" (hide 2)
(("2" (expand "member")
(("2" (skosimp*)
(("2" (split)
(("1" (skosimp*)
(("1" (inst + "i!1") (("1" (grind) nil nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst + "i!1") (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "metric_triangle?")
(("3" (skosimp*)
(("3"
(case "forall (x,y:Vector[n]): nonempty?[nnreal]({z: nnreal | EXISTS (i:below(n)): abs(x(i) - y(i)) = z})")
(("1" (expand "max")
(("1"
(case "forall (x,y:Vector[n]): above_bounded[nnreal]({z: nnreal | EXISTS (i:below(n)): abs(x(i) - y(i)) = z})")
(("1" (inst-cp - "x!1" "z!1")
(("1" (inst-cp - "x!1" "y!1")
(("1" (inst - "y!1" "z!1")
(("1" (inst-cp - "x!1" "z!1")
(("1" (inst-cp - "x!1" "y!1")
(("1" (inst - "y!1" "z!1")
(("1"
(typepred
"sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - z!1(i)) = z})")
(("1"
(typepred
"sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})")
(("1"
(typepred
"sup[nnreal]({z: nnreal | EXISTS i: abs(y!1(i) - z!1(i)) = z})")
(("1"
(expand "least_upper_bound")
(("1"
(flatten)
(("1"
(expand "upper_bound")
(("1"
(name-replace
"SXZ"
"sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - z!1(i)) = z})")
(("1"
(name-replace
"SXY"
"sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})")
(("1"
(name-replace
"SYZ"
"sup[nnreal]({z: nnreal | EXISTS i: abs(y!1(i) - z!1(i)) = z})")
(("1"
(inst -6 "SXY + SYZ")
(("1"
(split -6)
(("1"
(propax)
nil
nil)
("2"
(assert)
nil
nil)
("3"
(hide 2)
(("3"
(skosimp)
(("3"
(typepred
"z!2")
(("3"
(skosimp)
(("3"
(inst
-3
"abs(y!1(i!1) - z!1(i!1))")
(("1"
(inst
-5
"abs(x!1(i!1) - y!1(i!1))")
(("1"
(lemma
"triangle"
("x"
"x!1(i!1) - y!1(i!1)"
"y"
"y!1(i!1) - z!1(i!1)"))
(("1"
(assert)
nil
nil))
nil)
("2"
(inst
1
"i!1")
nil
nil))
nil)
("2"
(inst
+
"i!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (skosimp)
(("2" (expand "above_bounded")
(("2"
(inst +
"sigma(0,n-1,lambda (i: below(n)): abs(x!2(i) - y!2(i)))")
(("1" (expand "upper_bound")
(("1" (skosimp)
(("1" (typepred "z!2")
(("1"
(skosimp)
(("1"
(lemma
"sigma_split[below(n)]"
("low"
"0"
"high"
"n-1"
"F"
"LAMBDA (i: below(n)): abs(x!2(i) - y!2(i))"))
(("1"
(inst - "i!1-1")
(("1"
(assert)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma
"sigma_nonneg[below(n)]"
("low"
"0"
"high"
"i!1-1"
"F"
"LAMBDA (i: below(n)): abs(x!2(i) - y!2(i))"))
(("1"
(split -1)
(("1"
(lemma
"sigma_first[below(n)]"
("low"
"i!1"
"high"
"n-1"
"F"
" LAMBDA (i: below(n)): abs(x!2(i) - y!2(i))"))
(("1"
(assert)
(("1"
(replace -1)
(("1"
(lemma
"sigma_nonneg[below(n)]"
("low"
"1+i!1"
"high"
"i!1-1"
"F"
"LAMBDA (i: below(n)): abs(x!2(i) - y!2(i))"))
(("1"
(split -1)
(("1"
(assert)
nil
nil)
("2"
(skosimp)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) (("2" (assert) nil nil)) nil)
("3" (assert) (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (inst - "abs(x!2(0)-y!2(0))")
(("1" (expand "member")
(("1" (inst + "0") (("1" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((TRUE const-decl "bool" booleans nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(setof type-eq-decl nil defined_types nil)
(above_bounded const-decl "bool" bounded_reals "reals/")
(sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
"reals/")
(sup_set type-eq-decl nil bounded_reals "reals/")
(<= const-decl "bool" reals nil)
(least_upper_bound const-decl "bool" bound_defs "reals/")
(pred type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(XX skolem-const-decl "[nnreal -> boolean]" euclidean nil)
(x!1 skolem-const-decl "Vector[n]" euclidean nil)
(x!2 skolem-const-decl "Index[n]" euclidean nil)
(y!1 skolem-const-decl "Vector[n]" euclidean nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(max const-decl "T" bounded_reals "reals/")
(sigma_split formula-decl nil sigma "reals/")
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(sigma_nnreal application-judgement "nnreal" euclidean nil)
(sigma_first formula-decl nil sigma "reals/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sigma_nonneg formula-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(sigma def-decl "real" sigma "reals/")
(below type-eq-decl nil naturalnumbers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(nnreal type-eq-decl nil real_types nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets 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)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(n formal-const-decl "posnat" euclidean nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(metric_zero? const-decl "bool" metric_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(extensionality formula-decl nil sets_lemmas nil)
(metric_symmetric? const-decl "bool" metric_def nil)
(x!1 skolem-const-decl "Vector[n]" euclidean nil)
(triangle formula-decl nil real_props nil)
(i!1 skolem-const-decl "below[n]" euclidean nil)
(z!1 skolem-const-decl "Vector[n]" euclidean nil)
(y!1 skolem-const-decl "Vector[n]" euclidean nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(metric_triangle? const-decl "bool" metric_def nil)
(metric? const-decl "bool" metric_def nil))
nil))
(euclidean_d1 0
(euclidean_d1-1 nil 3293707277
("" (typepred "d1")
(("" (expand "metric_space?")
(("" (expand "metric?")
(("" (flatten)
(("" (split)
(("1" (expand "fullset")
(("1" (expand "metric_zero?")
(("1" (skosimp) (("1" (inst - "x!1" "y!1") nil nil))
nil))
nil))
nil)
("2" (expand "metric_symmetric?")
(("2" (skosimp) (("2" (inst - "x!1" "y!1") nil nil))
nil))
nil)
("3" (expand "metric_triangle?")
(("3" (skosimp)
(("3" (inst - "x!1" "y!1" "z!1") nil nil)) nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.77 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
