(vect3_Heinenil 3462097826"" (lemma "real_metric_space" )"" (inst - "fullset[real]" ) nil nil )) 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 )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets nil )nil real_metric_space "analysis/" ))nil ))nil 3462097826"" (lemma "vect3_metric_space" ) (("" (propax) nil nil )) nil )nil vect3_metric_space nil )) nil ))nil 3610811544"" (subtype-tcc) nil nil ) nil nil ))nil 3462267937"" (lemma "curried_min_exists" )"" (skosimp*)"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"" (prop)"1" (inst - "y!1" )"1" (expand "fullset" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" ) (("1" (prop) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (inst - "y!1" )"2" (expand "fullset" ) (("2" (assert ) nil nil )) nil ))nil )"3" (inst - "y!1" )"3" (expand "fullset" ) (("3" (prop) nil nil )) nil )) nil )"4" (inst - "y!1" )"4" (expand "fullset" ) (("4" (prop) nil nil )) nil )) nil )"5" (expand "nonempty?" )"5" (expand "empty?" )"5" (copy -2)"5" (inst - "(A!1 + B!1)/2" )"5" (expand "member" ) (("5" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "nonempty?" )"6" (expand "empty?" )"6" (copy -2)"6" (inst - "(A!1 + B!1)/2" )"6" (expand "member" ) (("6" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"7" (expand "nonempty?" )"7" (expand "empty?" )"7" (inst - "(A!1 + B!1)/2" )"7" (expand "member" ) (("7" (propax) nil nil )) nil ))nil ))nil ))nil )"8" (expand "nonempty?" )"8" (expand "empty?" )"8" (expand "member" )"8" (inst - "(A!1 + B!1)/2" ) (("8" (assert ) nil nil ))nil ))nil ))nil ))nil )"9" (expand "nonempty?" )"9" (expand "empty?" )"9" (expand "member" )"9" (inst - "f!1(A!1,y!1)" )"9" (inst + "A!1" ) nil nil )) nil ))nil ))nil ))nil )"10" (expand "continuous?" )"10" (expand "continuous_at?" )"10" (skosimp*)"10" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!2" )"2" expand "extend" )"2" (prop) nil nil ))nil ))nil )"3" "y!2" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil nil ))nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil nil )) nil ))nil )"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"11" (expand "continuous?" )"11" (expand "continuous_at?" )"11" (skosimp*)"11" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!2" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "y!2" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil nil ))nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil nil )) nil ))nil )"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" (hide 1)"12" (expand "continuous?" )"12" (expand "continuous_at?" )"12" (skosimp*)"12" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" expand "ball" )"1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!2" )"2" expand "extend" )"2" (prop) nil nil ))nil ))nil )"3" "y!2" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (prop)"1" (expand "fullset" )"1" (propax) nil nil )) nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil nil )) nil ))nil )"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (expand "nonempty?" )"13" (expand "empty?" )"13" (expand "member" )"13" (inst - "f!1(A!1,y!1)" )"13" (inst + "A!1" ) nil nil )) nil ))nil ))nil ))nil )"14" (lemma "curried_min_exists" )"14" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"14" (assert )"14" (prop)"1" (inst - "y!1" )"1" (expand "fullset" ) (("1" (propax) nil nil ))nil ))nil )"2" (lemma "closed_intervals_compact" )"2" (inst - "A!1" "B!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"15" (lemma "closed_intervals_compact" )"15" (inst - "A!1" "B!1" ) nil nil )) nil )"16" (lemma "closed_intervals_compact" )"16" (inst - "A!1" "B!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"real" reals nil )"bool" continuity_ms_def "analysis/" )"real" vect3_Heine nil )"{x: real | A!1 < x}" vect3_Heine nil )"bool" booleans nil )"R" extend nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" nil )"set[T]" metric_spaces "analysis/" )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" continuity_ms_def "analysis/" )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" nil )nil real_metric_space"analysis/" )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"set" sets nil )"(total_order?[real])" nil )nil cross_metric_real_fun"analysis/" )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 )"nnreal" real_metric_space "analysis/" )nil vectors_3D_def "vectors/" )"nnreal" distance_3D "vectors/" ))nil )nil 3462266266"" (lemma "curried_min_exists" )"" (skosimp*)"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"" (prop)"1" (inst - "y!1" )"1" (expand "fullset" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" ) (("1" (prop) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (inst - "y!1" )"2" (expand "fullset" ) (("2" (assert ) nil nil )) nil ))nil )"3" (inst - "y!1" )"3" (expand "fullset" ) (("3" (prop) nil nil )) nil )) nil )"4" (expand "nonempty?" )"4" (expand "empty?" )"4" (copy -2)"4" (expand "member" ) (("4" (postpone) nil nil ))nil ))nil ))nil ))nil )"5" (expand "nonempty?" )"5" (expand "empty?" )"5" (copy -2)"5" (inst - "(A!1 + B!1)/2" )"5" (expand "member" ) (("5" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "nonempty?" )"6" (expand "empty?" )"6" (copy -2)"6" (inst - "(A!1 + B!1)/2" )"6" (expand "member" ) (("6" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"7" (expand "nonempty?" )"7" (expand "empty?" )"7" (expand "member" )"7" (inst - "f!1(A!1,y!1)" )"7" (postpone) nil nil )) nil ))nil ))nil ))nil )"8" (expand "continuous?" )"8" (expand "continuous_at?" )"8" (expand "member" )"8" (expand "ball" )"8" (assert ) (("8" (postpone) nil nil )) nil )) nil ))nil ))nil ))nil )"9" (expand "continuous?" )"9" (expand "continuous_at?" )"9" (skosimp*)"9" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!2" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "y!2" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil nil ))nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil nil )) nil ))nil )"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"10" (postpone) nil nil )"11" (lemma "curried_min_exists" )"11" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"11" (assert )"11" (prop)"1" (inst - "y!1" )"1" (expand "fullset" ) (("1" (propax) nil nil ))nil ))nil )"2" (lemma "closed_intervals_compact" )"2" (inst - "A!1" "B!1" )"2" (postpone) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"12" (lemma "closed_intervals_compact" )"12" (inst - "A!1" "B!1" ) (("12" (postpone) nil nil ))nil ))nil )"13" (postpone) nil nil ) ("14" (postpone) nil nil )"15" (postpone) nil nil ) ("16" (postpone) nil nil ))nil ))nil ))nil ))nil )"set[T]" metric_spaces "analysis/" )nil real_metric_space"analysis/" )nil cross_metric_real_fun"analysis/" )"nnreal" real_metric_space "analysis/" )nil vectors_3D_def "vectors/" )"nnreal" distance_3D "vectors/" ))nil )nil 3462098999"" (lemma "curried_min_exists" )"" (skosimp*)"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"" (prop)"1" (inst - "y!1" )"1" (expand "fullset" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" ) (("1" (prop) nil )))))))))))"2" (inst - "y!1" )"2" (expand "fullset" ) (("2" (assert ) nil )))))"3" (inst - "y!1" )"3" (expand "fullset" ) (("3" (prop) nil )))))"4" (expand "nonempty?" )"4" (expand "empty?" )"4" (copy -2)"4" (inst - "(A!1 + B!1)/2" )"4" (expand "member" ) (("4" (propax) nil )))))))))))"5" (expand "nonempty?" )"5" (expand "empty?" )"5" (copy -2)"5" (inst - "(A!1 + B!1)/2" )"5" (expand "member" ) (("5" (propax) nil )))))))))))"6" (expand "nonempty?" )"6" (expand "empty?" )"6" (copy -2)"6" (inst - "(A!1 + B!1)/2" )"6" (expand "member" ) (("6" (propax) nil )))))))))))"7" (expand "nonempty?" )"7" (expand "empty?" )"7" (expand "member" )"7" (inst - "f(A!1,y!1)" )"7" (inst + "A!1" ) nil )))))))))"8" (expand "continuous?" )"8" (expand "continuous_at?" )"8" (skosimp*)"8" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!2" )"2" expand "extend" )"2" (prop) nil )))))"3" "y!2" )"3" expand "extend" )"3" assert )nil )))))))))))))))))))))))"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil )))"2" (typepred "x!1" )"2" (expand "extend" ) (("2" (assert ) nil )))))"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil )))))))))))))))))"9" (expand "continuous?" )"9" (expand "continuous_at?" )"9" (skosimp*)"9" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!2" )"2" expand "extend" )"2" (assert ) nil )))))"3" "y!2" )"3" expand "extend" )"3" assert )nil )))))))))))))))))))))))"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil )))"2" (typepred "x!1" )"2" (expand "extend" ) (("2" (assert ) nil )))))"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil )))))))))))))))))"10" (expand "nonempty?" )"10" (expand "empty?" )"10" (expand "member" )"10" (inst - "f(A!1,y!1)" )"10" (inst + "A!1" ) nil )))))))))"11" (lemma "curried_min_exists" )"11" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"11" (assert )"11" (prop)"1" (inst - "y!1" )"1" (expand "fullset" ) (("1" (propax) nil )))))"2" (lemma "closed_intervals_compact" )"2" (inst - "A!1" "B!1" ) nil )))))))))))"12" (lemma "closed_intervals_compact" )"12" (inst - "A!1" "B!1" ) nil ))))))))))nil )"set[T]" metric_spaces "analysis/" )nil real_metric_space"analysis/" )nil cross_metric_real_fun"analysis/" )"nnreal" real_metric_space "analysis/" )nil vectors_3D_def "vectors/" )"nnreal" distance_3D "vectors/" ))nil )nil 3462098804";;; Proof curried_min_exists_3D-1 for formula real_3D_problem.curried_min_exists_3D" "curried_min_exists" )";;; Proof curried_min_exists_3D-1 for formula real_3D_problem.curried_min_exists_3D" ";;; Proof curried_min_exists_3D-1 for formula real_3D_problem.curried_min_exists_3D" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )";;; Proof curried_min_exists_3D-1 for formula real_3D_problem.curried_min_exists_3D" "1" (inst - "y!1" )"1" (expand "fullset" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" ) (("1" (prop) nil )))))))))))"2" (inst - "y!1" )"2" (expand "fullset" ) (("2" (assert ) nil )))))"3" (inst - "y!1" )"3" (expand "fullset" ) (("3" (prop) nil )))))"4" (expand "nonempty?" )"4" (expand "empty?" )"4" (copy -2)"4" (inst - "(A!1 + B!1)/2" )"4" (expand "member" ) (("4" (propax) nil )))))))))))"5" (expand "nonempty?" )"5" (expand "empty?" )"5" (copy -2)"5" (inst - "(A!1 + B!1)/2" )"5" (expand "member" ) (("5" (propax) nil )))))))))))"6" (expand "nonempty?" )"6" (expand "empty?" )"6" (copy -2)"6" (inst - "(A!1 + B!1)/2" )"6" (expand "member" ) (("6" (propax) nil )))))))))))"7" (expand "nonempty?" )"7" (expand "empty?" )"7" (expand "member" )"7" (inst - "f(A!1,y!1)" )"7" (inst + "A!1" ) nil )))))))))"8" (expand "continuous?" )"8" (expand "continuous_at?" )"8" (skosimp*)"8" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!2" )"2" expand "extend" )"2" (prop) nil )))))"3" "y!2" )"3" expand "extend" )"3" assert )nil )))))))))))))))))))))))"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil )))"2" (typepred "x!1" )"2" (expand "extend" ) (("2" (assert ) nil )))))"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil )))))))))))))))))"9" (expand "continuous?" )"9" (expand "continuous_at?" )"9" (skosimp*)"9" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!2" )"2" expand "extend" )"2" (assert ) nil )))))"3" "y!2" )"3" expand "extend" )"3" assert )nil )))))))))))))))))))))))"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil )))"2" (typepred "x!1" )"2" (expand "extend" ) (("2" (assert ) nil )))))"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil )))))))))))))))))"10" (expand "nonempty?" )"10" (expand "empty?" )"10" (expand "member" )"10" (inst - "f(A!1,y!1)" )"10" (inst + "A!1" ) nil )))))))))"11" (lemma "curried_min_exists" )"11" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"11" (assert )"11" (prop)"1" (inst - "y!1" )"1" (expand "fullset" ) (("1" (propax) nil )))))"2" (lemma "closed_intervals_compact" )"2" (inst - "A!1" "B!1" ) nil )))))))))))"12" (lemma "closed_intervals_compact" )"12" (inst - "A!1" "B!1" ) nil ))))))))))";;; developed with shostak decision procedures") nil nil ))nil 3462268033"" (lemma "curried_min_exists" )"" (skosimp*)"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"" (prop)"1" (inst - "y!1" )"1" (expand "fullset" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" ) (("1" (prop) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (inst - "y!1" )"2" (expand "fullset" ) (("2" (assert ) nil nil )) nil ))nil )"3" (inst - "y!1" )"3" (expand "fullset" ) (("3" (prop) nil nil )) nil )) nil )"4" (expand "nonempty?" )"4" (expand "empty?" )"4" (copy -2)"4" (inst - "(A!1 + B!1)/2" )"4" (expand "member" ) (("4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"5" (expand "nonempty?" )"5" (expand "empty?" )"5" (copy -2)"5" (inst - "(A!1 + B!1)/2" )"5" (expand "member" ) (("5" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "nonempty?" )"6" (expand "empty?" )"6" (copy -2)"6" (inst - "(A!1 + B!1)/2" )"6" (expand "member" ) (("6" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"7" (expand "nonempty?" )"7" (expand "empty?" )"7" (expand "member" )"7" (inst - "f!1(A!1,y!1)" )"7" (inst + "A!1" ) nil nil )) nil ))nil ))nil ))nil )"8" (expand "continuous?" )"8" (expand "continuous_at?" )"8" (skosimp*)"8" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!2" )"2" expand "extend" )"2" (prop) nil nil ))nil ))nil )"3" "y!2" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil nil ))nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil nil )) nil ))nil )"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"9" (expand "continuous?" )"9" (expand "continuous_at?" )"9" (skosimp*)"9" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!2" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "y!2" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil nil ))nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil nil )) nil ))nil )"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"10" (expand "nonempty?" )"10" (expand "empty?" )"10" (expand "member" )"10" (inst - "f!1(A!1,y!1)" )"10" (inst + "A!1" ) nil nil )) nil ))nil ))nil ))nil )"11" (lemma "curried_min_exists" )"11" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"11" (assert )"11" (prop)"1" (inst - "y!1" )"1" (expand "fullset" ) (("1" (propax) nil nil ))nil ))nil )"2" (lemma "closed_intervals_compact" )"2" (inst - "A!1" "B!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"12" (lemma "closed_intervals_compact" )"12" (inst - "A!1" "B!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"real" reals nil )"bool" continuity_ms_def "analysis/" )"real" vect3_Heine nil )"{x: real | A!1 < x}" vect3_Heine nil )"bool" booleans nil )"R" extend nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" nil )"set[T]" metric_spaces "analysis/" )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" continuity_ms_def "analysis/" )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" nil )nil real_metric_space"analysis/" )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"set" sets nil )"(total_order?[real])" nil )nil cross_metric_real_fun"analysis/" )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 )"nnreal" real_metric_space "analysis/" )nil vectors_3D_def "vectors/" )"nnreal" distance_3D "vectors/" ))nil )nil 3462099667";;; Proof curried_min_is_cont_3D_TCC1-1 for formula real_3D_problem.curried_min_is_cont_3D_TCC1" "curried_min_is_cont_TCC1" )";;; Proof curried_min_is_cont_3D_TCC1-1 for formula real_3D_problem.curried_min_is_cont_3D_TCC1" ";;; Proof curried_min_is_cont_3D_TCC1-1 for formula real_3D_problem.curried_min_is_cont_3D_TCC1" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )";;; Proof curried_min_is_cont_3D_TCC1-1 for formula real_3D_problem.curried_min_is_cont_3D_TCC1" "1" (inst - "y!1" )"1" (expand "fullset" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" ) (("1" (prop) nil )))))))))))"2" (inst - "y!1" )"2" (expand "fullset" ) (("2" (assert ) nil )))))"3" (inst - "y!1" )"3" (expand "fullset" ) (("3" (prop) nil )))))"4" (expand "nonempty?" )"4" (expand "empty?" )"4" (copy -2)"4" (inst - "(A!1 + B!1)/2" )"4" (expand "member" ) (("4" (propax) nil )))))))))))"5" (expand "nonempty?" )"5" (expand "empty?" )"5" (copy -2)"5" (inst - "(A!1 + B!1)/2" )"5" (expand "member" ) (("5" (propax) nil )))))))))))"6" (expand "nonempty?" )"6" (expand "empty?" )"6" (copy -2)"6" (inst - "(A!1 + B!1)/2" )"6" (expand "member" ) (("6" (propax) nil )))))))))))"7" (expand "nonempty?" )"7" (expand "empty?" )"7" (expand "member" )"7" (inst - "f(A!1,y!1)" )"7" (inst + "A!1" ) nil )))))))))"8" (expand "continuous?" )"8" (expand "continuous_at?" )"8" (skosimp*)"8" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!2" )"2" expand "extend" )"2" (prop) nil )))))"3" "y!2" )"3" expand "extend" )"3" assert )nil )))))))))))))))))))))))"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil )))"2" (typepred "x!1" )"2" (expand "extend" ) (("2" (assert ) nil )))))"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil )))))))))))))))))"9" (expand "continuous?" )"9" (expand "continuous_at?" )"9" (skosimp*)"9" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!2" )"2" expand "extend" )"2" (assert ) nil )))))"3" "y!2" )"3" expand "extend" )"3" assert )nil )))))))))))))))))))))))"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil )))"2" (typepred "x!1" )"2" (expand "extend" ) (("2" (assert ) nil )))))"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil )))))))))))))))))"10" (expand "nonempty?" )"10" (expand "empty?" )"10" (expand "member" )"10" (inst - "f(A!1,y!1)" )"10" (inst + "A!1" ) nil )))))))))"11" (lemma "curried_min_is_cont_TCC1" )"11" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"11" (assert )"11" (prop)"1" (inst - "y!1" )"1" (expand "fullset" ) (("1" (propax) nil )))))"2" (lemma "closed_intervals_compact" )"2" (inst - "A!1" "B!1" ) nil )))))))))))"12" (lemma "closed_intervals_compact" )"12" (inst - "A!1" "B!1" ) nil ))))))))))";;; developed with shostak decision procedures") nil nil )nil 3462097826"" (subtype-tcc) nil nil ) nil nil ))nil 3462266508"" (skosimp*)"" (lemma "curried_min_is_cont" )"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"" (prop)"1" (expand "continuous?" +)"1" (expand "fullset" ) (("1" (propax) nil nil )) nil ))nil )"2" (lemma "closed_intervals_compact" )"2" (inst?) nil nil )) nil )"3" (hide 2)"3" (expand "continuous?" )"3" (skosimp*)"3" (inst - "x!1" )"1" (expand "continuous_at?" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta !1" )"1" (skosimp*)"1" expand "member" )"1" expand "ball" )"1" "y!1" )"1" "y!1" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (typepred "x!1" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "nonempty?" )"4" (expand "empty?" )"4" (expand "member" )"4" (inst - "(A!1 + B!1)/2" ) (("4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" distance_3D "vectors/" )nil vectors_3D_def "vectors/" )"nnreal" real_metric_space "analysis/" )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 )nil cross_metric_real_fun"analysis/" )"bool" continuity_ms_def "analysis/" )nil real_metric_space"analysis/" )"bool" continuity_ms_def "analysis/" )"real" vect3_Heine nil )"{x: real | A!1 < x}" vect3_Heine nil )"bool" booleans nil )"R" extend nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" nil )"set[T]" metric_spaces "analysis/" )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" continuity_ms_def "analysis/" )"bool" sets nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"real" reals nil )"bool" sets nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"set" sets nil )"(total_order?[real])" nil ))nil )nil 3462099117"" (skosimp*)"" (lemma "curried_min_is_cont" )"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"" (prop)"1" (expand "continuous?" +)"1" (expand "fullset" ) (("1" (propax) nil )))))"2" (lemma "closed_intervals_compact" ) (("2" (inst?) nil )))"3" (hide 2)"3" (expand "continuous?" )"3" (skosimp*)"3" (inst - "x!1" )"1" (expand "continuous_at?" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta !1" )"1" (skosimp*)"1" expand "member" )"1" expand "ball" )"1" "y!1" )"1" "y!1" )"1" (assert ) nil )"2" "2" nil )))))))))))))))))))))))"2" (hide 2)"2" (typepred "x!1" )"2" (grind) nil )))))))))))))"4" (expand "nonempty?" )"4" (expand "empty?" )"4" (expand "member" )"4" (inst - "(A!1 + B!1)/2" )"4" (assert ) nil ))))))))))))))))nil )"nnreal" distance_3D "vectors/" )nil vectors_3D_def "vectors/" )"nnreal" real_metric_space "analysis/" )nil cross_metric_real_fun"analysis/" )nil real_metric_space"analysis/" )"set[T]" metric_spaces "analysis/" ))nil )nil 3462098832";;; Proof curried_min_is_cont_3D-1 for formula real_3D_problem.curried_min_is_cont_3D" ";;; Proof curried_min_is_cont_3D-1 for formula real_3D_problem.curried_min_is_cont_3D" "curried_min_is_cont" )";;; Proof curried_min_is_cont_3D-1 for formula real_3D_problem.curried_min_is_cont_3D" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )";;; Proof curried_min_is_cont_3D-1 for formula real_3D_problem.curried_min_is_cont_3D" "1" (expand "continuous?" +)"1" (expand "fullset" ) (("1" (propax) nil )))))"2" (lemma "closed_intervals_compact" ) (("2" (inst?) nil )))"3" (hide 2)"3" (expand "continuous?" )"3" (skosimp*)"3" (inst - "x!1" )"1" (expand "continuous_at?" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta !1" )"1" (skosimp*)"1" expand "member" )"1" expand "ball" )"1" "y!1" )"1" "y!1" )"1" (assert ) nil )"2" "2" nil )))))))))))))))))))))))"2" (hide 2)"2" (typepred "x!1" )"2" (grind) nil )))))))))))))"4" (expand "nonempty?" )"4" (expand "empty?" )"4" (expand "member" )"4" (inst - "(A!1 + B!1)/2" )"4" (assert ) nil ))))))))))))))))";;; developed with shostak decision procedures") nil nil ))nil 3462268254"" (lemma "curried_min_is_cont_3D_TCC1" )"" (skosimp*)"" (inst - "f!1" "A!1" "B!1" )"" (prop)"1" (inst - "y1!1" ) (("1" (prop) nil nil )) nil )"2" (inst - "y1!1" ) (("2" (prop) nil nil )) nil )"3" (inst - "y1!1" ) (("3" (prop) nil nil )) nil )"4" (lemma "product_cont_product_subset" )"4" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"4" (prop)"1" (hide-all-but (-1 2))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" (inst - "x!1" )"1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" quality 97%
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.53Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤ *Eine klare Vorstellung vom Zielzustand
