|
(vect3_Heine
(IMP_cross_metric_real_fun_TCC1 0
(IMP_cross_metric_real_fun_TCC1-1 nil 3462097826
("" (lemma "real_metric_space")
(("" (inst - "fullset[real]") nil nil)) nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(real_metric_space formula-decl nil real_metric_space "analysis/"))
nil))
(IMP_cross_metric_real_fun_TCC2 0
(IMP_cross_metric_real_fun_TCC2-1 nil 3462097826
("" (lemma "vect3_metric_space") (("" (propax) nil nil)) nil)
((vect3_metric_space formula-decl nil vect3_metric_space nil)) nil))
(curried_min_exists_3D_TCC1 0
(curried_min_exists_3D_TCC1-1 nil 3610811544
("" (subtype-tcc) nil nil) nil nil))
(curried_min_exists_3D 0
(curried_min_exists_3D-4 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"
(inst - "y!2")
(("1" (assert) nil nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil nil))
nil)
("2"
(typepred "y!2")
(("2"
(expand "extend")
(("2" (prop) nil nil))
nil))
nil)
("3"
(typepred "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"
(inst - "y!2")
(("1" (assert) nil nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil nil))
nil)
("2"
(typepred "y!2")
(("2"
(expand "extend")
(("2" (assert) nil nil))
nil))
nil)
("3"
(typepred "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"
(inst - "y!2")
(("1" (assert) nil nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil nil))
nil)
("2"
(typepred "y!2")
(("2"
(expand "extend")
(("2" (prop) nil nil))
nil))
nil)
("3"
(typepred "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"
(inst - "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)
((empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(continuous_at? const-decl "bool" continuity_ms_def "analysis/")
(A!1 skolem-const-decl "real" vect3_Heine nil)
(B!1 skolem-const-decl "{x: real | A!1 < x}" vect3_Heine nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(x!1 skolem-const-decl "(extend
[[real, Vect3],
[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,
FALSE]
(fullset
[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))"
vect3_Heine nil)
(ball const-decl "set[T]" metric_spaces "analysis/")
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(y!2 skolem-const-decl "(extend
[[real, Vect3],
[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,
FALSE]
(fullset
[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))"
vect3_Heine nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(continuous? const-decl "bool" continuity_ms_def "analysis/")
(x!1 skolem-const-decl "(extend
[[real, Vect3],
[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,
FALSE]
(fullset
[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))"
vect3_Heine nil)
(y!2 skolem-const-decl "(extend
[[real, Vect3],
[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,
FALSE]
(fullset
[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))"
vect3_Heine nil)
(y!2 skolem-const-decl "(extend
[[real, Vect3],
[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,
FALSE]
(fullset
[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))"
vect3_Heine nil)
(x!1 skolem-const-decl "(extend
[[real, Vect3],
[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,
FALSE]
(fullset
[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))"
vect3_Heine nil)
(closed_intervals_compact formula-decl nil real_metric_space
"analysis/")
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(fullset const-decl "set" sets nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(curried_min_exists formula-decl nil cross_metric_real_fun
"analysis/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(dist const-decl "nnreal" distance_3D "vectors/"))
nil)
(curried_min_exists_3D-3 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"
(inst - "y!2")
(("1" (assert) nil nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil nil))
nil)
("2"
(typepred "y!2")
(("2"
(expand "extend")
(("2" (assert) nil nil))
nil))
nil)
("3"
(typepred "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"
(inst - "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)
((ball const-decl "set[T]" metric_spaces "analysis/")
(closed_intervals_compact formula-decl nil real_metric_space
"analysis/")
(curried_min_exists formula-decl nil cross_metric_real_fun
"analysis/")
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(dist const-decl "nnreal" distance_3D "vectors/"))
nil)
(curried_min_exists_3D-2 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"
(inst - "y!2")
(("1" (assert) nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil)))
("2"
(typepred "y!2")
(("2"
(expand "extend")
(("2" (prop) nil)))))
("3"
(typepred "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"
(inst - "y!2")
(("1" (assert) nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil)))
("2"
(typepred "y!2")
(("2"
(expand "extend")
(("2" (assert) nil)))))
("3"
(typepred "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)
((ball const-decl "set[T]" metric_spaces "analysis/")
(closed_intervals_compact formula-decl nil real_metric_space
"analysis/")
(curried_min_exists formula-decl nil cross_metric_real_fun
"analysis/")
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(dist const-decl "nnreal" distance_3D "vectors/"))
nil)
(curried_min_exists_3D-1 nil 3462098804
(";;; Proof curried_min_exists_3D-1 for formula real_3D_problem.curried_min_exists_3D"
(lemma "curried_min_exists")
((";;; Proof curried_min_exists_3D-1 for formula real_3D_problem.curried_min_exists_3D"
(skosimp*)
((";;; Proof curried_min_exists_3D-1 for formula real_3D_problem.curried_min_exists_3D"
(inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f")
((";;; Proof curried_min_exists_3D-1 for formula real_3D_problem.curried_min_exists_3D"
(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"
(inst - "y!2")
(("1" (assert) nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil)))
("2"
(typepred "y!2")
(("2"
(expand "extend")
(("2" (prop) nil)))))
("3"
(typepred "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"
(inst - "y!2")
(("1" (assert) nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil)))
("2"
(typepred "y!2")
(("2"
(expand "extend")
(("2" (assert) nil)))))
("3"
(typepred "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))
(curried_min_is_cont_3D_TCC1 0
(curried_min_is_cont_3D_TCC1-3 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"
(inst - "y!2")
(("1" (assert) nil nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil nil))
nil)
("2"
(typepred "y!2")
(("2"
(expand "extend")
(("2" (prop) nil nil))
nil))
nil)
("3"
(typepred "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"
(inst - "y!2")
(("1" (assert) nil nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil nil))
nil)
("2"
(typepred "y!2")
(("2"
(expand "extend")
(("2" (assert) nil nil))
nil))
nil)
("3"
(typepred "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"
(inst - "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)
((empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(continuous_at? const-decl "bool" continuity_ms_def "analysis/")
(A!1 skolem-const-decl "real" vect3_Heine nil)
(B!1 skolem-const-decl "{x: real | A!1 < x}" vect3_Heine nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(x!1 skolem-const-decl "(extend
[[real, Vect3],
[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,
FALSE]
(fullset
[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))"
vect3_Heine nil)
(ball const-decl "set[T]" metric_spaces "analysis/")
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(y!2 skolem-const-decl "(extend
[[real, Vect3],
[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,
FALSE]
(fullset
[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))"
vect3_Heine nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(continuous? const-decl "bool" continuity_ms_def "analysis/")
(x!1 skolem-const-decl "(extend
[[real, Vect3],
[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,
FALSE]
(fullset
[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))"
vect3_Heine nil)
(y!2 skolem-const-decl "(extend
[[real, Vect3],
[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,
FALSE]
(fullset
[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))"
vect3_Heine nil)
(closed_intervals_compact formula-decl nil real_metric_space
"analysis/")
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(fullset const-decl "set" sets nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(curried_min_exists formula-decl nil cross_metric_real_fun
"analysis/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(dist const-decl "nnreal" distance_3D "vectors/"))
nil)
(curried_min_is_cont_3D_TCC1-2 nil 3462099667
(";;; Proof curried_min_is_cont_3D_TCC1-1 for formula real_3D_problem.curried_min_is_cont_3D_TCC1"
(lemma "curried_min_is_cont_TCC1")
((";;; Proof curried_min_is_cont_3D_TCC1-1 for formula real_3D_problem.curried_min_is_cont_3D_TCC1"
(skosimp*)
((";;; Proof curried_min_is_cont_3D_TCC1-1 for formula real_3D_problem.curried_min_is_cont_3D_TCC1"
(inst - "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"
(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"
(inst - "y!2")
(("1" (assert) nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil)))
("2"
(typepred "y!2")
(("2"
(expand "extend")
(("2" (prop) nil)))))
("3"
(typepred "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"
(inst - "y!2")
(("1" (assert) nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil)))
("2"
(typepred "y!2")
(("2"
(expand "extend")
(("2" (assert) nil)))))
("3"
(typepred "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)
(curried_min_is_cont_3D_TCC1-1 nil 3462097826
("" (subtype-tcc) nil nil) nil nil))
(curried_min_is_cont_3D 0
(curried_min_is_cont_3D-3 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"
(typepred "y!1")
(("1"
(inst - "y!1")
(("1" (assert) nil nil)
("2"
(hide -2 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)
((dist const-decl "nnreal" distance_3D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(curried_min_is_cont formula-decl nil cross_metric_real_fun
"analysis/")
(continuous? const-decl "bool" continuity_ms_def "analysis/")
(closed_intervals_compact formula-decl nil real_metric_space
"analysis/")
(continuous? const-decl "bool" continuity_ms_def "analysis/")
(A!1 skolem-const-decl "real" vect3_Heine nil)
(B!1 skolem-const-decl "{x: real | A!1 < x}" vect3_Heine nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(x!1 skolem-const-decl "(extend
[[real, Vect3],
[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,
FALSE]
(fullset
[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))"
vect3_Heine nil)
(ball const-decl "set[T]" metric_spaces "analysis/")
(y!1 skolem-const-decl "(extend
[[real, Vect3],
[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool,
FALSE]
(fullset
[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))"
vect3_Heine nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(continuous_at? const-decl "bool" continuity_ms_def "analysis/")
(empty? const-decl "bool" sets nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(fullset const-decl "set" sets nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil)
(curried_min_is_cont_3D-2 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"
(typepred "y!1")
(("1"
(inst - "y!1")
(("1" (assert) nil)
("2"
(hide -2 2)
(("2"
(grind)
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)
((dist const-decl "nnreal" distance_3D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(curried_min_is_cont formula-decl nil cross_metric_real_fun
"analysis/")
(closed_intervals_compact formula-decl nil real_metric_space
"analysis/")
(ball const-decl "set[T]" metric_spaces "analysis/"))
nil)
(curried_min_is_cont_3D-1 nil 3462098832
(";;; Proof curried_min_is_cont_3D-1 for formula real_3D_problem.curried_min_is_cont_3D"
(skosimp*)
((";;; Proof curried_min_is_cont_3D-1 for formula real_3D_problem.curried_min_is_cont_3D"
(lemma "curried_min_is_cont")
((";;; Proof curried_min_is_cont_3D-1 for formula real_3D_problem.curried_min_is_cont_3D"
(inst - "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"
(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"
(typepred "y!1")
(("1"
(inst - "y!1")
(("1" (assert) nil)
("2"
(hide -2 2)
(("2"
(grind)
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))
(curried_min_is_cont_3D_ed_TCC1 0
(curried_min_is_cont_3D_ed_TCC1-4 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"
(inst - "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"
(inst - "epsilon!1")
(("1"
(skosimp*)
(("1"
(inst + "delta!1")
(("1"
(skosimp*)
(("1"
(inst - "y!1")
(("1" (assert) nil nil)
("2"
(expand "extend")
(("2"
(prop)
(("1"
(expand "fullset")
(("1" (propax) nil nil))
nil)
("2"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.59 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
