Quelle  bubblesort.prf   Sprache: Lisp

(bubblesort
 (epsilon_lem_TCC1 0
  (epsilon_lem_TCC1-1 nil 3271516179 ("" (subtype-tcc) nil nil)
   ((below type-eq-decl nil naturalnumbers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (<= formal-const-decl "(total_order?[T])" bubblesort nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil bubblesort nil)
    (N formal-const-decl "posnat" bubblesort 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)
    (sorted? const-decl "bool" sort_array nil))
   shostak))
 (epsilon_lem_TCC2 0
  (epsilon_lem_TCC2-1 nil 3271516180 ("" (existence-tcc) nil nil)
   ((below type-eq-decl nil naturalnumbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (<= formal-const-decl "(total_order?[T])" bubblesort nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil bubblesort nil)
    (N formal-const-decl "posnat" bubblesort 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)
    (sorted? const-decl "bool" sort_array nil))
   shostak))
 (epsilon_lem 0
  (epsilon_lem-1 nil 3271515427
   ("" (skosimp*)
    (("" (use "epsilon_ax[below(N)]")
      (("1" (split -)
        (("1" (replace -2 :dir rl :hide? t) (("1" (propax) nil nil))
          nil)
         ("2" (use "successive_inversion_exists")
          (("2" (assert) nil nil)) nil))
        nil)
       ("2" (hide-all-but 1)
        (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)
       ("3" (inst?) nil nil))
      nil))
    nil)
   ((TRUE const-decl "bool" booleans nil)
    (epsilon_ax formula-decl nil epsilons 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)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (N formal-const-decl "posnat" bubblesort nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= formal-const-decl "(total_order?[T])" bubblesort nil)
    (total_order? const-decl "bool" orders nil)
    (T formal-type-decl nil bubblesort nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (successive_inversion_exists formula-decl nil sort_inversions 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))
   shostak))
 (bubblesort_TCC1 0
  (bubblesort_TCC1-2 nil 3272301605
   ("" (skosimp*)
    (("" (use "epsilon_lem") (("" (assert) nil nil)) nil)) nil)
   ((epsilon_lem formula-decl nil bubblesort nil)
    (T formal-type-decl nil bubblesort nil)
    (below type-eq-decl nil naturalnumbers nil)
    (N formal-const-decl "posnat" bubblesort 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)
    (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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil)
  (bubblesort_TCC1-1 nil 3271184426 ("" (termination-tcc) nil nil)
   ((sorted? const-decl "bool" sort_array nil)) shostak))
 (bubblesort_TCC2 0
  (bubblesort_TCC2-2 nil 3272301630
   ("" (skosimp*)
    (("" (use "epsilon_lem")
      (("" (assert)
        (("" (flatten)
          (("" (use "card_inversions_transpose[N,T,<=]")
            (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((epsilon_lem formula-decl nil bubblesort nil)
    (T formal-type-decl nil bubblesort nil)
    (below type-eq-decl nil naturalnumbers nil)
    (N formal-const-decl "posnat" bubblesort 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)
    (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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (card_inversions_transpose formula-decl nil sort_inversions nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" bubblesort nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil)
  (bubblesort_TCC2-1 nil 3271514528 ("" (existence-tcc) nil nil)
   ((sorted? const-decl "bool" sort_array nil)) shostak))
 (sorted_bubblesort 0
  (sorted_bubblesort-1 nil 3271184528
   ("" (measure-induct+ "card(inversions(A))" ("A"))
    (("" (expand "bubblesort" 1 :assert? none)
      (("" (lift-if +)
        (("" (prop)
          ((""
            (name-replace "J"
             "epsilon! j: j < N - 1 & NOT x!1(j) <= x!1(j + 1)" :hide?
             nil)
            (("1" (assert)
              (("1" (use "epsilon_lem")
                (("1" (assert)
                  (("1" (flatten)
                    (("1" (hide -2)
                      (("1" (use "card_inversions_transpose")
                        (("1" (assert)
                          (("1" (inst?) (("1" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (inst + "0") (("2" (assert) nil nil)) nil)
             ("3" (hide-all-but 1)
              (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (O const-decl "T3" function_props nil)
    (bijective? const-decl "bool" functions nil)
    (permutation nonempty-type-eq-decl nil permutation nil)
    (transpose const-decl "permutation" permutation nil)
    (card_inversions_transpose formula-decl nil sort_inversions nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (epsilon_lem formula-decl nil bubblesort nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (epsilon const-decl "T" epsilons nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (TRUE const-decl "bool" booleans nil)
    (sorted? const-decl "bool" sort_array nil)
    (bubblesort def-decl "[below(N) -> T]" bubblesort nil)
    (wf_nat formula-decl nil naturalnumbers nil)
    (inversions const-decl "finite_set[index_pair]" sort_inversions
     nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (index_pair type-eq-decl nil sort_inversions nil)
    (<= formal-const-decl "(total_order?[T])" bubblesort nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil bubblesort nil)
    (below type-eq-decl nil naturalnumbers nil)
    (N formal-const-decl "posnat" bubblesort 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)
    (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)
    (measure_induction formula-decl nil measure_induction nil)
    (well_founded? const-decl "bool" orders nil))
   shostak)))