|
(delay_3D
(delay_conflict_free_rel 0
(delay_conflict_free_rel-1 nil 3524919248
("" (skeep)
(("" (case "conflict_3D?[D, H, 0, nnt](s, v)")
(("1" (hide 3)
(("1" (hide-all-but (-1 -2 1))
(("1" (expand "conflict_3D?")
(("1" (skeep -1)
(("1" (inst + "t")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (case "NOT rt > nnt")
(("1" (assert) nil nil)
("2" (hide -2)
(("2" (label "rtgtnnt" -1)
(("2" (assert)
(("2" (copy -3)
(("2" (expand "conflict?" -1)
(("2" (skolem -1 "pstar")
(("2" (flatten)
(("2" (lemma "conflict_sum_closed[D,H]")
(("2"
(inst - "s + rt*v" "(rt-nnt)*v"
"(pstar*nv) - ((rt-nnt)*v)")
(("2" (split -)
(("1"
(case "NOT (rt - nnt) * v + ((pstar * nv) - ((rt - nnt) * v)) = pstar*nv")
(("1"
(hide-all-but 1)
(("1" (grind) nil nil))
nil)
("2"
(replace -1)
(("2"
(hide -1)
(("2"
(hide-all-but (-1 3))
(("2"
(expand "conflict?")
(("2"
(skosimp*)
(("2"
(case "pstar = 0")
(("1"
(inst + "0")
(("1"
(replace -1)
(("1" (assert) nil nil))
nil))
nil)
("2"
(inst + "nnt!1*pstar")
(("2"
(grind
:exclude
("abs" "sqv"))
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-4 "rtgtnnt" 3 1))
(("2"
(case "conflict?[D,H](s + rt * v, v)")
(("1"
(hide-all-but (-1 -2 1))
(("1"
(expand "conflict?")
(("1"
(skosimp*)
(("1"
(inst + "nnt!1/(rt-nnt)")
(("1"
(case
"NOT (s + rt * v)`z + nnt!1 * v`z = (s + rt * v)`z + nnt!1 / (rt - nnt) * ((rt - nnt) * v)`z")
(("1"
(assert)
(("1"
(cross-mult 1)
(("1"
(rewrite "vz_scal")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(case
"vect2(s + rt * v) + nnt!1 * vect2(v) = vect2(s + rt * v) + nnt!1 / (rt - nnt) * vect2((rt - nnt) * v)")
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(case
"nnt!1 * vect2(v) = nnt!1 / (rt - nnt) * vect2((rt - nnt) * v)")
(("1"
(assert)
nil
nil)
("2"
(hide 2)
(("2"
(rewrite
"vect2_scal")
(("2"
(case
"nnt!1 = nnt!1/(rt-nnt) * (rt-nnt)")
(("1"
(assert)
nil
nil)
("2"
(cross-mult
1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (cross-mult 1) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "conflict?")
(("2"
(skosimp*)
(("2"
(case "nnt!1 <= rt")
(("1"
(hide 1)
(("1"
(expand "conflict_3D?")
(("1"
(inst + "nnt!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide 3)
(("2"
(inst + "nnt!1 - rt")
(("1"
(grind
:exclude
("abs" "sqv"))
nil
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "conflict?" 1)
(("3"
(inst + "1")
(("3"
(case
"(s + rt * v)`z + 1 * ((pstar * nv) - ((rt - nnt) * v))`z = (s + nnt * v)`z + pstar * nv`z")
(("1"
(case
"vect2(s + rt * v) + 1 * vect2((pstar * nv) - ((rt - nnt) * v)) = vect2(s + nnt * v) + pstar * vect2(nv)")
(("1" (assert) nil nil)
("2"
(hide-all-but 1)
(("2" (grind) 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))
nil))
nil))
nil))
nil)
((conflict_3D? const-decl "bool" cd3d nil)
(H formal-const-decl "posreal" delay_3D nil)
(D formal-const-decl "posreal" delay_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)
(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)
(number nonempty-type-decl nil numbers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(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)
(rt skolem-const-decl "posreal" delay_3D nil)
(t skolem-const-decl "Lookahead[0, nnt]" delay_3D nil)
(Lookahead type-eq-decl nil Lookahead nil)
(nnt skolem-const-decl "posreal" delay_3D nil)
(nnreal type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(conflict? const-decl "bool" space_3D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_3D "vectors/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "Vector" vectors_3D "vectors/")
(+ const-decl "Vector" vectors_3D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(scal_1 formula-decl nil vectors_2D "vectors/")
(nnt!1 skolem-const-decl "nnreal" delay_3D nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(times_div2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_cancel4 formula-decl nil real_props nil)
(vz_scal formula-decl nil vectors_3D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(vect2_scal formula-decl nil vect_3D_2D "vectors/")
(scal_assoc formula-decl nil vectors_2D "vectors/")
(nnt!1 skolem-const-decl "nnreal" delay_3D nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(scal_0 formula-decl nil vectors_2D "vectors/")
(add_zero_right formula-decl nil vectors_2D "vectors/")
(scal_zero formula-decl nil vectors_2D "vectors/")
(vect2_zero formula-decl nil vect_3D_2D "vectors/")
(comp_zero_z formula-decl nil vectors_3D "vectors/")
(scal_0 formula-decl nil vectors_3D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(conflict_sum_closed formula-decl nil space_3D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(delay_conflict_free 0
(delay_conflict_free-1 nil 3524918993
("" (lemma "delay_conflict_free_rel")
(("" (skeep)
(("" (inst - "nnt" "nvo-vi" "rt" "so-si" "vo-vi")
(("" (assert)
((""
(case "FORALL (zzrt:real): so - si + zzrt * (vo - vi) = (so + zzrt * vo) - (si + zzrt * vi)")
(("1" (inst-cp - "rt")
(("1" (inst - "nnt")
(("1" (replace -1)
(("1" (replace -2)
(("1" (hide (-1 -2)) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(* const-decl "Vector" vectors_3D "vectors/")
(+ const-decl "Vector" vectors_3D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "Vector" vectors_3D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(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)
(delay_conflict_free_rel formula-decl nil delay_3D nil))
shostak)))
¤ Dauer der Verarbeitung: 0.29 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.
|
