| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/digraphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 19 kB |
|
Quelle reduce_walks.prf Sprache: Lisp |
|||||||||
|
(reduce_walks
(reduce_TCC1 0 (reduce_TCC1-1 nil 3253624247 ("" (subtype-tcc) nil nil) nil nil)) (reduce_TCC2 0 (reduce_TCC2-1 nil 3253624247 ("" (subtype-tcc) nil nil) nil nil)) (reduce_TCC3 0 (reduce_TCC3-1 nil 3253624247 ("" (subtype-tcc) nil nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil)) (reduce_TCC4 0 (reduce_TCC4-1 nil 3253624247 ("" (subtype-tcc) nil nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil)) (reduce_TCC5 0 (reduce_TCC5-1 nil 3253624247 ("" (skosimp*) (("" (expand "finseq_appl") (("" (typepred "w!1") (("" (expand "walk?") (("" (expand "finseq_appl") (("" (flatten) (("" (split +) (("1" (hide -3) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (ground) (("1" (inst?) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lift-if) (("2" (typepred "k!1") (("2" (lift-if) (("2" (ground) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (case-replace "k!1=n!1+1") (("1" (assert) (("1" (replace -10) (("1" (hide -10) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (verts_in? const-decl "bool" walks nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil reduce_walks nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (edgetype type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (walk? const-decl "bool" walks nil) (Walk type-eq-decl nil walks nil) (Long_walk type-eq-decl nil reduce_walks nil)) nil)) (reduce_TCC6 0 (reduce_TCC6-1 nil 3254570698 ("" (skosimp*) (("" (typepred "w!1") (("" (assert) (("" (expand "walk?") (("" (expand "finseq_appl") (("" (prop) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (ground) (("1" (inst?) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lift-if) (("2" (ground) (("1" (lift-if) (("1" (ground) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (case-replace "k!1 = n!1+1") (("1" (assert) (("1" (replace -8) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Long_walk type-eq-decl nil reduce_walks nil) (Walk type-eq-decl nil walks nil) (walk? const-decl "bool" walks nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (edgetype type-eq-decl nil digraphs nil) (prewalk type-eq-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil reduce_walks nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (verts_in? const-decl "bool" walks nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (reduce_lem_TCC1 0 (reduce_lem_TCC1-1 nil 3253624247 ("" (subtype-tcc) nil nil) nil nil)) (reduce_lem_TCC2 0 (reduce_lem_TCC2-1 nil 3253624247 ("" (subtype-tcc) nil nil) nil nil)) (reduce_lem_TCC3 0 (reduce_lem_TCC3-1 nil 3253624247 ("" (subtype-tcc) nil nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil)) (reduce_lem_TCC4 0 (reduce_lem_TCC4-1 nil 3559414012 ("" (subtype-tcc) nil nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil)) (reduce_lem 0 (reduce_lem-1 nil 3253624247 ("" (skosimp*) (("" (expand "o ") (("" (expand "^") (("" (expand "min") (("" (auto-rewrite "finseq_appl") (("" (typepred "k!1") (("" (typepred w!1) (("" (assert) (("" (expand reduce) (("" (lift-if) (("" (prop) (("1" (decompose-equality) (("1" (lift-if) (("1" (prop) (("1" (expand empty_seq) (("1" (assert) nil nil)) nil) ("2" (expand empty_seq) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (decompose-equality) (("1" (skosimp*) (("1" (expand ^) (("1" (expand min) (("1" (prop) (("1" (lift-if) (("1" (expand empty_seq) (("1" (assert) nil nil)) nil)) nil) ("2" (expand empty_seq) (("2" (lift-if) (("2" (assert) (("2" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred n!1) (("2" (expand ^) (("2" (expand min) (("2" (expand empty_seq) (("2" (lift-if) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 2) (("3" (typepred n!1) (("3" (expand ^) (("3" (expand min) (("3" (expand empty_seq) (("3" (lift-if) (("3" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (expand* ^ min empty_seq) (("3" (lift-if) (("3" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) nil nil) ("5" (assert) nil nil) ("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (typepred n!1) (("4" (expand* ^ min empty_seq) (("4" (lift-if) (("4" (prop) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (typepred n!1) (("5" (expand* ^ min empty_seq) (("5" (lift-if) (("5" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) nil nil) ("5" (assert) nil nil) ("6" (assert) nil nil) ("7" (assert) nil nil) ("8" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (typepred n!1) (("6" (expand* ^ min empty_seq) (("6" (lift-if) (("6" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((O const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (Walk type-eq-decl nil walks nil) (walk? const-decl "bool" walks nil) (digraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (edgetype type-eq-decl nil digraphs nil) (prewalk type-eq-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil reduce_walks nil) (below type-eq-decl nil nat_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (> const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (G!1 skolem-const-decl "digraph[T]" reduce_walks nil) (w!1 skolem-const-decl "Walk[T](G!1)" reduce_walks nil) (k!1 skolem-const-decl "{n: nat | n > 0 AND n < length(w!1) - 1}" reduce_walks nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (empty_seq const-decl "finseq" finite_sequences nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (below type-eq-decl nil naturalnumbers nil) (reduce const-decl "Walk(G)" reduce_walks nil) (^ const-decl "finseq" finite_sequences nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil))) ¤ Dauer der Verarbeitung: 0.5 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28