Quelle vect3_Heine.prf
Sprache: Lisp
(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" "y!1" )"2" expand "extend" )"2" assert )nil nil ))nil ))nil )"3" "y!1" )"3" expand "extend" )"3" assert )nil nil ))nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "x!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "x!1" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" (inst - "z!1" "w!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide 1)"5" (lemma "product_cont_product_subset" )"5" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"5" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" "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" nil nil ))nil )"2" "y!1" )"2" expand "extend" )"2" assert )nil nil ))nil ))nil )"3" "y!1" )"3" expand "extend" )"3" assert )nil nil ))nil ))nil )"4" expand "fullset" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "x!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "x!1" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" "z!1" "w!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide 1)"6" (lemma "product_cont_product_subset" )"6" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"6" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" "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" nil nil ))nil )"2" "y!1" )"2" expand "extend" )"2" assert )nil nil ))nil ))nil )"3" "y!1" )"3" expand "extend" )"3" assert )nil nil ))nil ))nil )"4" expand "fullset" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "x!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "x!1" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" "z!1" "w!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"set" sets nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" continuity_ms_def "analysis/" )"set[T]" metric_spaces "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), Vect3],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" nil )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), Vect3],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" sets nil )"bool" continuity_ms_def "analysis/" )nil cross_metric_cont"analysis/" )"bool" reals nil )nil real_types nil )"nnreal" real_metric_space "analysis/" )"nnreal" distance_3D "vectors/" )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" nil )"bool" reals nil )nil booleans nil )nil vectors_3D_def "vectors/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vect3_Heine nil ))nil )nil 3462268134"" (lemma "curried_min_is_cont_3D_TCC1" )"" (skosimp*)"" (inst - "A!1" "B!1" )"" (prop)"1" (inst - "y1!1" ) (("1" (prop) nil )))"2" (inst - "y1!1" ) (("2" (prop) nil )))"3" (inst - "y1!1" ) (("3" (prop) nil )))"4" (lemma "product_cont_product_subset" )"4" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"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 )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "y!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "x!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "x!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))))))"2" (hide-all-but (-1 1))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" (inst - "z!1" "w!1" )"2" (assert ) nil )))))))))))))))))))))"5" (hide 1)"5" (lemma "product_cont_product_subset" )"5" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"5" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" "x!1" )"1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!1" )"2" expand "extend" )"2" assert )nil )))))"3" "y!1" )"3" expand "extend" )"3" assert )nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "x!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "x!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))))))"2" (hide-all-but (-1 1))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" "z!1" "w!1" )"2" assert )nil )))))))))))))))))))))))"6" (hide 1)"6" (lemma "product_cont_product_subset" )"6" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"6" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" "x!1" )"1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!1" )"2" expand "extend" )"2" assert )nil )))))"3" "y!1" )"3" expand "extend" )"3" assert )nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "x!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "x!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))))))"2" (hide-all-but (-1 1))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" "z!1" "w!1" )"2" assert )nil ))))))))))))))))))))))))))))))nil )nil nil )nil 3462099695";;; Proof curried_min_is_cont_3D_ed_TCC1-1 for formula real_3D_problem.curried_min_is_cont_3D_ed_TCC1" "curried_min_is_cont_3D_TCC1" )";;; Proof curried_min_is_cont_3D_ed_TCC1-1 for formula real_3D_problem.curried_min_is_cont_3D_ed_TCC1" ";;; Proof curried_min_is_cont_3D_ed_TCC1-1 for formula real_3D_problem.curried_min_is_cont_3D_ed_TCC1" "A!1" "B!1" )";;; Proof curried_min_is_cont_3D_ed_TCC1-1 for formula real_3D_problem.curried_min_is_cont_3D_ed_TCC1" "1" (inst - "y1!1" ) (("1" (prop) nil )))"2" (inst - "y1!1" ) (("2" (prop) nil )))"3" (inst - "y1!1" ) (("3" (prop) nil )))"4" (lemma "product_cont_product_subset" )"4" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"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 )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "y!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "x!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "x!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))))))"2" (hide-all-but (-1 1))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" (inst - "z!1" "w!1" )"2" (assert ) nil )))))))))))))))))))))"5" (hide 1)"5" (lemma "product_cont_product_subset" )"5" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"5" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" "x!1" )"1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!1" )"2" expand "extend" )"2" assert )nil )))))"3" "y!1" )"3" expand "extend" )"3" assert )nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "x!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "x!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))))))"2" (hide-all-but (-1 1))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" "z!1" "w!1" )"2" assert )nil )))))))))))))))))))))))"6" (hide 1)"6" (lemma "product_cont_product_subset" )"6" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"6" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" "x!1" )"1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!1" )"2" expand "extend" )"2" assert )nil )))))"3" "y!1" )"3" expand "extend" )"3" assert )nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "x!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "x!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))))))"2" (hide-all-but (-1 1))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" "z!1" "w!1" )"2" assert )nil ))))))))))))))))))))))))))))))";;; developed with shostak decision procedures") nil nil )nil 3462097826"" (subtype-tcc) nil nil ) nil nil ))nil 3462266557"" (skosimp*)"" (skoletin 1)"1" (skosimp*)"1" (lemma "curried_min_is_cont_3D" )"1" (inst - "f!1" "A!1" "B!1" )"1" (prop)"1" (assert )"1" (replace -2 - rl)"1" (expand "continuous?" )"1" (expand "continuous?" )"1" (inst - "y!1" )"1" (expand "continuous_at?" )"1" (inst - "epsilon!1" )"1" (expand "member" )"1" expand "ball" )"1" "1" "delta!1" )"1" "1" "q!1" )"1" (assert ) nil nil )"2" expand "fullset" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "fullset" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "product_cont_product_subset" )"2" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"2" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" expand "ball" )"1" "1" "x!1" )"1" "epsilon!2" )"1" "1" "delta!1" )"1" "1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" 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 )"4" expand "fullset" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "x!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "x!1" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "x!1" "y!2" "epsilon!2" )"2" (skosimp*)"2" (inst + "delta!1" )"2" "2" "z!1" "w!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -)"2" (lemma "curried_min_is_cont_TCC1" )"2" (skosimp*)"2" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"2" case "nonempty?(LAMBDA (x: real): A!1 <= x AND x <= B!1)" )"1" (assert )"1" (reveal -2)"1" (label "cont_ed" -1)"1" (label "nonempty" -2)"1" (label "bigpred" -3)"1" (prop)"1" "y!1" )"1" expand "fullset" )"1" (assert ) nil nil ))nil ))nil )"2" "y!1" )"2" expand "fullset" )"2" (assert ) nil nil ))nil ))nil )"3" "y!1" )"3" expand "fullset" )"3" (assert ) nil nil ))nil ))nil )"4" expand "nonempty?" )"4" expand "empty?" )"4" expand "member" )"4" "f!1(A!1,y!1)" )"4" (inst + "A!1" ) nil nil ))nil ))nil ))nil ))nil )"5" "product_cont_product_subset" )"5" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"5" assert )"5" "cont_ed" 1))"5" "5" "x!1" "y!2" "epsilon!1" )"5" "5" "delta!1" )"5" "5" "z!1" "w!1" )"5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" "product_cont_product_subset" )"6" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"6" assert )"6" "cont_ed" 1))"6" "6" "x!1" "y!2" "epsilon!1" )"6" "6" "delta!1" )"6" "6" "z!1" "w!1" )"6" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" expand "nonempty?" )"7" expand "empty?" )"7" expand "member" )"7" "f!1(A!1,y!1)" )"7" (inst + "A!1" ) nil nil ))nil ))nil ))nil ))nil )"8" "closed_intervals_compact" )"8" (inst - "A!1" "B!1" ) nil nil ))nil )"9" "closed_intervals_compact" )"9" (inst - "A!1" "B!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "A!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )nil reals nil )nil vectors_3D_def "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" reals nil ) (< const-decl "bool" reals nil )"[T, T -> boolean]" equalities nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )ext const-decl "set[real]" bounded_reals "reals/" )nil defined_types nil )"bool" bound_defs "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"[bool, bool -> bool]" booleans nil )min const-decl "T" bounded_reals "reals/" )nil bounded_reals "reals/" )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )nil real_types nil )"nnreal" distance_3D "vectors/" )"nnreal" real_metric_space "analysis/" )nil vect3_Heine nil )"bool" continuity_ms_def "analysis/" )"bool" continuity_ms_def "analysis/" )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"Vect3" vect3_Heine nil )"set[T]" metric_spaces "analysis/" )"Vect3" vect3_Heine nil )"set" sets nil )"bool" continuity_ms_def "analysis/" )nil cross_metric_cont"analysis/" )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" nil )NOT const-decl "[bool -> bool]" booleans nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" nil )"R" extend nil )"bool" booleans nil )"{x: real | A!1 < x}" vect3_Heine nil )"real" vect3_Heine nil )"(total_order?[real])" nil ))nil )nil 3462099137"" (skosimp*)"" (skoletin 1)"1" (skosimp*)"1" (lemma "curried_min_is_cont_3D" )"1" (inst - "A!1" "B!1" )"1" (prop)"1" (assert )"1" (replace -2 - rl)"1" (expand "continuous?" )"1" (expand "continuous?" )"1" (inst - "y!1" )"1" (expand "continuous_at?" )"1" (inst - "epsilon!1" )"1" (expand "member" )"1" expand "ball" )"1" "1" "delta!1" )"1" "1" "q!1" )"1" (assert ) nil )"2" expand "fullset" )"2" nil )))))))))))))))))))"2" (expand "fullset" )"2" (propax) nil )))))))))))))"2" (hide 2)"2" (lemma "product_cont_product_subset" )"2" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"2" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" expand "ball" )"1" "1" "x!1" )"1" "epsilon!2" )"1" "1" "delta!1" )"1" "1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" nil )))"2" "y!2" )"2" expand "extend" )"2" assert )nil )))))"3" "y!2" )"3" expand "extend" )"3" assert )nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "x!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "x!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))))))"2" (skosimp*)"2" (inst - "x!1" "y!2" "epsilon!2" )"2" (skosimp*)"2" (inst + "delta!1" )"2" "2" "z!1" "w!1" )"2" assert )nil )))))))))))))))))))))))))))))"2" (hide 2)"2" (hide -)"2" (lemma "curried_min_is_cont_TCC1" )"2" (skosimp*)"2" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"2" case "nonempty?(LAMBDA (x: real): A!1 <= x AND x <= B!1)" )"1" (assert )"1" (reveal -2)"1" (label "cont_ed" -1)"1" (label "nonempty" -2)"1" (label "bigpred" -3)"1" (prop)"1" "y!1" )"1" expand "fullset" )"1" (assert ) nil )))))"2" "y!1" )"2" expand "fullset" )"2" (assert ) nil )))))"3" "y!1" )"3" expand "fullset" )"3" (assert ) nil )))))"4" expand "nonempty?" )"4" expand "empty?" )"4" expand "member" )"4" "f(A!1,y!1)" )"4" (inst + "A!1" ) nil )))))))))"5" "product_cont_product_subset" )"5" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"5" assert )"5" "cont_ed" 1))"5" "5" "x!1" "y!2" "epsilon!1" )"5" "5" "delta!1" )"5" "5" "z!1" "w!1" )"5" assert )nil )))))))))))))))))))))"6" "product_cont_product_subset" )"6" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"6" assert )"6" "cont_ed" 1))"6" "6" "x!1" "y!2" "epsilon!1" )"6" "6" "delta!1" )"6" "6" "z!1" "w!1" )"6" assert )nil )))))))))))))))))))))"7" expand "nonempty?" )"7" expand "empty?" )"7" expand "member" )"7" "f(A!1,y!1)" )"7" (inst + "A!1" ) nil )))))))))"8" "closed_intervals_compact" )"8" (inst - "A!1" "B!1" ) nil )))"9" "closed_intervals_compact" )"9" "A!1" "B!1" )nil )))))))))))))))"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "A!1" )"2" (assert ) nil ))))))))))))))))))))))))nil )min const-decl "T" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" bound_defs "reals/" )ext const-decl "set[real]" bounded_reals "reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )nil vectors_3D_def "vectors/" )"nnreal" real_metric_space "analysis/" )"nnreal" distance_3D "vectors/" )"set[T]" metric_spaces "analysis/" )nil cross_metric_cont"analysis/" )nil real_metric_space"analysis/" )nil cross_metric_real_fun"analysis/" ))nil )nil 3462098864";;; Proof curried_min_is_cont_3D_ed-1 for formula real_3D_problem.curried_min_is_cont_3D_ed" ";;; Proof curried_min_is_cont_3D_ed-1 for formula real_3D_problem.curried_min_is_cont_3D_ed" "1" (skosimp*)"1" (lemma "curried_min_is_cont_3D" )"1" (inst - "A!1" "B!1" )"1" (prop)"1" (assert )"1" (replace -2 - rl)"1" (expand "continuous?" )"1" (expand "continuous?" )"1" (inst - "y!1" )"1" (expand "continuous_at?" )"1" (inst - "epsilon!1" )"1" (expand "member" )"1" expand "ball" )"1" "1" "delta!1" )"1" "1" "q!1" )"1" (assert ) nil )"2" expand "fullset" )"2" nil )))))))))))))))))))"2" (expand "fullset" )"2" (propax) nil )))))))))))))"2" (hide 2)"2" (lemma "product_cont_product_subset" )"2" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"2" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" expand "ball" )"1" "1" "x!1" )"1" "epsilon!2" )"1" "1" "delta!1" )"1" "1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" nil )))"2" "y!2" )"2" expand "extend" )"2" assert )nil )))))"3" "y!2" )"3" expand "extend" )"3" assert )nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "x!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "x!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))))))"2" (skosimp*)"2" (inst - "x!1" "y!2" "epsilon!2" )"2" (skosimp*)"2" (inst + "delta!1" )"2" "2" "z!1" "w!1" )"2" assert )nil )))))))))))))))))))))))))))))"2" (hide 2)"2" (hide -)"2" (lemma "curried_min_is_cont_TCC1" )"2" (skosimp*)"2" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"2" case "nonempty?(LAMBDA (x: real): A!1 <= x AND x <= B!1)" )"1" (assert )"1" (reveal -2)"1" (label "cont_ed" -1)"1" (label "nonempty" -2)"1" (label "bigpred" -3)"1" (prop)"1" "y!1" )"1" expand "fullset" )"1" (assert ) nil )))))"2" "y!1" )"2" expand "fullset" )"2" (assert ) nil )))))"3" "y!1" )"3" expand "fullset" )"3" (assert ) nil )))))"4" expand "nonempty?" )"4" expand "empty?" )"4" expand "member" )"4" "f(A!1,y!1)" )"4" (inst + "A!1" ) nil )))))))))"5" "product_cont_product_subset" )"5" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"5" assert )"5" "cont_ed" 1))"5" "5" "x!1" "y!2" "epsilon!1" )"5" "5" "delta!1" )"5" "5" "z!1" "w!1" )"5" assert )nil )))))))))))))))))))))"6" "product_cont_product_subset" )"6" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"6" assert )"6" "cont_ed" 1))"6" "6" "x!1" "y!2" "epsilon!1" )"6" "6" "delta!1" )"6" "6" "z!1" "w!1" )"6" assert )nil )))))))))))))))))))))"7" expand "nonempty?" )"7" expand "empty?" )"7" expand "member" )"7" "f(A!1,y!1)" )"7" (inst + "A!1" ) nil )))))))))"8" "closed_intervals_compact" )"8" (inst - "A!1" "B!1" ) nil )))"9" "closed_intervals_compact" )"9" "A!1" "B!1" )nil )))))))))))))))"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "A!1" )"2" (assert ) nil ))))))))))))))))))))))))";;; developed with shostak decision procedures") nil nil ))nil 3462267300"" (skosimp*)"" (lemma "multiary_Heine" )"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"" (assert )"" (prop)"1" (lemma "closed_intervals_compact" )"1" (inst - "A!1" "B!1" ) nil nil )) nil )"2" (expand "continuous?" )"2" (skosimp*)"2" (inst - "x!1" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp*)"1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "y!1" )"3" expand "extend" )"3" (assert ) nil nil ))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 ))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_uniform_continuity"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 )"bool" sets nil )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 )"set[T]" metric_spaces "analysis/" )"bool" continuity_ms_def "analysis/" )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 )nil 3462099162"" (skosimp*)"" (lemma "multiary_Heine" )"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"" (assert )"" (prop)"1" (lemma "closed_intervals_compact" )"1" (inst - "A!1" "B!1" ) nil )))"2" (expand "continuous?" )"2" (skosimp*)"2" (inst - "x!1" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp*)"1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "y!1" )"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 ))))))))))))))))))))))))nil )"nnreal" distance_3D "vectors/" )nil vectors_3D_def "vectors/" )"nnreal" real_metric_space "analysis/" )nil cross_metric_uniform_continuity"analysis/" )"set[T]" metric_spaces "analysis/" )nil real_metric_space"analysis/" ))nil )nil 3462098883";;; Proof multiary_Heine_3D-1 for formula real_3D_problem.multiary_Heine_3D" ";;; Proof multiary_Heine_3D-1 for formula real_3D_problem.multiary_Heine_3D" "multiary_Heine" )";;; Proof multiary_Heine_3D-1 for formula real_3D_problem.multiary_Heine_3D" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )";;; Proof multiary_Heine_3D-1 for formula real_3D_problem.multiary_Heine_3D" assert )";;; Proof multiary_Heine_3D-1 for formula real_3D_problem.multiary_Heine_3D" "1" (lemma "closed_intervals_compact" )"1" (inst - "A!1" "B!1" ) nil )))"2" (expand "continuous?" )"2" (skosimp*)"2" (inst - "x!1" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp*)"1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "y!1" )"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 ))))))))))))))))))))))))";;; developed with shostak decision procedures") nil nil ))nil 3462267342"" (skosimp*)"" (lemma "multiary_Heine_3D" )"" (inst - "f!1" "A!1" "B!1" )"" (expand "uniformly_continuous_in_first?" )"" (prop)"1" (inst - "y1!1" "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst - "x1!1" "x2!1" "y2!1" )"1" (assert ) nil nil )"2" (expand "fullset" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "fullset" ) (("2" (propax) nil nil )) nil ))nil )"2" (lemma "product_cont_product_subset" )"2" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1" )"2" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" "x!1" )"1" "epsilon!2" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" nil nil ))nil )"2" "y!1" )"2" expand "extend" )"2" assert )nil nil ))nil ))nil )"3" "y!1" )"3" expand "extend" )"3" assert )nil nil ))nil ))nil )"4" expand "fullset" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "x!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "x!1" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!2" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" (inst - "z!1" "w!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vect3_Heine nil )"bool" cross_metric_cont"analysis/" )"nnreal" distance_3D "vectors/" )"nnreal" real_metric_space "analysis/" )nil real_types nil )nil cross_metric_cont"analysis/" )"bool" continuity_ms_def "analysis/" )"bool" sets nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" nil )NOT const-decl "[bool -> bool]" booleans nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" nil )"R" extend nil )"bool" booleans nil )"{x: real | A!1 < x}" vect3_Heine nil )"real" vect3_Heine nil )"set[T]" metric_spaces "analysis/" )"bool" continuity_ms_def "analysis/" )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets nil )"Vect3" vect3_Heine nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"Vect3" vect3_Heine nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )nil booleans nil )nil vectors_3D_def "vectors/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )nil 3462099184"" (skosimp*)"" (lemma "multiary_Heine_3D" )"" (inst - "A!1" "B!1" )"" (expand "uniformly_continuous_in_first?" )"" (prop)"1" (inst - "y1!1" "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst - "x1!1" "x2!1" "y2!1" )"1" (assert ) nil )"2" (expand "fullset" )"2" (propax) nil )))))))))))"2" (expand "fullset" ) (("2" (propax) nil )))))"2" (lemma "product_cont_product_subset" )"2" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"2" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" "x!1" )"1" "epsilon!2" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!1" )"2" expand "extend" )"2" assert )nil )))))"3" "y!1" )"3" expand "extend" )"3" assert )nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "x!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "x!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))))))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!2" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" (inst - "z!1" "w!1" )"2" assert )nil ))))))))))))))))))))))))))))nil )"bool" cross_metric_cont"analysis/" )"nnreal" distance_3D "vectors/" )"nnreal" real_metric_space "analysis/" )nil cross_metric_cont"analysis/" )"set[T]" metric_spaces "analysis/" )nil vectors_3D_def "vectors/" ))nil )nil 3462098901";;; Proof multiary_Heine_3D_ed-1 for formula real_3D_problem.multiary_Heine_3D_ed" ";;; Proof multiary_Heine_3D_ed-1 for formula real_3D_problem.multiary_Heine_3D_ed" "multiary_Heine_3D" )";;; Proof multiary_Heine_3D_ed-1 for formula real_3D_problem.multiary_Heine_3D_ed" "A!1" "B!1" )";;; Proof multiary_Heine_3D_ed-1 for formula real_3D_problem.multiary_Heine_3D_ed" expand "uniformly_continuous_in_first?" )";;; Proof multiary_Heine_3D_ed-1 for formula real_3D_problem.multiary_Heine_3D_ed" "1" (inst - "y1!1" "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst - "x1!1" "x2!1" "y2!1" )"1" (assert ) nil )"2" (expand "fullset" )"2" (propax) nil )))))))))))"2" (expand "fullset" ) (("2" (propax) nil )))))"2" (lemma "product_cont_product_subset" )"2" "closed_intv(A!1,B!1)" "fullset[Vect3]" "f" )"2" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" "x!1" )"1" "epsilon!2" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!1" )"2" expand "extend" )"2" assert )nil )))))"3" "y!1" )"3" expand "extend" )"3" assert )nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "x!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "x!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))))))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!2" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" (inst - "z!1" "w!1" )"2" assert )nil ))))))))))))))))))))))))))))";;; developed with shostak decision procedures") nil nil )))
Messung V0.5 in Prozent C=100 H=97 G=98
¤ Dauer der Verarbeitung: 0.145 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
