| products/Sources/formale Sprachen/PVS/TRS/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: measure_completion_aux.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(robinsonunificationEF
(IMP_robinsonunification_TCC1 0 (IMP_robinsonunification_TCC1-1 nil 3522686037 ("" (lemma var_countable) (("" (propax) nil nil)) nil) ((var_countable formula-decl nil robinsonunificationEF nil)) nil)) (IMP_robinsonunification_TCC2 0 (IMP_robinsonunification_TCC2-1 nil 3522686037 ("" (lemma var_nonempty) (("" (propax) nil nil)) nil) ((var_nonempty formula-decl nil robinsonunificationEF nil)) nil)) (IMP_robinsonunification_TCC3 0 (IMP_robinsonunification_TCC3-1 nil 3522686037 ("" (lemma symbol_nonempty) (("" (propax) nil nil)) nil) ((symbol_nonempty formula-decl nil robinsonunificationEF nil)) nil)) (right_pos_TCC1 0 (right_pos_TCC1-1 nil 3506350454 ("" (skosimp) (("" (skosimp) (("" (assert) (("" (lemma empty_0[posnat]) (("" (inst -1 p!1) (("" (assert) 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) (empty_0 formula-decl nil seq_extras "structures/") (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (variable formal-nonempty-type-decl nil robinsonunificationEF 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) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (right_pos_TCC2 0 (right_pos_TCC2-1 nil 3506350454 ("" (skosimp*) (("" (lemma delete_is_position) (("" (inst -1 p!1 s!1) (("" (assert) (("" (flatten) (("" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (variable formal-nonempty-type-decl nil robinsonunificationEF nil) (delete_is_position formula-decl nil positions nil) (int_minus_int_is_int application-judgement "int" integers nil) (finseq type-eq-decl nil finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/") (term type-decl nil term_adt 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)) nil)) (right_pos_TCC3 0 (right_pos_TCC3-1 nil 3506350454 ("" (skosimp*) (("" (lemma subterm_is_app) (("" (inst -1 p!1 s!1) (("" (assert) (("" (flatten) (("" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (variable formal-nonempty-type-decl nil robinsonunificationEF nil) (subterm_is_app formula-decl nil subterm nil) (int_minus_int_is_int application-judgement "int" integers nil) (finseq type-eq-decl nil finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/") (term type-decl nil term_adt 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)) nil)) (right_pos_TCC4 0 (right_pos_TCC4-1 nil 3506350454 ("" (skosimp*) (("" (hide -1 -3 -4) (("" (replaces -1) (("" (expand delete 2) (("" (lemma empty_0[posnat]) (("" (inst -1 p!1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((delete const-decl "finseq" 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) (variable formal-nonempty-type-decl nil robinsonunificationEF nil) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (position type-eq-decl nil positions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (empty_0 formula-decl nil 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)) nil)) (right_pos_TCC5 0 (right_pos_TCC5-1 nil 3506350454 ("" (skosimp*) (("" (lemma positions_of_arg) (("" (inst -1 "subtermOF(s!1, p1!1)" "j!1 + i!1") (("1" (lemma pos_o_term) (("1" (inst -1 "p1!1" "#(j!1 + i!1 + 1)" "s!1") (("1" (lemma delete_is_position) (("1" (inst -1 p!1 s!1) (("1" (lemma empty_0[posnat]) (("1" (inst -1 p!1) (("1" (assert) (("1" (hide-all-but (-2 3)) (("1" (case "p1!1 o #(1 + i!1 + j!1) = add_last(p1!1, 1 + i!1 + j!1)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred j!1) (("2" (typepred "args(subtermOF(s!1, p1!1))") (("2" (replace -1 1) (("2" (replace -6 1 rl) (("2" (hide-all-but (-2 1)) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (variable formal-nonempty-type-decl nil robinsonunificationEF nil) (positions_of_arg formula-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (pos_o_term formula-decl nil subterm nil) (delete_is_position formula-decl nil positions nil) (empty_0 formula-decl nil seq_extras "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (O const-decl "finseq" finite_sequences nil) (add_last const-decl "finseq" seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (insert? const-decl "finseq" seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "nat" robinsonunificationEF nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (n!1 skolem-const-decl "nat" robinsonunificationEF nil) (below type-eq-decl nil naturalnumbers nil) (j!1 skolem-const-decl "below(n!1 - i!1)" robinsonunificationEF nil) (term type-decl nil term_adt nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (below type-eq-decl nil nat_types 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) (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) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions? type-eq-decl nil positions nil) (subtermOF def-decl "term" subterm nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" robinsonunificationEF nil) (p1!1 skolem-const-decl "position[variable, symbol, arity]" robinsonunificationEF nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (right_pos_TCC6 0 (right_pos_TCC6-1 nil 3506350454 ("" (skosimp*) (("" (lemma positions_of_arg) (("" (inst -1 "subtermOF(s!1, p1!1)" "j!1 + i!1") (("1" (lemma pos_o_term) (("1" (inst -1 "p1!1" "#(j!1 + i!1 + 1)" "s!1") (("1" (lemma delete_is_position) (("1" (inst -1 p!1 s!1) (("1" (lemma empty_0[posnat]) (("1" (inst -1 p!1) (("1" (assert) (("1" (hide-all-but (-2 3)) (("1" (case "p1!1 o #(1 + i!1 + j!1) = add_last(p1!1, 1 + i!1 + j!1)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred j!1) (("2" (typepred "args(subtermOF(s!1, p1!1))") (("2" (replace -1 1) (("2" (replace -6 1 rl) (("2" (hide-all-but (-2 1)) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (variable formal-nonempty-type-decl nil robinsonunificationEF nil) (positions_of_arg formula-decl nil positions nil) (delete_is_position formula-decl nil positions nil) (empty_0 formula-decl nil seq_extras "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (finseq type-eq-decl nil finite_sequences nil) (term type-decl nil term_adt 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) (pos_o_term formula-decl nil subterm nil)) nil)) (next_position_TCC1 0 (next_position_TCC1-1 nil 3488040223 ("" (skosimp) (("" (lemma empty_0[posnat]) (("" (inst -1 p!1) (("" (assert) 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) (empty_0 formula-decl nil seq_extras "structures/") (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) (positions type-eq-decl nil positions nil) (term type-decl nil term_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (variable formal-nonempty-type-decl nil robinsonunificationEF 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)) nil)) (next_position_TCC2 0 (next_position_TCC2-1 nil 3488040223 ("" (skosimp) (("" (rewrite delete_is_position) (("" (hide 3) (("" (flatten) (("" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil) ((delete_is_position formula-decl nil positions nil) (below type-eq-decl nil nat_types 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (variable formal-nonempty-type-decl nil robinsonunificationEF nil) (symbol formal-nonempty-type-decl nil robinsonunificationEF 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]" robinsonunificationEF nil) (int_minus_int_is_int application-judgement "int" integers nil) (finseq type-eq-decl nil finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/")) nil)) (next_position_TCC3 0 (next_position_TCC3-1 nil 3488040223 ("" (skosimp*) (("" (lemma "subterm_is_app") (("" (inst -1 p!1 s!1) (("" (assert) (("" (hide 3) (("" (flatten) (("" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (variable formal-nonempty-type-decl nil robinsonunificationEF nil) (subterm_is_app formula-decl nil subterm nil) (int_minus_int_is_int application-judgement "int" integers nil) (finseq type-eq-decl nil finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/") (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (term type-decl nil term_adt nil) (AND const-decl "[bool, bool -> 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) (below type-eq-decl nil nat_types nil)) nil)) (next_position_TCC4 0 (next_position_TCC4-1 nil 3488040223 ("" (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) (variable formal-nonempty-type-decl nil robinsonunificationEF nil) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (position type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" 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)) (next_position_TCC5 0 (next_position_TCC5-1 nil 3496419653 ("" (skosimp) (("" (name-replace "q!1" "delete(p!1, length(p!1) - 1)" :hide? nil) (("1" (lemma empty_0[posnat]) (("1" (inst -1 p!1) (("1" (assert) (("1" (typepred "args(subtermOF(s!1, q!1))") (("1" (replace -1 3 rl) (("1" (hide -1) (("1" (lemma add_last_delete[posnat]) (("1" (inst -1 p!1) (("1" (assert) (("1" (replace -2 -1) (("1" (lemma add_last_delete_is_o[posnat]) (("1" (inst -1 p!1) (("1" (assert) (("1" (expand finseq_appl) (("1" (replace -3 -1) (("1" (replace -2 -1 rl) (("1" (lemma pos_subterm_ax) (("1" (inst -1 "q!1" "#(p!1`seq(p!1`length - 1))" "s!1") (("1" (assert) (("1" (expand positionsOF -1) (("1" (lift-if) (("1" (ground) (("1" (hide-all-but -2) (("1" (grind) nil nil)) nil) ("2" (hide-all-but -2) (("2" (grind) nil nil)) nil) ("3" (expand* union IUnion member) (("3" (split) (("1" (hide-all-but -1) (("1" (grind) nil nil)) nil) ("2" (skosimp) (("2" (expand finseq_appl) (("2" (expand catenate) (("2" (skosimp) (("2" (expand member) (("2" (typepred i!1) (("2" (expand add_first) (("2" (expand insert?) (("2" (decompose-equality -4) (("2" (expand finseq_appl) (("2" (expand "#" -1) (("2" (expand "#" -2) (("2" (decompose-equality -2) (("2" (inst?) (("2" (case "p!1`seq(p!1`length - 1) = last(p!1)") (("1" (assert) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma empty_0[posnat]) (("2" (inst -1 p!1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types 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) (finseq type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (delete const-decl "finseq" seq_extras "structures/") (variable formal-nonempty-type-decl nil robinsonunificationEF nil) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (position type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences 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) (positions? type-eq-decl nil positions nil) (subtermOF def-decl "term" subterm nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (empty_seq const-decl "finseq" finite_sequences nil) (only_empty_seq const-decl "positions" positions nil) (<= const-decl "bool" reals nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (insert? const-decl "finseq" seq_extras "structures/") (last const-decl "T" seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (/= const-decl "boolean" notequal 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (add_first const-decl "finseq" seq_extras "structures/") (catenate const-decl "positions" positions nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (pos_subterm_ax formula-decl nil subterm nil) (add_last_delete_is_o formula-decl nil seq_extras "structures/") (add_last_delete formula-decl nil seq_extras "structures/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (empty_0 formula-decl nil seq_extras "structures/")) nil)) (next_position_TCC6 0 (next_position_TCC6-1 nil 3496419653 ("" (skosimp*) (("" (typepred "length(z!1`3)") (("" (case "length(z!1`3)=0") (("1" (rewrite "empty_0") nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> 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) (below type-eq-decl nil nat_types nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (variable formal-nonempty-type-decl nil robinsonunificationEF 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (empty_0 formula-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil)) nil)) (next_position_TCC7 0 (next_position_TCC7-1 nil 3496419653 ("" (skosimp) (("" (rewrite delete_is_position) (("" (hide 3) (("" (flatten) (("" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil) ((delete_is_position formula-decl nil positions nil) (below type-eq-decl nil nat_types 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) (term type-decl nil term_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (variable formal-nonempty-type-decl nil robinsonunificationEF nil) (symbol formal-nonempty-type-decl nil robinsonunificationEF 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]" robinsonunificationEF nil) (int_minus_int_is_int application-judgement "int" integers nil) (finseq type-eq-decl nil finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/")) nil)) (next_position_TCC8 0 (next_position_TCC8-1 nil 3496419653 ("" (skosimp*) (("" (lemma "subterm_is_app") (("" (inst?) (("" (assert) (("" (prop) (("" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (variable formal-nonempty-type-decl nil robinsonunificationEF nil) (subterm_is_app formula-decl nil subterm nil) (int_minus_int_is_int application-judgement "int" integers nil) (empty_0 formula-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt 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)) nil)) (next_position_TCC9 0 (next_position_TCC9-1 nil 3496419653 ("" (skosimp) (("" (name-replace "q!1" "delete(z!1`3, length(z!1`3) - 1)" :hide? nil) (("1" (lemma empty_0[posnat]) (("1" (inst -1 "z!1`3") (("1" (assert) (("1" (typepred "args(subtermOF(z!1`1, q!1))") (("1" (replace -1 3 rl) (("1" (hide -1) (("1" (lemma add_last_delete[posnat]) (("1" (inst -1 "z!1`3") (("1" (assert) (("1" (replace -2 -1) (("1" (lemma add_last_delete_is_o[posnat]) (("1" (inst -1 "z!1`3") (("1" (assert) (("1" (expand finseq_appl) (("1" (replace -3 -1) (("1" (replace -2 -1 rl) (("1" (lemma pos_subterm_ax) (("1" (inst -1 "q!1" "#(z!1`3`seq(z!1`3`length - 1))" "z!1`1") (("1" (assert) (("1" (expand positionsOF -1) (("1" (lift-if) (("1" (ground) (("1" (hide-all-but -2) (("1" (grind) nil nil)) nil) ("2" (hide-all-but -2) (("2" (grind) nil nil)) nil) ("3" (expand* union IUnion member) (("3" (split) (("1" (hide-all-but -1) (("1" (grind) nil nil)) nil) ("2" (skosimp) (("2" (expand finseq_appl) (("2" (expand catenate) (("2" (skosimp) (("2" (expand member) (("2" (typepred i!1) (("2" (expand add_first) (("2" (expand insert?) (("2" (decompose-equality -4) (("2" (expand finseq_appl) (("2" (expand "#" -1) (("2" (expand "#" -2) (("2" (decompose-equality -2) (("2" (inst?) (("2" (case "z!1`3`seq(z!1`3`length - 1) = last(z!1`3)") (("1" (assert) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma empty_0[posnat]) (("2" (inst -1 "z!1`3") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) 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) (int_minus_int_is_int application-judgement "int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types 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) (finseq type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (delete const-decl "finseq" seq_extras "structures/") (variable formal-nonempty-type-decl nil robinsonunificationEF nil) (symbol formal-nonempty-type-decl nil robinsonunificationEF nil) (arity formal-const-decl "[symbol -> nat]" robinsonunificationEF nil) (term type-decl nil term_adt nil) (position type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (empty_0 formula-decl nil seq_extras "structures/")) nil)) (next_position_TCC10 0 (next_position_TCC10-1 nil 3496419653 ("" (skosimp) (("" (name-replace "q!1" "delete(z!1`3, length(z!1`3) - 1)" :hide? nil) (("1" (lemma empty_0[posnat]) (("1" (inst -1 "z!1`3") (("1" (assert) (("1" (typepred "args(subtermOF(z!1`1, q!1))") (("1" (replace -1 3 rl) (("1" (hide -1) (("1" (lemma add_last_delete[posnat]) (("1" (inst -1 "z!1`3") (("1" (assert) (("1" (replace -2 -1) (("1" (lemma add_last_delete_is_o[posnat]) (("1" (inst -1 "z!1`3") (("1" (assert) (("1" (expand finseq_appl) (("1" (replace -3 -1) (("1" (replace -2 -1 rl) (("1" (lemma pos_subterm_ax) (("1" (inst -1 "q!1" "#(z!1`3`seq(z!1`3`length - 1))" "z!1`1") (("1" (assert) (("1" (expand positionsOF -1) (("1" (lift-if) (("1" (ground) (("1" (hide-all-but -2) (("1" (grind) nil nil)) nil) ("2" (hide-all-but -2) (("2" (grind) nil nil)) nil) ("3" (expand* union IUnion member) (("3" (split) (("1" (hide-all-but -1) (("1" (grind) nil nil)) nil) ("2" (skosimp) (("2" (expand finseq_appl) (("2" (expand catenate) (("2" (skosimp) (("2" (expand member) (("2" (typepred i!1) (("2" (expand add_first) (("2" (expand insert?) (("2" (decompose-equality -4) (("2" (expand finseq_appl) (("2" (expand "#" -1) (("2" (expand "#" -2) (("2" (decompose-equality -2) (("2" (inst?) (("2" (case "z!1`3`seq(z!1`3`length - 1) = last(z!1`3)") (("1" (assert) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.91 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 |
