|
(cr3d
(cr_satifies_criterion_3D 0
(cr_satifies_criterion_3D-1 nil 3513101503
("" (skeep)
(("" (expand "cr?")
(("" (expand "criterion_3D?")
(("" (flatten)
(("" (split -2)
(("1" (flatten)
(("1" (hide 2)
(("1" (assert)
(("1" (lemma "horizontal_cr_is_line_solution")
(("1" (inst?)
(("1" (assert)
(("1"
(lemma
"line_solution_meets_horizontal_criterion")
(("1" (inst?)
(("1" (assert)
(("1"
(rewrite "vect2_sub" :dir rl)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case-replace "nvo - vi - (vo - vi) = nvo-vo")
(("1" (hide -1)
(("1" (lemma "vertical_horizontal_conflict")
(("1" (inst -1 "sp" "vo-vi")
(("1" (assert)
(("1" (flatten)
(("1"
(lemma
"vertical_cr_meets_vertical_criterion")
(("1" (inst?)
(("1" (assert)
(("1"
(lemma
"hor_circle_meets_horizontal_criterion")
(("1"
(inst
-1
"hst(vect2(sp), vect2(vo - vi))"
"vst(sp, vo - vi)"
"nvo"
"sp"
"vi"
"vo")
(("1"
(split -1)
(("1" (assert) nil nil)
("2" (assert) nil nil)
("3"
(expand "vertical_cr?")
(("3"
(assert)
(("3"
(ground)
(("3"
(case-replace
"vect2(nvo-vo)=zero")
(("1"
(hide-all-but 4)
(("1" (grind) nil nil))
nil)
("2"
(hide-all-but (-4 1))
(("2"
(expand "vs_circle?")
(("2"
(flatten)
(("2"
(typepred
"vs_circle(sp, vo, vi, vst(sp, vo - vi))")
(("2"
(assert)
(("2"
(replaces
-2
:dir
rl)
(("2"
(decompose-equality
1)
(("1"
(grind)
nil
nil)
("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cr? const-decl "bool" cr3d nil)
(vertical_horizontal_conflict formula-decl nil space_3D nil)
(vertical_cr_meets_vertical_criterion formula-decl nil vertical_cr
nil)
(vertical_cr? const-decl "bool" vertical_cr nil)
(vs_circle const-decl
"{nvo | vect2(nvo) /= zero IMPLIES vs_only?(vo)(nvo)}" vs_circle
nil)
(vs_only? const-decl "bool" definitions_3D nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(vs_circle? const-decl "bool" vs_circle nil)
(real_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)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(horizontal_criterion? const-decl "bool" horizontal_criteria nil)
(det const-decl "real" det_2D "vectors/")
(R const-decl "nnreal" horizontal_criteria nil)
(* const-decl "real" vectors_2D "vectors/")
(comp_zero_y formula-decl nil vectors_2D "vectors/")
(comp_zero_x formula-decl nil vectors_2D "vectors/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(hor_circle_meets_horizontal_criterion formula-decl nil vertical_cr
nil)
(Vertical_Strategy nonempty-type-eq-decl nil space_3D nil)
(- const-decl "Vector" vectors_3D "vectors/")
(zero const-decl "Vector" vectors_3D "vectors/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(Horizontal_Strategy nonempty-type-eq-decl nil definitions nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(H formal-const-decl "posreal" cr3d nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(Sp_vect3 type-eq-decl nil space_3D nil)
(Vector type-eq-decl nil vectors_3D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(line_solution_meets_horizontal_criterion formula-decl nil
line_solutions nil)
(vect2_sub formula-decl nil vect_3D_2D "vectors/")
(horizontal_cr_is_line_solution formula-decl nil horizontal_cr 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" cr3d nil)
(criterion_3D? const-decl "bool" criteria_3D nil))
shostak))
(cr3d_satifies_criterion_3D 0
(cr3d_satifies_criterion_3D-1 nil 3513105782
("" (skeep)
(("" (expand "cr3d?")
(("" (lemma "cr_satifies_criterion_3D")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((cr3d? const-decl "bool" cr3d nil)
(verticalCoordinationConflict_strategy name-judgement
"Vertical_Strategy" cr3d nil)
(horizontalCoordination_strategy name-judgement
"Horizontal_Strategy" definitions nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(Horizontal_Strategy nonempty-type-eq-decl nil definitions nil)
(horizontalCoordination const-decl "Sign" definitions nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(H formal-const-decl "posreal" cr3d nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(D formal-const-decl "posreal" cr3d nil)
(Sp_vect3 type-eq-decl nil space_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(Vector type-eq-decl nil vectors_3D "vectors/")
(zero const-decl "Vector" vectors_3D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(Vertical_Strategy nonempty-type-eq-decl nil space_3D nil)
(verticalCoordinationConflict const-decl "Sign" space_3D nil)
(cr_satifies_criterion_3D formula-decl nil cr3d nil))
shostak))
(cr_independence 0
(cr_independence-1 nil 3471195808
("" (skeep)
(("" (lemma "cr_satifies_criterion_3D")
(("" (inst?)
(("" (assert)
(("" (lemma "criterion_3D_independence")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((cr_satifies_criterion_3D formula-decl nil cr3d nil)
(- const-decl "Vector" vectors_3D "vectors/")
(criterion_3D_independence formula-decl nil criteria_3D nil)
(Vertical_Strategy nonempty-type-eq-decl nil space_3D nil)
(- const-decl "Vector" vectors_3D "vectors/")
(zero const-decl "Vector" vectors_3D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(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)
(D formal-const-decl "posreal" cr3d nil)
(sq const-decl "nonneg_real" sq "reals/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(H formal-const-decl "posreal" cr3d nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Horizontal_Strategy nonempty-type-eq-decl nil definitions nil)
(- const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "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)
(bool nonempty-type-eq-decl nil 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_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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil))
nil))
(cr3d_independence 0
(cr3d_independence-1 nil 3451930988
("" (skeep)
(("" (expand "cr3d?")
(("" (lemma "cr_independence")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((cr3d? const-decl "bool" cr3d nil)
(verticalCoordinationConflict_strategy name-judgement
"Vertical_Strategy" cr3d nil)
(horizontalCoordination_strategy name-judgement
"Horizontal_Strategy" definitions nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(Horizontal_Strategy nonempty-type-eq-decl nil definitions nil)
(horizontalCoordination const-decl "Sign" definitions nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(H formal-const-decl "posreal" cr3d nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(D formal-const-decl "posreal" cr3d nil)
(Sp_vect3 type-eq-decl nil space_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(Vector type-eq-decl nil vectors_3D "vectors/")
(zero const-decl "Vector" vectors_3D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(Vertical_Strategy nonempty-type-eq-decl nil space_3D nil)
(verticalCoordinationConflict const-decl "Sign" space_3D nil)
(cr_independence formula-decl nil cr3d nil))
shostak))
(cr_coordination 0
(cr_coordination-1 nil 3513105974
("" (skeep)
(("" (lemma "cr_satifies_criterion_3D")
(("" (inst?)
(("" (assert)
(("" (hide -3)
(("" (lemma "cr_satifies_criterion_3D")
(("" (inst -1 "hst" "nvi" "-sp" "vo" "vi" "vst")
(("" (assert)
(("" (split -1)
(("1" (lemma "criterion_3D_coordination")
(("1" (rewrite "vect2_neg")
(("1"
(inst -1 "hst(vect2(sp), vect2(vo - vi))"
"vst(sp, vo - vi)" "nvi" "nvo" "sp" "vi"
"vo")
(("1" (assert)
(("1" (typepred "hst")
(("1"
(inst?)
(("1"
(case-replace
"vect2(vi - vo) = -vect2(vo - vi)")
(("1"
(hide -1)
(("1"
(replaces -1)
(("1"
(typepred "vst")
(("1"
(inst -1 "sp" "vo-vi")
(("1"
(split -1)
(("1"
(case-replace
"-(vo-vi) = vi-vo")
(("1" (assert) nil nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(flatten)
(("2"
(typepred "sp")
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "conflict_symm")
(("2" (inst -1 "sp" "vo-vi")
(("2" (case-replace "-(vo-vi) = vi-vo")
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cr_satifies_criterion_3D formula-decl nil cr3d nil)
(neg_sp application-judgement "Sp_vect3[D, H]" cr3d nil)
(neg_nzv application-judgement "Nz_vector" vectors_3D "vectors/")
(conflict_symm formula-decl nil space_3D nil)
(criterion_3D_coordination formula-decl nil criteria_3D nil)
(- const-decl "Vector" vectors_3D "vectors/")
(NOT const-decl "[bool -> bool]" booleans nil)
(* const-decl "real" vectors_2D "vectors/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(vect2_neg formula-decl nil vect_3D_2D "vectors/")
(Vertical_Strategy nonempty-type-eq-decl nil space_3D nil)
(- const-decl "Vector" vectors_3D "vectors/")
(zero const-decl "Vector" vectors_3D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(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)
(D formal-const-decl "posreal" cr3d nil)
(sq const-decl "nonneg_real" sq "reals/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(H formal-const-decl "posreal" cr3d nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Horizontal_Strategy nonempty-type-eq-decl nil definitions nil)
(- const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "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)
(bool nonempty-type-eq-decl nil 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_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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil))
shostak))
(cr3d_coordination 0
(cr3d_coordination-1 nil 3451931256
("" (skeep)
(("" (expand "cr3d?")
(("" (lemma "cr_coordination")
(("" (inst? -1)
(("" (inst -1 "nvi") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((cr3d? const-decl "bool" cr3d nil)
(verticalCoordinationConflict_strategy name-judgement
"Vertical_Strategy" cr3d nil)
(horizontalCoordination_strategy name-judgement
"Horizontal_Strategy" definitions nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(Horizontal_Strategy nonempty-type-eq-decl nil definitions nil)
(horizontalCoordination const-decl "Sign" definitions nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(H formal-const-decl "posreal" cr3d nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(D formal-const-decl "posreal" cr3d nil)
(Sp_vect3 type-eq-decl nil space_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(Vector type-eq-decl nil vectors_3D "vectors/")
(zero const-decl "Vector" vectors_3D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(Vertical_Strategy nonempty-type-eq-decl nil space_3D nil)
(verticalCoordinationConflict const-decl "Sign" space_3D nil)
(neg_sp application-judgement "Sp_vect3[D, H]" cr3d nil)
(neg_nzv application-judgement "Nz_vector" vectors_3D "vectors/")
(cr_coordination formula-decl nil cr3d nil))
shostak)))
¤ Dauer der Verarbeitung: 0.10 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.
|
