(predicate_coordinationnil 3489503696"" case "FORALL (C, Crit1, Crit2: Criter): C))") "1" (skeep)"1" (inst-cp - "C" "Crit1" "Crit2" )"1" (inst - "C" "Crit2" "Crit1" ) (("1" (ground) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "coordinated?" )"2" (skeep)"2" (inst - "vi" "vo" "nvi" "nvo" "-s" )"2" (assert )"2" (expand "symmetric?" )"2" (copy -1)"2" (inst - "s" "vo-vi" "nvo-nvi" )"2" case "-(vo-vi) = vi-vo AND -(nvo-nvi) = nvi-nvo" )"1" (ground)"1" (inst - "s" "vo-vi" "vo-vi" )"1" (ground) nil nil )) nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"real" reals nil )"real" reals nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil vectors_3D "vectors/" )nil reals nil )nil vectors_3D_def "vectors/" )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil predicate_coordination nil )"[bool, bool -> bool]" booleans nil )nil predicate_coordinationnil )"bool" predicate_coordination nil )"bool" predicate_coordination nil ))nil 3489507263"" (skeep)"" (ground)"" (expand "coordinated?" )"" (skeep)"" (expand "crit_symmetric?" )"" (inst - "vo-vi" "s" "vo-nvi" )"" (case "-(vo-vi) = vi-vo" )"1" (replace -1)"1" (hide -1)"1" (case "-(vo-nvi) = nvi-vo" )"1" (replace -1)"1" (hide -1)"1" (assert )"1" (name "AA" "vo-vi" )"1" "BB" "nvo-vi" )"1" "CC" "vo-nvi" )"1" "nvo-nvi = CC+BB-AA" )"1" "1" replace -1)"1" replace -2)"1" replace -3)"1" expand "sum_closed?" )"1" "s" "AA" "CC+BB-AA" "AA" )"1" assert )"1" expand "sum_independent?" )"1" "AA" "s" "CC" "BB" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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 )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )nil vectors_3D_def "vectors/" )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"real" reals nil )"real" reals nil )"bool" predicate_coordination nil )nil vectors_3D "vectors/" )"bool" predicate_coordination nil )"Vector" vectors_3D "vectors/" )"real" reals nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"Vector" vectors_3D "vectors/" )"bool" predicate_coordination nil )"bool" predicate_coordination nil ))nil ))nil 3489507292"" (skeep)"" (label "Clem" -4)"" (hide "Clem" )"" (label "Cindep" -4)"" (hide "Cindep" )"" (label "symmetric" -1)"" (label "length" -2)"" (label "coord" -3)"" (label "sumindep" 1)"" (expand "sum_independent?" )"" (skeep)"" (label "vnv" -4)"" (label "vnw" -5)"" (label "Cv" -6)"" "Cv" )"" "Cnvnw" -6)"" case "v /= zero" )"1" "1" "Clem" )"1" expand "open?" )"1" "s" "v" "nv+nw" )"1" assert )"1" "1" case "norm(v) > 0" )"1" case "(epsilon!1/(2*norm(v))) > 0" )"1" "const1" "(epsilon!1/(2*norm(v)))" )"1" "constname" "1" replace -1)"1" "const1pos" "1" "const1pos" )"1" "Clem" "-const1*v" )"1" "Clem" )"1" "length" )"1" "length" )"1" "1" expand "crit_independent_of_length?" )"1" "v" "s" "nv" "const1" )"1" "v" "s" "nw" "const1" )"1" assert )"1" "cvnv" "1" "cvnw" "1" "newv" "const1*v" )"1" "newvname" "1" "vo1" "vectors_3D.zero" )"1" "voname" "1" "vi1" "-newv" )"1" "viname" "1" "nvo1" "nv-newv" )"1" "nvoname" "1" "nvi1" "-nw" )"1" "nviname" "1" case "nvo1 - vi1 = nv" )"1" "nvovi" "1" case "vo1-nvi1 = nw" )"1" "vonvi" "1" case "vo1-vi1 = newv" )"1" "vovi" "1" case "nvo1-nvi1 = nv+nw-newv" )"1" "nvonvi" "1" replace "newvname" )"1" expand "coordinated?" )"1" "vo1" "vi1" "nvo1" "nvi1" "s" )"1" assert )"1" expand "crit_symmetric?" )"1" "newv" "s" "vo1-nvi1" )"1" case "-(vo1-nvi1) = nvi1-vo1" )"1" case "vi1-vo1 = -newv" )"1" assert )"1" "1" "1" case "nvo1-nvi1 = nv + nw + -const1 * v" )"1" assert )"1" replace "vovi" )"1" replace "newvname" "1" replace "1" "Cindep" )"1" "Cv" )"1" expand "independent_of_length?" )"1" "s" "v" "v" "const1" "const1" )"1" assert )"1" "s" "v" "nvo1-nvi1" "1" "const1" )"1" assert )nil nil )"2" "const1pos" )"2" assert )nil nil ))nil ))nil ))nil )"2" "const1pos" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "nvonvi" )"2" replace "newvname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "vovi" )"2" "vovi" "2" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "nvoname" "2" replace "nviname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "voname" "2" replace "viname" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "voname" "2" replace "nviname" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "nvoname" "2" replace "viname" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "const1pos" )"2" assert )nil nil ))nil ))nil )"2" "const1pos" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "norm_scal" )"2" "const1pos" )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" assert )nil nil ))nil )"2" "vectors_3D.norm_eq_0" )"2" "v" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "Cv" )"2" "2" replace -2)"2" expand "crit_symmetric?" )"2" "zero " "s" "nv" )"2" assert )"2" expand "coordinated?" )"2" "zero" "zero" "nw" "-nv" "s" )"2" assert )"2" case "nw - - nv = nv + nw" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" predicate_coordination nil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"bool" predicate_coordination nil )"nnreal" vectors_3D "vectors/" )nil real_types nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil booleans nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil extra_real_props nil )"Vect3" predicate_coordination nil )"[T, T -> boolean]" equalities nil )nil reals nil )"bool" nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"bool" predicate_coordination nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"bool" predicate_coordinationnil )nil vectors_3D "vectors/" )"bool" predicate_coordination nil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"nzreal" predicate_coordination nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{y: posreal | y >= x}" nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"[numfield -> numfield]" number_fields nil )"nzreal" real_typesnil )"nnreal" nil )"nzreal" nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil reals nil )nil vectors_3D_def "vectors/" )nil booleans nil )"boolean" notequal nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" ))nil ))nil 3489507336"" (skeep)"" (ground)"" (expand "coordinated?" )"" (skeep)"" (expand "crit_antisymmetric?" )"" (inst - "vo-vi" "s" "vo-nvi" "eps" )"" (case "-(vo-vi) = vi-vo" )"1" (replace -1)"1" (hide -1)"1" (case "-(vo-nvi) = nvi-vo" )"1" (replace -1)"1" (hide -1)"1" (assert )"1" (name "AA" "vo-vi" )"1" "BB" "nvo-vi" )"1" "CC" "vo-nvi" )"1" "nvo-nvi = CC+BB-AA" )"1" "1" replace -1)"1" replace -2)"1" replace -3)"1" expand "sum_closed?" )"1" "s" "AA" "CC+BB-AA" "AA" )"1" assert )"1" expand "sum_independent?" )"1" "AA" "s" "CC" "BB" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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 )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Sign" sign "reals/" )nil reals nil )nil vectors_3D_def "vectors/" )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"real" reals nil )"real" reals nil )"bool" predicate_coordination nil )nil vectors_3D "vectors/" )"bool" predicate_coordination nil )"Vector" vectors_3D "vectors/" )"real" reals nil )"Vector" vectors_3D "vectors/" )"bool" predicate_coordination nil )"bool" predicate_coordination nil ))nil ))nil 3489507368"" (skeep)"" (label "Clem" -4)"" (hide "Clem" )"" (label "Cindep" -4)"" (hide "Cindep" )"" (label "symmetric" -1)"" (label "length" -2)"" (label "coord" -3)"" (label "sumindep" 1)"" (expand "sum_independent?" )"" (skeep)"" (label "vnv" -4)"" (label "vnw" -5)"" (label "Cv" -6)"" "Cv" )"" "Cnvnw" -6)"" case "v /= zero" )"1" "1" "Clem" )"1" expand "open?" )"1" "s" "v" "nv+nw" )"1" assert )"1" "1" case "norm(v) > 0" )"1" case "(epsilon!1/(2*norm(v))) > 0" )"1" "const1" "(epsilon!1/(2*norm(v)))" )"1" "constname" "1" replace -1)"1" "const1pos" "1" "const1pos" )"1" "Clem" "-const1*v" )"1" "Clem" )"1" expand "crit_independent_of_length?" )"1" "length" )"1" "length" )"1" "1" "v" "s" "nv" "const1" )"1" "v" "s" "nw" "const1" )"1" assert )"1" "cvnv" "1" "cvnw" "1" "newv" "const1*v" )"1" "newvname" "1" "vo1" "vectors_3D.zero" )"1" "voname" "1" "vi1" "-newv" )"1" "viname" "1" "nvo1" "nv-newv" )"1" "nvoname" "1" "nvi1" "-nw" )"1" "nviname" "1" case "nvo1 - vi1 = nv" )"1" "nvovi" "1" case "vo1-nvi1 = nw" )"1" "vonvi" "1" case "vo1-vi1 = newv" )"1" "vovi" "1" case "nvo1-nvi1 = nv+nw-newv" )"1" "nvonvi" "1" expand "coordinated?" )"1" replace "newvname" )"1" "vo1" "vi1" "nvo1" "nvi1" "s" )"1" assert )"1" expand "crit_antisymmetric?" )"1" "newv" "s" "vo1-nvi1" "eps" )"1" case "-(vo1-nvi1) = nvi1-vo1" )"1" case "vi1-vo1 = -newv" )"1" assert )"1" "1" "1" case "nvo1-nvi1 = nv + nw + -const1 * v" )"1" assert )"1" replace "vovi" )"1" replace "newvname" "1" replace "1" "Cindep" )"1" "Cv" )"1" expand "independent_of_length?" )"1" "s" "v" "v" "const1" "const1" )"1" assert )"1" "s" "v" "nvo1-nvi1" "1" "const1" )"1" assert )nil nil )"2" "const1pos" )"2" assert )nil nil ))nil ))nil ))nil )"2" "const1pos" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "nvonvi" )"2" replace "newvname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "vovi" )"2" "vovi" "2" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "nvoname" "2" replace "nviname" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "voname" "2" replace "viname" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "voname" "2" replace "nviname" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "nvoname" "2" replace "viname" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "const1pos" )"2" assert )nil nil ))nil ))nil )"2" "const1pos" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "norm_scal" )"2" "const1pos" )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" assert )nil nil ))nil )"2" "vectors_3D.norm_eq_0" )"2" "v" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "Cv" )"2" "2" replace -2)"2" expand "crit_antisymmetric?" )"2" "zero " "s" "nv" "eps" )"2" assert )"2" expand "coordinated?" )"2" "zero" "zero" "nw" "-nv" "s" )"2" assert )"2" case "nw - - nv = nv + nw" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" predicate_coordination nil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"bool" predicate_coordination nil )"Sign" sign "reals/" )"nnreal" vectors_3D "vectors/" )nil real_types nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil booleans nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil extra_real_props nil )"Vect3" predicate_coordination nil )"[T, T -> boolean]" equalities nil )nil reals nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"bool" predicate_coordination nil )"bool" predicate_coordination nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"bool" predicate_coordinationnil )nil vectors_3D "vectors/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sign "reals/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"nzreal" predicate_coordination nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" nil )"(strict_total_order?[real])" real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{y: posreal | y >= x}" nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"[numfield -> numfield]" number_fields nil )"nzreal" real_typesnil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"nzreal" nil )"nnreal" nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil reals nil )nil vectors_3D_def "vectors/" )nil booleans nil )"boolean" notequal nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" ))nil ))nil 3489144195"" (skeep)"" (expand "deriv" )"" (decompose-equality) (("" (decompose-equality) nil nil ))nil ))nil ))nil )"Criter" predicate_coordination nil )nil reals nil )nil vectors_3D_def "vectors/" )nil booleans nil )"Vector" vectors_3D "vectors/" )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil predicate_coordination nil )set type-eq-decl nil sets nil )nil booleans nil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" ))nil 3488897466"" (skeep)"" (expand "subset?" )"" (skeep)"" (expand "member" )"" (expand "deriv" )"" (expand "crit_sum_closed?" )"" (inst - "s" "v" "x" "-l*v" ) (("" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"bool" predicate_coordination nil )"real" reals nil )"real" reals nil )"real" reals nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors_3D_def "vectors/" )nil reals nil )"real" reals nil )"Criter" predicate_coordination nil ))nil ))nil 3489507437"" (skeep)"" (expand "coordinated?" )"" (skeep)"" (expand "deriv" )"" (assert )"" (expand "crit_symmetric?" )"" (inst - "vo-vi" "s" "vo-nvi-l2*(vo-vi)" )"" case "-(vo - nvi - l2 * (vo - vi)) /= nvi - vo - l2 * (vi - vo)" )"1" (hide-all-but -1) (("1" (grind) nil nil )) nil )"2" (flatten)"2" (assert )"2" (replace -1)"2" (case "-(vo-vi) = vi-vo" )"1" (assert )"1" (hide -4)"1" expand "sum_independent?" )"1" "vo-vi" "s" "nvo - vi - l1 * (vo - vi)" "vo - nvi - l2 * (vo - vi)" )"1" assert )"1" case "nvo - vi - l1 * (vo - vi) + (vo - nvi - l2 * (vo - vi)) /= (nvo-nvi) + (1-(l1+l2))*(vo-vi)" )"1" "1" "1" (grind) nil nil ))nil ))nil )"2" "2" replace -1)"2" "2" replace -3)"2" (assert ) 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 ))nil ))nil ))nil ))nil ))nil ))nil )"bool" predicate_coordination nil )"Criter" predicate_coordination nil )"bool" predicate_coordination nil )"boolean" notequal nil )"Vector" vectors_3D "vectors/" )"real" reals nil )"real" reals nil )"real" reals nil )"[T, T -> boolean]" equalities nil )"Vector" vectors_3D "vectors/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"even_int" integersnil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"bool" predicate_coordination nil )"Vector" vectors_3D "vectors/" )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D_def "vectors/" )nil reals nil )"real" reals nil ))nil ))nil 3489507523"" (skeep)"" (lemma "deriv_coordinated" )"" (inst - "C" "Crit" "1" "0" )"" (assert ) (("" (rewrite "deriv_0" ) nil nil )) nil )) nil ))nil ))nil )nil predicate_coordination nil )"odd_int" integers nil )"posint" nil )nil predicate_coordination nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil predicate_coordination nil )nil predicate_coordinationnil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil vectors_3D_def "vectors/" )nil reals nil ))nil )nil 3489507460";;; Proof deriv_coordinated_oriented_1-1 for formula predicate_coordination.deriv_coordinated_oriented_1" ";;; Proof deriv_coordinated_oriented_1-1 for formula predicate_coordination.deriv_coordinated_oriented_1" "deriv_coordinated_oriented" )";;; Proof deriv_coordinated_oriented_1-1 for formula predicate_coordination.deriv_coordinated_oriented_1" "C" "Crit" "1" "0" )";;; Proof deriv_coordinated_oriented_1-1 for formula predicate_coordination.deriv_coordinated_oriented_1" assert )";;; Proof deriv_coordinated_oriented_1-1 for formula predicate_coordination.deriv_coordinated_oriented_1" rewrite "deriv_0" ) nil ))))))))";;; developed with shostak decision procedures") nil nil ))nil 3488897293"" (skeep)"" (expand "coordinated?" +)"" (skeep)"" (expand "Comb" )"" (ground)"1" (lemma "sum_indep_coordinated" )"1" (inst - "C" "Crit1" )"1" (assert )"1" (expand "coordinated?" )"1" (inst - "vo" "vi" "nvo" "nvi" "s" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (lemma "deriv_coordinated_1" )"2" (inst - "C" "Crit1" )"2" (split -)"1" (expand "coordinated?" )"1" (inst - "vi" "vo" "nvi" "nvo" "-s" )"1" (assert )"1" (expand "symmetric?" )"1" (inst-cp - "s" "vo-vi" "vo-vi" )"1" (inst - "s" "vo-vi" "nvo-nvi" )"1" assert )"1" case "-(vo-vi) = vi-vo AND -(nvo-nvi) = nvi-nvo" )"1" "1" (assert ) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil )"3" (lemma "deriv_coordinated_1" )"3" (inst - "C" "Crit1" )"3" (assert )"3" (expand "coordinated?" )"3" (inst - "vo" "vi" "nvo" "nvi" "s" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (expand "coordinated?" )"4" (inst - "vo" "vi" "nvo" "nvi" "s" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" predicate_coordination nil )"Criter" predicate_coordination nil )nil predicate_coordination nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"bool" predicate_coordination nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"real" reals nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil predicate_coordination nil )nil predicate_coordination nil )nil predicate_coordinationnil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil vectors_3D_def "vectors/" )nil reals nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.72Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27)
¤ *Eine klare Vorstellung vom Zielzustand
