("sort_array_def" |sort_array_def| |sort_in?| "" (SKOSIMP*) (("" (LEMMA "sort_lem") (("" (INST?) (("" (FLATTEN) (("" (LEMMA "perm_in?") (("" (INST?) (("" (INST -1 "sort(A!1)") (("" (ASSERT) (("" (REPLACE -1) (("" (HIDE -1) (("" (GROUND) NIL)))))))))))))))))))))("sort_array_def" |sort_array_def| |sort_lem| "" (SKOSIMP*) (("" (TYPEPRED "sort(A!1)") (("" (ASSERT) NIL)))))("sort_array_def" |sort_array_def| |sort_TCC1| "" (INST 1 "(LAMBDA A: asort(A,N-1))") (("1" (SKOSIMP*) (("1" (REWRITE "asort_perm") (("1" (ASSERT) (("1" (LEMMA "asort_P_and_Q") (("1" (INST?) (("1" (EXPAND "is_increasing") (("1" (SKOSIMP*) (("1" (EXPAND "P") (("1" (INST?) (("1" (ASSERT) NIL))))))))))))))))))) ("2" (ASSERT) NIL)))("sort_array_def" |sort_array_def| |swap_TCC3| "" (SUBTYPE-TCC) NIL)("caret_arrays" |caret_arrays| |caret_elim_TCC3| "" (SUBTYPE-TCC) NIL)("array_ops" |array_ops| |array_decomp_TCC7| "" (SUBTYPE-TCC) NIL)("array_ops" |array_ops| |array_decomp_TCC6| "" (SUBTYPE-TCC) NIL)("majority_seq" |majority_seq| |Maj_TCC2| "" (SKOSIMP*) (("" (POSTPONE) NIL)))("majority_seq" |majority_seq| |Maj_TCC1| "" (SKOSIMP*) (("" (REWRITE "maj_in_seq") (("" (LEMMA "maj_lem") (("" (INST?) (("" (ASSERT) NIL)))))))))("majority_seq" |majority_seq| |seqset_TCC1| "" (SKOSIMP*) (("" (EXPAND "is_finite") (("" (INST 1 "length(fs!1)" "(LAMBDA (x: {x: T | in_seq(x, fs!1)}):
			       choose({i: below(length(fs!1)) |
                                         seq(fs!1)(i) = x}))") (("1" (EXPAND "injective?") (("1" (SKOSIMP*) (("1" (ASSERT) NIL))))) ("2" (SKOSIMP*) (("2" (TYPEPRED "x!1") (("2" (EXPAND "in_seq") (("2" (EXPAND "nonempty?") (("2" (EXPAND "empty?") (("2" (SKOSIMP*) (("2" (INST -2 "i!1") (("2" (EXPAND "member") (("2" (PROPAX) NIL)))))))))))))))))))))))("sort_seq" |sort_seq| |increasing?_TCC2| "" (SUBTYPE-TCC) NIL)("min_array_def" |min_array_def| IMPORTING2_TCC1 "" (REWRITE "ge_total") NIL)("sort_array" |sort_array| (|sort_TCC1| "" (INST 1 "(LAMBDA A: asort(A,N-1))") (("1" (SKOSIMP*) (("1" (REWRITE "asort_perm") (("1" (ASSERT) (("1" (LEMMA "asort_P_and_Q") (("1" (INST?) (("1" (EXPAND "sorted?") (("1" (SKOSIMP*) (("1" (EXPAND "P") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) (|sort_lem| "" (SKOSIMP*) (("" (TYPEPRED "sort(A!1)") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sort_in?| "" (SKOSIMP*) (("" (LEMMA "sort_lem") (("" (INST?) (("" (FLATTEN) (("" (LEMMA "perm_in?") (("" (INST?) (("" (INST -1 "sort(A!1)") (("" (ASSERT) (("" (REPLACE -1) (("" (HIDE -1) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sort_map_TCC1| "" (INST + "(LAMBDA (A: [below(N) -> T]):
      		choose({map: [below(N) -> below(N)] |
                             bijective?[below(N), below(N)](map) AND
                                  FORALL i: A(i) = sort(A)(map(i))}))") (("" (SKOSIMP*) (("" (EXPAND "nonempty?") (("" (EXPAND "empty?") (("" (EXPAND "member") (("" (LEMMA "sort_lem") (("" (INST?) (("" (FLATTEN) (("" (EXPAND "permutation_of?") (("" (SKOSIMP*) (("" (INST -4 "f!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sort_map_def| "" (SKOSIMP*) (("" (ASSERT) (("" (TYPEPRED "sort_map(A!1)") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|sort_map_bij| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|isort_map_TCC1| "" (INST + "(LAMBDA (A: [below(N) -> T]):
         		choose({map: [below(N) -> below(N)] |
                            bijective?[below(N), below(N)](map) AND
                               FORALL i: A(map(i)) = sort(A)(i)}))") (("" (SKOSIMP*) (("" (EXPAND "nonempty?") (("" (EXPAND "empty?") (("" (EXPAND "member") (("" (LEMMA "sort_lem") (("" (INST?) (("" (FLATTEN) (("" (EXPAND "permutation_of?") (("" (SKOSIMP*) (("" (INST -4 "inverse(f!1)") (("1" (PROP) (("1" (LEMMA "bij_inv_is_bij[below(N), below(N)]") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "0") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST -2 "inverse(f!1)(i!1)") (("1" (ASSERT) (("1" (EXPAND "bijective?") (("1" (FLATTEN) (("1" (LEMMA "comp_inverse_right_surj[below(N),below(N)]") (("1" (INST -1 "i!1" "f!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "0") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "0") NIL NIL)) NIL)) NIL)) NIL) ("2" (INST + "0") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|isort_map_def| "" (SKOSIMP*) (("" (ASSERT) (("" (TYPEPRED "isort_map(A!1)") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|isort_map_bij| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL))