Quelle robinsonunification.prf Sprache: Lisp

(robinsonunification
(IMP_unification_TCC1 0
  (IMP_unification_TCC1-1 nil 3467989055
   ("" (lemma var_countable) (("" (propax) nil nil)) nil)
   ((var_countable formula-decl nil robinsonunification nil)) nil))
(xx_TCC1 0
  (xx_TCC1-1 nil 3468765193
   ("" (lemma var_nonempty)
    (("" (expand* nonempty? empty?)
      (("" (skosimp*)
        (("" (inst 1 x!1)
          (("" (assert)
            (("" (expand member) (("" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (variable formal-nonempty-type-decl nil robinsonunification nil)
    (symbol formal-nonempty-type-decl nil robinsonunification 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]" robinsonunification nil)
    (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
    (V const-decl "set[term]" variables_term nil)
    (x!1 skolem-const-decl "term[variable, symbol, arity]"
     robinsonunification nil)
    (member const-decl "bool" sets nil)
    (var_nonempty formula-decl nil robinsonunification nil))
   nil))
(ff_TCC1 0
  (ff_TCC1-1 nil 3474208611
   ("" (lemma symbol_nonempty)
    (("" (expand* nonempty? empty?)
      (("" (skosimp)
        (("" (expand member) (("" (inst 1 x!1) nil nil)) nil)) nil))
      nil))
    nil)
   ((empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (x!1 skolem-const-decl "symbol" robinsonunification nil)
    (arity formal-const-decl "[symbol -> nat]" robinsonunification 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (symbol formal-nonempty-type-decl nil robinsonunification nil)
    (symbol_nonempty formula-decl nil robinsonunification nil))
   nil))
(fail_TCC1 0
  (fail_TCC1-1 nil 3467989055
   ("" (typepred ff) (("" (assert) (("" (grind) nil nil)) nil)) nil)
   ((term type-decl nil term_adt nil)
    (variable formal-nonempty-type-decl nil robinsonunification nil)
    (|#| const-decl "finite_sequence[T]" set2seq "structures/")
    (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)
    (symbol formal-nonempty-type-decl nil robinsonunification 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]" robinsonunification nil)
    (ff const-decl "{f: symbol | arity(f) = 1}" robinsonunification
     nil))
   nil))
(fail_TCC2 0
  (fail_TCC2-1 nil 3474208611
   ("" (expand Sub?)
    ((""
      (case-replace "Dom((id[(V)]
                       WITH [xx
                               := app[variable, symbol, arity]
                                      (ff,
                                        #[term[variable, symbol, arity]]
                                       (xx))])) = singleton(xx)")
      (("1" (hide -1) (("1" (rewrite finite_singleton) nil nil)) nil)
       ("2" (hide 2)
        (("2" (decompose-equality)
          (("2" (iff)
            (("2" (prop)
              (("1" (expand singleton)
                (("1" (expand Dom)
                  (("1" (flatten)
                    (("1" (expand id) (("1" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (expand* singleton Dom)
                (("2" (flatten)
                  (("2" (grind)
                    (("2" (replaces -1)
                      (("2" (typepred xx)
                        (("2" (expand V) (("2" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty_singleton_finite application-judgement
     "non_empty_finite_set" robinsonunification nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[term]" robinsonunification nil)
    (variable formal-nonempty-type-decl nil robinsonunification nil)
    (symbol formal-nonempty-type-decl nil robinsonunification 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]" robinsonunification nil)
    (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
    (V const-decl "set[term]" variables_term nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Dom const-decl "set[(V)]" substitution nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (below type-eq-decl nil nat_types nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
    (app adt-constructor-decl
     "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] ->
   (app?)]" term_adt nil)
    (ff const-decl "{f: symbol | arity(f) = 1}" robinsonunification
     nil)
    (|#| const-decl "finite_sequence[T]" set2seq "structures/")
    (xx const-decl "(V)" robinsonunification nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (finite_singleton judgement-tcc nil finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (Sub? const-decl "bool" substitution nil))
   nil))
(first_diff_TCC1 0
  (first_diff_TCC1-1 nil 3467989055
   ("" (skosimp*)
    (("" (lemma "positions_of_arg")
      (("" (inst -1 "s!1" "k!1")
        (("1" (typepred "k!1")
          (("1" (typepred st!1)
            (("1" (typepred stp!1)
              (("1" (replace -4 1) (("1" (assert) nil nil)) nil)) nil))
            nil))
          nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((arity formal-const-decl "[symbol -> nat]" robinsonunification 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 robinsonunification nil)
    (variable formal-nonempty-type-decl nil robinsonunification nil)
    (positions_of_arg formula-decl nil positions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (fp!1 skolem-const-decl "symbol" robinsonunification nil)
    (stp!1 skolem-const-decl
     "{args: finite_sequence[term[variable, symbol, arity]] |
         args`length = arity(fp!1)}" robinsonunification nil)
    (k!1 skolem-const-decl "below[length(stp!1)]" robinsonunification
     nil)
    (s!1 skolem-const-decl "term[variable, symbol, arity]"
     robinsonunification 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)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
    (term type-decl nil term_adt nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(first_diff_TCC2 0
  (first_diff_TCC2-1 nil 3467989055
   ("" (skosimp*)
    (("" (lemma "positions_of_arg")
      (("" (inst -1 "t!1" "k!1")
        (("1" (typepred st!1)
          (("1" (typepred stp!1)
            (("1" (replace -5 1) (("1" (assert) nil nil)) nil)) nil))
          nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((arity formal-const-decl "[symbol -> nat]" robinsonunification 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 robinsonunification nil)
    (variable formal-nonempty-type-decl nil robinsonunification nil)
    (positions_of_arg formula-decl nil positions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (fp!1 skolem-const-decl "symbol" robinsonunification nil)
    (stp!1 skolem-const-decl
     "{args: finite_sequence[term[variable, symbol, arity]] |
         args`length = arity(fp!1)}" robinsonunification nil)
    (k!1 skolem-const-decl "below[length(stp!1)]" robinsonunification
     nil)
    (s!1 skolem-const-decl "term[variable, symbol, arity]"
     robinsonunification nil)
    (t!1 skolem-const-decl "{t: term | s!1 /= t}" robinsonunification
     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)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (/= const-decl "boolean" notequal nil)
    (app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
    (term type-decl nil term_adt nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(first_diff_TCC3 0
  (first_diff_TCC3-1 nil 3467989055
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
(first_diff_TCC4 0
  (first_diff_TCC4-1 nil 3467989055
   ("" (skosimp*)
    (("" (expand "<<")
      (("" (lift-if)
        (("" (prop)
          (("1" (hide-all-but (-1 -2)) (("1" (assert) nil nil)) nil)
           ("2" (inst 2 k!1)
            (("1" (assert) (("1" (grind) nil nil)) nil)
             ("2" (replace -1 1) (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((<< adt-def-decl "(strict_well_founded?[term])" term_adt nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers 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)
    (nat_min application-judgement "{k: nat | 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)
    (subterm adt-def-decl "boolean" term_adt nil)
    (subtermOF def-decl "term" subterm nil)
    (rest const-decl "finseq" seq_extras "structures/")
    (^ const-decl "finseq" finite_sequences nil)
    (empty_seq const-decl "finseq" finite_sequences nil)
    (first const-decl "T" seq_extras "structures/")
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (|#| const-decl "finite_sequence[T]" set2seq "structures/")
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" 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)
    (below type-eq-decl nil nat_types nil)
    (variable formal-nonempty-type-decl nil robinsonunification nil)
    (symbol formal-nonempty-type-decl nil robinsonunification nil)
    (arity formal-const-decl "[symbol -> nat]" robinsonunification nil)
    (term type-decl nil term_adt nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (fp!1 skolem-const-decl "symbol" robinsonunification nil)
    (stp!1 skolem-const-decl
     "{args: finite_sequence[term[variable, symbol, arity]] |
         args`length = arity(fp!1)}" robinsonunification nil)
    (k!1 skolem-const-decl "below[length(stp!1)]" robinsonunification
     nil)
    (app? adt-recognizer-decl "[term -> boolean]" term_adt 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)
    (s!1 skolem-const-decl "term[variable, symbol, arity]"
     robinsonunification nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(first_diff_TCC5 0
  (first_diff_TCC5-1 nil 3468147562
   ("" (skosimp*)
    (("" (lemma "positions_of_arg")
      (("" (inst -1 "s!1" "kk!1")
        (("1" (replace -1 1) (("1" (assert) nil nil)) nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((arity formal-const-decl "[symbol -> nat]" robinsonunification 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 robinsonunification nil)
    (variable formal-nonempty-type-decl nil robinsonunification nil)
    (positions_of_arg formula-decl nil positions nil)
    (fp!1 skolem-const-decl "symbol" robinsonunification nil)
    (stp!1 skolem-const-decl
     "{args: finite_sequence[term[variable, symbol, arity]] |
         args`length = arity(fp!1)}" robinsonunification nil)
    (kk!1 skolem-const-decl "below[length(stp!1)]" robinsonunification
     nil)
    (s!1 skolem-const-decl "term[variable, symbol, arity]"
     robinsonunification 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)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
    (term type-decl nil term_adt nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(first_diff_TCC6 0
  (first_diff_TCC6-1 nil 3516387399
   ("" (skosimp*)
    (("" (lemma "positions_of_arg")
      (("" (inst -1 "t!1" "kk!1")
        (("1" (typepred "kk!1")
          (("1" (replace -4 1) (("1" (assert) nil nil)) nil)) nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((arity formal-const-decl "[symbol -> nat]" robinsonunification 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 robinsonunification nil)
    (variable formal-nonempty-type-decl nil robinsonunification nil)
    (positions_of_arg formula-decl nil positions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (fp!1 skolem-const-decl "symbol" robinsonunification nil)
    (stp!1 skolem-const-decl
     "{args: finite_sequence[term[variable, symbol, arity]] |
         args`length = arity(fp!1)}" robinsonunification nil)
    (kk!1 skolem-const-decl "below[length(stp!1)]" robinsonunification
     nil)
    (s!1 skolem-const-decl "term[variable, symbol, arity]"
     robinsonunification nil)
    (t!1 skolem-const-decl "{t: term | s!1 /= t}" robinsonunification
     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)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (/= const-decl "boolean" notequal nil)
    (app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
    (term type-decl nil term_adt nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(first_diff_TCC7 0
  (first_diff_TCC7-1 nil 3516387399
   ("" (skosimp*)
    (("" (case "st!1 = stp!1")
      (("1" (hide +) (("1" (grind) nil nil)) nil)
       ("2" (decompose-equality 1)
        (("2" (decompose-equality 1)
          (("2" (typepred x!1)
            (("2" (expand* "nonempty?" "empty?")
              (("2" (inst -5 "x!1")
                (("2" (expand "member")
                  (("2" (replace -2 -5)
                    (("2" (replace -4 -5)
                      (("2" (assert)
                        (("2" (expand subtermOF)
                          (("2" (lift-if)
                            (("2" (assert) (("2" (grind) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((= const-decl "[T, T -> boolean]" equalities nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (term type-decl nil term_adt nil)
    (arity formal-const-decl "[symbol -> nat]" robinsonunification 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 robinsonunification nil)
    (variable formal-nonempty-type-decl nil robinsonunification nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (< const-decl "bool" reals nil) (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (subtermOF def-decl "term" subterm 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 "finite_sequence[T]" set2seq "structures/")
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (first const-decl "T" seq_extras "structures/")
    (empty_seq const-decl "finseq" finite_sequences nil)
    (^ const-decl "finseq" finite_sequences nil)
    (rest const-decl "finseq" seq_extras "structures/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nat_min application-judgement "{k: nat | k <= i AND k <= j}"
     real_defs nil)
    (int_min application-judgement "{k: int | k <= i AND k <= j}"
     real_defs 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)
    (NOT const-decl "[bool -> bool]" booleans nil))
   nil))
(comutative_first_diff_TCC1 0
  (comutative_first_diff_TCC1-1 nil 3468654719
   ("" (skosimp) (("" (typepred "t!1") (("" (assert) nil nil)) nil))
    nil)
   ((/= const-decl "boolean" notequal nil)
    (term type-decl nil term_adt nil)
    (arity formal-const-decl "[symbol -> nat]" robinsonunification 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 robinsonunification nil)
    (variable formal-nonempty-type-decl nil robinsonunification nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(comutative_first_diff 0
  (comutative_first_diff-1 nil 3468654726
   ("" (measure-induct+ "length(p)" "p")
    (("" (skosimp)
      (("" (expand "first_diff" -2)
        (("" (lift-if)
          (("" (assert)
            ((""
              (name-replace "k!11"
               "min({kk: below[length(args(t!1))] | NOT
                    subtermOF(s!1,  #(1 + kk)) = subtermOF (t!1,  #(1 + kk))})"
               :hide? nil)
              (("1" (name-replace "k!1" "1 + k!11")
                (("1" (prop)
                  (("1" (hide -3 -4)
                    (("1" (expand "first_diff" 1)
                      (("1" (assert)
                        (("1" (lift-if) (("1" (prop) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide -3 -4)
                    (("2" (expand "first_diff")
                      (("2" (assert)
                        (("2" (lift-if)
                          (("2" (prop)
                            (("2" (reveal -1) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("3" (assert)
                    (("3" (hide -4)
                      (("3" (expand "first_diff" 3)
                        (("3" (propax) nil nil)) nil))
                      nil))
                    nil)
                   ("4"
                    (inst -4 "first_diff(subtermOF(s!1, #(k!1)),
                                              subtermOF(t!1,  #(k!1)))")
                    (("4"
                      (inst -4 "subtermOF(s!1, #(k!1))"
                       "subtermOF(t!1, #(k!1))")
                      (("4" (prop)
                        (("1" (expand "first_diff" 4)
                          (("1" (assert)
                            (("1"
                              (name-replace "k!22"
                               "min({kk: below[length(args(s!1))] | NOT
                                     subtermOF(t!1,  #(1 + kk)) = subtermOF(s!1,  #(1 + kk))})"
                               :hide? nil)
                              (("1"
                                (name-replace "k!2" "1 + k!22")
                                (("1"
                                  (reveal -4 -1)
                                  (("1"
                                    (replace -3 -1 rl)
                                    (("1"
                                      (replace -7 -2 rl)
                                      (("1"
                                        (hide (-3 -7))
                                        (("1"
                                          (case "k!1 = k!2")
                                          (("1"
                                            (replaces -1)
                                            (("1" (assert) nil nil))
                                            nil)
                                           ("2"
                                            (case
                                             "length(args(s!1))=length(args(t!1))")
                                            (("1"
                                              (replace -1)
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (replace -2 1 rl)
                                                  (("1"
                                                    (replace -3 1 rl)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (name-replace
                                                         "myset"
                                                         " min({kk: below[length(args(s!1))] |
                                                        NOT subtermOF(t!1,  #(1 + kk)) = subtermOF(s!1,  #(1 + kk))})"
                                                         :hide?
                                                         nil)
                                                        (("1"
                                                          (rewrite
                                                           min_def)
                                                          (("1"
                                                            (rewrite
                                                             min_def)
                                                            (("1"
                                                              (hide-all-but
                                                               (-1 1))
                                                              (("1"
                                                                (expand
                                                                 minimum?)
                                                                (("1"
                                                                  (skosimp*)
                                                                  (("1"
                                                                    (inst
                                                                     -1
                                                                     x!2)
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (hide-all-but
                                                               (1
                                                                3
                                                                4
                                                                5))
                                                              (("2"
                                                                (lemma
                                                                 first_diff_TCC7)
                                                                (("2"
                                                                  (inst
                                                                   -1
                                                                   "s!1"
                                                                   "t!1"
                                                                   "f(s!1)"
                                                                   "args(s!1)")
                                                                  (("2"
                                                                    (case
                                                                     "s!1 = app(f(s!1), args(s!1))")
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (hide
                                                                         -1)
                                                                        (("1"
                                                                          (inst
                                                                           -1
                                                                           "f(t!1)"
                                                                           "args(t!1)")
                                                                          (("1"
                                                                            (case
                                                                             "t!1 = app(f(t!1), args(t!1))")
                                                                            (("1"
                                                                              (assert)
                                                                              nil
                                                                              nil)
                                                                             ("2"
                                                                              (hide-all-but
                                                                               (1
                                                                                3))
                                                                              (("2"
                                                                                (decompose-equality)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide-all-but
                                                                       (1
                                                                        5))
                                                                      (("2"
                                                                        (decompose-equality)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("3"
                                                              (hide-all-but
                                                               (-6
                                                                1
                                                                3
                                                                4
                                                                5))
                                                              (("3"
                                                                (skosimp*)
                                                                (("3"
                                                                  (lemma
                                                                   "positions_of_arg")
                                                                  (("3"
                                                                    (inst
                                                                     -1
                                                                     "t!1"
                                                                     "kk!1")
                                                                    (("3"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("4"
                                                              (hide
                                                               -
                                                               6)
                                                              (("4"
                                                                (skosimp*)
                                                                (("4"
                                                                  (lemma
                                                                   "positions_of_arg")
                                                                  (("4"
                                                                    (inst
                                                                     -1
                                                                     "s!1"
                                                                     "kk!1")
                                                                    (("4"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide-all-but
                                                             (-6
                                                              1
                                                              3
                                                              4
                                                              5))
                                                            (("2"
                                                              (lemma
                                                               first_diff_TCC7)
                                                              (("2"
                                                                (inst
                                                                 -1
                                                                 "t!1"
                                                                 "s!1"
                                                                 "f(t!1)"
                                                                 "args(t!1)")
                                                                (("2"
                                                                  (case
                                                                   "t!1 = app(f(t!1), args(t!1))")
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (hide
                                                                       -1)
                                                                      (("1"
                                                                        (inst
                                                                         -1
                                                                         "f(s!1)"
                                                                         "args(s!1)")
                                                                        (("1"
                                                                          (case
                                                                           "s!1 = app(f(s!1), args(s!1))")
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil)
                                                                           ("2"
                                                                            (hide-all-but
                                                                             (1
                                                                              5))
                                                                            (("2"
                                                                              (decompose-equality)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (hide-all-but
                                                                     (1
                                                                      3))
                                                                    (("2"
                                                                      (decompose-equality)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("3"
                                                            (hide-all-but
                                                             (-6
                                                              1
                                                              3
                                                              4
                                                              5))
                                                            (("3"
                                                              (skosimp*)
                                                              (("3"
                                                                (lemma
                                                                 "positions_of_arg")
                                                                (("3"
                                                                  (inst
                                                                   -1
                                                                   "s!1"
                                                                   "kk!1")
                                                                  (("3"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("4"
                                                            (hide - 6)
                                                            (("4"
                                                              (skosimp*)
                                                              (("4"
                                                                (lemma
                                                                 "positions_of_arg")
                                                                (("4"
                                                                  (inst
                                                                   -1
                                                                   "t!1"
                                                                   "kk!1")
                                                                  (("4"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (hide-all-but
                                                           (-5
                                                            1
                                                            3
                                                            4
                                                            5))
                                                          (("2"
                                                            (lemma
                                                             first_diff_TCC7)
                                                            (("2"
                                                              (inst
                                                               -1
                                                               "t!1"
                                                               "s!1"
                                                               "f(t!1)"
                                                               "args(t!1)")
                                                              (("2"
                                                                (case
                                                                 "t!1 = app(f(t!1), args(t!1))")
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (hide
                                                                     -1)
                                                                    (("1"
                                                                      (inst
                                                                       -1
                                                                       "f(s!1)"
                                                                       "args(s!1)")
                                                                      (("1"
                                                                        (case
                                                                         "s!1 = app(f(s!1), args(s!1))")
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil)
                                                                         ("2"
                                                                          (hide-all-but
                                                                           (1
                                                                            5))
                                                                          (("2"
                                                                            (decompose-equality)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide-all-but
                                                                   (1
                                                                    3))
                                                                  (("2"
                                                                    (decompose-equality)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("3"
                                                          (hide
                                                           -
                                                           (2 6))
                                                          (("3"
                                                            (skosimp*)
                                                            (("3"
                                                              (lemma
                                                               "positions_of_arg")
                                                              (("3"
                                                                (inst
                                                                 -1
                                                                 "s!1"
                                                                 "kk!1")
                                                                (("3"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("4"
                                                          (hide
                                                           -
                                                           (2 6))
                                                          (("4"
                                                            (skosimp*)
                                                            (("4"
                                                              (lemma
                                                               "positions_of_arg")
                                                              (("4"
                                                                (inst
                                                                 -1
                                                                 "t!1"
                                                                 "kk!1")
                                                                (("4"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide-all-but (-4 1))
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide-all-but (-2 1 2 3 4))
                                (("2"
                                  (lemma first_diff_TCC7)
                                  (("2"
                                    (inst
                                     -1
                                     "t!1"
                                     "s!1"
                                     "f(t!1)"
                                     "args(t!1)")
                                    (("2"
                                      (case
                                       "t!1 = app(f(t!1), args(t!1))")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (hide -1)
                                          (("1"
                                            (inst
                                             -1
                                             "f(s!1)"
                                             "args(s!1)")
                                            (("1"
                                              (case
                                               "s!1 = app(f(s!1), args(s!1))")
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (hide-all-but (1 5))
                                                (("2"
                                                  (decompose-equality)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide-all-but (1 3))
                                        (("2"
                                          (decompose-equality)
                                          nil
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("3"
                                (hide-all-but (-2 1 2 3 4))
                                (("3"
                                  (skosimp*)
                                  (("3"
                                    (lemma "positions_of_arg")
                                    (("3"
                                      (inst -1 "s!1" "kk!1")
                                      (("3" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("4"
                                (hide - 5)
                                (("4"
                                  (skosimp*)
                                  (("4"
                                    (lemma "positions_of_arg")
                                    (("4"
                                      (inst -1 "t!1" "kk!1")
                                      (("4" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide-all-but (-2 1))
                          (("2" (expand* "add_first" "insert?")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("5" (hide -2 -3)
                    (("5" (expand "first_diff")
                      (("5" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (prop)
                (("1" (hide -3 1)
                  (("1" (expand "first_diff")
                    (("1" (assert)
                      (("1" (lift-if) (("1" (prop) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide -3 2)
                  (("2" (expand "first_diff")
                    (("2" (assert)
                      (("2" (lift-if)
                        (("2" (prop) (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("3" (hide -3 3)
                  (("3" (expand "first_diff") (("3" (assert) nil nil))
                    nil))
                  nil)
                 ("4" (hide - 5)
                  (("4" (lemma "first_diff_TCC7")
                    (("4" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)")
                      (("4" (case "s!1 = app(f(s!1), args(s!1))")
                        (("1" (assert)
                          (("1" (hide -1)
                            (("1" (inst -1 "f(t!1)" "args(t!1)")
                              (("1"
                                (case "t!1 = app(f(t!1), args(t!1))")
                                (("1"
                                  (assert)
                                  (("1"
                                    (reveal -4)
                                    (("1" (propax) nil nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide-all-but (1 2))
                                  (("2" (decompose-equality) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide-all-but (1 4))
                          (("2" (decompose-equality) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("5" (hide -2 5)
                  (("5" (expand "first_diff") (("5" (assert) nil nil))
                    nil))
                  nil))
                nil)
               ("3" (prop)
                (("1" (hide -3 1)
                  (("1" (expand "first_diff")
                    (("1" (assert)
                      (("1" (lift-if) (("1" (prop) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide -3 2)
                  (("2" (expand "first_diff")
                    (("2" (lift-if)
                      (("2" (prop) (("2" (assert) nil nil)) nil)) nil))
                    nil))
                  nil)
                 ("3" (hide -3 3)
                  (("3" (expand "first_diff") (("3" (assert) nil nil))
                    nil))
                  nil)
                 ("4" (hide -2 -3 5)
                  (("4" (skosimp*)
                    (("4" (lemma "positions_of_arg")
                      (("4" (inst -1 "t!1" "kk!1")
                        (("4" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("5" (hide -)
                  (("5" (skosimp*)
                    (("5" (lemma "positions_of_arg")
                      (("5" (inst -1 "t!1" "kk!1")
                        (("5" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
--> --------------------

--> maximum size reached

--> --------------------

quality96%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.40Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.