Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: derivatives_def.pvs   Sprache: PVS

Untersuchungsergebnis.summary Download desMT940 {MT940[670] Hlasm[1084] Haskell[1492]}zum Wurzelverzeichnis wechseln

*** 
*** top (16:7:44 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
*** 
 Proof summary for theory top
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory const_fun_def
    image_const...........................proved - complete   [shostak](0.09 s)
    inverse_image_const...................proved - complete   [shostak](0.02 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.11 s)

 Proof summary for theory function_image_bis
    image_emptyset........................proved - complete   [shostak](0.01 s)
    inverse_image_emptyset................proved - complete   [shostak](0.02 s)
    surjective_image_inverse_image........proved - complete   [shostak](0.03 s)
    injective_inverse_image_image.........proved - complete   [shostak](0.02 s)
    bijective_image_iff_inverse_image.....proved - complete   [shostak](0.01 s)
    bijective_image_inverse_alt_TCC1......proved - complete   [shostak](0.01 s)
    bijective_image_inverse_alt...........proved - complete   [shostak](0.09 s)
    Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.19 s)

 Proof summary for theory function_inverse_alt_aux
    inverse_inverse_alt_TCC1..............proved - complete   [shostak](0.00 s)
    inverse_inverse_alt_TCC2..............proved - complete   [shostak](0.01 s)
    inverse_inverse_alt...................proved - complete   [shostak](0.06 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.08 s)

 Proof summary for theory function_props_aux
    inverse_image_composition.............proved - complete   [shostak](0.02 s)
    composition_inverse_alt_TCC1..........proved - complete   [shostak](0.01 s)
    composition_inverse_alt_TCC2..........proved - complete   [shostak](0.00 s)
    composition_inverse_alt_TCC3..........proved - complete   [shostak](0.01 s)
    composition_inverse_alt...............proved - complete   [shostak](0.08 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.13 s)

 Proof summary for theory top_array
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory min_array
    imin_TCC1.............................proved - complete   [shostak](0.12 s)
    min_TCC1..............................proved - complete   [shostak](0.01 s)
    min_lem...............................proved - complete   [shostak](0.01 s)
    min_in?...............................proved - complete   [shostak](0.01 s)
    min_def...............................proved - complete   [shostak](0.03 s)
    min_it_is.............................proved - complete   [shostak](0.02 s)
    imin_lem..............................proved - complete   [shostak](0.03 s)
    imin_1................................proved - complete   [shostak](0.00 s)
    min_2_TCC1............................proved - complete   [shostak](0.01 s)
    min_2_TCC2............................proved - complete   [shostak](0.00 s)
    min_2.................................proved - complete   [shostak](0.04 s)
    Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.29 s)

 Proof summary for theory min_array_def
    ge_total..............................proved - complete   [shostak](0.03 s)
    IMP_max_array_def_TCC1................proved - complete   [shostak](0.00 s)
    Imin_TCC1.............................proved - complete   [shostak](0.00 s)
    Imin_TCC2.............................proved - complete   [shostak](0.10 s)
    Imin_1_TCC1...........................proved - complete   [shostak](0.00 s)
    Imin_1................................proved - complete   [shostak](0.02 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.15 s)

 Proof summary for theory below_arrays
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory max_array_def
    imax_rec_TCC1.........................proved - complete   [shostak](0.01 s)
    imax_rec_TCC2.........................proved - complete   [shostak](0.00 s)
    imax_rec_lem..........................proved - complete   [shostak](0.15 s)
    imax_rec_rng..........................proved - complete   [shostak](0.08 s)
    Imax_rec_TCC1.........................proved - complete   [shostak](0.01 s)
    Imax_rec_TCC2.........................proved - complete   [shostak](0.01 s)
    Imax_TCC1.............................proved - complete   [shostak](0.00 s)
    Imax_TCC2.............................proved - complete   [shostak](0.03 s)
    Imax_1_TCC1...........................proved - complete   [shostak](0.01 s)
    Imax_1................................proved - complete   [shostak](0.01 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.32 s)

 Proof summary for theory max_array
    imax_TCC1.............................proved - complete   [shostak](0.03 s)
    max_TCC1..............................proved - complete   [shostak](0.01 s)
    max_lem...............................proved - complete   [shostak](0.01 s)
    max_in?...............................proved - complete   [shostak](0.01 s)
    imax_lem..............................proved - complete   [shostak](0.02 s)
    max_def...............................proved - complete   [shostak](0.02 s)
    max_it_is.............................proved - complete   [shostak](0.02 s)
    imax_1................................proved - complete   [shostak](0.01 s)
    max_2_TCC1............................proved - complete   [shostak](0.00 s)
    max_2_TCC2............................proved - complete   [shostak](0.00 s)
    max_2.................................proved - complete   [shostak](0.04 s)
    Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.19 s)

 Proof summary for theory permutations
    perm_reflexive........................proved - complete   [shostak](0.03 s)
    perm_symmetric........................proved - complete   [shostak](0.06 s)
    perm_tran.............................proved - complete   [shostak](0.07 s)
    perm_in?..............................proved - complete   [shostak](0.03 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.19 s)

 Proof summary for theory sort_array
    sort_TCC1.............................proved - complete   [shostak](0.06 s)
    sort_lem..............................proved - complete   [shostak](0.00 s)
    sort_in?..............................proved - complete   [shostak](0.01 s)
    sort_map_TCC1.........................proved - complete   [shostak](0.03 s)
    sort_map_def..........................proved - complete   [shostak](0.00 s)
    sort_map_bij..........................proved - complete   [shostak](0.00 s)
    isort_map_TCC1........................proved - complete   [shostak](0.08 s)
    isort_map_def.........................proved - complete   [shostak](0.00 s)
    isort_map_bij.........................proved - complete   [shostak](0.00 s)
    Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.18 s)

 Proof summary for theory sort_array_def
    swap_TCC1.............................proved - complete   [shostak](0.01 s)
    swap_TCC2.............................proved - complete   [shostak](0.02 s)
    asort_TCC1............................proved - complete   [shostak](0.01 s)
    asort_TCC2............................proved - complete   [shostak](0.00 s)
    swap_perm.............................proved - complete   [shostak](0.24 s)
    asort_perm............................proved - complete   [shostak](0.06 s)
    swap_P_and_Q_TCC1.....................proved - complete   [shostak](0.02 s)
    swap_P_and_Q..........................proved - complete   [shostak](0.33 s)
    asort_P_and_Q.........................proved - complete   [shostak](0.18 s)
    Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.88 s)

 Proof summary for theory sort_array_lems
    sort_min_TCC1.........................proved - complete   [shostak](0.00 s)
    sort_min..............................proved - complete   [shostak](0.07 s)
    sort_max_TCC1.........................proved - complete   [shostak](0.01 s)
    sort_max..............................proved - complete   [shostak](0.07 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.14 s)

 Proof summary for theory array_ops
    caret_fill0_TCC1......................proved - complete   [shostak](0.04 s)
    caret_fill0_TCC2......................proved - complete   [shostak](0.05 s)
    caret_fill0...........................proved - complete   [shostak](0.17 s)
    caret_fill1...........................proved - complete   [shostak](0.17 s)
    caret_concat_bot_TCC1.................proved - complete   [shostak](0.00 s)
    caret_concat_bot......................proved - complete   [shostak](1.03 s)
    caret_concat_top_TCC1.................proved - complete   [shostak](0.02 s)
    caret_concat_top_TCC2.................proved - complete   [shostak](0.05 s)
    caret_concat_top_TCC3.................proved - complete   [shostak](0.05 s)
    caret_concat_top_TCC4.................proved - complete   [shostak](0.06 s)
    caret_concat_top......................proved - complete   [shostak](0.34 s)
    caret_concat_all_TCC1.................proved - complete   [shostak](0.00 s)
    caret_concat_all_TCC2.................proved - complete   [shostak](0.01 s)
    caret_concat_all_TCC3.................proved - complete   [shostak](0.00 s)
    caret_concat_all_TCC4.................proved - complete   [shostak](0.02 s)
    caret_concat_all_TCC5.................proved - complete   [shostak](0.01 s)
    caret_concat_all_TCC6.................proved - complete   [shostak](0.00 s)
    caret_concat_all......................proved - complete   [shostak](0.12 s)
    array_decomp_TCC1.....................proved - complete   [shostak](0.00 s)
    array_decomp_TCC2.....................proved - complete   [shostak](0.00 s)
    array_decomp_TCC3.....................proved - complete   [shostak](0.01 s)
    array_decomp_TCC4.....................proved - complete   [shostak](0.01 s)
    array_decomp..........................proved - complete   [shostak](0.22 s)
    caret_bot_all_TCC1....................proved - complete   [shostak](0.00 s)
    caret_bot_all_TCC2....................proved - complete   [shostak](0.00 s)
    caret_bot_all.........................proved - complete   [shostak](0.18 s)
    caret_top_all_TCC1....................proved - complete   [shostak](0.04 s)
    caret_top_all_TCC2....................proved - complete   [shostak](0.05 s)
    caret_top_all.........................proved - complete   [shostak](0.26 s)
    concat_array_bot_TCC1.................proved - complete   [shostak](0.01 s)
    concat_array_bot......................proved - complete   [shostak](0.01 s)
    concat_array_top_TCC1.................proved - complete   [shostak](0.01 s)
    concat_array_top_TCC2.................proved - complete   [shostak](0.00 s)
    concat_array_top......................proved - complete   [shostak](0.06 s)
    concat_array_r........................proved - complete   [shostak](0.02 s)
    concat_array_l........................proved - complete   [shostak](0.02 s)
    concat_array_assoc....................proved - complete   [shostak](0.13 s)
    Theory totals: 37 formulas, 37 attempted, 37 succeeded (3.19 s)

 Proof summary for theory caret_arrays
    caret_TCC1............................proved - complete   [shostak](0.02 s)
    caret_TCC2............................proved - complete   [shostak](0.04 s)
    caret_TCC3............................proved - complete   [shostak](0.03 s)
    caret_TCC4............................proved - complete   [shostak](0.06 s)
    caret_TCC5............................proved - complete   [shostak](0.03 s)
    caret_all_TCC1........................proved - complete   [shostak](0.01 s)
    caret_all_TCC2........................proved - complete   [shostak](0.00 s)
    caret_all.............................proved - complete   [shostak](0.05 s)
    caret_ii_0............................proved - complete   [shostak](0.04 s)
    caret_elim_TCC1.......................proved - complete   [shostak](0.06 s)
    caret_elim_TCC2.......................proved - complete   [shostak](0.06 s)
    caret_elim............................proved - complete   [shostak](0.09 s)
    Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.50 s)

 Proof summary for theory empty_array_def
    empty_array_TCC1......................proved - complete   [shostak](0.00 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s)

 Proof summary for theory concat_arrays
    oh_TCC1...............................proved - complete   [shostak](0.04 s)
    concat_array_bot0_TCC1................proved - complete   [shostak](0.00 s)
    concat_array_bot0.....................proved - complete   [shostak](0.01 s)
    concat_array_top0_TCC1................proved - complete   [shostak](0.01 s)
    concat_array_top0.....................proved - complete   [shostak](0.02 s)
    concat_array_bot_TCC1.................proved - complete   [shostak](0.02 s)
    concat_array_bot......................proved - complete   [shostak](0.01 s)
    concat_array_top_TCC1.................proved - complete   [shostak](0.02 s)
    concat_array_top_TCC2.................proved - complete   [shostak](0.01 s)
    concat_array_top......................proved - complete   [shostak](0.00 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.15 s)

 Proof summary for theory majority_array
    is_majority_TCC1......................proved - incomplete [shostak](0.01 s)
    maj_TCC1..............................proved - incomplete [shostak](0.07 s)
    is_majority_unique....................proved - incomplete [shostak](0.15 s)
    maj_lem...............................proved - incomplete [shostak](0.01 s)
    maj_subset............................proved - incomplete [shostak](0.08 s)
    maj_in_array..........................proved - incomplete [shostak](0.06 s)
    is_majority_const.....................proved - incomplete [shostak](0.04 s)
    maj_const.............................proved - incomplete [shostak](0.00 s)
    Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.43 s)

 Proof summary for theory top_seq
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory seqs
    seq1_def_TCC1.........................proved - complete   [shostak](0.01 s)
    seq1_def..............................proved - complete   [shostak](0.00 s)
    rev_TCC1..............................proved - complete   [shostak](0.00 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.01 s)

 Proof summary for theory max_seq
    Imax_TCC1.............................proved - complete   [shostak](0.01 s)
    Imax_TCC2.............................proved - complete   [shostak](0.01 s)
    Imax_TCC3.............................proved - complete   [shostak](0.27 s)
    Imax_1_TCC1...........................proved - complete   [shostak](0.01 s)
    Imax_1................................proved - complete   [shostak](0.03 s)
    imax_TCC1.............................proved - complete   [shostak](0.06 s)
    max_TCC1..............................proved - complete   [shostak](0.03 s)
    max_seq_lem...........................proved - complete   [shostak](0.02 s)
    max_seq_in?...........................proved - complete   [shostak](0.02 s)
    imax_seq_lem..........................proved - complete   [shostak](0.03 s)
    max_seq_def...........................proved - complete   [shostak](0.02 s)
    max_seq_it_is.........................proved - complete   [shostak](0.04 s)
    imax_seq_1............................proved - complete   [shostak](0.01 s)
    max_seq_2_TCC1........................proved - complete   [shostak](0.01 s)
    max_seq_2_TCC2........................proved - complete   [shostak](0.01 s)
    max_seq_2.............................proved - complete   [shostak](0.05 s)
    Theory totals: 16 formulas, 16 attempted, 16 succeeded (0.65 s)

 Proof summary for theory min_seq
    Imin_TCC1.............................proved - complete   [shostak](0.01 s)
    Imin_TCC2.............................proved - complete   [shostak](0.04 s)
    Imin_TCC3.............................proved - complete   [shostak](0.26 s)
    Imin_seq_1_TCC1.......................proved - complete   [shostak](0.00 s)
    Imin_seq_1............................proved - complete   [shostak](0.04 s)
    imin_TCC1.............................proved - complete   [shostak](0.06 s)
    min_TCC1..............................proved - complete   [shostak](0.03 s)
    min_seq_lem...........................proved - complete   [shostak](0.02 s)
    min_seq_in?...........................proved - complete   [shostak](0.02 s)
    min_seq_def...........................proved - complete   [shostak](0.02 s)
    min_seq_it_is.........................proved - complete   [shostak](0.04 s)
    imin_seq_lem..........................proved - complete   [shostak](0.03 s)
    imin_seq_1............................proved - complete   [shostak](0.02 s)
    min_seq_2_TCC1........................proved - complete   [shostak](0.01 s)
    min_seq_2_TCC2........................proved - complete   [shostak](0.01 s)
    min_seq_2.............................proved - complete   [shostak](0.04 s)
    Theory totals: 16 formulas, 16 attempted, 16 succeeded (0.68 s)

 Proof summary for theory permutations_seq
    perm_length...........................proved - incomplete [shostak](0.13 s)
    perm_reflexive........................proved - complete   [shostak](0.05 s)
    perm_symmetric........................proved - incomplete [shostak](0.19 s)
    perm_tran.............................proved - complete   [shostak](0.08 s)
    perm_in?..............................proved - incomplete [shostak](0.03 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.49 s)

 Proof summary for theory majority_seq
    is_majority_TCC1......................proved - incomplete [shostak](0.01 s)
    maj_TCC1..............................proved - incomplete [shostak](0.03 s)
    is_majority_unique....................proved - incomplete [shostak](0.14 s)
    maj_lem...............................proved - incomplete [shostak](0.02 s)
    maj_subset............................proved - incomplete [shostak](0.09 s)
    maj_in_seq............................proved - incomplete [shostak](0.08 s)
    length_eq_1...........................proved - incomplete [shostak](0.05 s)
    is_majority_const.....................proved - incomplete [shostak](0.05 s)
    maj_const.............................proved - incomplete [shostak](0.01 s)
    Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.48 s)

 Proof summary for theory bubblesort
    epsilon_lem_TCC1......................proved - complete   [shostak](0.06 s)
    epsilon_lem_TCC2......................proved - complete   [shostak](0.13 s)
    epsilon_lem...........................proved - complete   [shostak](0.36 s)
    bubblesort_TCC1.......................proved - complete   [shostak](0.04 s)
    bubblesort_TCC2.......................proved - complete   [shostak](0.14 s)
    sorted_bubblesort.....................proved - complete   [shostak](0.59 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.33 s)

 Proof summary for theory sort_inversions
    finite_inversions.....................proved - complete   [shostak](0.32 s)
    inversions_TCC1.......................proved - complete   [shostak](0.00 s)
    finite_ap.............................proved - complete   [shostak](0.08 s)
    ap_TCC1...............................proved - complete   [shostak](0.01 s)
    card_ap...............................proved - complete   [shostak](0.19 s)
    inversions_transpose_TCC1.............proved - complete   [shostak](0.04 s)
    inversions_transpose..................proved - complete   [shostak](0.51 s)
    card_inversions_transpose.............proved - complete   [shostak](0.07 s)
    sorted_iff_no_inversions..............proved - complete   [shostak](0.03 s)
    successive_inversion_lem..............proved - complete   [shostak](0.18 s)
    successive_inversion_exists...........proved - complete   [shostak](0.05 s)
    Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.48 s)

 Proof summary for theory permutation_ops
    sorted_iff_id_lem.....................proved - complete   [shostak](0.16 s)
    sorted_iff_id.........................proved - complete   [shostak](0.06 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.22 s)

 Proof summary for theory permutation
    inverse_id_TCC1.......................proved - complete   [shostak](0.00 s)
    inverse_id............................proved - complete   [shostak](0.03 s)
    inverse_composition...................proved - complete   [shostak](0.09 s)
    transpose_TCC1........................proved - complete   [shostak](0.06 s)
    involutorian_transpose................proved - complete   [shostak](0.02 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.20 s)

 Proof summary for theory sort_seq
    increasing?_TCC1......................proved - complete   [shostak](0.02 s)
    sort_TCC1.............................proved - complete   [shostak](0.08 s)
    sort_length...........................proved - incomplete [shostak](0.01 s)
    sort_seq_lem..........................proved - complete   [shostak](0.00 s)
    sort_seq_in?..........................proved - incomplete [shostak](0.10 s)
    sort_seq_in_TCC1......................proved - incomplete [shostak](0.00 s)
    sort_seq_in...........................proved - incomplete [shostak](0.02 s)
    sort_seq_in2..........................proved - incomplete [shostak](0.03 s)
    sort_map_TCC1.........................proved - incomplete [shostak](0.01 s)
    sort_map_TCC2.........................proved - incomplete [shostak](0.13 s)
    sort_map_def_TCC1.....................proved - incomplete [shostak](0.02 s)
    sort_map_def..........................proved - incomplete [shostak](0.02 s)
    sort_map_bij..........................proved - incomplete [shostak](0.01 s)
    isort_map_TCC1........................proved - incomplete [shostak](0.17 s)
    isort_map_def_TCC1....................proved - complete   [shostak](0.01 s)
    isort_map_def.........................proved - incomplete [shostak](0.02 s)
    isort_map_bij.........................proved - incomplete [shostak](0.01 s)
    Theory totals: 17 formulas, 17 attempted, 17 succeeded (0.67 s)

 Proof summary for theory sort_seq_lems
    sort_seq_min_TCC1.....................proved - incomplete [shostak](0.01 s)
    sort_seq_min..........................proved - incomplete [shostak](0.11 s)
    sort_seq_max_TCC1.....................proved - incomplete [shostak](0.01 s)
    sort_seq_max..........................proved - incomplete [shostak](0.13 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.27 s)

 Proof summary for theory set2seq
    gen_seq_lem_TCC1......................proved - complete   [shostak](0.00 s)
    gen_seq_lem...........................proved - complete   [shostak](0.01 s)
    set2seq_TCC1..........................proved - complete   [shostak](0.00 s)
    set2seq_TCC2..........................proved - complete   [shostak](0.01 s)
    set2seq_length........................proved - incomplete [shostak](0.14 s)
    set2seq_lem...........................proved - incomplete [shostak](0.16 s)
    set2seq_exists........................proved - incomplete [shostak](0.45 s)
    set2seq_neq...........................proved - incomplete [shostak](0.22 s)
    Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.98 s)

 Proof summary for theory seq2set
    seq2set_TCC1..........................proved - complete   [shostak](0.05 s)
    seq2set_lem...........................proved - complete   [shostak](0.02 s)
    card_seq2set..........................proved - complete   [shostak](0.10 s)
    seq2set_TCC2..........................proved - complete   [shostak](0.02 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.19 s)

 Proof summary for theory seq_extras
    first_TCC1............................proved - complete   [shostak](0.01 s)
    last_TCC1.............................proved - complete   [shostak](0.01 s)
    rest_TCC1.............................proved - complete   [shostak](0.01 s)
    delete_TCC1...........................proved - complete   [shostak](0.00 s)
    delete_TCC2...........................proved - complete   [shostak](0.01 s)
    insert?_TCC1..........................proved - complete   [shostak](0.04 s)
    insert?_TCC2..........................proved - complete   [shostak](0.04 s)
    add_first_TCC1........................proved - complete   [shostak](0.00 s)
    add_last_TCC1.........................proved - complete   [shostak](0.01 s)
    empty_0...............................proved - complete   [shostak](0.05 s)
    empty_o_seq...........................proved - complete   [shostak](0.16 s)
    seq_o_empty...........................proved - complete   [shostak](0.15 s)
    length_rest...........................proved - complete   [shostak](0.13 s)
    length_delete_TCC1....................proved - complete   [shostak](0.02 s)
    length_delete.........................proved - complete   [shostak](0.02 s)
    seq_empty.............................proved - complete   [shostak](0.14 s)
    seq_first_rest........................proved - complete   [shostak](0.32 s)
    seq_first_rest_1......................proved - complete   [shostak](0.28 s)
    add_first_empty_seq...................proved - complete   [shostak](0.05 s)
    length_rest_0.........................proved - complete   [shostak](0.21 s)
    rest_add_first........................proved - complete   [shostak](0.22 s)
    first_add_TCC1........................proved - complete   [shostak](0.05 s)
    first_add.............................proved - complete   [shostak](0.02 s)
    nth_add_first_TCC1....................proved - complete   [shostak](0.02 s)
    nth_add_first_TCC2....................proved - complete   [shostak](0.03 s)
    nth_add_first_TCC3....................proved - complete   [shostak](0.03 s)
    nth_add_first.........................proved - complete   [shostak](0.03 s)
    first_add_last_TCC1...................proved - complete   [shostak](0.05 s)
    first_add_last........................proved - complete   [shostak](0.06 s)
    rest_add_last.........................proved - complete   [shostak](0.44 s)
    add_first_last_commute................proved - complete   [shostak](0.25 s)
    add_first_last........................proved - complete   [shostak](0.39 s)
    add_last_delete.......................proved - complete   [shostak](0.11 s)
    add_last_delete_is_o..................proved - complete   [shostak](0.09 s)
    nth_add_last_TCC1.....................proved - complete   [shostak](0.02 s)
    nth_add_last_TCC2.....................proved - complete   [shostak](0.03 s)
    nth_add_last_TCC3.....................proved - complete   [shostak](0.04 s)
    nth_add_last..........................proved - complete   [shostak](0.03 s)
    add_first_compo.......................proved - complete   [shostak](0.24 s)
    first_compo_TCC1......................proved - complete   [shostak](0.07 s)
    first_compo...........................proved - complete   [shostak](0.06 s)
    rest_compo............................proved - complete   [shostak](0.02 s)
    rest_pos_TCC1.........................proved - complete   [shostak](0.11 s)
    rest_pos_TCC2.........................proved - complete   [shostak](0.08 s)
    rest_pos_TCC3.........................proved - complete   [shostak](0.09 s)
    rest_pos..............................proved - complete   [shostak](0.15 s)
    delete_is_empty_TCC1..................proved - complete   [shostak](0.01 s)
    delete_is_empty.......................proved - complete   [shostak](0.06 s)
    delete_pos_TCC1.......................proved - complete   [shostak](0.01 s)
    delete_pos_TCC2.......................proved - complete   [shostak](0.02 s)
    delete_pos............................proved - complete   [shostak](0.02 s)
    insert_delete_TCC1....................proved - complete   [shostak](0.02 s)
    insert_delete.........................proved - complete   [shostak](0.12 s)
    add_first_delete_TCC1.................proved - complete   [shostak](0.00 s)
    add_first_delete......................proved - complete   [shostak](0.75 s)
    delete_rest_TCC1......................proved - complete   [shostak](0.00 s)
    delete_rest_TCC2......................proved - complete   [shostak](0.10 s)
    delete_rest...........................proved - complete   [shostak](0.68 s)
    first_equal...........................proved - complete   [shostak](0.30 s)
    nth_x_TCC1............................proved - complete   [shostak](0.02 s)
    nth_x.................................proved - complete   [shostak](0.03 s)
    replace_nth...........................proved - complete   [shostak](0.05 s)
    replace_n2............................proved - complete   [shostak](0.15 s)
    delete_equivalent.....................proved - complete   [shostak](0.60 s)
    equal_prefix..........................proved - complete   [shostak](0.29 s)
    o_equals_o............................proved - complete   [shostak](0.32 s)
    o_length_o............................proved - complete   [shostak](0.70 s)
    add_last_is_o.........................proved - complete   [shostak](0.20 s)
    add_first_is_o........................proved - complete   [shostak](0.12 s)
    Theory totals: 69 formulas, 69 attempted, 69 succeeded (9.00 s)

 Proof summary for theory seq_pigeon
    seq_pigeon_lem........................proved - incomplete [shostak](0.06 s)
    seq_pigeon_hole.......................proved - incomplete [shostak](0.02 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.08 s)

 Proof summary for theory minmax_set2seq
    minmax_set2seq_TCC1...................proved - incomplete [shostak](0.04 s)
    minmax_set2seq_TCC2...................proved - complete   [shostak](0.02 s)
    minmax_set2seq........................proved - incomplete [shostak](0.28 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.34 s)

 Proof summary for theory minmax_seq2set
    minmax_seq2set_TCC1...................proved - complete   [shostak](0.03 s)
    minmax_seq2set........................proved - incomplete [shostak](1.06 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.09 s)

 Proof summary for theory top_bags
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory bags_aux
    choose_TCC1...........................proved - complete   [shostak](0.03 s)
    rest_TCC1.............................proved - complete   [shostak](0.01 s)
    choose_gt_zero........................proved - complete   [shostak](0.03 s)
    insert_choose_rest....................proved - complete   [shostak](0.03 s)
    filter_emptybag.......................proved - complete   [shostak](0.00 s)
    filter_insert.........................proved - complete   [shostak](0.04 s)
    filter_delete.........................proved - complete   [shostak](0.04 s)
    filter_prop...........................proved - complete   [shostak](0.02 s)
    Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.20 s)

 Proof summary for theory bags
    delete_TCC1...........................proved - complete   [shostak](0.01 s)
    emptybag_is_empty?....................proved - complete   [shostak](0.01 s)
    delete_purge..........................proved - complete   [shostak](0.03 s)
    insert_unique.........................proved - complete   [shostak](0.05 s)
    insert_exchange.......................proved - complete   [shostak](0.05 s)
    delete_insert_TCC1....................proved - complete   [shostak](0.02 s)
    delete_insert.........................proved - complete   [shostak](0.05 s)
    insert_delete.........................proved - complete   [shostak](0.01 s)
    delete_insert_diff....................proved - complete   [shostak](0.07 s)
    decomposition.........................proved - complete   [shostak](0.02 s)
    bag_equality..........................proved - complete   [shostak](0.00 s)
    subbag_empty..........................proved - complete   [shostak](0.01 s)
    subbag_equality.......................proved - complete   [shostak](0.01 s)
    subbag_trans..........................proved - complete   [shostak](0.02 s)
    bag_plus_union........................proved - complete   [shostak](0.08 s)
    bag_plus_comm.........................proved - complete   [shostak](0.01 s)
    plus_emptybag.........................proved - complete   [shostak](0.01 s)
    bag_plus_insert.......................proved - complete   [shostak](0.01 s)
    bag_distributive......................proved - complete   [shostak](0.44 s)
    extract_subbag........................proved - complete   [shostak](0.01 s)
    extract_disj..........................proved - complete   [shostak](0.03 s)
    bag_disj_comm.........................proved - complete   [shostak](0.08 s)
    bag_union_comm........................proved - complete   [shostak](0.02 s)
    bag_union_fix_pt......................proved - complete   [shostak](0.02 s)
    bag_purge_extract.....................proved - complete   [shostak](0.01 s)
    bag_disj_extract_perge................proved - complete   [shostak](0.02 s)
    bag_extract_union_subbag..............proved - complete   [shostak](0.06 s)
    union_upper_bound.....................proved - complete   [shostak](0.03 s)
    Theory totals: 28 formulas, 28 attempted, 28 succeeded (1.20 s)

 Proof summary for theory bags_to_sets
    insert_bag_lem........................proved - complete   [shostak](0.06 s)
    purge_bag_lem.........................proved - complete   [shostak](0.04 s)
    bag_union_lem.........................proved - complete   [shostak](0.05 s)
    bag_intersection_lem..................proved - complete   [shostak](0.06 s)
    subbag_lem............................proved - complete   [shostak](0.01 s)
    bag_to_set_emptybag...................proved - complete   [shostak](0.00 s)
    empty_bts_bag.........................proved - complete   [shostak](0.02 s)
    bag_intersection_commutative..........proved - complete   [shostak](0.07 s)
    bag_union_commutative.................proved - complete   [shostak](0.07 s)
    bag_plus_lem..........................proved - complete   [shostak](0.06 s)
    extract_empty_or_singlton_set.........proved - complete   [shostak](0.03 s)
    extract_singleton.....................proved - complete   [shostak](0.05 s)
    bag_disj_set..........................proved - complete   [shostak](0.05 s)
    bag_set_dist_union....................proved - complete   [shostak](0.09 s)
    bag_non_empty.........................proved - complete   [shostak](0.02 s)
    Theory totals: 15 formulas, 15 attempted, 15 succeeded (0.69 s)

 Proof summary for theory finite_bags_lems
    card_bag_plus.........................proved - incomplete [shostak](0.10 s)
    card_bag_union........................proved - incomplete [shostak](0.05 s)
    card_bag_disj_union...................proved - incomplete [shostak](0.04 s)
    card_subbag_strict....................proved - incomplete [shostak](0.11 s)
    card_subbag_strict2...................proved - incomplete [shostak](0.12 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.42 s)

 Proof summary for theory finite_bags
    bag_to_set_TCC1.......................proved - complete   [shostak](0.03 s)
    finite_bag............................proved - complete   [shostak](0.04 s)
    finite_emptybag.......................proved - complete   [shostak](0.01 s)
    finite_singleton_bag..................proved - complete   [shostak](0.02 s)
    finite_insert.........................proved - complete   [shostak](0.02 s)
    finite_purge..........................proved - complete   [shostak](0.01 s)
    finite_delete.........................proved - complete   [shostak](0.06 s)
    finite_bag_union......................proved - complete   [shostak](0.01 s)
    finite_bag_intersection...............proved - complete   [shostak](0.01 s)
    finite_bag_plus.......................proved - complete   [shostak](0.01 s)
    finite_update.........................proved - complete   [shostak](0.13 s)
    finite_set............................proved - complete   [shostak](0.01 s)
    finite_extract........................proved - complete   [shostak](0.02 s)
    subtype_TCC1..........................proved - complete   [shostak](0.02 s)
    singleton_bag_TCC1....................proved - complete   [shostak](0.00 s)
    union_TCC1............................proved - complete   [shostak](0.00 s)
    intersection_TCC1.....................proved - complete   [shostak](0.01 s)
    plus_TCC1.............................proved - complete   [shostak](0.00 s)
    union_TCC2............................proved - complete   [shostak](0.16 s)
    plus_TCC2.............................proved - complete   [shostak](0.17 s)
    union_TCC3............................proved - complete   [shostak](0.17 s)
    plus_TCC3.............................proved - complete   [shostak](0.17 s)
    insert_TCC1...........................proved - complete   [shostak](0.16 s)
    purge_TCC1............................proved - complete   [shostak](0.00 s)
    delete_TCC1...........................proved - complete   [shostak](0.01 s)
    emptybag_TCC1.........................proved - complete   [shostak](0.00 s)
    extract_TCC1..........................proved - complete   [shostak](0.00 s)
    card_emptybag.........................proved - incomplete [shostak](0.11 s)
    card_bag_empty?.......................proved - incomplete [shostak](0.62 s)
    card_singleton_bag....................proved - incomplete [shostak](0.10 s)
    card_subbag?..........................proved - incomplete [shostak](0.02 s)
    card_bag_particular_TCC1..............proved - complete   [shostak](-.00 s)
    card_bag_particular...................proved - incomplete [shostak](0.44 s)
    card_bag_delete.......................proved - incomplete [shostak](0.15 s)
    card_bag_insert.......................proved - incomplete [shostak](0.07 s)
    card_nonempty_bag?....................proved - incomplete [shostak](0.23 s)
    card_disj_intersection................proved - incomplete [shostak](0.00 s)
    sum_bag_disj_union....................proved - incomplete [shostak](0.17 s)
    card_extract..........................proved - incomplete [shostak](0.01 s)
    card_extract_bag......................proved - incomplete [shostak](0.32 s)
    card_disjoint_add.....................proved - incomplete [shostak](0.10 s)
    card_purge_extract....................proved - incomplete [shostak](0.02 s)
    card_union_extract_add................proved - incomplete [shostak](0.06 s)
    card_union_extract....................proved - incomplete [shostak](0.02 s)
    card_geq_count........................proved - incomplete [shostak](0.01 s)
    card_geq_count_add....................proved - incomplete [shostak](0.04 s)
    Theory totals: 46 formulas, 46 attempted, 46 succeeded (3.78 s)

 Proof summary for theory finite_bags_inductions
    cardinal_induction....................proved - incomplete [shostak](0.47 s)
    finite_bag_induction..................proved - incomplete [shostak](0.46 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.93 s)

 Proof summary for theory finite_bags_aux
    finite_bag_rest.......................proved - complete   [shostak](0.01 s)
    rest_TCC1.............................proved - complete   [shostak](0.00 s)
    card_bag_rest.........................proved - incomplete [shostak](0.17 s)
    finite_filter.........................proved - complete   [shostak](0.18 s)
    filter_TCC1...........................proved - complete   [shostak](0.01 s)
    card_filter_insert....................proved - incomplete [shostak](0.04 s)
    card_filter_delete....................proved - incomplete [shostak](0.13 s)
    Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.54 s)

 Proof summary for theory fault_masking_vote
    mid_val_is_maj........................proved - incomplete [shostak](0.43 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.43 s)

 Proof summary for theory majority_vote
    maj_size..............................proved - incomplete [shostak](0.13 s)
    maj_single_or_empty...................proved - incomplete [shostak](0.17 s)
    maj_unique............................proved - incomplete [shostak](0.43 s)
    maj_pigeonhole........................proved - incomplete [shostak](0.01 s)
    maj_is_extraction.....................proved - incomplete [shostak](0.07 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.80 s)

 Proof summary for theory middle_value_select
    mid_val_singleton.....................proved - incomplete [shostak](1.62 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (1.62 s)

 Proof summary for theory bag_filters
    finite_l_filter.......................proved - complete   [shostak](0.03 s)
    finite_u_filter.......................proved - complete   [shostak](0.03 s)
    l_filter_TCC1.........................proved - complete   [shostak](0.01 s)
    u_filter_TCC1.........................proved - complete   [shostak](0.00 s)
    l_filter_extract......................proved - complete   [shostak](0.05 s)
    u_filter_extract......................proved - complete   [shostak](0.06 s)
    l_filter_singleton....................proved - complete   [shostak](0.05 s)
    u_filter_singleton....................proved - complete   [shostak](0.05 s)
    l_filter_subbag.......................proved - complete   [shostak](0.01 s)
    u_filter_subbag.......................proved - complete   [shostak](0.02 s)
    l_filter_orders.......................proved - complete   [shostak](0.02 s)
    u_filter_orders.......................proved - complete   [shostak](0.03 s)
    l_filter_orders_2.....................proved - complete   [shostak](0.06 s)
    u_filter_orders_2.....................proved - complete   [shostak](0.06 s)
    l_filter_insert_assoc.................proved - complete   [shostak](0.08 s)
    u_filter_insert_assoc.................proved - complete   [shostak](0.08 s)
    l_filter_insert.......................proved - complete   [shostak](0.04 s)
    u_filter_insert.......................proved - complete   [shostak](0.04 s)
    l_filter_purge........................proved - complete   [shostak](0.05 s)
    u_filter_purge........................proved - complete   [shostak](0.05 s)
    l_u_diff_disj.........................proved - complete   [shostak](0.09 s)
    l_u_fullset...........................proved - complete   [shostak](0.13 s)
    l_u_fullset2..........................proved - complete   [shostak](0.13 s)
    l_u_diff..............................proved - incomplete [shostak](0.53 s)
    subset_diff_elements..................proved - complete   [shostak](0.20 s)
    card_diff_elements....................proved - incomplete [shostak](0.17 s)
    card_plus.............................proved - incomplete [shostak](1.53 s)
    pigeonhole............................proved - incomplete [shostak](0.26 s)
    maj_pigeonhole........................proved - incomplete [shostak](0.08 s)
    l_filter_nonempty.....................proved - incomplete [shostak](0.25 s)
    u_filter_nonempty.....................proved - incomplete [shostak](0.25 s)
    l_filter_max..........................proved - incomplete [shostak](0.75 s)
    u_filter_min..........................proved - incomplete [shostak](0.64 s)
    l_filter_max_purge....................proved - incomplete [shostak](0.35 s)
    u_filter_min_purge....................proved - incomplete [shostak](0.35 s)
    filter_exists.........................proved - incomplete [shostak](3.92 s)
    Theory totals: 36 formulas, 36 attempted, 36 succeeded (10.46 s)

 Proof summary for theory finite_bags_minmax
    max_TCC1..............................proved - complete   [shostak](0.15 s)
    max_member............................proved - incomplete [shostak](0.02 s)
    min_member............................proved - incomplete [shostak](0.02 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.19 s)

 Proof summary for theory more_list_props
    prefix?_TCC1..........................proved - complete   [shostak](0.06 s)
    suffix?_TCC1..........................proved - complete   [shostak](0.08 s)
    caret_TCC1............................proved - complete   [shostak](0.01 s)
    caret_TCC2............................proved - complete   [shostak](0.00 s)
    caret_TCC3............................proved - complete   [shostak](0.01 s)
    caret_TCC4............................proved - complete   [shostak](0.02 s)
    caret_TCC5............................proved - complete   [shostak](0.02 s)
    caret_TCC6............................proved - complete   [shostak](0.06 s)
    prefix_length.........................proved - complete   [shostak](0.01 s)
    suffix_length.........................proved - complete   [shostak](0.00 s)
    every_forall..........................proved - complete   [shostak](0.01 s)
    some_exists...........................proved - complete   [shostak](0.19 s)
    list_extensionality_TCC1..............proved - complete   [shostak](0.01 s)
    list_extensionality...................proved - complete   [shostak](0.23 s)
    list_pigeonhole.......................proved - complete   [shostak](0.30 s)
    nth_append_TCC1.......................proved - complete   [shostak](0.03 s)
    nth_append_TCC2.......................proved - complete   [shostak](0.04 s)
    nth_append............................proved - complete   [shostak](0.23 s)
    length_null...........................proved - complete   [shostak](0.00 s)
    length_singleton......................proved - complete   [shostak](0.00 s)
    length_null_list......................proved - complete   [shostak](0.03 s)
    reverse_def_TCC1......................proved - complete   [shostak](0.01 s)
    reverse_def_TCC2......................proved - complete   [shostak](0.02 s)
    reverse_def...........................proved - complete   [shostak](0.50 s)
    cons_append...........................proved - complete   [shostak](0.09 s)
    expand_list_TCC1......................proved - complete   [shostak](0.01 s)
    expand_list...........................proved - complete   [shostak](0.03 s)
    append_null_left......................proved - complete   [shostak](0.01 s)
    Theory totals: 28 formulas, 28 attempted, 28 succeeded (2.02 s)

 Proof summary for theory listn
    listn_ext_TCC1........................proved - complete   [shostak](0.01 s)
    listn_ext_TCC2........................proved - complete   [shostak](0.00 s)
    listn_ext.............................proved - complete   [shostak](0.17 s)
    listn_0...............................proved - complete   [shostak](0.01 s)
    setnth_TCC1...........................proved - complete   [shostak](0.00 s)
    setnth_TCC2...........................proved - complete   [shostak](0.01 s)
    setnth_TCC3...........................proved - complete   [shostak](0.04 s)
    setnth_TCC4...........................proved - complete   [shostak](0.09 s)
    setnth_TCC5...........................proved - complete   [shostak](0.02 s)
    setnth_TCC6...........................proved - complete   [shostak](0.02 s)
    setnth_TCC7...........................proved - complete   [shostak](0.13 s)
    normalize_fseq_TCC1...................proved - complete   [shostak](0.42 s)
    normalize_fseq_def....................proved - complete   [shostak](0.01 s)
    Theory totals: 13 formulas, 13 attempted, 13 succeeded (0.94 s)

 Proof summary for theory array2list
    array2list_it_TCC1....................proved - complete   [shostak](0.00 s)
    array2list_it_TCC2....................proved - complete   [shostak](0.01 s)
    array2list_it_TCC3....................proved - complete   [shostak](0.01 s)
    array2list_it_TCC4....................proved - complete   [shostak](0.02 s)
    array2list_it_TCC5....................proved - complete   [shostak](0.04 s)
    array2list_it_TCC6....................proved - complete   [shostak](0.00 s)
    array2list_it_TCC7....................proved - complete   [shostak](0.13 s)
    array2list_TCC1.......................proved - complete   [shostak](0.00 s)
    array2list_TCC2.......................proved - complete   [shostak](0.00 s)
    array2list_TCC3.......................proved - complete   [shostak](0.02 s)
    list2array_TCC1.......................proved - complete   [shostak](0.01 s)
    list2array_TCC2.......................proved - complete   [shostak](0.01 s)
    list2array_TCC3.......................proved - complete   [shostak](0.02 s)
    list2array_TCC4.......................proved - complete   [shostak](0.01 s)
    list2array_sound......................proved - complete   [shostak](0.14 s)
    default_TCC1..........................proved - complete   [shostak](0.01 s)
    array2list_inv........................proved - complete   [shostak](0.02 s)
    list2array_inv_TCC1...................proved - complete   [shostak](0.02 s)
    list2array_inv........................proved - complete   [shostak](0.03 s)
    list2array_inv_ext....................proved - complete   [shostak](0.04 s)
    fill_TCC1.............................proved - complete   [shostak](0.01 s)
    Theory totals: 21 formulas, 21 attempted, 21 succeeded (0.56 s)

 Proof summary for theory set_as_list
    empty_sl_is_empty.....................proved - complete   [shostak](0.02 s)
    subset_sl?_TCC1.......................proved - complete   [shostak](0.01 s)
    subset_sl?_TCC2.......................proved - complete   [shostak](0.03 s)
    subset_sl?_TCC3.......................proved - complete   [shostak](0.05 s)
    add_sl_TCC1...........................proved - complete   [shostak](0.01 s)
    add_sl_TCC2...........................proved - complete   [shostak](0.03 s)
    add_sl_TCC3...........................proved - complete   [shostak](0.01 s)
    add_sl_TCC4...........................proved - complete   [shostak](0.05 s)
    remove_sl_TCC1........................proved - complete   [shostak](0.01 s)
    remove_sl_TCC2........................proved - complete   [shostak](0.02 s)
    remove_sl_TCC3........................proved - complete   [shostak](0.04 s)
    remove_sl_TCC4........................proved - complete   [shostak](0.04 s)
    equal_sl_TCC1.........................proved - complete   [shostak](0.88 s)
    strict_subset_sl?_TCC1................proved - complete   [shostak](0.02 s)
    union_sl_TCC1.........................proved - complete   [shostak](0.01 s)
    union_sl_TCC2.........................proved - complete   [shostak](0.02 s)
    union_sl_TCC3.........................proved - complete   [shostak](0.05 s)
    intersection_sl_TCC1..................proved - complete   [shostak](0.01 s)
    intersection_sl_TCC2..................proved - complete   [shostak](0.03 s)
    intersection_sl_TCC3..................proved - complete   [shostak](0.03 s)
    difference_sl_TCC1....................proved - complete   [shostak](0.01 s)
    difference_sl_TCC2....................proved - complete   [shostak](0.02 s)
    difference_sl_TCC3....................proved - complete   [shostak](0.03 s)
    list2set_TCC1.........................proved - complete   [shostak](0.01 s)
    list2set_TCC2.........................proved - complete   [shostak](0.03 s)
    card_sl_TCC1..........................proved - complete   [shostak](0.01 s)
    card_sl_TCC2..........................proved - complete   [shostak](0.05 s)
    card_sl_TCC3..........................proved - complete   [shostak](0.12 s)
    reduce_sl_TCC1........................proved - complete   [shostak](0.04 s)
    reduce_sl_TCC2........................proved - complete   [shostak](0.11 s)
    reduce_sl_TCC3........................proved - complete   [shostak](0.13 s)
    equal_sl_card.........................proved - complete   [shostak](0.04 s)
    Theory totals: 32 formulas, 32 attempted, 32 succeeded (2.01 s)

 Proof summary for theory set_as_list_props
    strict_subset_card_lt.................proved - complete   [shostak](0.19 s)
    empty_l2s.............................proved - complete   [shostak](0.16 s)
    emptyset_l2s..........................proved - complete   [shostak](0.03 s)
    nonempty_l2s..........................proved - complete   [shostak](0.16 s)
    subset_l2s............................proved - complete   [shostak](0.07 s)
    remove_l2s............................proved - complete   [shostak](0.04 s)
    equal_l2s.............................proved - complete   [shostak](0.17 s)
    strict_subset_l2s.....................proved - complete   [shostak](0.11 s)
    union_l2s.............................proved - complete   [shostak](0.05 s)
    intersection_l2s......................proved - complete   [shostak](0.05 s)
    disjoint_l2s..........................proved - complete   [shostak](0.02 s)
    difference_l2s........................proved - complete   [shostak](0.09 s)
    symmetric_difference_l2s..............proved - complete   [shostak](0.06 s)
    subset_sl_emptyset_sl.................proved - complete   [shostak](0.03 s)
    subset_sl_reflexive...................proved - complete   [shostak](0.01 s)
    subset_sl_transitive..................proved - complete   [shostak](0.28 s)
    subset_sl_preorder....................proved - complete   [shostak](0.02 s)
    subset_sl_is_preorder.................proved - complete   [shostak](0.01 s)
    equal_sl_reflexive....................proved - complete   [shostak](0.02 s)
    equal_sl_transitive...................proved - complete   [shostak](0.03 s)
    equal_sl_symmetric....................proved - complete   [shostak](0.05 s)
    strict_subset_sl_irreflexive..........proved - complete   [shostak](0.02 s)
    strict_subset_sl_transitive...........proved - complete   [shostak](0.08 s)
    strict_subset_sl_strict_order.........proved - complete   [shostak](0.03 s)
    strict_subset_sl_is_strict_order......proved - complete   [shostak](0.00 s)
    strict_subset_sl_wf...................proved - complete   [shostak](0.27 s)
    strict_subset_sl_is_wf................proved - complete   [shostak](-.00 s)
    Theory totals: 27 formulas, 27 attempted, 27 succeeded (2.08 s)

 Proof summary for theory for_iterate
    for_def_TCC1..........................proved - complete   [shostak](0.04 s)
    for_def_TCC2..........................proved - complete   [shostak](0.06 s)
    for_def_inv...........................proved - complete   [shostak](0.09 s)
    for_shift.............................proved - complete   [shostak](0.13 s)
    for_def_ext...........................proved - complete   [shostak](0.14 s)
    for_def_induction_TCC1................proved - complete   [shostak](0.01 s)
    for_def_induction_TCC2................proved - complete   [shostak](0.00 s)
    for_def_induction_TCC3................proved - complete   [shostak](0.05 s)
    for_def_induction.....................proved - complete   [shostak](0.27 s)
    ext2int_TCC1..........................proved - complete   [shostak](0.01 s)
    for_it_TCC1...........................proved - complete   [shostak](0.05 s)
    for_it_TCC2...........................proved - complete   [shostak](0.01 s)
    for_it_TCC3...........................proved - complete   [shostak](0.00 s)
    for_it_TCC4...........................proved - complete   [shostak](0.02 s)
    for_it_TCC5...........................proved - complete   [shostak](0.04 s)
    for_it_TCC6...........................proved - complete   [shostak](0.06 s)
    for_TCC1..............................proved - complete   [shostak](0.00 s)
    for_eq................................proved - complete   [shostak](0.02 s)
    for_induction_TCC1....................proved - complete   [shostak](0.02 s)
    for_induction_TCC2....................proved - complete   [shostak](0.02 s)
    for_induction_TCC3....................proved - complete   [shostak](0.03 s)
    for_induction_TCC4....................proved - complete   [shostak](0.00 s)
    for_induction_TCC5....................proved - complete   [shostak](0.02 s)
    for_induction.........................proved - complete   [shostak](0.07 s)
    for_down_def_TCC1.....................proved - complete   [shostak](0.04 s)
    for_down_def_TCC2.....................proved - complete   [shostak](0.05 s)
    for_down_def_ext......................proved - complete   [shostak](0.11 s)
    for_down_up...........................proved - complete   [shostak](0.13 s)
    for_down_def_induction_TCC1...........proved - complete   [shostak](0.00 s)
    for_down_def_induction_TCC2...........proved - complete   [shostak](0.00 s)
    for_down_def_induction_TCC3...........proved - complete   [shostak](0.06 s)
    for_down_def_induction................proved - complete   [shostak](0.05 s)
    for_down_TCC1.........................proved - complete   [shostak](0.02 s)
    for_down_induction_TCC1...............proved - complete   [shostak](0.02 s)
    for_down_induction_TCC2...............proved - complete   [shostak](0.02 s)
    for_down_induction_TCC3...............proved - complete   [shostak](0.02 s)
    for_down_induction_TCC4...............proved - complete   [shostak](0.01 s)
    for_down_induction_TCC5...............proved - complete   [shostak](0.02 s)
    for_down_induction....................proved - complete   [shostak](0.06 s)
    for_down_eq...........................proved - complete   [shostak](0.09 s)
    iterate_left_def_TCC1.................proved - complete   [shostak](0.00 s)
    iterate_left_def_TCC2.................proved - complete   [shostak](0.01 s)
    iterate_left_def_TCC3.................proved - complete   [shostak](0.01 s)
    iterate_left_def_ext..................proved - complete   [shostak](0.15 s)
    ext2int_TCC2..........................proved - complete   [shostak](0.01 s)
    iterate_left_TCC1.....................proved - complete   [shostak](0.00 s)
    iterate_left_TCC2.....................proved - complete   [shostak](0.01 s)
    iterate_left_eq.......................proved - complete   [shostak](0.25 s)
    iterate_left_induction_TCC1...........proved - complete   [shostak](0.00 s)
    iterate_left_induction_TCC2...........proved - complete   [shostak](0.01 s)
    iterate_left_induction_TCC3...........proved - complete   [shostak](0.00 s)
    iterate_left_induction_TCC4...........proved - complete   [shostak](0.02 s)
    iterate_left_induction_TCC5...........proved - complete   [shostak](0.03 s)
    iterate_left_induction................proved - complete   [shostak](0.13 s)
    iterate_right_def_TCC1................proved - complete   [shostak](0.03 s)
    iterate_right_def_TCC2................proved - complete   [shostak](0.03 s)
    iterate_right_def_ext.................proved - complete   [shostak](0.12 s)
    iterate_right_TCC1....................proved - complete   [shostak](0.00 s)
    iterate_right_TCC2....................proved - complete   [shostak](0.01 s)
    iterate_right_eq......................proved - complete   [shostak](0.25 s)
    iterate_right_induction_TCC1..........proved - complete   [shostak](0.01 s)
    iterate_right_induction_TCC2..........proved - complete   [shostak](0.00 s)
    iterate_right_induction_TCC3..........proved - complete   [shostak](0.01 s)
    iterate_right_induction_TCC4..........proved - complete   [shostak](0.00 s)
    iterate_right_induction...............proved - complete   [shostak](0.09 s)
    Theory totals: 65 formulas, 65 attempted, 65 succeeded (3.06 s)

 Proof summary for theory for_examples
    expit_test............................proved - complete   [shostak](0.08 s)
    expit_sound_TCC1......................proved - complete   [shostak](0.00 s)
    expit_sound...........................proved - complete   [shostak](0.20 s)
    factit_test...........................proved - complete   [shostak](0.14 s)
    factit_sound..........................proved - complete   [shostak](0.39 s)
    maxit_TCC1............................proved - complete   [shostak](0.03 s)
    maxit_TCC2............................proved - complete   [shostak](0.03 s)
    maxit_test............................proved - complete   [shostak](0.16 s)
    maxit_sound...........................proved - complete   [shostak](0.16 s)
    minit_test............................proved - complete   [shostak](0.16 s)
    minit_sound...........................proved - complete   [shostak](0.19 s)
    Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.52 s)

 Proof summary for theory big_ops_nat
    big_ops_nat_TCC1......................proved - complete   [shostak](0.00 s)
    big_ops_nat_eq........................proved - complete   [shostak](0.06 s)
    big_ops_nat_expand_right_TCC1.........proved - complete   [shostak](0.01 s)
    big_ops_nat_expand_right..............proved - complete   [shostak](0.15 s)
    big_ops_nat_expand_left...............proved - complete   [shostak](0.21 s)
    big_ops_nat_split.....................proved - complete   [shostak](0.34 s)
    big_ops_nat_shift.....................proved - complete   [shostak](0.32 s)
    big_ops_nat_reverse...................proved - complete   [shostak](0.45 s)
    big_ops_nat_id........................proved - complete   [shostak](0.13 s)
    big_ops_nat_comp......................proved - complete   [shostak](0.26 s)
    big_ops_nat_distrib...................proved - complete   [shostak](0.16 s)
    Theory totals: 11 formulas, 11 attempted, 11 succeeded (2.09 s)

 Proof summary for theory arrays
    init_TCC1.............................proved - complete   [shostak](0.01 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.01 s)

 Proof summary for theory arrays_examples
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory runs
    invariant_rule........................proved - complete   [shostak](0.08 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.08 s)

 Proof summary for theory fseqs
    default_TCC1..........................proved - complete   [shostak](0.00 s)
    empty_seq_fseq........................proved - complete   [shostak](0.01 s)
    emptyseq_fseq.........................proved - complete   [shostak](0.00 s)
    singleton_TCC1........................proved - complete   [shostak](0.01 s)
    tofseq_TCC1...........................proved - complete   [shostak](0.01 s)
    singleton_length......................proved - complete   [shostak](0.14 s)
    fseqs_eq..............................proved - complete   [shostak](0.04 s)
    fseq_length_zero......................proved - complete   [shostak](0.02 s)
    oh_TCC1...............................proved - complete   [shostak](0.06 s)
    oh_TCC2...............................proved - complete   [shostak](0.06 s)
    concat_length_add.....................proved - complete   [shostak](0.01 s)
    member_composition....................proved - complete   [shostak](0.13 s)
    concat_right_emptyseq.................proved - complete   [shostak](0.03 s)
    concat_left_emptyseq..................proved - complete   [shostak](0.03 s)
    member_singleton......................proved - complete   [shostak](0.02 s)
    caret_TCC1............................proved - complete   [shostak](0.02 s)
    caret_TCC2............................proved - complete   [shostak](0.06 s)
    caret_TCC3............................proved - complete   [shostak](0.07 s)
    o_assoc...............................proved - complete   [shostak](0.25 s)
    fseq1_TCC1............................proved - complete   [shostak](0.02 s)
    fseq2_TCC1............................proved - complete   [shostak](0.01 s)
    fseq1_def.............................proved - complete   [shostak](0.00 s)
    const_seq_TCC1........................proved - complete   [shostak](0.02 s)
    rev_TCC1..............................proved - complete   [shostak](0.02 s)
    rev_TCC2..............................proved - complete   [shostak](0.01 s)
    Theory totals: 25 formulas, 25 attempted, 25 succeeded (1.07 s)

 Proof summary for theory fsq
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory fseqs_def
    empty_seq_fseq........................proved - complete   [shostak](0.00 s)
    emptyseq_fseq.........................proved - complete   [shostak](0.00 s)
    singleton_TCC1........................proved - complete   [shostak](0.01 s)
    tofseq_TCC1...........................proved - complete   [shostak](0.01 s)
    singleton_length......................proved - complete   [shostak](0.14 s)
    fseqs_eq..............................proved - complete   [shostak](0.04 s)
    fseq_length_zero......................proved - complete   [shostak](0.03 s)
    oh_TCC1...............................proved - complete   [shostak](0.05 s)
    oh_TCC2...............................proved - complete   [shostak](0.05 s)
    concat_length_add.....................proved - complete   [shostak](0.01 s)
--> --------------------

--> maximum size reached

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

[ zur Elbe Produktseite wechseln0.234Quellennavigators  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik