SSL euclidean.prf
Interaktion und
(euclideannil 3508674642 ("" (subtype-tcc) nil nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3508674648"" (skosimp)"" "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" "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 )nil naturalnumbers nil )"posnat" euclidean nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil sigma "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil nat_types nil )nil real_types nil )nil sigma "reals/" )"int" integers nil )nil sigma "reals/" )"nat" euclidean nil )nil integers nil )"(total_order?[real])" nil )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nnreal" euclidean nil ))nil ))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" "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" "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" "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)): ")) "3" (split -1)"1" (propax) nil nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )"nat" euclidean nil )"{j: nonneg_int | j >= i}" nil )nil functions nil )nil euclidean nil )nil nat_types nil )nil real_types nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )nil vectors "vectors/" )nil vectors "vectors/" )"posnat" euclidean nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" metric_def nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" metric_def nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"real" reals nil )"real" reals nil )"nnreal" nil )nil sigma "reals/" )"bool" metric_def nil )"bool" metric_def nil )"nnreal" euclidean nil )"real" reals nil ))nil )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" "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" "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" "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)): ")) "3" (split -1)"1" (propax) nil nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )nil functions nil )nil vectors "vectors/" )nil vectors "vectors/" )"bool" metric_def nil )"bool" metric_def nil )nil sigma "reals/" )nil sigma "reals/" )"bool" metric_def nil )"bool" metric_def nil ))nil ))nil 3382851446"" (expand "metric?" )"" (split)"1" (expand "metric_zero?" )"1" (skosimp)"1" (split)"1" (flatten)"1" "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" "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" "sub_eq_zero[n]" "u" "x!1" "v" "y!1" ))"1" replace -1 1 rl)"1" "1" expand "-" 1)"1" "1" "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" "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" "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" "DRL1" "LAMBDA (i_1: Index[n]): ") "3" "DRL2" "LAMBDA (i_2: Index[n]): ") "3" "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)))LAMBDA (i: Index[n]): x!1(i) - y!1(i)) +LAMBDA (i: Index[n]): y!1(i) - z!1(i)))" "g" "LAMBDA i: ")) "3" "1" replace -1)"1" (propax) nil nil ))nil )"2" "2" "2" expand "+" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma "reals/" )nil sqrt "reals/" )nil sq "reals/" )nil functions nil )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil vectors "vectors/" )"Vector" vectors "vectors/" )nil vectors "vectors/" )nil sq "reals/" )"real" vectors "vectors/" )"int" integers nil )"real" reals nil )"nnreal" euclidean nil )nil sqrt "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" euclidean nil )nil naturalnumbers nil )nil naturalnumbers nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil nat_types nil )"nonneg_real" sq "reals/" )nil vectors "vectors/" )nil vectors "vectors/" )"bool" metric_def nil )nil sq "reals/" )"bool" metric_def nil )"nnreal" vectors "vectors/" )"nnreal" vectors "vectors/" )"real" reals nil )"real" vectors "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"real" vectors "vectors/" )"nnreal" nil )nil vectors "vectors/" )"bool" metric_def nil )"bool" metric_def nil ))nil ))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" "nonempty?[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})" )"1" "above_bounded[nnreal] ") "1" (expand "in_set" )"1" "sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z}) >= 0" )"1" (skolem!)"1" (inst + "K!1" )"1" "sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})" )"1" "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" "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" "3" expand "upper_bound" )"3" "3" "z!1" )"3" expand "NNS" -2)"3" "3" "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" "sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})" )"1" "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" "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]): ") "1" "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 )nil vectors "vectors/" )nil vectors "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil nat_types nil )"posnat" euclidean nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" sets nil )"bool" sets nil )"bool" bounded_reals "reals/" )nil defined_types nil )nil bounded_reals "reals/" )nil defined_types nil )"bool" bound_defs "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"[nnreal -> boolean]" euclidean nil )"Vector[n]" euclidean nil )"below[n]" euclidean nil )"Vector[n]" euclidean nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" bound_defs "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"[nnreal -> boolean]" euclidean nil )"(strict_total_order?[real])" real_props nil )"bool" bounded_reals "reals/" )"[T, T -> boolean]" equalities nil )"bool" sets nil )set type-eq-decl nil sets nil )nil real_types nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil naturalnumbers nil )nil bounded_nat_inductions nil )"posint" nil )"below[2 + jb!1]" euclidean nil )"below(n)" euclidean nil )"below[2 + jb!1]" euclidean nil )"real" reals nil ))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] ") "1" (expand "max" )"1" "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" "XX" "{z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z}" )"1" "1" expand "upper_bound" )"1" "1" "abs(x!1(x!2)-y!1(x!2))" )"1" "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" "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" "1" "i!1" )"1" "sigma_split[below(n)]" "low" "0" "high" "n-1" "F" "LAMBDA (i: below(n)): abs(x!1(i) - y!1(i))" ))"1" "i!1-1" )"1" assert )"1" replace -1 1)"1" "1" "sigma_nonneg" "low" "0" "high" "i!1-1" "F" " LAMBDA (i: below(n)): abs(x!1(i) - y!1(i))" ))"1" "1" "DRL1" "sigma(0, i!1 - 1, LAMBDA (i: below(n)): abs(x!1(i) - y!1(i)))" )"1" "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" "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" "1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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" "sup[nnreal]({z: nnreal | EXISTS i: 0 = z})" )"1" (expand "least_upper_bound" )"1" (flatten)"1" (expand "upper_bound" )"1" "0" )"1" assert )"1" "0" )"1" "1" (assert ) nil nil )"2" (propax) nil nil )"3" "3" "z!1" )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (split)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" expand "member" )"1" "0" )"1" "0" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "above_bounded" )"2" (inst + "0" )"2" expand "upper_bound" )"2" "2" "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" "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" "sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - z!1(i)) = z})" )"1" "sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})" )"1" "sup[nnreal]({z: nnreal | EXISTS i: abs(y!1(i) - z!1(i)) = z})" )"1" expand "least_upper_bound" )"1" "1" expand "upper_bound" )"1" "SXZ" "sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - z!1(i)) = z})" )"1" "SXY" "sup[nnreal]({z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z})" )"1" "SYZ" "sup[nnreal]({z: nnreal | EXISTS i: abs(y!1(i) - z!1(i)) = z})" )"1" "SXY + SYZ" )"1" "1" nil nil )"2" assert )nil nil )"3" "3" "3" "z!2" )"3" "3" "abs(y!1(i!1) - z!1(i!1))" )"1" "abs(x!1(i!1) - y!1(i!1))" )"1" "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" "i!1" )nil nil ))nil )"2" "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" "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" "1" "sigma_split[below(n)]" "low" "0" "high" "n-1" "F" "LAMBDA (i: below(n)): abs(x!2(i) - y!2(i))" ))"1" "i!1-1" )"1" assert )"1" replace -1)"1" "1" "sigma_nonneg[below(n)]" "low" "0" "high" "i!1-1" "F" "LAMBDA (i: below(n)): abs(x!2(i) - y!2(i))" ))"1" "1" "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" "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" "1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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 )"bool" booleans nil )"bool" sets nil )"bool" sets nil )nil defined_types nil )"bool" bounded_reals "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )nil bounded_reals "reals/" )"bool" reals nil )"bool" bound_defs "reals/" )nil defined_types nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" bound_defs "reals/" )"[nnreal -> boolean]" euclidean nil )"Vector[n]" euclidean nil )"Index[n]" euclidean nil )"Vector[n]" euclidean nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )max const-decl "T" bounded_reals "reals/" )nil sigma "reals/" )"odd_int" integersnil )"nnreal" euclidean nil )nil sigma "reals/" )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" nil )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )set type-eq-decl nil sets nil )"bool" sets nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" euclidean nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors "vectors/" )nil vectors "vectors/" )"bool" metric_def nil )"real" reals nil )"odd_int" integers nil )nil sets_lemmas nil )"bool" metric_def nil )"Vector[n]" euclidean nil )nil real_props nil )"below[n]" euclidean nil )"Vector[n]" euclidean nil )"Vector[n]" euclidean nil )"real" reals nil )"bool" metric_def nil )"bool" metric_def nil ))nil ))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 ))nil ))nil ))nil ))nil )"bool" metric_space_def nil )"bool" metric_def nil )"bool" metric_space_def nil )"bool" metric_def nil )"bool" metric_space_def nil )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets nil )"bool" booleans nil )"bool" metric_space_def nil )"bool" metric_def nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" euclidean nil )nil vectors "vectors/" )nil vectors "vectors/" )nil real_types nil )"bool" metric_def nil )nil metric_def nil )"metric" euclidean nil ))nil 3293708530"" (typepred "d2" )"" (expand "metric?" )"" (expand "metric_space?" )"" (expand "fullset" )"" (flatten)"" (split)"1" (expand "metric_zero?" )"1" (skosimp) (("1" (inst - "x!1" "y!1" ) 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 ))nil ))nil ))nil ))nil ))nil )"set" sets nil )"bool" booleans nil )"bool" metric_space_def nil )"bool" metric_def nil )"bool" metric_space_def nil )"bool" metric_def nil )"bool" metric_space_def nil )"bool" metric_def nil )"bool" metric_space_def nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" euclidean nil )nil vectors "vectors/" )nil vectors "vectors/" )nil real_types nil )"bool" metric_def nil )nil metric_def nil )"metric" euclidean nil ))nil 3313054965"" (skosimp)"" (expand "metric_space?" )"" (expand "restrict" )"" (split)"1" (expand "metric_zero?" )"1" (skosimp*)"1" (expand "dinf" )"1" (expand "max" )"1" (rewrite "sup_def" )"1" (split 1)"1" (expand "least_upper_bound" )"1" (skosimp*)"1" (expand "upper_bound" )"1" (apply-extensionality 1 :hide? t)"1" "abs(x!1(x!2) - y!1(x!2))" )"1" "1" expand "<=" )"1" "1" (assert ) nil nil )"2" expand "abs" )"2" "x!1(x!2) - y!1(x!2) < 0" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "x!2" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "least_upper_bound" )"2" (skosimp*)"2" (split)"1" (expand "upper_bound" )"1" "1" "z!1" )"1" "1" replace -3)"1" assert )"1" expand "abs" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" expand "upper_bound" )"2" "0" )"2" "0" )"1" replace -1)"1" assert )"1" expand "abs" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (split)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" )"1" "abs(x!1(0)-y!1(0))" )"1" "0" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (expand "above_bounded" )"2" (expand "upper_bound" )"2" (inst + "d1(x!1,y!1)" )"2" "2" "z!1" )"2" expand "d1" )"2" "2" "sigma_nn_ge_comps" "Fnnr" "LAMBDA (i:below[n]): abs(x!1(i) - y!1(i))" "low" "0" "high" "n-1" "i" "i!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" (expand "dinf" )"2" "{z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z} = {z: nnreal | EXISTS i: abs(y!1(i) - x!1(i)) = z}" )"2" (hide 2)"2" (apply-extensionality :hide? t)"2" "EXISTS i: abs(x!1(i) - y!1(i)) = x!2" )"1" (skosimp)"1" (inst + "i!1" )"1" (expand "abs" )"1" "trich_lt" "x" "x!1(i!1)" "y" "y!1(i!1)" ))"1" "1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1 2)"2" (assert )"2" (skosimp)"2" "i!1" )"2" expand "abs" )"2" "trich_lt" "x" "x!1(i!1)" "y" "y!1(i!1)" ))"2" "1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "metric_triangle?" )"3" (skosimp*)"3" (expand "dinf" )"3" (expand "max" )"3" "XZS" "{z: nnreal | EXISTS i: abs(x!1(i) - z!1(i)) = z}" )"3" "XYS" "{z: nnreal | EXISTS i: abs(x!1(i) - y!1(i)) = z}" )"3" "YZS" "{z: nnreal | EXISTS i: abs(y!1(i) - z!1(i)) = z}" )"3" (name-replace "XZ" "sup(XZS)" )"1" (typepred "XZ" )"1" (name-replace "XY" "sup(XYS)" )"1" "YZ" "sup(YZS)" )"1" "XY" )"1" "YZ" )"1" expand "least_upper_bound" )"1" "1" expand "YZS" )"1" expand "XYS" )"1" expand "XZS" )"1" expand "upper_bound" )"1" "XY+YZ" )"1" "1" nil nil )"2" assert )nil nil )"3" "3" "3" "z!2" )"3" "3" "3" "abs(y!1(i!1)-z!1(i!1))" )"1" "abs(x!1(i!1)-y!1(i!1))" )"1" "triangle" )"1" "y!1(i!1) - z!1(i!1)" "x!1(i!1) - y!1(i!1)" )"1" assert )nil nil ))nil ))nil )"2" "i!1" )nil nil ))nil )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "nonempty?" )"1" expand "YZS" )"1" expand "empty?" )"1" expand "member" )"1" "abs(y!1(0)-z!1(0))" )"1" "0" )"1" assert )nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "YZS" )"2" expand "above_bounded" )"2" expand "upper_bound" )"2" "d1(y!1,z!1)" )"2" "2" "z!2" )"2" "2" expand "d1" )"2" "sigma_nn_ge_comps" "low" "0" "high" "n-1" "i" "i!1" "Fnnr" "LAMBDA (i:below[n]): abs(y!1(i) - z!1(i))" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "XYS" )"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "abs(x!1(0)-y!1(0))" )"1" "0" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" expand "above_bounded" )"2" expand "upper_bound" )"2" "d1(x!1,y!1)" )"2" "2" "z!2" )"2" "2" "sigma_nn_ge_comps" "low" "0" "high" "n-1" "i" "i!1" "Fnnr" "LAMBDA (i:below[n]): abs(x!1(i) - y!1(i))" ))"2" expand "d1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (split)"1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" expand "XZS" )"1" "abs(x!1(0)-z!1(0))" )"1" "0" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "above_bounded" )"2" expand "XZS" )"2" expand "upper_bound" )"2" "d1(x!1,z!1)" )"2" "2" expand "d1" )"2" "z!2" )"2" "2" "sigma_nn_ge_comps" "low" "0" "high" "n-1" "i" "i!1" "Fnnr" "LAMBDA (i:below[n]): abs(x!1(i) - z!1(i))" ))"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 )max const-decl "T" bounded_reals "reals/" )"metric" euclidean nil )nil metric_def nil )"bool" metric_def nil )"nnreal" euclidean nil )nil naturalnumbers nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )"int" integers nil )"bool" sets nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"bool" reals nil )"Index[n]" euclidean nil )"(fullset[Vector])" euclidean nil )"(fullset[Vector])" euclidean nil )"bool" bound_defs "reals/" )"bool" bound_defs "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"set" sets nil )nil vectors "vectors/" )nil vectors "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"posnat" euclidean nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil )nil bounded_reals "reals/" )"metric" euclidean nil )"real" reals nil )"bool" metric_space_def nil )nil real_props nil )"bool" metric_space_def nil )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )nil defined_types nil )"[nnreal -> boolean]" euclidean nil )"[nnreal -> boolean]" euclidean nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"(fullset[Vector])" euclidean nil )"nnreal" nil )nil real_props nil )"below[n]" euclidean nil )"(fullset[Vector])" euclidean nil )"(fullset[Vector])" euclidean nil )"[nnreal -> boolean]" euclidean nil )"bool" metric_space_def nil )"bool" metric_space_def nil ))nil 3391058802 ("" (subtype-tcc) nil nil )"posnat" euclidean nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"Vector" vectors "vectors/" ))nil ))nil 3391066001"" case "forall (n:posnat): is_countable(fullset[[below(n)->rat]])" )"1" (inst - "n" ) nil nil )"2" (hide 2)"2" (induct "n" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skosimp*)"3" (case-replace "j!1=0" )"1" (assert )"1" (hide -2 -3)"1" (lemma "nat_rational" )"1" (expand "is_countably_infinite_type" )"1" (expand "fullset" )"1" (expand "is_countable" )"1" (skosimp)"1" (typepred "f!1" )"1" "lambda (i:[below(1 + j!1) -> rat]): f!1(i(0))" )"1" expand "bijective?" )"1" "1" expand "restrict" )"1" expand "injective?" )"1" "1" "1" "x!1" )"1" replace -5)"1" "x1!1(0)" "x2!1(0)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "1<=j!1" )"1" (hide -3 1)"1" (case "is_countable(fullset[rat])" )"1" "is_countable_cross[rat,[[below(j!1) -> rat]]]" "X" "fullset[rat]" "Y" "fullset[[below(j!1) -> rat]]" ))"1" (assert )"1" (hide -2 -4)"1" (expand "fullset" )"1" (expand "cross_product" )"1" expand "is_countable" )"1" "1" "f!1" )"1" "lambda (v:[below(1 + j!1) -> rat]): f!1(v(j!1),lambda (i:[below(j!1)]): v(i))" )"1" expand "restrict" )"1" expand "injective?" )"1" "1" "(x1!1(j!1), LAMBDA (i: [below(j!1)]): x1!1(i))" "(x2!1(j!1), LAMBDA (i: [below(j!1)]): x2!1(i))" )"1" assert )"1" "1" "1" "x!1" )"1" "x!1=j!1" )"1" rewrite "extensionality_postulate" "1" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (lemma "nat_rational" )"2" (expand "is_countably_infinite_type" )"2" (expand "fullset" )"2" (expand "is_countable" )"2" "2" "f!1" )"2" expand "bijective?" )"2" "2" (inst + "f!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil countable_cross nil )"set[[T1, T2]]" cross_product"topology/" )"(injective?[({z | TRUE}), nat])" euclideannil )nil functions nil )"(total_order?[real])" nil )"bool" reals nil )"odd_int" integers nil )"posint" nil )nil countable_types "sets_aux/" )"(strict_total_order?[real])" real_props nil )"posint" nil )"R" restrict nil )"bool" functions nil )"bool" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nat" euclidean nil )"(bijective?[rational, nat])" euclidean nil )"odd_int" integers nil )"bool" functions nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" countability"sets_aux/" )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"posnat" euclidean nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil rationals nil )set type-eq-decl nil sets nil )"bool" countability "sets_aux/" )"set" sets nil ))nil 3391058802 ("" (subtype-tcc) nil nil )nil real_types nil )nil real_types nil )"Vector" vectors "vectors/" )nil vectors "vectors/" )nil vectors "vectors/" )"posnat" euclidean nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3391058802 ("" (subtype-tcc) nil nil )nil rationals nil )nil rationals nil )nil vectors "vectors/" )nil euclidean nil )nil rationals nil )nil vectors "vectors/" )"bool" reals nil )nil naturalnumbers nil )"Vector" vectors "vectors/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" euclidean nil ))nil ))nil 3507983654"" (assert )"" (lemma "metric_space_is_topology?" ) (("" (propax) nil nil ))nil ))nil )"metric" euclidean nil )nil metric_def nil )"bool" metric_def nil )nil real_types nil )nil vectors "vectors/" )nil vectors "vectors/" )"posnat" euclidean nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil metric_space nil )"(hausdorff?)" euclideannil )"hausdorff" euclideannil ))nil ))nil 3391058849"" (expand "fullset" )"" (expand "extend" )"" (expand "base?" )"" (split)"1" (expand "subset?" )"1" (expand "member" )"1" (skosimp*)"1" (prop)"1" (skosimp)"1" (expand "metric_induced_topology" )"1" "metric_open_ball[Vector,d2]" "x" "x!2" "r" "r!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "A!1" )"2" (expand "metric_induced_topology" )"2" (inst + "{X:balls|subset?(X,A!1)}" )"2" (split)"1" (expand "extend" )"1" (expand "subset?" )"1" (expand "member" )"1" (skosimp*) (("1" (prop) nil nil )) nil ))nil ))nil ))nil )"2" (apply-extensionality 1 :hide? t)"2" (expand "extend" )"2" (expand "subset?" )"2" (expand "member" )"2" (expand "Union" )"2" "A!1(x!1)" )"1" expand "metric_open?" )"1" "x!1" )"1" assert )"1" "1" "ball(x!1, r!1)" )"1" "ball_centre" "x" "x!1" "r" "r!1" ))"1" (assert ) nil nil ))nil )"2" "1" "1" expand "subset?" )"1" "x!3" )"1" assert )nil nil ))nil ))nil ))nil )"2" "x!1" "r!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "a!1" )"2" replace -2 -1)"2" "2" "x!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 )"R" extend nil )"bool" sets nil )"setofsets[T]" metric_space_defnil )"metric_open" euclideannil )nil metric_space nil )nil real_types nil )nil real_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" euclidean nil )nil vectors "vectors/" )nil vectors "vectors/" )nil real_types nil )"bool" metric_def nil )nil metric_def nil )"metric" euclidean nil )"bool" sets nil )nil sets nil )nil defined_types nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"set[T]" metric_space_def nil )nil euclidean nil )"bool" booleans nil )"set" sets nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"bool" metric_space_def nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[Index[n] -> real]" euclidean nil )"posreal" euclidean nil )"[bool, bool -> bool]" booleans nil )"(metric_induced_topology[Vector, d2])" nil )nil metric_space nil )"bool" basis "topology/" )"set" sets nil ))nil 3396336618"" (expand "fullset" )"" (expand "dense_in?" )"" (expand "subset?" )"" (expand "member" )"" (skosimp*)"" (expand "metric_closure" )"" (expand "metric_adherent?" )"" (skosimp)"" (expand "intersection" )"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (expand "ball" )"" case "FORALL i: ") "1" "Q" "lambda i: choose[rat]({q:rat | sq(x!1(i) - q) < sq(r!1) / n})" )"1" "Q" )"1" "1" (inst + "Q" ) nil nil )"2" expand "d2" )"2" rewrite "sq_lt" 1 :dir rl)"2" rewrite "sq_sqrt" )"2" "sigma_lt" "low" "0" "high" "n-1" "F" "LAMBDA i: sq(x!1(i) - Q(i))" "G" "lambda i: sq(r!1)/n" ))"2" rewrite "sigma_const" "2" rewrite "div_cancel1" "2" assert )"2" "2" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "i!1" )"2" "2" "q!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "density" "x" "x!1(i!1)-r!1/sqrt(n)" "y" "x!1(i!1)+r!1/sqrt(n)" ))"2" "posreal_div_posreal_is_posreal" "px" "r!1" "py" "sqrt(n)" ))"2" assert )"2" "2" "r!2" )"2" rewrite "sqrt_lt" "2" rewrite "sqrt_div" 1)"2" "R" "r!1 / sqrt(n)" )"2" rewrite "sqrt_sq_abs" )"2" "2" 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 )"bool" metric_space_def nil )"bool" sets nil )"set[T]" metric_space_def nil )"bool" sets nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil vectors "vectors/" )nil vectors "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nonneg_real" sq "reals/" )nil real_types nil )nil rationals nil )nil nat_types nil )"posnat" euclidean nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"real" reals nil )"metric" euclidean nil )nil sqrt "reals/" )nil sigma "reals/" )"int" integers nil )"real" reals nil )nil real_props nil )nil reals nil )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integers nil )"nnreal" euclidean nil )nil sq "reals/" )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil euclidean nil )"(p)" sets nil ) (set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"posreal" sq "reals/" )"posreal" sqrt "reals/" )"real" reals nil )nil rational_props nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )nil sqrt "reals/" )nil sqrt "reals/" )nil sqrt "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil sqrt "reals/" )nil real_types nil )"set[T]" metric_space_def nil )"bool" sets nil )"set" sets nil )"bool" metric_space_def nil )"bool" sets nil )"set" sets nil ))nil 3391059839"" (expand "fullset" )"" (expand "extend" )"" (expand "base?" )"" (split)"1" (expand "metric_induced_topology" )"1" (expand "subset?" )"1" (expand "member" )"1" (skosimp*)"1" (prop)"1" (skosimp)"1" (expand "metric_open?" )"1" (skosimp)"1" (case-replace "x!1(x!2)" )"1" (assert )"1" replace -2)"1" "1" expand "ball" )"1" "d2(q!1, x!2)" )"1" "pq!1-d2(q!1, x!2)" )"1" expand "subset?" )"1" expand "member" )"1" "1" "d2" )"1" expand "metric?" )"1" "1" expand "metric_triangle?" )"1" "q!1" "x!2" "x!3" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "2" expand "subset?" )"2" "x!2" )"2" "ball_centre" "x" "x!2" "r" "r!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst + "{X:rational_balls|subset?(X,A!1)}" )"2" (split)"1" (expand "extend" )"1" (expand "subset?" )"1" (expand "member" )"1" (skosimp*) (("1" (prop) nil nil )) nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (apply-extensionality :hide? t)"2" (case-replace "A!1(x!1)" )"1" (expand "Union" )"1" (typepred "A!1" )"1" (expand "metric_induced_topology" )"1" (expand "metric_open?" )"1" "x!1" )"1" assert )"1" "1" "density" "x" "0" "y" "r!1" ))"1" assert )"1" "1" case "exists q: d2(q,x!1)<r!2/4" )"1" "1" case "subset?(ball[Vector,d2](q!1,r!2/2),ball[Vector,d2](x!1, r!1)) & ball[Vector,d2](q!1,r!2/2)(x!1)" )"1" "1" "ball[Vector, d2](q!1, r!2 / 2)" )"1" "1" "1" expand "subset?" )"1" "1" "x!2" )"1" "x!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "q!1" "r!2/2" )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" "1" expand "subset?" )"1" expand "member" )"1" expand "ball" )"1" "1" "d2" )"1" expand "metric?" )"1" "1" expand "metric_triangle?" )"1" "x!1" "q!1" "x!2" )"1" expand "metric_symmetric?" )"1" "x!1" "q!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "ball" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" assert )nil nil ))nil ))nil )"2" "2" expand "d2" )"2" case "exists q: forall i: sq(q(i)-x!1(i)) < sq(r!2/4)/n" )"1" "1" "q!1" )"1" "sigma_lt" "low" "0" "high" "n-1" "F" "LAMBDA i: sq(q!1(i) - x!1(i))" "G" "LAMBDA i: sq(r!2 / 4) / n" ))"1" "1" "sigma_const" "low" "0" "high" "n-1" "x" "sq(r!2 / 4) / n" ))"1" assert )"1" rewrite "div_cancel1" "1" replace "1" "sqrt_lt" "nny" "sigma(0, n - 1, LAMBDA (i_1: below[n]): sq(q!1(i_1) - x!1(i_1)))" "nnz" "sq(r!2 / 4)" ))"1" assert )nil nil )"2" "sigma_Fnnr[below(n)]" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "n1!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "posreal_div_posreal_is_posreal" "px" "r!2" "py" "4*n" ))"1" case "FORALL i: nonempty?({q: rat | abs(q - x!1(i)) < r!2 / (4 * n)})" )"1" "Q" "lambda i: choose[rat]({q: rat | abs(q - x!1(i)) < r!2 / (4 * n)})" )"1" case "FORALL i:abs(Q(i)-x!1(i))<r!2/(4*n)" )"1" "Q" )"1" "1" "i!1" )"1" "sq_lt" "nna" "abs(Q(i!1) - x!1(i!1))" "nnb" "r!2 / (4 * n)" ))"1" rewrite "sq_abs" )"1" assert )"1" "LHS" "sq(Q(i!1) - x!1(i!1))" )"1" rewrite "sq_div" "1" rewrite "sq_div" "1" expand "sq" "1" expand "sq" "1" rewrite "div_div2" "1" "both_sides_div_pos_le2" )"1" "16*n*n" "16*n" "sq(r!2)" )"1" assert )"1" "both_sides_times_pos_le1" "pz" "16*n" "x" "1" "y" "n" ))"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "Q" )"2" "choose_member[rat]" "a" "{q: rat | abs(q - x!1(i!1)) < r!2 / (4 * n)}" ))"2" "i!1" )"2" expand "nonempty?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "density" "x" "x!1(i!1)-r!2 / (4 * n)" "y" "x!1(i!1)+r!2 / (4 * n)" ))"2" assert )"2" "2" "r!3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "Union" )"2" (skosimp*)"2" (typepred "a!1" )"2" replace -2 -1)"2" "2" expand "subset?" )"2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"R" extend nil )"bool" sets nil )nil metric_space nil )"metric_open" euclideannil )NOT const-decl "[bool -> bool]" booleans nil )nil real_types nil )"bool" metric_def nil )nil metric_def nil )"metric" euclidean nil )nil rationals nil )nil euclidean nil )"bool" metric_def nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"(total_order?[real])" nil )nil real_types nil )nil real_types nil )"Vector[n]" euclidean nil )"Qn" euclidean nil )"posrat" euclidean nil )nil rationals nil )nil rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"set[T]" metric_space_def nil )nil defined_types nil )nil vectors "vectors/" )nil vectors "vectors/" )"posnat" euclidean nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" metric_space_def nil )"bool" sets nil )"setofsets[T]" metric_space_defnil )nil sets nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )nil euclidean nil )"bool" booleans nil )nil rational_props nil )"nnreal" nil )nil nat_types nil )"nonneg_real" sq "reals/" )"int" integers nil )"real" reals nil )"nnreal" euclidean nil )nil sqrt "reals/" )"real" sigma "reals/" )nil sqrt "reals/" )nil real_props nil )nil reals nil )nil sigma "reals/" )nil integers nil )nil naturalnumbers nil )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )"int" integers nil )"bool" sets nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil sq "reals/" )nil sq "reals/" )"posreal" sq "reals/" )nil real_props nil )nil real_props nil )"even_int" integersnil )nil real_props nil )nil sq "reals/" )nil sets_lemmas nil )"[i: below[n] -> ({q: rat | abs(q - x!1(i)) < r!2 / (4 * n)})]" nil )"(p)" sets nil )"bool" sets nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"bool" metric_def nil )"(metric_induced_topology[Vector, d2])" nil )"Qn" euclidean nil )"rat" euclidean nil )"[bool, bool -> bool]" booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"rat" rationals nil )"(partial_order?[set[T]])" nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"set" sets nil )"bool" basis "topology/" )"set" sets nil ))nil 3391072197"" (lemma "Qn_countable" )"" (case "is_countable(fullset[posrat])" )"1" "is_countable_cross[Qn,posrat]" "X" "fullset[Qn]" "Y" "fullset[posrat]" ))"1" (assert )"1" "countable_image[[Qn,posrat],rational_balls]" "S" "cross_product(fullset[Qn], fullset[posrat])" "f" "lambda (q:Qn,pq:posrat): ball[Vector,d2](q,pq)" ))"1" (replace -2)"1" (expand "fullset" -1)"1" (expand "cross_product" -1)"1" (expand "image" -1)"1" (expand "image" -1)"1" (expand "fullset" 1)"1" "{y: rational_balls | ") "1" (apply-extensionality :hide? t)"1" (hide-all-but 1)"1" "x!1" )"1" "1" (inst + "(q!1,pq!1)" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp) (("2" (inst + "q!1" "pq!1" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "is_countable_cross[posnat,posnat]" "X" "fullset[posnat]" "Y" "fullset[posnat]" ))"2" (case-replace "is_countable(fullset[posnat])" )"1" (hide -1)"1" "countable_image[[posnat,posnat],posrat]" "S" "cross_product(fullset[posnat], fullset[posnat])" "f" "lambda (pn,pr:posnat): pn/pr" ))"1" (assert )"1" (expand "fullset" )"1" (expand "cross_product" )"1" (expand "image" )"1" (expand "image" )"1" (hide -2)"1" "{y: posrat | ") "1" "1" "1" "DEN" "lambda (q:rat): min({p:posnat | integer_pred(q*p)})" )"1" "NUM" "LAMBDA (q: rat): q*DEN(q)" )"1" case "forall (q:rat): NUM(q)/DEN(q) = q" )"1" "(NUM(x!1),DEN(x!1))" )"1" "x!1" )"1" replace -1)"1" (propax) nil nil ))nil ))nil )"2" assert )"2" "1" assert )"1" "x!1" )"1" expand "NUM" )"1" assert )nil nil ))nil ))nil ))nil )"2" "x!1" )"2" expand "NUM" )"2" assert )nil nil ))nil ))nil )"3" "x!1" )"3" expand "NUM" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "NUM" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "rational_pred_ax2" "r" "q!1" ))"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" "p!1" )"2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "is_countable" )"2" (inst + "lambda (pn:posnat): pn-1" )"1" (expand "restrict" )"1" (expand "injective?" )"1" (skosimp) nil nil )) nil ))nil )"2" (expand "restrict" )"2" (expand "injective?" )"2" (skosimp) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set" sets nil )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil rationals nil )"bool" reals nil )nil rationals nil )"bool" reals nil )nil booleans nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"set[R]" function_image nil )"bool" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"set[R]" function_image nil )"metric_open" euclideannil )nil countable_image "sets_aux/" )"set[[T1, T2]]" cross_product"topology/" )nil vectors "vectors/" )"[T, T -> boolean]" equalities nil )nil real_types nil )nil real_types nil )nil real_types nil )"bool" metric_def nil )nil metric_def nil )"metric" euclidean nil )"set[T]" metric_space_def nil )nil euclidean nil )nil countable_cross nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )nil integers nil )"posnat" euclidean nil )nil vectors "vectors/" )nil rationals nil )nil euclidean nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" functions nil )nil rational_props nil )"bool" sets nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posrat" nil )"[rat -> rat]" euclidean nil )"posrat" euclidean nil )"rat" rationals nil )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" nil )"bool" sets nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"rat" rationals nil )"posrat" nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil euclidean nil ))nil 3396338346"" (expand "second_countable?" )"" (expand "has_countable_basis?" )"" (typepred "metric_induced_topology[Vector[n], d2]" )"" (expand "hausdorff_space?" )"" (assert )"" (inst + "fullset[rational_balls]" )"" (split)"1" (lemma "countable_rational_balls" )"1" (hide -2 -3)"1" (expand "fullset" )"1" (expand "extend" )"1" (expand "is_countable" )"1" (skosimp)"1" (inst + "f!1" )"1" "f!1" )"1" "1" "1" "(EXISTS q, pq: x2!1 = ball[Vector[n], d2](q, pq))" )"1" (assert ) nil nil )"2" replace 1 2)"2" (assert ) nil nil ))nil ))nil ))nil )"2" expand "injective?" )"2" "2" "x1!1" "x2!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "Qn_basis" )"2" "base_is_synthetic_base" "U" "extend[setof[Vector[n]], rational_balls, bool, FALSE](fullset[rational_balls])" "t" "metric_induced_topology[Vector, d2]" ))"2" (assert ) nil nil )) nil ))nil )"3" (apply-extensionality :hide? t)"3" (expand "metric_induced_topology" )"3" (case-replace "metric_open?(x!1)" )"1" (expand "fullset" )"1" (expand "extend" )"1" expand "synthetic_generated_topology_set" )"1" "{X:rational_balls| subset?(X,x!1)}" )"1" "1" expand "extend" )"1" expand "subset?" )"1" expand "member" )"1" "1" (prop) nil nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" expand "Union" )"2" "2" "x!1(x!2)" )"1" expand "metric_open?" )"1" "x!2" )"1" assert )"1" "1" case "exists q, pq: subset?(ball[Vector, d2](q, pq),ball(x!2, r!1)) & ball[Vector, d2](q, pq)(x!2)" )"1" "1" "ball[Vector, d2](q!1, pq!1)" )"1" "1" "1" expand "subset?" )"1" "1" expand "member" )"1" "x!3" )"1" "x!3" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "q!1" "pq!1" )nil nil ))nil ))nil ))nil )"2" "2" "density" "x" "0" "y" "r!1" ))"2" assert )"2" "2" "posreal_div_posreal_is_posreal" "px" "r!2" "py" "sqrt(n)" ))"1" "R" "r!2 / sqrt(n)" )"1" replace "1" "VV" "{q | ball[Vector, d2](q,r!2/2)(x!2)}" )"1" case "nonempty?(VV)" )"1" "choose(VV)" "r!2/2" )"1" "choose_member" "a" "VV" ))"1" "1" expand "member" )"1" expand "VV" "1" assert )"1" expand "subset?" "1" expand "member" )"1" "1" "CC" "choose(VV)" )"1" "1" expand "ball" )"1" "metric_triangle" "x" "x!2" "y" "CC" "z" "x!3" ))"1" rewrite "metric_symmetric" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" expand "VV" )"2" "2" expand "ball" )"2" case "FORALL i: nonempty?[rat]({q: rat | sq(q - x!2(i)) < sq(r!2 / 2) / n})" )"1" "lambda i: choose[rat]({q:rat | sq(q-x!2(i)) < sq(r!2/2)/n})" )"1" "v" "LAMBDA i: choose[rat]({q: rat | sq(q - x!2(i)) < sq(r!2 / 2) / n})" )"1" expand "d2" )"1" "sqrt_lt" "nny" "sigma(0, n - 1, LAMBDA i: sq(v(i) - x!2(i)))" "nnz" "sq(r!2/2)" ))"1" rewrite "sqrt_sq" )"1" replace "1" "1" "sigma_lt" "low" "0" "high" "n-1" "F" "LAMBDA i: sq(v(i) - x!2(i))" "G" "LAMBDA i: sq(r!2/2)/n" ))"1" rewrite "sigma_const" )"1" assert )"1" "1" "1" "n1!1" )"1" expand "nonempty?" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "sigma_nnreal" )"2" "2" "sigma_Fnnr[below(n)]" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" "density" "x" "x!2(i!1)-r!2/(2*sqrt(n))" "y" "x!2(i!1)+r!2/(2*sqrt(n))" ))"2" assert )"2" "2" "r!3" )"2" "sq_abs" "a" "r!3 - x!2(i!1)" ))"2" replace "2" "2" "sqrt_lt" "nny" "sq(abs(r!3 - x!2(i!1)))" "nnz" "sq(r!2 / 2) / n" ))"2" replace "2" "2" rewrite "sqrt_sq" )"2" rewrite "sqrt_div" )"2" rewrite "div_div2" )"2" "r!2 / (2 * sqrt(n))=R/2" )"1" "1" nil nil ))nil )"2" expand "R" )"2" rewrite "div_div2" )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 )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "a!1" )"2" replace -2 -1)"2" expand "subset?" )"2" expand "member" )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1 2)"2" (assert )"2" (expand "fullset" )"2" (expand "extend" )"2" expand "synthetic_generated_topology_set" )"2" "2" "open_Union" ("Y" "V!1" ))"2" replace -3 -1)"2" rewrite "metric_open_def" )"2" assert )"2" "2" expand "every" )"2" "2" "x!2" )"2" "2" rewrite "metric_open_def" "2" expand "subset?" )"2" expand "member" )"2" "x!2" )"2" assert )"2" "2" "2" replace "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 ))nil ))nil ))nil )"bool" topology_def "topology/" )set type-eq-decl nil sets nil )nil rationals nil )nil euclidean nil )nil rationals nil )nil rationals nil )"[T, T -> boolean]" equalities nil )nil real_types nil )nil real_types nil )"set[T]" metric_space_def nil )nil euclidean nil )"bool" booleans nil )"R" extend nil )"set" sets nil )"bool" basis "topology/" )nil basis "topology/" )"setofsets[T]" basis"topology/" )"topology[Vector]" euclidean nil )"bool" metric_space_def nil )"bool" sets nil )"[bool, bool -> bool]" booleans nil )"Qn" euclidean nil )"posrat" euclidean nil )"[[Index[n] -> real] -> boolean]" euclideannil )nil rational_props nil )"real" reals nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"rat" rationals nil )"bool" sets nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil sqrt "reals/" )"real" euclidean nil )nil real_props nil )nil reals nil )nil sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"posreal" nil )"[Index[n] -> real]" euclidean nil )nil sqrt "reals/" )nil sigma "reals/" )nil integers nil )nil sigma "reals/" )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sqrt "reals/" )"nnreal" euclidean nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_real" sq "reals/" )nil nat_types nil )"nnreal" nil )"real" reals nil )"[Qn -> bool]" euclidean nil )"rat" euclidean nil )"(p)" sets nil )nil metric_space nil )"nnreal" nil )"(total_order?[real])" nil )nil metric_space nil )nil sets_lemmas nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"posreal" sqrt "reals/" )"(partial_order?[set[T]])" nil )"(strict_total_order?[real])" real_props nil )"set" sets nil )"bool" sets nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"bool" sets nil )nil metric_space nil )nil topology "topology/" )nil euclidean nil )nil topology_prelim "topology/" )"bool" topology_prelim "topology/" )nil basis "topology/" )nil euclidean nil )"bool" countability "sets_aux/" )"bool" functions nil )"bool" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"(injective?[({x | TRUE}), nat])" euclideannil )"metric_open" euclideannil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" euclidean nil )nil vectors "vectors/" )nil vectors "vectors/" )nil defined_types nil )nil sets nil )"bool" topology_prelim "topology/" )nil real_types nil )"bool" metric_def nil )nil metric_def nil )"metric" euclidean nil )"setofsets[T]" metric_space_defnil )"bool" topology_prelim "topology/" )"bool" topology_def "topology/" )"hausdorff" euclideannil )"(hausdorff?)" euclideannil ))nil ))nil 3407039473"" (lemma "real_is_complete" )"" (expand "complete_metric_space?" )"" (flatten)"" (split)"1" (hide -1 -2)"1" (lemma "euclidean_d2" ) (("1" (propax) nil nil )) nil ))nil )"2" (hide -1)"2" case "forall (m:posnat): metric_complete?[[below[m]->real],(LAMBDA (x,y:[[below[m]->real]]): sqrt(sigma[below[m]](0,m-1,(LAMBDA (i:below[m]): sq(x(i)-y(i))))))](fullset[[below[m]->real]])" )"1" (inst - "n" )"1" (hide -2)"1" (expand "fullset" )"1" (expand "metric_complete?" )"1" (skosimp)"1" (inst - "u!1" )"1" (assert )"1" (split -1)"1" "1" expand "metric_convergent?" )"1" "1" "x!1" )"1" expand "metric_converges_to" )"1" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" assert )"1" expand "ball" )"1" expand "d2" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "cauchy?" )"2" "2" "r!1" )"2" "2" "n!1" )"2" "2" "i!1" "j!1" )"2" assert )"2" expand "ball" )"2" expand "d2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "m" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skosimp*)"3" (case-replace "j!1=0" )"1" (hide -2 -3)"1" (expand "fullset" )"1" (expand "metric_complete?" )"1" (skosimp)"1" "lambda (n:nat): u!1(n)(0)" )"1" "1" expand "metric_convergent?" )"1" "1" "lambda (n:below[1 + j!1]): x!1" )"1" expand "metric_converges_to" )"1" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" assert )"1" expand "ball" )"1" expand "sigma" )"1" expand "sigma" )"1" replace "1" rewrite "sqrt_sq_abs" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "cauchy?" )"2" "2" "r!1" )"2" "2" "n!1" )"2" "2" "i!1" "j!2" )"2" assert )"2" expand "ball" )"2" replace -3)"2" expand "sigma" )"2" expand "sigma" )"2" rewrite "sqrt_sq_abs" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "j!1>=1" )"1" (hide -3 1)"1" "complete_d2[real,[below[j!1] -> real],(LAMBDA (x,y:real): abs(x-y)),(LAMBDA (x, y: [[below[j!1] -> real]]): LAMBDA (i: below[j!1]): sq(x(i) - y(i)))))]") "1" replace -4)"1" replace -3)"1" "1" expand "fullset" )"1" expand "metric_complete?" )"1" "1" "lambda (n:nat): (u!1(n)(j!1),lambda (i:below[j!1]): u!1(n)(i))" )"1" "1" expand "metric_convergent?" )"1" "1" "lambda (n:below[1 + j!1]): if n = j!1 then x!1`1 else x!1`2(n) endif" )"1" expand "metric_converges_to" )"1" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" assert )"1" expand "ball" )"1" expand "sigma" "1" rewrite "sq_abs" )"1" rewrite "sq_sqrt" )"1" case "forall (n:nat): n <= j!1-1 => sigma[below[j!1]] LAMBDA (i_1: below[j!1]): sq(x!1`2(i_1) - u!1(i!1)(i_1))) = sigma[below[1+j!1]](0, n,LAMBDA (i: below[1 + j!1]):IF i = j!1 THEN x!1`1 ELSE x!1`2(i) ENDIF -") "1" "j!1-1" )"1" assert )nil nil ))nil )"2" "2" "n" )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" assert )nil nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil )"4" "4" "4" assert )nil nil ))nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" "6" assert )nil nil ))nil ))nil )"7" "7" assert )nil nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil )"4" "4" "4" assert )nil nil ))nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" "6" assert )nil nil ))nil ))nil )"7" "7" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "cauchy?" )"2" "2" "r!1" )"2" "2" "n!1" )"2" "2" "i!1" "j!2" )"2" assert )"2" expand "ball" )"2" rewrite "sq_sqrt" )"2" expand "sigma" "2" "sigma[below[j!1+1]](0, j!1 - 1, LAMBDA (i: below[1 + j!1]):LAMBDA (i_1: below[j!1]):") "1" rewrite "sq_abs" nil nil )"2" "2" case "forall (n:nat): n <= j!1-1 => sigma[below[j!1 + 1]] LAMBDA (i: below[1 + j!1]): sq(u!1(j!2)(i) - u!1(i!1)(i)))LAMBDA (i_1: below[j!1]): sq(u!1(j!2)(i_1) - u!1(i!1)(i_1)))") "1" "j!1-1" )"1" assert )nil nil ))nil )"2" "2" "n" )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" assert )nil nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" "5" assert )nil nil ))nil ))nil )"6" "6" assert )nil nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" "5" assert )nil nil ))nil ))nil )"6" "6" assert )nil nil ))nil ))nil ))nil )"3" "3" 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 )"2" "2" "2" expand "metric?" )"2" "1" expand "metric_zero?" )"1" "1" "1" "1" "sqrt_eq_0" "nnx" "sigma[below(j!1)](0, j!1 - 1, LAMBDA (i: below[j!1]): sq(x!1(i) - y!1(i)))" ))"1" replace -2)"1" "1" "sigma_nonneg_eq_0[below(j!1)]" "Fnnr" "LAMBDA (i_1: below[j!1]): sq(x!1(i_1) - y!1(i_1))" "low" "0" "high" "j!1-1" ))"1" replace -2)"1" "1" "sub_eq_zero[j!1]" "u" "x!1" "v" "y!1" ))"1" replace "1" "1" expand "-" )"1" "1" "x!2" )"1" rewrite "sq_eq_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sigma_Fnnr[below(j!1)]" )"1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1 1 rl)"2" "2" "extensionality" "f" "LAMBDA (i:below[j!1]): sq(x!1(i) - x!1(i))" "g" "lambda (i:below[j!1]): 0" ))"2" "1" replace -1)"1" rewrite "sigma_zero[below[j!1]]" )"1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" expand "sq" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "metric_symmetric?" )"2" "2" "extensionality" "f" "lambda (i:below[j!1]): sq(x!1(i) - y!1(i))" "g" "lambda (i:below[j!1]): sq(y!1(i) - x!1(i))" ))"2" "1" replace -1)"1" nil nil ))nil )"2" "2" "2" rewrite "sq_neg_minus" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "metric_triangle?" )"3" "3" "norm_add_le[j!1]" "u" "vectors[j!1].-(x!1,y!1)" "v" "vectors[j!1].-(y!1,z!1)" ))"3" expand "norm" )"3" expand "-" )"3" expand "sqv" )"3" expand "*" )"3" expand "sq" )"3" "(LAMBDA (i_1: Index[j!1]): LAMBDA (i: below[j!1]):") "3" "3" "(LAMBDA (i_1: Index[j!1]): LAMBDA (i: below[j!1]):") "3" "RHS" " sqrt(sigma[below[j!1]] LAMBDA (i: below[j!1]):LAMBDA (i: below[j!1]):") "1" expand "+" )"1" nil nil ))nil )"2" "2" "sigma_nonneg[below[j!1]]" "F" "LAMBDA (i: below[j!1]): " "low" "0" "high" "j!1-1" ))"1" assert )"1" "1" "sq_pos" "a" "y!1(i!1)-z!1(i!1)" ))"1" expand "sq" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" "sigma_nonneg[below[j!1]]" "F" "LAMBDA (i: below[j!1]): " "low" "0" "high" "j!1-1" ))"1" "1" nil nil )"2" "2" "sq_pos" "a" "x!1(i!1)-y!1(i!1)" ))"2" expand "sq" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "sigma_Fnnr[below(j!1)]" )"1" "1" (assert ) nil nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" assert )"4" "4" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" (hide -1 2) (("4" (grind) nil nil )) nil )"5" (skosimp) (("5" (assert ) nil nil )) nil )"6" (skosimp) (("6" (assert ) nil nil )) nil ))nil ))nil )"3" (skosimp)"3" (skosimp) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"clopen[T, (metric_induced_topology)]" real_topology nil )"metric_complete" real_topologynil )"clopen[T, (metric_induced_topology)]" euclidean nil )"bool" metric_space_def nil )nil euclidean nil )"set" sets nil )"bool" metric_space_def nil )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )nil real_types nil )set type-eq-decl nil sets nil )nil nat_types nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nnreal" vectors "vectors/" )"real" reals nil )"int" integers nil )"[bool, bool -> bool]" booleans nil )nil integers nil )nil vectors "vectors/" )nil vectors "vectors/" )nil sequences nil )"bool" booleans nil )"bool" metric_space_def nil )"metric_open" euclideannil )"(total_order?[real])" nil )"bool" sets nil )"metric" euclidean nil )"set[T]" metric_space_def nil )nil real_types nil )"bool" metric_space_def nil )"bool" metric_space_def nil )"posnat" euclidean nil )nil defined_types nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )nil sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil complete_product nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"bool" metric_def nil )nil sq "reals/" )"nnreal" nil )"(total_order?[real])" nil )nil sqrt "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )NOT const-decl "[bool -> bool]" booleans nil )"nat" euclidean nil )nil sigma "reals/" )nil sq "reals/" )"nat" vectors "vectors/" )nil sqrt "reals/" )nil functions nil )nil sigma "reals/" )nil sigma "reals/" )"real" vectors "vectors/" )nil sq "reals/" )nil vectors "vectors/" )"Vector" vectors "vectors/" )nil vectors "vectors/" )nil naturalnumbers nil )nil sqrt "reals/" )"bool" metric_def nil )nil sq "reals/" )"bool" metric_def nil )"nnreal" vectors "vectors/" )"nnreal" vectors "vectors/" )"real" vectors "vectors/" )nil sigma "reals/" )nil sq "reals/" )"real" reals nil )"real" vectors "vectors/" )"real" reals nil )nil vectors "vectors/" )"bool" metric_def nil )"real" reals nil )"odd_int" integers nil )"posint" nil )nil real_topology nil ))nil )))
Messung V0.5 in Prozent C=97 H=99 G=97
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.469Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-28)
¤ *Bot Zugriff
2026-05-26
