|
(predicate_coordination
(coordinated_symmetric 0
(coordinated_symmetric-1 nil 3489503696
(""
(case "FORALL (C, Crit1, Crit2: Criter):
symmetric?(C) IMPLIES (coordinated?(Crit1, Crit2, C) IMPLIES coordinated?(Crit2, Crit1, 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)
((- const-decl "Vector" vectors_3D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(minus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(neg_neg formula-decl nil vectors_3D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(Criter type-eq-decl nil predicate_coordination nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(Vector_Predicate nonempty-type-eq-decl nil predicate_coordination
nil)
(symmetric? const-decl "bool" predicate_coordination nil)
(coordinated? const-decl "bool" predicate_coordination nil))
shostak))
(sum_indep_coordinated 0
(sum_indep_coordinated-1 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"
(name "BB" "nvo-vi")
(("1"
(name "CC" "vo-nvi")
(("1"
(case-replace "nvo-nvi = CC+BB-AA")
(("1"
(hide -1)
(("1"
(replace -1)
(("1"
(replace -2)
(("1"
(replace -3)
(("1"
(expand "sum_closed?")
(("1"
(inst
-
"s"
"AA"
"CC+BB-AA"
"AA")
(("1"
(assert)
(("1"
(expand
"sum_independent?")
(("1"
(inst
-
"AA"
"s"
"CC"
"BB")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 -2 -3 1))
(("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)
((real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sum_closed? const-decl "bool" predicate_coordination nil)
(add_cancel2 formula-decl nil vectors_3D "vectors/")
(sum_independent? const-decl "bool" predicate_coordination nil)
(+ const-decl "Vector" vectors_3D "vectors/")
(minus_real_is_real application-judgement "real" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "Vector" vectors_3D "vectors/")
(crit_symmetric? const-decl "bool" predicate_coordination nil)
(coordinated? const-decl "bool" predicate_coordination nil))
nil))
(coordinated_sum_indep 0
(coordinated_sum_indep-1 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)
((""
(hide "Cv")
((""
(label "Cnvnw" -6)
((""
(case "v /= zero")
(("1"
(flatten)
(("1"
(reveal "Clem")
(("1"
(expand "open?")
(("1"
(inst - "s" "v" "nv+nw")
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(case "norm(v) > 0")
(("1"
(case
"(epsilon!1/(2*norm(v))) > 0")
(("1"
(name
"const1"
"(epsilon!1/(2*norm(v)))")
(("1"
(label
"constname"
-1)
(("1"
(replace -1)
(("1"
(label
"const1pos"
-2)
(("1"
(hide
"const1pos")
(("1"
(inst
"Clem"
"-const1*v")
(("1"
(split
"Clem")
(("1"
(copy
"length")
(("1"
(hide
"length")
(("1"
(copy
-1)
(("1"
(expand
"crit_independent_of_length?")
(("1"
(inst
-1
"v"
"s"
"nv"
"const1")
(("1"
(inst
-2
"v"
"s"
"nw"
"const1")
(("1"
(assert)
(("1"
(label
"cvnv"
-1)
(("1"
(label
"cvnw"
-2)
(("1"
(name
"newv"
"const1*v")
(("1"
(label
"newvname"
-1)
(("1"
(name
"vo1"
"vectors_3D.zero")
(("1"
(label
"voname"
-1)
(("1"
(name
"vi1"
"-newv")
(("1"
(label
"viname"
-1)
(("1"
(name
"nvo1"
"nv-newv")
(("1"
(label
"nvoname"
-1)
(("1"
(name
"nvi1"
"-nw")
(("1"
(label
"nviname"
-1)
(("1"
(case
"nvo1 - vi1 = nv")
(("1"
(label
"nvovi"
-1)
(("1"
(case
"vo1-nvi1 = nw")
(("1"
(label
"vonvi"
-1)
(("1"
(case
"vo1-vi1 = newv")
(("1"
(label
"vovi"
-1)
(("1"
(case
"nvo1-nvi1 = nv+nw-newv")
(("1"
(label
"nvonvi"
-1)
(("1"
(replace
"newvname")
(("1"
(expand
"coordinated?")
(("1"
(inst
-
"vo1"
"vi1"
"nvo1"
"nvi1"
"s")
(("1"
(assert)
(("1"
(expand
"crit_symmetric?")
(("1"
(inst
-
"newv"
"s"
"vo1-nvi1")
(("1"
(case
"-(vo1-nvi1) = nvi1-vo1")
(("1"
(case
"vi1-vo1 = -newv")
(("1"
(assert)
(("1"
(hide
-1)
(("1"
(hide
-1)
(("1"
(case
"nvo1-nvi1 = nv + nw + -const1 * v")
(("1"
(assert)
(("1"
(replace
"vovi")
(("1"
(replace
"newvname"
:dir
rl)
(("1"
(replace
-1
:dir
rl)
(("1"
(reveal
"Cindep")
(("1"
(reveal
"Cv")
(("1"
(expand
"independent_of_length?")
(("1"
(inst-cp
-
"s"
"v"
"v"
"const1"
"const1")
(("1"
(assert)
(("1"
(inst
-
"s"
"v"
"nvo1-nvi1"
"1"
"const1")
(("1"
(assert)
nil
nil)
("2"
(reveal
"const1pos")
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(reveal
"const1pos")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
"nvonvi")
(("2"
(replace
"newvname"
:dir
rl)
(("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
"vovi")
(("2"
(hide-all-but
("vovi"
1))
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
"nvoname"
:dir
rl)
(("2"
(replace
"nviname"
:dir
rl)
(("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
"voname"
:dir
rl)
(("2"
(replace
"viname"
:dir
rl)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(replace
"voname"
:dir
rl)
(("2"
(replace
"nviname"
:dir
rl)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(replace
"nvoname"
:dir
rl)
(("2"
(replace
"viname"
:dir
rl)
(("2"
(hide-all-but
1)
(("2"
(grind)
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(reveal
"const1pos")
(("2"
(assert)
nil
nil))
nil))
nil)
("2"
(reveal
"const1pos")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite
"norm_scal")
(("2"
(reveal
"const1pos")
(("2"
(expand
"abs")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(cross-mult 1)
(("2"
(assert)
nil
nil))
nil)
("3"
(assert)
nil
nil))
nil)
("2"
(lemma
"vectors_3D.norm_eq_0")
(("2"
(inst - "v")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(reveal "Cv")
(("2"
(flatten)
(("2"
(replace -2)
(("2"
(expand "crit_symmetric?")
(("2"
(inst - "zero " "s" "nv")
(("2"
(assert)
(("2"
(expand
"coordinated?")
(("2"
(inst
-
"zero"
"zero"
"nw"
"-nv"
"s")
(("2"
(assert)
(("2"
(case
"nw - - nv = nv + nw")
(("1"
(assert)
nil
nil)
("2"
(hide-all-but
1)
(("2"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.92 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.
|
