| products/Sources/formale Sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispOriginal von: PVS© |
|
||||||
|
(predicate_coordination_2D
(coordinated_symmetric_2D 0 (coordinated_symmetric_2D-1 nil 3489509336 ("" (case "FORALL (C, Crit1, Crit2: Criter): symmetric_2D?(C) IMPLIES (coordinated_2D?(Crit1, Crit2, C) IMPLIES coordinated_2D?(Cri (("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_2D?") (("2" (skeep) (("2" (inst - "vi" "vo" "nvi" "nvo" "-s") (("2" (assert) (("2" (expand "symmetric_2D?") (("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_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "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_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_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_2D nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Vector_Predicate nonempty-type-eq-decl nil predicate_coordination_2D nil) (symmetric_2D? const-decl "bool" predicate_coordination_2D nil) (coordinated_2D? const-decl "bool" predicate_coordination_2D nil)) nil)) (sum_indep_coordinated_2D 0 (sum_indep_coordinated_2D-1 nil 3489509368 ("" (skeep) (("" (ground) (("" (expand "coordinated_2D?") (("" (skeep) (("" (expand "crit_symmetric_2D?") (("" (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_2D?") (("1" (inst - "s" "AA" "CC+BB-AA" "AA") (("1" (assert) (("1" (expand "sum_independent_2D?") (("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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sum_closed_2D? const-decl "bool" predicate_coordination_2D nil) (add_cancel2 formula-decl nil vectors_2D "vectors/") (sum_independent_2D? const-decl "bool" predicate_coordination_2D nil) (+ const-decl "Vector" vectors_2D "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_2D "vectors/") (crit_symmetric_2D? const-decl "bool" predicate_coordination_2D nil) (coordinated_2D? const-decl "bool" predicate_coordination_2D nil)) nil)) (coordinated_sum_indep_2D 0 (coordinated_sum_indep_2D-1 nil 3489509396 ("" (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_2D?") (("" (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_2D?") (("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_2D?") (("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_2D.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_2D?") (("1" (inst - "vo1" "vi1" "nvo1" "nvi1" "s") (("1" (assert) (("1" (expand "crit_symmetric_2D?") (("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_2D?") (("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_2D.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_2D?") (("2" (inst - "zero " "s" "nv") (("2" (assert) (("2" (expand "coordinated_2D?") (("2" (inst - "zero" "zero" "nw" "-nv" "s") (("2" (assert) (("2" (case "nw - - nv = nv + nw") (("1" (assert) nil nil) ("2" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.34 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.Bot Zugriff |
