|
(criteria_3D
(criterion_3D?_TCC1 0
(criterion_3D?_TCC1-1 nil 3566321073 ("" (subtype-tcc) nil nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Sp_vect3 type-eq-decl nil space_3D nil)
(/= const-decl "boolean" notequal nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nzint nonempty-type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Sign type-eq-decl nil sign "reals/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(det const-decl "real" det_2D "vectors/")
(D formal-const-decl "posreal" criteria_3D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-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)
(Delta const-decl "real" horizontal nil)
(discr2b const-decl "real" quadratic_2b "reals/")
(root2b const-decl "real" quadratic_2b "reals/")
(Theta_D const-decl "real" horizontal nil)
(* const-decl "Vector" vectors_3D "vectors/")
(+ const-decl "Vector" vectors_3D "vectors/")
(H formal-const-decl "posreal" criteria_3D nil)
(closed_region_3D const-decl "bool" vertical_criterion nil)
(vertical_criterion? const-decl "SignedCrit" vertical_criterion
nil)
(R const-decl "nnreal" horizontal_criteria nil)
(horizontal_criterion? const-decl "bool" horizontal_criteria nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(sign_mult_clos application-judgement "Sign" sign "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_nz_pos application-judgement "posreal" sq "reals/"))
nil))
(criterion_3D_independence 0
(criterion_3D_independence-2 nil 3566321145
("" (skeep)
(("" (expand "criterion_3D?")
(("" (split)
(("1" (flatten)
(("1" (lemma "horizontal_criterion_independence")
(("1" (inst -1 "sp" "nv")
(("1" (flatten)
(("1" (hide -2)
(("1" (split -1)
(("1" (hide-all-but (-4 1))
(("1" (lemma "vertical_horizontal_conflict")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (inst? 1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (hide -2)
(("2" (lemma "vertical_criterion_independence")
(("2" (inst -1 "epsv" "nv" "sp" "v")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((criterion_3D? const-decl "bool" criteria_3D nil)
(vertical_criterion_independence formula-decl nil
vertical_criterion nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(Sp_vect2 type-eq-decl nil horizontal nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(H formal-const-decl "posreal" criteria_3D nil)
(Sp_vect3 type-eq-decl nil space_3D nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Sign type-eq-decl nil sign "reals/")
(vertical_horizontal_conflict formula-decl nil space_3D nil)
(horizontal_criterion_independence formula-decl nil
horizontal_criteria nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" criteria_3D nil))
nil)
(criterion_3D_independence-1 nil 3566321081 ("" (postpone) nil nil)
nil shostak))
(criterion_3D_coordination 0
(criterion_3D_coordination-1 nil 3566321160
("" (skeep)
(("" (expand "criterion_3D?")
(("" (ground)
(("1" (lemma "horizontal_criterion_coordination")
(("1" (inst - "epsh" "nvi" "nvo" "sp" "vi" "vo")
(("1" (rewrite "vect2_sub")
(("1" (rewrite "vect2_sub")
(("1" (assert)
(("1" (rewrite "vect2_neg")
(("1" (assert)
(("1" (split -)
(("1" (hide-all-but (-6 1))
(("1" (rewrite "vect2_sub" :dir rl)
(("1"
(lemma "vertical_horizontal_conflict")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-5 1))
(("2" (rewrite "vect2_sub" :dir rl)
(("2"
(lemma "vertical_horizontal_conflict")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 -3)) (("2" (grind) nil nil)) nil)
("3" (case "nvi-vo-(vi-vo) = nvi-vi")
(("1" (replace -1)
(("1" (hide -1)
(("1"
(lemma " horizontal_criterion_special_coordination")
(("1" (inst - "epsh" "nvo" "nvi" "-sp" "vi")
(("1" (rewrite "vect2_sub" :dir rl)
(("1" (rewrite "vect2_sub" :dir rl)
(("1" (rewrite "vect2_neg" :dir rl)
(("1" (assert)
(("1" (hide-all-but (-6 1))
(("1" (rewrite "vect2_neg")
(("1"
(rewrite "vect2_sub" :dir rl)
(("1"
(case-replace
"vect2(nvi-nvo)=-vect2(nvo-nvi)")
(("1"
(rewrite
"horizontal_conflict_symm")
(("1"
(lemma
"vertical_horizontal_conflict")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide -)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -) (("2" (grind) nil nil)) nil))
nil)
("4" (hide-all-but (-1 -3)) (("4" (grind) nil nil)) nil)
("5" (lemma "vertical_criterion_coordination")
(("5" (inst -1 "epsv" "nvi" "nvo" "sp" "vi" "vo")
(("5" (assert) nil nil)) nil))
nil)
("6" (lemma "vertical_criterion_coordination")
(("6" (inst -1 "epsv" "nvi" "nvo" "sp" "vi" "vo")
(("6" (assert) nil nil)) nil))
nil)
("7" (case "nvo-vi-(vo-vi) = nvo-vo")
(("1" (replace -1)
(("1" (lemma " horizontal_criterion_special_coordination")
(("1" (inst - "epsh" "nvi" "nvo" "sp" "vo")
(("1" (hide -2)
(("1" (rewrite "vect2_sub" :dir rl)
(("1" (rewrite "vect2_sub" :dir rl)
(("1" (rewrite "vect2_sub" :dir rl)
(("1" (rewrite "vect2_neg")
(("1" (assert)
(("1" (hide-all-but (-6 1))
(("1"
(lemma "vertical_horizontal_conflict")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -) (("2" (grind) nil nil)) nil))
nil)
("8" (lemma "vertical_criterion_coordination")
(("8" (inst -1 "epsv" "nvi" "nvo" "sp" "vi" "vo")
(("8" (assert) nil nil)) nil))
nil)
("9" (lemma "vertical_criterion_coordination")
(("9" (inst -1 "epsv" "nvi" "nvo" "sp" "vi" "vo")
(("9" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((criterion_3D? const-decl "bool" criteria_3D nil)
(vertical_criterion_coordination formula-decl nil
vertical_criterion nil)
(- const-decl "Vector" vectors_2D "vectors/")
(horizontal_conflict_symm formula-decl nil horizontal nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(neg_neg formula-decl nil vectors_3D "vectors/")
(horizontal_criterion_special_coordination formula-decl nil
horizontal_criterion_line nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(* const-decl "real" vectors_2D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(D formal-const-decl "posreal" criteria_3D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-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)
(horizontal_criterion_coordination formula-decl nil
horizontal_criteria nil)
(vect2_sub formula-decl nil vect_3D_2D "vectors/")
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(sqv_neg formula-decl nil vectors_2D "vectors/")
(vertical_horizontal_conflict formula-decl nil space_3D nil)
(Vector type-eq-decl nil vectors_3D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(vect2_neg formula-decl nil vect_3D_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Sp_vect3 type-eq-decl nil space_3D nil)
(H formal-const-decl "posreal" criteria_3D nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(neg_nzv application-judgement "Nz_vector" vectors_3D "vectors/"))
nil)))
¤ Dauer der Verarbeitung: 0.35 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.
|
