| products/Sources/formale Sprachen/PVS/TRS/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: replace_positions.prf Sprache: UnknownOriginal von: PVS© |
|
||||||
|
(replace_positions
(IMP_substitution_TCC1 0 (IMP_substitution_TCC1-1 nil 3455272043 ("" (lemma "var_countable") (("" (propax) nil nil)) nil) ((var_countable formula-decl nil replace_positions nil)) nil)) (replace_pos_TCC1 0 (replace_pos_TCC1-1 nil 3455272043 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (variable formal-nonempty-type-decl nil replace_positions nil) (symbol formal-nonempty-type-decl nil replace_positions 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" replace_positions nil) (term type-decl nil term_adt 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) (finseq type-eq-decl nil finite_sequences nil) (SPP? const-decl "bool" positions nil) (SPP type-eq-decl nil positions nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (SP? const-decl "bool" positions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (replace_pos_TCC2 0 (replace_pos_TCC2-1 nil 3455272043 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (variable formal-nonempty-type-decl nil replace_positions nil) (symbol formal-nonempty-type-decl nil replace_positions 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" replace_positions nil) (term type-decl nil term_adt 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) (finseq type-eq-decl nil finite_sequences nil) (SPP? const-decl "bool" positions nil) (SPP type-eq-decl nil positions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (SP? const-decl "bool" positions nil) (< const-decl "bool" reals nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil)) (replace_pos_TCC3 0 (replace_pos_TCC3-1 nil 3455272043 ("" (skosimp*) (("" (typepred "fssp!1") (("" (expand "SPP?") (("" (flatten) (("" (split) (("1" (rewrite "rest_of_PP_is_PP") nil nil) ("2" (expand "SP?") (("2" (expand "PP?") (("2" (prop) (("1" (grind) nil nil) ("2" (skosimp*) (("2" (lemma "fspos.rest_pos") (("2" (inst?) (("2" (assert) (("2" (expand "finseq_appl") (("2" (inst -1 "i!1") (("1" (replace -1 2 rl) (("1" (hide -1) (("1" (copy -2) (("1" (inst -1 "0") (("1" (inst -3 "1 + i!1") (("1" (inst -2 "0" "1 + i!1") (("1" (assert) (("1" (lemma "replace_preserv_parallel_pos") (("1" (inst -1 "fssp!1`seq(0)" "fssp!1`seq(1 + i!1)" "s!1" "t!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) 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)) nil)) nil)) nil)) nil)) nil)) nil) ((SPP type-eq-decl nil positions nil) (SPP? 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]" replace_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 replace_positions nil) (variable formal-nonempty-type-decl nil replace_positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (SP? const-decl "bool" positions nil) (< const-decl "bool" reals nil) (rest const-decl "finseq" seq_extras "structures/") (^ const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (finseq_appl const-decl "[below[length(fs)] -> T]" 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) (rest_pos formula-decl nil seq_extras "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (i!1 skolem-const-decl "below[length(rest[position[variable, symbol, arity]](fssp!1))]" replace_positions nil) (fssp!1 skolem-const-decl "SPP[variable, symbol, arity](s!1)" replace_positions nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" replace_positions nil) (replace_preserv_parallel_pos formula-decl nil replacement nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (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) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (rest_of_PP_is_PP formula-decl nil positions nil) (PP? const-decl "bool" positions nil) (PP type-eq-decl nil positions nil)) nil)) (replace_pos_TCC4 0 (replace_pos_TCC4-1 nil 3455272043 ("" (termination-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (finseq type-eq-decl nil finite_sequences nil) (SPP? const-decl "bool" positions nil) (SPP type-eq-decl nil positions nil) (/= const-decl "boolean" notequal nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (O const-decl "finseq" finite_sequences nil) (<= const-decl "bool" positions nil) (parallel const-decl "bool" positions nil) (PP? const-decl "bool" positions nil) (SP? const-decl "bool" positions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty_seq const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" replace_positions nil) (symbol formal-nonempty-type-decl nil replace_positions nil) (variable formal-nonempty-type-decl nil replace_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) (rest const-decl "finseq" seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (replace_pos_is_stable_TCC1 0 (replace_pos_is_stable_TCC1-1 nil 3455272043 ("" (skosimp*) (("" (typepred "fss!1") (("" (expand "SPP?") (("" (flatten) (("" (assert) (("" (hide -1) (("" (expand "SP?") (("" (skosimp*) (("" (inst?) (("" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((SPP type-eq-decl nil positions nil) (SPP? 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]" replace_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 replace_positions nil) (variable formal-nonempty-type-decl nil replace_positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (ext_preserv_pos formula-decl nil substitution nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (< const-decl "bool" reals nil) (SP? const-decl "bool" positions nil)) nil)) (replace_pos_is_stable 0 (replace_pos_is_stable-1 nil 3455272189 ("" (measure-induct+ "length(fss)" ("s" "fss")) (("1" (skosimp*) (("1" (case "length(x!2) = 0") (("1" (hide -2) (("1" (expand "replace_pos") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "replace_pos" 2 1) (("2" (assert) (("2" (inst -1 "replaceTerm(x!1, t!1, x!2(0))" "rest(x!2)") (("2" (inst -1 "t!1" "sig!1") (("2" (rewrite "length_rest") (("2" (replaces -1) (("2" (rewrite "ext_replace_ext") (("1" (expand "replace_pos" 2 2) (("1" (propax) nil nil)) nil) ("2" (hide (2 3)) (("2" (typepred "x!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (hide -1) (("2" (expand "SP?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "y!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (assert) (("2" (hide -1) (("2" (expand "SP?") (("2" (skosimp*) (("2" (inst?) (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 2)) (("3" (skosimp*) (("3" (rewrite "replace_pos_is_stable_TCC1") nil nil)) nil)) nil) ("4" (hide (-1 2)) (("4" (skosimp*) (("4" (rewrite "replace_pos_is_stable_TCC1") nil nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (rewrite "replace_pos_is_stable_TCC1") nil nil)) nil) ("6" (hide (-1 2)) (("6" (skosimp*) (("6" (rewrite "replace_pos_is_stable_TCC1") nil nil)) nil)) nil) ("7" (hide 2) (("7" (rewrite "replace_pos_is_stable_TCC1") nil nil)) nil)) nil) ((replace_pos_is_stable_TCC1 subtype-tcc nil replace_positions nil) (ext_preserv_pos formula-decl nil substitution nil) (rest const-decl "finseq" seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (replaceTerm def-decl "term" replacement nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (length_rest formula-decl nil seq_extras "structures/") (ext_replace_ext formula-decl nil substitution nil) (NOT const-decl "[bool -> bool]" booleans nil) (SP? const-decl "bool" positions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (replace_pos def-decl "term" replace_positions nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (ext def-decl "term" substitution nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (SPP type-eq-decl nil positions nil) (SPP? 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]" replace_positions 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 replace_positions nil) (variable formal-nonempty-type-decl nil replace_positions 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)) (preserv_first_position_TCC1 0 (preserv_first_position_TCC1-1 nil 3455272043 ("" (skolem-typepred) (("" (skosimp*) (("" (expand "SPP?") (("" (flatten) (("" (split) (("1" (rewrite "add_first_parallel_pos_to_PP_is_PP") nil nil) ("2" (rewrite "add_first_parallel_pos_to_SP_is_SP") nil nil)) nil)) nil)) nil)) nil)) nil) ((add_first_parallel_pos_to_SP_is_SP formula-decl nil positions nil) (SP? const-decl "bool" positions nil) (SP type-eq-decl nil positions nil) (add_first_parallel_pos_to_PP_is_PP formula-decl nil positions nil) (PP? const-decl "bool" positions nil) (PP 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) (SPP type-eq-decl nil positions nil) (SPP? 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]" replace_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 replace_positions nil) (variable formal-nonempty-type-decl nil replace_positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (preserv_first_position 0 (preserv_first_position-1 nil 3455272317 ("" (measure-induct+ "length(fss)" ("s" "fss")) (("1" (skosimp*) (("1" (expand "replace_pos" 1) (("1" (prop) (("1" (hide-all-but -1) (("1" (expand* "add_first" "insert?") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "fspos.rest_add_first") (("2" (inst -1 "x!2" "q!1") (("2" (replaces -1) (("2" (lemma "fspos.nth_add_first") (("2" (inst -1 "x!2" "q!1" "0") (("1" (replace -1) (("1" (case "length(x!2) = 0") (("1" (hide -3) (("1" (expand "replace_pos") (("1" (prop) (("1" (hide-all-but 1) (("1" (lemma "replace_preserv_pos") (("1" (inst -1 "q!1" "x!1" "t!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "replace_pos" 3) (("2" (prop) (("2" (lemma "replace_commutativity") (("2" (inst -1 "q!1" "x!2(0)" "t!1" "x!1" "t!1") (("2" (typepred "q!1" "x!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (copy -3) (("2" (expand "SP?" -4) (("2" (inst -4 "0") (("2" (copy -8) (("2" (inst -9 "0") (("2" (assert) (("2" (rewrite "parallel_comm") (("2" (replace -6 2) (("2" (case "length(rest(x!2)) = 0") (("1" (hide-all-but (-1 -3 -4 -10 2 3)) (("1" (expand "replace_pos") (("1" (prop) (("1" (lemma "replace_preserv_parallel_pos") (("1" (inst -1 "x!2(0)" "q!1" "x!1" "t!1") (("1" (expand "SP?") (("1" (inst -4 "0") (("1" (assert) (("1" (lemma "replace_preserv_pos") (("1" (inst -1 "q!1" "replaceTerm(x!1, t!1, x!2(0))" "t!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -8 "replaceTerm(x!1, t!1, x!2(0))" "rest(x!2)") (("1" (inst -8 "t!1" "q!1") (("1" (prop) (("1" (expand "finseq_appl") (("1" (expand "replace_pos" -1) (("1" (prop) (("1" (hide-all-but -1) (("1" (grind) nil nil)) nil) ("2" (lemma "fspos.nth_add_first") (("2" (inst -1 "rest(x!2)" "q!1" "0") (("1" (replaces -1) (("1" (rewrite "rest_add_first") nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1 2 3)) (("2" (skosimp*) (("2" (inst -1 "i!1 + 1") (("1" (lemma "fspos.rest_pos") (("1" (expand "finseq_appl") (("1" (inst -1 "x!2") (("1" (assert) (("1" (inst -1 "i!1") (("1" (assert) nil nil) ("2" (typepred "i!1") (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 3)) (("3" (rewrite "length_rest") nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -4 1 2 3)) (("2" (expand "SPP?") (("2" (split) (("1" (rewrite "rest_of_PP_is_PP") nil nil) ("2" (copy -1) (("2" (expand "SP?") (("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (inst -2 "i!1 + 1") (("1" (lemma "fspos.rest_pos") (("1" (inst?) (("1" (assert) (("1" (inst -1 "i!1") (("1" (expand "PP?") (("1" (prop) (("1" (hide (-2 -3 -4 1)) (("1" (grind) nil nil)) nil) ("2" (expand "finseq_appl") (("2" (replace -2 2 rl) (("2" (inst -1 "0" "1 + i!1") (("2" (assert) (("2" (lemma "replace_preserv_parallel_pos") (("2" (inst -1 "x!2`seq(0)" "x!2`seq(1 + i!1)" "x!1" "t!1") (("2" (inst -4 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2 2)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) 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)) 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)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (typepred "y!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (split) (("1" (rewrite "add_first_parallel_pos_to_PP_is_PP") nil nil) ("2" (rewrite "add_first_parallel_pos_to_SP_is_SP") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 2) (("3" (skosimp*) (("3" (typepred "y!2") (("3" (expand "SPP?") (("3" (flatten) (("3" (split) (("1" (rewrite "add_first_parallel_pos_to_PP_is_PP") nil nil) ("2" (rewrite "add_first_parallel_pos_to_SP_is_SP") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide -1 2) (("4" (skosimp*) (("4" (typepred "x!1`2") (("4" (expand "SPP?") (("4" (flatten) (("4" (split) (("1" (rewrite "add_first_parallel_pos_to_PP_is_PP") nil nil) ("2" (rewrite "add_first_parallel_pos_to_SP_is_SP") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but (-1 1)) (("5" (typepred "y!1`2") (("5" (expand "SPP?") (("5" (flatten) (("5" (split) (("1" (rewrite "add_first_parallel_pos_to_PP_is_PP") nil nil) ("2" (rewrite "add_first_parallel_pos_to_SP_is_SP") nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide -1 2) (("6" (skosimp*) (("6" (typepred "y!1`2") (("6" (expand "SPP?") (("6" (flatten) (("6" (split) (("1" (rewrite "add_first_parallel_pos_to_PP_is_PP") nil nil) ("2" (rewrite "add_first_parallel_pos_to_SP_is_SP") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (hide 2) (("7" (typepred "fss!1") (("7" (expand "SPP?") (("7" (flatten) (("7" (split) (("1" (rewrite "add_first_parallel_pos_to_PP_is_PP") nil nil) ("2" (rewrite "add_first_parallel_pos_to_SP_is_SP") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((add_first_parallel_pos_to_PP_is_PP formula-decl nil positions nil) (add_first_parallel_pos_to_SP_is_SP formula-decl nil positions nil) (SP type-eq-decl nil positions nil) (insert? const-decl "finseq" seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nth_add_first formula-decl nil seq_extras "structures/") (replace_commutativity formula-decl nil replacement nil) (NOT const-decl "[bool -> bool]" booleans nil) (SP? const-decl "bool" positions nil) (t!1 skolem-const-decl "term[variable, symbol, arity]" replace_positions nil) (int_plus_int_is_int application-judgement "int" integers 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) (int_minus_int_is_int application-judgement "int" integers nil) (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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (rest_pos formula-decl nil seq_extras "structures/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (<= const-decl "bool" positions nil) (O const-decl "finseq" finite_sequences nil) (i!1 skolem-const-decl "below[length(rest(x!2))]" replace_positions nil) (length_rest formula-decl nil seq_extras "structures/") (i!1 skolem-const-decl "below[length(rest[position[variable, symbol, arity]](x!2))]" replace_positions nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (/= const-decl "boolean" notequal nil) (PP type-eq-decl nil positions nil) (PP? const-decl "bool" positions nil) (rest_of_PP_is_PP formula-decl nil positions nil) (replaceTerm def-decl "term" replacement nil) (replace_preserv_parallel_pos formula-decl nil replacement nil) (rest const-decl "finseq" seq_extras "structures/") (parallel_comm formula-decl nil positions nil) (replace_preserv_pos formula-decl nil replacement nil) (x!2 skolem-const-decl "SPP[variable, symbol, arity](x!1)" replace_positions nil) (x!1 skolem-const-decl "term[variable, symbol, arity]" replace_positions nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rest_add_first formula-decl nil seq_extras "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (replace_pos def-decl "term" replace_positions nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions? type-eq-decl nil positions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (parallel const-decl "bool" positions nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (add_first const-decl "finseq" seq_extras "structures/") (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (SPP type-eq-decl nil positions nil) (SPP? 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]" replace_positions 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 replace_positions nil) (variable formal-nonempty-type-decl nil replace_positions 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)) (preserv_all_parallel_positions 0 (preserv_all_parallel_positions-1 nil 3455272446 ("" (measure-induct+ "length(fss)" ("s" "fss")) (("" (skosimp*) (("" (case "length(x!2) = 0") (("1" (hide (-2 -3)) (("1" (typepred "q!1") (("1" (expand "replace_pos") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "replace_pos" 2) (("2" (assert) (("2" (inst -1 "replaceTerm(x!1, t!1, x!2(0))" "rest(x!2)") (("2" (inst -1 "t!1" "q!1") (("1" (rewrite "length_rest") (("1" (assert) (("1" (hide 3) (("1" (case "length(rest(x!2)) = 0") (("1" (hide -2) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (lemma "fspos.rest_pos") (("2" (expand "finseq_appl") (("2" (inst?) (("2" (assert) (("2" (inst -1 "i!1") (("1" (inst -2 "i!1 + 1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "i!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)) nil)) nil) ("2" (hide 3) (("2" (inst -1 "0") (("2" (typepred "q!1") (("2" (lemma "replace_preserv_parallel_pos") (("2" (inst -1 "x!2(0)" "q!1" "x!1" "t!1") (("2" (assert) (("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (expand "SP?") (("2" (inst -2 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rest const-decl "finseq" seq_extras "structures/") (replaceTerm def-decl "term" replacement nil) (SP? const-decl "bool" positions nil) (replace_preserv_parallel_pos formula-decl nil replacement nil) (length_rest formula-decl nil seq_extras "structures/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.79 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 |
