| products/sources/formale Sprachen/PVS/TRS/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: GAMCSDUP.jcl Sprache: JCLOriginal von: PVS© |
|
||||||
|
(positions
(positionsOF_TCC1 0 (positionsOF_TCC1-1 nil 3388744728 ("" (subtype-tcc) nil nil) nil nil)) (positionsOF_TCC2 0 (positionsOF_TCC2-1 nil 3389723936 ("" (grind) nil 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) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (variable formal-nonempty-type-decl nil positions nil) (symbol formal-nonempty-type-decl nil positions 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (term type-decl nil term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (<< adt-def-decl "(strict_well_founded?[term])" term_adt nil) (subterm adt-def-decl "boolean" term_adt nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (position type-eq-decl nil positions nil) (<= const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil)) (left_without_children_TCC1 0 (left_without_children_TCC1-1 nil 3511797058 ("" (skosimp) (("" (rewrite empty_0) nil nil)) nil) ((empty_0 formula-decl nil seq_extras "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil)) nil)) (left_without_children_TCC2 0 (left_without_children_TCC2-1 nil 3511797058 ("" (skosimp) (("" (rewrite empty_0) nil nil)) nil) ((empty_0 formula-decl nil seq_extras "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil)) nil)) (positions_of_terms_finite 0 (positions_of_terms_finite-1 nil 3415310384 ("" (induct "t") (("1" (skosimp*) (("1" (expand* "positionsOF" "only_empty_seq") (("1" (case-replace "{x: position | x = empty_seq} = singleton(empty_seq)" :hide? T) (("1" (rewrite "finite_singleton") nil nil) ("2" (hide 2) (("2" (expand "singleton") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "positionsOF" 1) (("2" (prop) (("1" (expand "only_empty_seq") (("1" (case-replace "{x: position | x = empty_seq} = singleton(empty_seq)" :hide? T) (("1" (rewrite "finite_singleton") nil nil) ("2" (hide (-1 -2 2)) (("2" (expand "singleton") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_sets[position].finite_union") (("2" (inst?) (("1" (hide 3) (("1" (expand "finseq_appl") (("1" (lemma "IUnion_of_finite_is_finite") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (inst -1 "i!1 - 1") (("1" (expand "is_finite") (("1" (skolem-typepred) (("1" (inst?) (("1" (inst 1 "LAMBDA (x: (catenate(i!1, positionsOF(app2_var!1`seq(i!1 - 1))))): f!1(rest(x)) (("1" (expand "injective?") (("1" (skolem-typepred) (("1" (expand "catenate") (("1" (skosimp*) (("1" (expand "member") (("1" (replaces -2) (("1" (replaces -3) (("1" (rewrite "rest_add_first") (("1" (rewrite "rest_add_first") (("1" (inst -5 "x!1" "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem-typepred) (("2" (expand "catenate") (("2" (skosimp*) (("2" (expand "member") (("2" (replaces -2) (("2" (rewrite "rest_add_first") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2 3)) (("2" (expand "only_empty_seq") (("2" (case-replace "{x: position | x = empty_seq} = singleton(empty_seq)" :hide? T) (("1" (rewrite "finite_singleton") nil nil) ("2" (hide 2) (("2" (expand "singleton") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (finite_set type-eq-decl nil finite_sets nil) (<= const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (IUnion const-decl "set[T]" indexed_sets nil) (catenate const-decl "positions" positions nil) (< const-decl "bool" reals nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (app2_var!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(app1_var!1)}" positions nil) (app1_var!1 skolem-const-decl "symbol" positions nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (i!1 skolem-const-decl "upto?[position](length(app2_var!1))" positions nil) (rest const-decl "finseq" seq_extras "structures/") (rest_add_first formula-decl nil seq_extras "structures/") (member const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (IUnion_of_finite_is_finite formula-decl nil IUnion_extra nil) (finite_union judgement-tcc nil finite_sets nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (empty_seq const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[position]" positions nil) (finite_singleton judgement-tcc nil finite_sets nil) (only_empty_seq const-decl "positions" positions nil) (term_induction formula-decl nil term_adt nil) (variable formal-nonempty-type-decl nil positions nil) (symbol formal-nonempty-type-decl nil positions nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (term type-decl nil term_adt nil)) shostak)) (empty_pos 0 (empty_pos-1 nil 3390055503 ("" (skeep) (("" (expand "<=") (("" (skolem * "p1") (("" (replaces -1) (("" (expand* "o" "empty_seq") (("" (flatten) (("" (apply-extensionality) (("" (hide 2) (("" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" positions nil) (< const-decl "bool" reals nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (FALSE const-decl "bool" booleans nil) (pred type-eq-decl nil defined_types nil) (epsilon const-decl "T" epsilons nil) (TRUE const-decl "bool" booleans nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (O const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil)) shostak)) (closed_positions 0 (closed_positions-1 nil 3388746243 ("" (measure-induct+ "length(q)" "q") (("" (skeep) (("" (expand "positionsOF" (-2 1)) (("" (lift-if) (("" (prop) (("1" (hide (-1 -2 -4)) (("1" (expand "only_empty_seq") (("1" (lemma "empty_pos") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2 -4 2 3)) (("2" (expand "only_empty_seq") (("2" (lemma "empty_pos") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand* "union" "member" "only_empty_seq") (("3" (prop) (("1" (hide-all-but (-1 -3 2)) (("1" (lemma "empty_pos") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "IUnion") (("2" (skolem * "i1") (("2" (expand "catenate" -1) (("2" (skolem * "q1") (("2" (flatten) (("2" (expand "member") (("2" (inst -3 "q1") (("2" (expand "<=" -4) (("2" (skolem * "p1") (("2" (inst -3 "rest(p)" "args(t)(i1 - 1)") (("2" (prop) (("1" (inst 3 "i1") (("1" (expand "catenate") (("1" (inst 3 "rest(p)") (("1" (expand "member") (("1" (assert) (("1" (hide-all-but (-3 -4 2 3)) (("1" (lemma "fsepn.seq_first_rest") (("1" (inst -1 "p") (("1" (prop) (("1" (replaces -1 -3) (("1" (lemma "fsepn.add_first_compo") (("1" (inst -1 "rest(p)" "p1" "first(p)") (("1" (replaces -1 -3) (("1" (replaces -1) (("1" (lemma "fsepn.first_equal") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (replaces -1) (("1" (lemma "fsepn.seq_first_rest") (("1" (inst -1 "p") (("1" (assert) (("1" (prop) (("1" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "empty_0") (("2" (hide-all-but (-2 -3 1 3)) (("2" (expand "<=") (("2" (inst 1 "p1") (("2" (lemma "fsepn.seq_first_rest") (("2" (inst -1 "p") (("2" (prop) (("1" (replaces -1 -3) (("1" (rewrite "fsepn.add_first_compo") (("1" (replaces -1 -2) (("1" (lemma "fsepn.first_equal") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-2 -3 1 3)) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (catenate const-decl "positions" positions nil) (first const-decl "T" seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (/= const-decl "boolean" notequal nil) (O const-decl "finseq" finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/") (first_equal formula-decl nil seq_extras "structures/") (add_first_compo formula-decl nil seq_extras "structures/") (seq_first_rest formula-decl nil seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (insert? const-decl "finseq" seq_extras "structures/") (add_first const-decl "finseq" seq_extras "structures/") (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) (finseq type-eq-decl nil finite_sequences nil) (rest const-decl "finseq" seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (empty_pos formula-decl nil positions nil) (only_empty_seq const-decl "positions" positions nil) (<= const-decl "bool" positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-decl nil positions nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (equal_symbol_equal_length_arg 0 (equal_symbol_equal_length_arg-1 nil 3496152694 ("" (skosimp*) (("" (grind) nil nil)) nil) nil shostak)) (not_var 0 (not_var-1 nil 3388757591 ("" (skeep) (("" (grind) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (add_first const-decl "finseq" seq_extras "structures/") (insert? const-decl "finseq" seq_extras "structures/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (positionsOF def-decl "positions" positions nil) (empty_seq const-decl "finseq" finite_sequences nil) (only_empty_seq const-decl "positions" positions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (not_var1 0 (not_var1-1 nil 3496151134 ("" (skosimp) (("" (grind) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (add_last const-decl "finseq" seq_extras "structures/") (insert? const-decl "finseq" seq_extras "structures/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (positionsOF def-decl "positions" positions nil) (empty_seq const-decl "finseq" finite_sequences nil) (only_empty_seq const-decl "positions" positions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (pos_ax 0 (pos_ax-1 nil 3388757621 ("" (lemma "closed_positions") (("" (assert) (("" (expand "<=") (("" (skosimp) (("" (inst -1 p!1 "p!1 o q!1" t!1) (("" (assert) (("" (inst 1 q!1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-decl nil positions nil) (O const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" positions nil) (closed_positions formula-decl nil positions nil)) shostak)) (rest_of_positions_TCC1 0 (rest_of_positions_TCC1-1 nil 3411856776 ("" (skosimp*) (("" (lemma "not_var") (("" (inst -1 "first(p!1)" "p!1" "rest(p!1)" "s!1") (("1" (assert) (("1" (lemma "fsepn.seq_first_rest") (("1" (inst?) (("1" (assert) (("1" (expand "positionsOF") (("1" (prop) (("1" (expand "only_empty_seq") (("1" (rewrite "empty_0") nil nil)) nil) ("2" (expand* "union" "member") (("2" (prop) (("1" (expand "only_empty_seq") (("1" (rewrite "empty_0") nil nil)) nil) ("2" (expand "IUnion") (("2" (skosimp*) (("2" (expand "catenate") (("2" (skosimp*) (("2" (expand "member") (("2" (expand "finseq_appl") (("2" (replace -3 -2) (("2" (lemma "fsepn.first_equal") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((not_var formula-decl nil positions nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (positionsOF def-decl "positions" positions nil) (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (catenate const-decl "positions" positions nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (<= const-decl "bool" reals nil) (first_equal formula-decl nil seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (only_empty_seq const-decl "positions" positions nil) (empty_0 formula-decl nil seq_extras "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (seq_first_rest formula-decl nil seq_extras "structures/") (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-decl nil positions nil) (rest const-decl "finseq" seq_extras "structures/") (first const-decl "T" seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (p!1 skolem-const-decl "position" positions nil)) nil)) (rest_of_positions_TCC2 0 (rest_of_positions_TCC2-1 nil 3411856776 ("" (skosimp*) (("" (expand "positionsOF") (("" (grind) nil nil)) nil)) nil) ((positionsOF def-decl "positions" positions nil) (empty_seq const-decl "finseq" finite_sequences nil) (only_empty_seq const-decl "positions" positions nil)) nil)) (rest_of_positions 0 (rest_of_positions-1 nil 3411856777 ("" (skeep) (("" (expand "positionsOF" -1) (("" (lift-if) (("" (prop) (("1" (expand "only_empty_seq") (("1" (rewrite "empty_0") nil nil)) nil) ("2" (expand "only_empty_seq") (("2" (rewrite "empty_0") nil nil)) nil) ("3" (expand "only_empty_seq") (("3" (expand* "union" "member") (("3" (prop) (("1" (rewrite "empty_0") nil nil) ("2" (expand "IUnion") (("2" (skolem * "i1") (("2" (expand "catenate") (("2" (skolem * "y1") (("2" (expand "member") (("2" (flatten) (("2" (lemma "fsepn.seq_first_rest") (("2" (inst?) (("2" (assert) (("2" (replaces -1 -3) (("2" (lemma "fsepn.first_equal") (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((positionsOF def-decl "positions" positions nil) (empty_0 formula-decl nil seq_extras "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (only_empty_seq const-decl "positions" positions nil) (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (catenate const-decl "positions" positions nil) (seq_first_rest formula-decl nil seq_extras "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (first_equal formula-decl nil seq_extras "structures/") (upto? nonempty-type-eq-decl nil IUnion_extra nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-decl nil positions nil) (<= const-decl "bool" reals nil) (first const-decl "T" seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (/= const-decl "boolean" notequal nil) (rest const-decl "finseq" seq_extras "structures/")) shostak)) (delete_is_position_TCC1 0 (delete_is_position_TCC1-1 nil 3495982353 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (delete_is_position 0 (delete_is_position-1 nil 3495982633 ("" (skosimp*) (("" (lemma "fsepn.add_last_delete") (("" (inst?) (("" (assert) (("" (lemma "fsepn.add_last_delete_is_o") (("" (inst?) (("" (assert) (("" (expand "finseq_appl") (("" (replaces -1 -2) (("" (replaces -1 -2) (("" (lemma "pos_ax") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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 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) (add_last_delete formula-decl nil seq_extras "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (delete const-decl "finseq" seq_extras "structures/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (finite_sequence type-eq-decl nil finite_sequences nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (variable formal-nonempty-type-decl nil positions nil) (symbol formal-nonempty-type-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (term type-decl nil term_adt nil) (pos_ax formula-decl nil positions nil) (add_last_delete_is_o formula-decl nil seq_extras "structures/") (position type-eq-decl nil positions nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (parallel_comm 0 (parallel_comm-1 nil 3394367640 ("" (skeep) (("" (expand* "parallel" "<=") (("" (prop) nil nil)) nil)) nil) ((<= const-decl "bool" positions nil) (parallel const-decl "bool" positions nil)) shostak)) (rest_parallel 0 (rest_parallel-1 nil 3394301450 ("" (skeep) (("" (lemma "fsepn.seq_first_rest") (("" (copy -1) (("" (inst -1 "p") (("" (inst -2 "q") (("" (assert) (("" (expand "parallel") (("" (expand "<=") (("" (skosimp*) (("" (assert) (("" (prop) (("1" (skosimp*) (("1" (replace -2 3) (("1" (replace -3 3) (("1" (inst 3 "p1!1") (("1" (replaces -1) (("1" (replaces -4) (("1" (replaces -3) (("1" (rewrite "add_first_compo") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -2 4) (("2" (replace -3 4) (("2" (inst 3 "p1!1") (("2" (inst 4 "p1!1") (("2" (replaces -4) (("2" (replaces -1) (("2" (rewrite "add_first_compo") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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 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) (seq_first_rest formula-decl nil seq_extras "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (<= const-decl "bool" positions nil) (add_first_compo formula-decl nil seq_extras "structures/") (rest const-decl "finseq" seq_extras "structures/") (/= const-decl "boolean" notequal nil) (not_empty_seq type-eq-decl nil seq_extras "structures/") (first const-decl "T" seq_extras "structures/") (parallel const-decl "bool" positions nil)) shostak)) (rest_of_PP_is_PP 0 (rest_of_PP_is_PP-1 nil 3411908006 ("" (skolem-typepred) (("" (expand "PP?") (("" (prop) (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (inst -1 "i!1 + 1" "j!1 + 1") (("1" (assert) (("1" (expand "finseq_appl") (("1" (lemma "fspos.rest_pos") (("1" (inst?) (("1" (lemma "fspos.rest_pos") (("1" (inst?) (("1" (assert) (("1" (inst -1 "i!1") (("1" (inst -2 "j!1") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "i!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rest_pos formula-decl nil seq_extras "structures/") (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (j!1 skolem-const-decl "below[length(rest(fss!1))]" positions nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (fss!1 skolem-const-decl "PP" positions nil) (i!1 skolem-const-decl "below[length(rest(fss!1))]" positions nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (rest const-decl "finseq" seq_extras "structures/") (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences 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) (PP type-eq-decl nil positions nil) (PP? const-decl "bool" positions nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (rest_of_SP_is_SP 0 (rest_of_SP_is_SP-1 nil 3411908172 ("" (skolem-typepred) (("" (expand "SP?") (("" (case "length(rest(fss!1)) = 0") (("1" (hide -2) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (inst -1 "i!1 + 1") (("1" (lemma "fspos.rest_pos") (("1" (inst?) (("1" (prop) (("1" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil) ("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rest_pos formula-decl nil seq_extras "structures/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" positions nil) (fss!1 skolem-const-decl "SP(s!1)" positions nil) (i!1 skolem-const-decl "below[length(rest(fss!1))]" positions nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (rest const-decl "finseq" seq_extras "structures/") (SP type-eq-decl nil positions nil) (SP? const-decl "bool" positions nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions 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) (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) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (delete_of_PP_is_PP 0 (delete_of_PP_is_PP-1 nil 3411908236 ("" (skolem 1 ("fss" "_")) (("" (case "length(fss) = 0") (("1" (grind) nil nil) ("2" (skolem-typepred) (("2" (typepred "fss") (("2" (expand "PP?") (("2" (prop) (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (case "i!2 < i!1") (("1" (case "j!1 < i!1") (("1" (expand "delete" 3) (("1" (assert) (("1" (expand "finseq_appl") (("1" (inst -3 "i!2" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "delete" 4) (("2" (assert) (("2" (expand "finseq_appl") (("2" (inst -2 "i!2" "j!1 + 1") (("1" (assert) nil nil) ("2" (typepred "j!1") (("2" (hide (3 5)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1 < i!1") (("1" (expand "delete" 4) (("1" (assert) (("1" (expand "finseq_appl") (("1" (inst -2 "i!2 + 1" "j!1") (("1" (assert) nil nil) ("2" (hide (3 5)) (("2" (typepred "i!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "delete" 5) (("2" (assert) (("2" (expand "finseq_appl") (("2" (inst -1 "i!2 + 1" "j!1 + 1") (("1" (assert) nil nil) ("2" (hide (4 6)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.337 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 |
