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


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: compatibility.prf   Sprache: PVS

Untersuchungsergebnis.summary Download desMT940 {MT940[559] Hlasm[1205] Haskell[1615]}zum Wurzelverzeichnis wechseln

*** 
*** top (19:52:56 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 trs
    IMP_critical_pairs_TCC1...............proved - complete   [shostak](0.03 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.03 s)

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

 Proof summary for theory critical_pairs
    IMP_critical_pairs_aux_TCC1...........proved - complete   [shostak](0.01 s)
    CP?_TCC1..............................proved - complete   [shostak](0.05 s)
    CP_lemma_aux1a_TCC1...................proved - complete   [shostak](0.04 s)
    CP_lemma_aux1a........................proved - complete   [shostak](0.17 s)
    CP_lemma_aux1_TCC1....................proved - complete   [shostak](0.03 s)
    CP_lemma_aux1.........................proved - complete   [shostak](1.46 s)
    CP_lemma_aux2_TCC1....................proved - complete   [shostak](0.03 s)
    CP_lemma_aux2_TCC2....................proved - incomplete [shostak](1.35 s)
    CP_lemma_aux2.........................proved - incomplete [shostak](1.37 s)
    CP_Theorem............................proved - incomplete [shostak](8.78 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (13.29 s)

 Proof summary for theory critical_pairs_aux
    IMP_rewrite_rules_TCC1................proved - complete   [shostak](0.01 s)
    CP_lemma_aux2b_TCC1...................proved - complete   [shostak](0.05 s)
    CP_lemma_aux2b_TCC2...................proved - complete   [shostak](0.80 s)
    CP_lemma_aux2b........................proved - complete   [shostak](4.10 s)
    CP_lemma_aux2c1_TCC1..................proved - complete   [shostak](0.51 s)
    CP_lemma_aux2c1_TCC2..................proved - complete   [shostak](0.93 s)
    CP_lemma_aux2c1_TCC3..................proved - complete   [shostak](0.12 s)
    CP_lemma_aux2c1.......................proved - complete   [shostak](6.05 s)
    CP_lemma_aux2c_TCC1...................proved - complete   [shostak](0.04 s)
    CP_lemma_aux2c_TCC2...................proved - complete   [shostak](0.94 s)
    CP_lemma_aux2c_TCC3...................proved - complete   [shostak](0.78 s)
    CP_lemma_aux2c........................proved - complete   [shostak](4.50 s)
    CP_lemma_aux2d_TCC1...................proved - complete   [shostak](0.03 s)
    CP_lemma_aux2d_TCC2...................proved - incomplete [shostak](0.05 s)
    CP_lemma_aux2d........................proved - incomplete [shostak](6.05 s)
    Theory totals: 15 formulas, 15 attempted, 15 succeeded (24.95 s)

 Proof summary for theory rewrite_rules
    IMP_substitution_TCC1.................proved - complete   [shostak](0.01 s)
    ren_rewrite...........................proved - complete   [shostak](0.11 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.12 s)

 Proof summary for theory substitution
    Ren?_TCC1.............................proved - complete   [shostak](0.02 s)
    range_finite..........................proved - complete   [shostak](0.07 s)
    exists_var............................proved - complete   [shostak](2.92 s)
    restriction_Dom.......................proved - complete   [shostak](0.03 s)
    restriction_Dom_fin...................proved - complete   [shostak](0.03 s)
    restriction_Subs......................proved - complete   [shostak](0.02 s)
    dom_restriction.......................proved - complete   [shostak](0.03 s)
    Dom_union.............................proved - complete   [shostak](0.05 s)
    union_is_sub..........................proved - complete   [shostak](0.04 s)
    union_commute_TCC1....................proved - complete   [shostak](0.07 s)
    union_commute_TCC2....................proved - complete   [shostak](0.12 s)
    union_commute.........................proved - complete   [shostak](0.25 s)
    ext_TCC1..............................proved - complete   [shostak](0.06 s)
    ext_TCC2..............................proved - complete   [shostak](0.19 s)
    ext_TCC3..............................proved - complete   [shostak](0.20 s)
    iden_subs.............................proved - complete   [shostak](0.03 s)
    iden_rename_TCC1......................proved - complete   [shostak](0.01 s)
    iden_rename...........................proved - complete   [shostak](1.35 s)
    ext_iden..............................proved - complete   [shostak](0.87 s)
    restriction_term_TCC1.................proved - complete   [shostak](0.02 s)
    restriction_term......................proved - complete   [shostak](1.10 s)
    restriction_union_TCC1................proved - complete   [shostak](0.02 s)
    restriction_union.....................proved - complete   [shostak](1.15 s)
    dom_o.................................proved - complete   [shostak](0.20 s)
    dom_o_fin.............................proved - complete   [shostak](0.03 s)
    subs_o................................proved - complete   [shostak](0.01 s)
    ext_o_TCC1............................proved - complete   [shostak](0.01 s)
    ext_o.................................proved - complete   [shostak](1.42 s)
    subs_o_identity.......................proved - complete   [shostak](0.27 s)
    ext_subs_o_identity_TCC1..............proved - complete   [shostak](0.02 s)
    ext_subs_o_identity...................proved - complete   [shostak](0.02 s)
    o_ass.................................proved - complete   [shostak](0.04 s)
    inverse_renaming......................proved - complete   [shostak](0.22 s)
    inverse_rename_identity_TCC1..........proved - complete   [shostak](0.02 s)
    inverse_rename_identity...............proved - complete   [shostak](0.28 s)
    idemp_sub_term_empty_inter............proved - complete   [shostak](1.14 s)
    idemp_sub_iff_empty_intersection......proved - complete   [shostak](0.14 s)
    Dom_DSigma............................proved - complete   [shostak](0.05 s)
    Dom_DSigma_is_finite..................proved - complete   [shostak](0.10 s)
    DSigma_is_Sub.........................proved - complete   [shostak](0.03 s)
    DSigma_do_nothing_TCC1................proved - complete   [shostak](0.02 s)
    DSigma_do_nothing.....................proved - complete   [shostak](0.90 s)
    Rhop_TCC1.............................proved - complete   [shostak](0.04 s)
    SigmaP_Dom............................proved - complete   [shostak](0.04 s)
    SigmaP_Dom_fin........................proved - complete   [shostak](0.07 s)
    SigmaP_Subs...........................proved - complete   [shostak](0.03 s)
    SigmaP_is_RSigma_TCC1.................proved - complete   [shostak](0.03 s)
    SigmaP_is_RSigma......................proved - complete   [shostak](0.08 s)
    gamma_Dom.............................proved - complete   [shostak](0.22 s)
    gamma_Dom_fin.........................proved - complete   [shostak](0.08 s)
    gamma_Subs............................proved - complete   [shostak](0.02 s)
    gamma_is_RSigma_TCC1..................proved - complete   [shostak](0.03 s)
    gamma_is_RSigma_TCC2..................proved - complete   [shostak](0.02 s)
    gamma_is_RSigma.......................proved - complete   [shostak](0.05 s)
    gamma_term_TCC1.......................proved - complete   [shostak](0.03 s)
    gamma_term_TCC2.......................proved - complete   [shostak](0.02 s)
    gamma_term............................proved - complete   [shostak](1.20 s)
    Rhop_Dom..............................proved - complete   [shostak](0.10 s)
    Rhop_Ran..............................proved - complete   [shostak](0.16 s)
    Rhop_Dom_fin..........................proved - complete   [shostak](0.05 s)
    Rhop_Subs.............................proved - complete   [shostak](0.02 s)
    Rhop_Ren_TCC1.........................proved - complete   [shostak](0.02 s)
    Rhop_Ren..............................proved - complete   [shostak](0.33 s)
    ext_preserv_pos.......................proved - complete   [shostak](1.00 s)
    subterm_ext_commute_TCC1..............proved - complete   [shostak](0.03 s)
    subterm_ext_commute...................proved - complete   [shostak](0.90 s)
    ext_replace_ext.......................proved - complete   [shostak](4.61 s)
    positions_of_ext......................proved - complete   [shostak](2.30 s)
    rename_preserv_pos....................proved - complete   [shostak](1.16 s)
    subterm_of_ext_TCC1...................proved - complete   [shostak](0.06 s)
    subterm_of_ext........................proved - complete   [shostak](0.08 s)
    rename_preserv_inclusion..............proved - complete   [shostak](1.58 s)
    same_substitution.....................proved - complete   [shostak](0.80 s)
    same_term.............................proved - complete   [shostak](0.81 s)
    term_is_a_var.........................proved - complete   [shostak](0.20 s)
    vars_term_rename......................proved - complete   [shostak](0.89 s)
    exists_renaming.......................proved - complete   [shostak](-.34 s)
    add_parallel_pos......................proved - complete   [shostak](0.66 s)
    ext_parallel_pos......................proved - complete   [shostak](0.05 s)
    rest_parallel_first_TCC1..............proved - complete   [shostak](0.61 s)
    rest_parallel_first...................proved - complete   [shostak](1.05 s)
    rest_parallel_pos_parallel............proved - complete   [shostak](1.33 s)
    vars_subst_not_in.....................proved - complete   [shostak](0.99 s)
    ext_preserve_symbol_TCC1..............proved - complete   [shostak](0.03 s)
    ext_preserve_symbol_TCC2..............proved - complete   [shostak](0.05 s)
    ext_preserve_symbol...................proved - complete   [shostak](0.60 s)
    Theory totals: 86 formulas, 86 attempted, 86 succeeded (35.68 s)

 Proof summary for theory compatibility
    close_op?_TCC1........................proved - complete   [shostak](0.06 s)
    close_op?_TCC2........................proved - complete   [shostak](0.06 s)
    close_op?_TCC3........................proved - complete   [shostak](0.09 s)
    close_op?_TCC4........................proved - complete   [shostak](0.11 s)
    comp_op?_TCC1.........................proved - complete   [shostak](0.05 s)
    comp_op?_TCC2.........................proved - complete   [shostak](0.22 s)
    comp_op?_TCC3.........................proved - complete   [shostak](0.27 s)
    comp_op_iff_comp_cont.................proved - complete   [shostak](0.82 s)
    closure_comp_op.......................proved - complete   [shostak](3.08 s)
    closure_comp_cont.....................proved - complete   [shostak](0.07 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (4.83 s)

 Proof summary for theory replacement
    replaceTerm_TCC1......................proved - complete   [shostak](0.03 s)
    replaceTerm_TCC2......................proved - complete   [shostak](0.12 s)
    replaceTerm_TCC3......................proved - complete   [shostak](0.13 s)
    replaceTerm_TCC4......................proved - complete   [shostak](0.05 s)
    replaceTerm_TCC5......................proved - complete   [shostak](0.79 s)
    replaceTerm_TCC6......................proved - complete   [shostak](0.72 s)
    replaceTerm_TCC7......................proved - complete   [shostak](0.05 s)
    replace_preserv_pos...................proved - complete   [shostak](0.83 s)
    replace_compose_pos...................proved - complete   [shostak](0.60 s)
    replace_preserv_parallel_pos..........proved - complete   [shostak](1.13 s)
    preserv_unchanged_pos.................proved - complete   [shostak](1.27 s)
    subterm_of_replace_TCC1...............proved - complete   [shostak](0.03 s)
    subterm_of_replace....................proved - complete   [shostak](0.32 s)
    replace_subterm_of_term...............proved - complete   [shostak](0.21 s)
    replace_embedding_TCC1................proved - complete   [shostak](0.05 s)
    replace_embedding.....................proved - complete   [shostak](0.06 s)
    replace_associativity.................proved - complete   [shostak](0.54 s)
    replace_distributivity_TCC1...........proved - complete   [shostak](0.05 s)
    replace_distributivity_TCC2...........proved - complete   [shostak](0.03 s)
    replace_distributivity_TCC3...........proved - complete   [shostak](0.04 s)
    replace_distributivity................proved - complete   [shostak](0.41 s)
    replace_dominance.....................proved - complete   [shostak](0.54 s)
    replace_persistence_TCC1..............proved - complete   [shostak](0.04 s)
    replace_persistence...................proved - complete   [shostak](0.58 s)
    replace_commutativity_TCC1............proved - complete   [shostak](0.04 s)
    replace_commutativity.................proved - complete   [shostak](1.74 s)
    pos_replaces_is_subset................proved - complete   [shostak](0.40 s)
    pos_occ_var_replace...................proved - complete   [shostak](0.23 s)
    pos_occ_var_replace_as_diff...........proved - complete   [shostak](0.74 s)
    Theory totals: 29 formulas, 29 attempted, 29 succeeded (11.78 s)

 Proof summary for theory subterm
    subtermOF_TCC1........................proved - complete   [shostak](0.03 s)
    subtermOF_TCC2........................proved - complete   [shostak](0.71 s)
    subtermOF_TCC3........................proved - complete   [shostak](0.11 s)
    subtermOF_TCC4........................proved - complete   [shostak](0.04 s)
    subtermOF_TCC5........................proved - complete   [shostak](0.04 s)
    pos_vars_subset_pos...................proved - complete   [shostak](0.56 s)
    Pos_var_is_finite.....................proved - complete   [shostak](0.10 s)
    Vars_is_var...........................proved - complete   [shostak](0.07 s)
    vars_term_is_union....................proved - complete   [shostak](0.68 s)
    vars_of_term_finite...................proved - complete   [shostak](0.62 s)
    pos_subterm_ax_TCC1...................proved - complete   [shostak](0.03 s)
    pos_subterm_ax........................proved - complete   [shostak](0.25 s)
    pos_subterm_TCC1......................proved - complete   [shostak](0.02 s)
    pos_subterm...........................proved - complete   [shostak](0.35 s)
    pos_o_term............................proved - complete   [shostak](0.85 s)
    subterm_is_app_TCC1...................proved - complete   [shostak](0.23 s)
    subterm_is_app_TCC2...................proved - complete   [shostak](0.03 s)
    subterm_is_app........................proved - complete   [shostak](0.10 s)
    vars_subterm..........................proved - complete   [shostak](0.05 s)
    disjoint_subterm......................proved - complete   [shostak](0.05 s)
    variable_positions_parallel...........proved - complete   [shostak](0.09 s)
    variable_positions....................proved - complete   [shostak](0.18 s)
    pos_occ_var_HAStypePP_TCC1............proved - complete   [shostak](0.02 s)
    pos_occ_var_HAStypePP.................proved - incomplete [shostak](1.02 s)
    pos_occ_var_HAStypeSP.................proved - incomplete [shostak](0.21 s)
    no_empty_set_positions................proved - complete   [shostak](0.08 s)
    length_seq_var_g0.....................proved - incomplete [shostak](1.31 s)
    subterm_empty_seq_TCC1................proved - complete   [shostak](0.05 s)
    subterm_empty_seq.....................proved - complete   [shostak](0.03 s)
    equal_subterms_equal_term.............proved - complete   [shostak](0.08 s)
    subt_of_subt_is_subt_of_term_TCC1.....proved - complete   [shostak](0.24 s)
    subt_of_subt_is_subt_of_term..........proved - complete   [shostak](0.98 s)
    subterm_to_subtermOF..................proved - complete   [shostak](0.81 s)
    subtermOF_to_subterm..................proved - complete   [shostak](0.19 s)
    subterm_to_subterm....................proved - complete   [shostak](0.13 s)
    comp_of_pos_TCC1......................proved - complete   [shostak](0.02 s)
    comp_of_pos_TCC2......................proved - complete   [shostak](0.02 s)
    n_for_a_pstart........................proved - complete   [shostak](0.02 s)
    length_comp_p.........................proved - complete   [shostak](0.12 s)
    m_neq_n...............................proved - complete   [shostak](0.07 s)
    is_injective_function_inj_TCC1........proved - complete   [shostak](0.14 s)
    is_injective_function_inj.............proved - complete   [shostak](0.07 s)
    infinite_set_of_seq_pos...............proved - complete   [shostak](0.04 s)
    comp_of_pos_is_pos....................proved - complete   [shostak](0.08 s)
    subset_of_seq_pos.....................proved - complete   [shostak](0.04 s)
    term_eq_subterm.......................proved - complete   [shostak](0.05 s)
    app_term..............................proved - complete   [shostak](0.05 s)
    positions_of_a_term...................proved - complete   [shostak](0.62 s)
    equal_app_term........................proved - complete   [shostak](0.06 s)
    equal_term_TCC1.......................proved - complete   [shostak](0.03 s)
    equal_term_TCC2.......................proved - complete   [shostak](0.03 s)
    equal_term............................proved - complete   [shostak](1.30 s)
    Theory totals: 52 formulas, 52 attempted, 52 succeeded (13.11 s)

 Proof summary for theory positions
    positionsOF_TCC1......................proved - complete   [shostak](0.02 s)
    positionsOF_TCC2......................proved - complete   [shostak](0.14 s)
    left_without_children_TCC1............proved - complete   [shostak](0.02 s)
    left_without_children_TCC2............proved - complete   [shostak](0.03 s)
    positions_of_terms_finite.............proved - complete   [shostak](0.33 s)
    empty_pos.............................proved - complete   [shostak](0.11 s)
    closed_positions......................proved - complete   [shostak](0.79 s)
    equal_symbol_equal_length_arg.........proved - complete   [shostak](0.03 s)
    not_var...............................proved - complete   [shostak](0.30 s)
    not_var1..............................proved - complete   [shostak](0.30 s)
    pos_ax................................proved - complete   [shostak](0.03 s)
    rest_of_positions_TCC1................proved - complete   [shostak](0.10 s)
    rest_of_positions_TCC2................proved - complete   [shostak](0.26 s)
    rest_of_positions.....................proved - complete   [shostak](0.09 s)
    delete_is_position_TCC1...............proved - complete   [shostak](0.22 s)
    delete_is_position....................proved - complete   [shostak](0.06 s)
    parallel_comm.........................proved - complete   [shostak](0.02 s)
    rest_parallel.........................proved - complete   [shostak](0.08 s)
    rest_of_PP_is_PP......................proved - complete   [shostak](0.62 s)
    rest_of_SP_is_SP......................proved - complete   [shostak](0.72 s)
    delete_of_PP_is_PP....................proved - complete   [shostak](0.51 s)
    delete_of_SP_is_SP....................proved - complete   [shostak](0.52 s)
    add_first_parallel_pos_to_PP_is_PP....proved - complete   [shostak](0.68 s)
    add_first_parallel_pos_to_SP_is_SP....proved - complete   [shostak](0.39 s)
    add_last_parallel_pos_to_PP_is_PP.....proved - complete   [shostak](0.62 s)
    add_last_parallel_pos_to_SP_is_SP.....proved - complete   [shostak](0.38 s)
    positions_of_arg......................proved - complete   [shostak](0.41 s)
    left_pos_transitive...................proved - complete   [shostak](0.40 s)
    lwc_is_left_pos.......................proved - complete   [shostak](0.03 s)
    lwc_transitive........................proved - complete   [shostak](0.25 s)
    subterm_if_le_arity...................proved - complete   [shostak](0.10 s)
    subterms_acc_arity....................proved - complete   [shostak](0.28 s)
    lwc_add_last_delete_TCC1..............proved - complete   [shostak](0.02 s)
    lwc_add_last_delete_TCC2..............proved - complete   [shostak](0.02 s)
    lwc_add_last_delete...................proved - complete   [shostak](1.22 s)
    lwc_add_last_delete1_TCC1.............proved - complete   [shostak](0.03 s)
    lwc_add_last_delete1_TCC2.............proved - complete   [shostak](0.02 s)
    lwc_add_last_delete1..................proved - complete   [shostak](0.48 s)
    leftmost_pos..........................proved - complete   [shostak](0.23 s)
    Theory totals: 39 formulas, 39 attempted, 39 succeeded (10.88 s)

 Proof summary for theory IUnion_extra
    upto?_TCC1............................proved - complete   [shostak](0.00 s)
    disjoint_subset.......................proved - complete   [shostak](0.02 s)
    disjoint_commute......................proved - complete   [shostak](0.02 s)
    IUnion_of_finite_is_finite............proved - complete   [shostak](0.19 s)
    IUnion_of_finite_is_finite1...........proved - complete   [shostak](0.19 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.42 s)

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

 Proof summary for theory results_commutation
    Local_Comu_and_Noeth..................proved - complete   [shostak](0.40 s)
    commute_and_iterate_one...............proved - complete   [shostak](0.15 s)
    commute_and_iterate_two...............proved - complete   [shostak](0.15 s)
    Comutation_Lemma......................proved - complete   [shostak](0.07 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.77 s)

 Proof summary for theory noetherian
    R_is_Noet_iff_TC_is...................proved - complete   [shostak](0.07 s)
    noetherian_induction..................proved - complete   [shostak](0.05 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.12 s)

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

 Proof summary for theory relations_closure
    RC_TCC1...............................proved - complete   [shostak](0.02 s)
    change_to_RC..........................proved - complete   [shostak](0.00 s)
    R_subset_RC...........................proved - complete   [shostak](0.01 s)
    RC_idempotent.........................proved - complete   [shostak](0.13 s)
    RC_characterization...................proved - complete   [shostak](0.05 s)
    SC_TCC1...............................proved - complete   [shostak](0.03 s)
    change_to_SC..........................proved - complete   [shostak](0.00 s)
    R_subset_SC...........................proved - complete   [shostak](0.01 s)
    SC_idempotent.........................proved - complete   [shostak](0.13 s)
    SC_characterization...................proved - complete   [shostak](0.04 s)
    TC_TCC1...............................proved - complete   [shostak](0.04 s)
    change_to_TC..........................proved - complete   [shostak](0.00 s)
    R_subset_TC...........................proved - complete   [shostak](0.01 s)
    TC_converse...........................proved - complete   [shostak](0.10 s)
    TC_idempotent.........................proved - complete   [shostak](0.13 s)
    TC_characterization...................proved - complete   [shostak](0.04 s)
    RTC_TCC1..............................proved - complete   [shostak](0.05 s)
    change_to_RTC.........................proved - complete   [shostak](0.01 s)
    R_subset_RTC..........................proved - complete   [shostak](0.01 s)
    iterate_RTC...........................proved - complete   [shostak](0.01 s)
    RTC_idempotent........................proved - complete   [shostak](0.14 s)
    RTC_characterization..................proved - complete   [shostak](0.05 s)
    EC_TCC1...............................proved - complete   [shostak](0.12 s)
    change_to_EC..........................proved - complete   [shostak](0.01 s)
    R_subset_EC...........................proved - complete   [shostak](0.06 s)
    RTC_subset_EC.........................proved - complete   [shostak](0.13 s)
    EC_idempotent.........................proved - complete   [shostak](0.12 s)
    EC_characterization...................proved - complete   [shostak](0.05 s)
    Theory totals: 28 formulas, 28 attempted, 28 succeeded (1.52 s)

 Proof summary for theory modulo_equivalence
    van_oostrom94.........................proved - complete   [shostak](0.12 s)
    newman_lemma_general..................proved - complete   [shostak](0.65 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.77 s)

 Proof summary for theory confluence_commute
    RC_RTC_is_RTC.........................proved - complete   [shostak](0.01 s)
    RTC_o_RTC_is_RTC......................proved - complete   [shostak](0.07 s)
    RC_o_RTC_is_RTC.......................proved - complete   [shostak](0.10 s)
    RTC_converse_RTC_R....................proved - complete   [shostak](0.16 s)
    semi_comm_implies_comm................proved - complete   [shostak](0.13 s)
    sub_comm_rtc_implies_conf.............proved - complete   [shostak](0.02 s)
    conf_local_request_implies_request....proved - complete   [shostak](0.15 s)
    comp_rtc_req_conf_impl_diamond........proved - complete   [shostak](0.10 s)
    union_req_conf_is_confluent...........proved - complete   [shostak](0.04 s)
    comp_rtc_confs_req_impl_diamond.......proved - complete   [shostak](0.07 s)
    union_confs_req_is_confluent..........proved - complete   [shostak](0.03 s)
    CR_iff_PP.............................proved - complete   [shostak](0.04 s)
    confluent_iff_postponement............proved - complete   [shostak](0.01 s)
    hip_Hindley_implies_semi_comm.........proved - complete   [shostak](0.36 s)
    lemma_Hindley_1964....................proved - complete   [shostak](0.01 s)
    ref_condition_to_refcomp..............proved - complete   [shostak](0.18 s)
    semi_implies_CR.......................proved - complete   [shostak](0.12 s)
    semi_implies_conf.....................proved - complete   [shostak](0.10 s)
    sub_comm_implies_semi_conf............proved - complete   [shostak](0.16 s)
    sub_comm_implies_conf.................proved - complete   [shostak](0.01 s)
    lemma_Rosen_1973......................proved - complete   [shostak](0.02 s)
    lcomm_and_snunion_implies_comm........proved - complete   [shostak](-.73 s)
    UN_implies_UNseta.....................proved - complete   [shostak](0.04 s)
    Theory totals: 23 formulas, 23 attempted, 23 succeeded (1.19 s)

 Proof summary for theory results_confluence
    Joinable_implies_Equiv................proved - complete   [shostak](0.09 s)
    reduct_transitive.....................proved - complete   [shostak](0.09 s)
    semi_and_iterate......................proved - complete   [shostak](0.21 s)
    Confl_implies_Semi....................proved - complete   [shostak](0.08 s)
    Semi_implies_CR.......................proved - complete   [shostak](0.08 s)
    CR_iff_Confluent......................proved - complete   [shostak](0.12 s)
    strong_and_iterate....................proved - complete   [shostak](0.15 s)
    Str_Confl_implies_Semi_Confl..........proved - complete   [shostak](0.10 s)
    Strong_Confl_implies_Confl............proved - complete   [shostak](0.07 s)
    DP_implies_StC........................proved - complete   [shostak](0.09 s)
    R1_Confl_iff_R2_Confl.................proved - complete   [shostak](0.12 s)
    R1_equal_R2...........................proved - complete   [shostak](0.09 s)
    R2_Str_Confl_implies_R1_Confl.........proved - complete   [shostak](0.07 s)
    Confluence_Commute....................proved - complete   [shostak](0.12 s)
    R1_R2_RTC_R1_R2.......................proved - complete   [shostak](0.18 s)
    Commutative_Union_Lemma...............proved - complete   [shostak](0.09 s)
    Theory totals: 16 formulas, 16 attempted, 16 succeeded (1.77 s)

 Proof summary for theory results_normal_form
    NF_doesnot_rewrite....................proved - complete   [shostak](0.05 s)
    NF_implies_RTC........................proved - complete   [shostak](0.02 s)
    NFs_implies_Equal.....................proved - complete   [shostak](0.02 s)
    Norm_and_Confl_implies_UNF............proved - complete   [shostak](0.03 s)
    Normalizing_and_Confl.................proved - complete   [shostak](0.09 s)
    Normal_Confl_iff_UNF..................proved - complete   [shostak](0.06 s)
    Noetherian_implies_normalizing........proved - complete   [shostak](0.05 s)
    Convergent_UNF........................proved - complete   [shostak](0.01 s)
    Noet_and_Confl_iff_UNF................proved - complete   [shostak](0.01 s)
    Convergent_iff_eqNF...................proved - complete   [shostak](0.07 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.41 s)

 Proof summary for theory newman_yokouchi
    Newman_lemma..........................proved - complete   [shostak](0.29 s)
    Yokouchi_lemma_ax1....................proved - complete   [shostak](0.41 s)
    Yokouchi_lemma........................proved - complete   [shostak](0.49 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (1.20 s)

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

 Proof summary for theory replace_positions
    IMP_substitution_TCC1.................proved - complete   [shostak](0.01 s)
    replace_pos_TCC1......................proved - complete   [shostak](0.45 s)
    replace_pos_TCC2......................proved - complete   [shostak](0.47 s)
    replace_pos_TCC3......................proved - complete   [shostak](1.07 s)
    replace_pos_TCC4......................proved - complete   [shostak](0.78 s)
    replace_pos_is_stable_TCC1............proved - complete   [shostak](0.10 s)
    replace_pos_is_stable.................proved - complete   [shostak](0.33 s)
    preserv_first_position_TCC1...........proved - complete   [shostak](0.11 s)
    preserv_first_position................proved - complete   [shostak](2.58 s)
    preserv_all_parallel_positions........proved - complete   [shostak](1.38 s)
    preserv_all_replaced_positions........proved - complete   [shostak](2.28 s)
    preserv_unchanged_subterms_TCC1.......proved - complete   [shostak](0.09 s)
    preserv_unchanged_subterms............proved - complete   [shostak](1.59 s)
    replace_pos_subterm_to_term_TCC1......proved - complete   [shostak](0.47 s)
    replace_pos_subterm_to_term...........proved - complete   [shostak](1.60 s)
    replace_pos_to_term_TCC1..............proved - complete   [shostak](0.08 s)
    replace_pos_to_term_TCC2..............proved - incomplete [shostak](0.09 s)
    replace_pos_to_term...................proved - incomplete [shostak](0.14 s)
    CP_lemma_aux2a_TCC1...................proved - complete   [shostak](0.10 s)
    CP_lemma_aux2a........................proved - complete   [shostak](2.94 s)
    CP_lemma_aux2a1.......................proved - complete   [shostak](1.26 s)
    CP_lemma_aux2a2_TCC1..................proved - complete   [shostak](0.10 s)
    CP_lemma_aux2a2_TCC2..................proved - complete   [shostak](1.18 s)
    CP_lemma_aux2a2.......................proved - complete   [shostak](3.86 s)
    CP_lemma_aux2a3.......................proved - complete   [shostak](1.56 s)
    Theory totals: 25 formulas, 25 attempted, 25 succeeded (24.59 s)

 Proof summary for theory reduction
    IMP_rewrite_rules_TCC1................proved - complete   [shostak](0.01 s)
    closure_close_subs....................proved - complete   [shostak](0.53 s)
    reduction_is_subs_op..................proved - complete   [shostak](2.41 s)
    lhs_reduces_to_rhs....................proved - complete   [shostak](0.92 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (3.88 s)

 Proof summary for theory unification
    IMP_substitution_TCC1.................proved - complete   [shostak](0.01 s)
    mg_po.................................proved - complete   [shostak](0.12 s)
    uni_diff_equal_length_arg.............proved - complete   [shostak](0.37 s)
    resolving_diff_TCC1...................proved - complete   [shostak](0.18 s)
    resolving_diff_TCC2...................proved - complete   [shostak](0.12 s)
    resolving_diff_TCC3...................proved - complete   [shostak](1.15 s)
    resolving_diff_TCC4...................proved - complete   [shostak](0.80 s)
    resolving_diff_TCC5...................proved - complete   [shostak](0.18 s)
    resolving_diff_TCC6...................proved - complete   [shostak](0.13 s)
    resolving_diff_TCC7...................proved - complete   [shostak](0.85 s)
    resol_diff_nonempty_implies_funct_terms...proved - complete   [shostak](0.15 s)
    resol_diff_to_rest_resol_diff_TCC1....proved - complete   [shostak](0.08 s)
    resol_diff_to_rest_resol_diff_TCC2....proved - complete   [shostak](0.65 s)
    resol_diff_to_rest_resol_diff_TCC3....proved - complete   [shostak](0.66 s)
    resol_diff_to_rest_resol_diff_TCC4....proved - complete   [shostak](0.82 s)
    resol_diff_to_rest_resol_diff.........proved - complete   [shostak](0.50 s)
    position_s_resolving_diff.............proved - complete   [shostak](0.66 s)
    position_t_resolving_diff.............proved - complete   [shostak](0.62 s)
    resolving_diff_has_diff_argument......proved - complete   [shostak](2.07 s)
    resolving_diff_has_unifiable_argument...proved - complete   [shostak](0.67 s)
    resolving_diff_vars...................proved - complete   [shostak](2.09 s)
    unifier_o_TCC1........................proved - complete   [shostak](0.08 s)
    unifier_o.............................proved - complete   [shostak](0.09 s)
    mgu_o_TCC1............................proved - complete   [shostak](0.07 s)
    mgu_o_TCC2............................proved - complete   [shostak](0.07 s)
    mgu_o.................................proved - complete   [shostak](0.09 s)
    unifier_and_subs_TCC1.................proved - complete   [shostak](0.09 s)
    unifier_and_subs......................proved - complete   [shostak](0.09 s)
    idemp_mgu_iff_all_unifier.............proved - complete   [shostak](0.09 s)
    unifiable_terms_unifiable_args........proved - complete   [shostak](0.10 s)
    var_term_unifiable_not_var_in_term_TCC1...proved - complete   [shostak](0.18 s)
    var_term_unifiable_not_var_in_term....proved - complete   [shostak](0.26 s)
    sub_of_frst_diff_TCC1.................proved - complete   [shostak](0.08 s)
    sub_of_frst_diff_TCC2.................proved - complete   [shostak](0.09 s)
    sub_of_frst_diff_TCC3.................proved - complete   [shostak](0.18 s)
    sub_of_frst_diff_TCC4.................proved - complete   [shostak](0.18 s)
    dom_sub_of_frst_diff_is_TCC1..........proved - complete   [shostak](0.08 s)
    dom_sub_of_frst_diff_is...............proved - complete   [shostak](0.33 s)
    var_sub_1stdiff_not_member_term.......proved - complete   [shostak](0.43 s)
    sub_of_frst_diff_unifier_o............proved - complete   [shostak](0.27 s)
    ext_sub_of_frst_diff_unifiable........proved - complete   [shostak](0.11 s)
    sub_of_frst_diff_remove_x.............proved - complete   [shostak](0.13 s)
    vars_sub_of_frst_diff_s_is_subset_union...proved - complete   [shostak](2.26 s)
    vars_sub_of_frst_diff_t_is_subset_union...proved - complete   [shostak](2.35 s)
    union_vars_ext_sub_of_frst_diff.......proved - complete   [shostak](0.28 s)
    vars_ext_sub_of_frst_diff_decrease_TCC1...proved - complete   [shostak](0.10 s)
    vars_ext_sub_of_frst_diff_decrease_TCC2...proved - complete   [shostak](0.10 s)
    vars_ext_sub_of_frst_diff_decrease....proved - complete   [shostak](0.40 s)
    unification_algorithm_TCC1............proved - complete   [shostak](0.09 s)
    unification_algorithm_TCC2............proved - complete   [shostak](0.09 s)
    unification_algorithm_TCC3............proved - complete   [shostak](0.08 s)
    unification_algorithm_TCC4............proved - complete   [shostak](0.08 s)
    unification_algorithm_TCC5............proved - complete   [shostak](0.11 s)
    unification_algorithm_TCC6............proved - complete   [shostak](0.10 s)
    unification_algorithm_TCC7............proved - complete   [shostak](0.07 s)
    unification_algorithm_gives_unifier...proved - complete   [shostak](0.32 s)
    unification_algorithm_gives_mg_subs_TCC1...proved - complete   [shostak](0.19 s)
    unification_algorithm_gives_mg_subs...proved - complete   [shostak](0.53 s)
    unification...........................proved - complete   [shostak](0.08 s)
    Theory totals: 59 formulas, 59 attempted, 59 succeeded (23.25 s)

 Proof summary for theory robinsonunificationEF
    IMP_robinsonunification_TCC1.........proved - complete   [shostak]( 0.01 s)
    IMP_robinsonunification_TCC2.........proved - complete   [shostak]( 0.01 s)
    IMP_robinsonunification_TCC3.........proved - complete   [shostak]( 0.01 s)
    right_pos_TCC1.......................proved - complete   [shostak]( 0.08 s)
    right_pos_TCC2.......................proved - complete   [shostak]( 0.09 s)
    right_pos_TCC3.......................proved - complete   [shostak]( 0.10 s)
    right_pos_TCC4.......................proved - complete   [shostak]( 0.11 s)
    right_pos_TCC5.......................proved - complete   [shostak]( 0.98 s)
    right_pos_TCC6.......................proved - complete   [shostak]( 0.11 s)
    next_position_TCC1...................proved - complete   [shostak]( 0.09 s)
    next_position_TCC2...................proved - complete   [shostak]( 0.09 s)
    next_position_TCC3...................proved - complete   [shostak]( 0.10 s)
    next_position_TCC4...................proved - complete   [shostak]( 0.08 s)
    next_position_TCC5...................proved - complete   [shostak]( 2.07 s)
    next_position_TCC6...................proved - complete   [shostak]( 0.09 s)
    next_position_TCC7...................proved - complete   [shostak]( 0.09 s)
    next_position_TCC8...................proved - complete   [shostak]( 0.09 s)
    next_position_TCC9...................proved - complete   [shostak]( 0.10 s)
    next_position_TCC10..................proved - complete   [shostak]( 2.10 s)
    next_position_TCC11..................proved - complete   [shostak]( 0.10 s)
    next_position_TCC12..................proved - complete   [shostak]( 0.10 s)
    next_position_TCC13..................proved - complete   [shostak]( 0.10 s)
    next_position_TCC14..................proved - complete   [shostak]( 0.10 s)
    next_position_TCC15..................proved - complete   [shostak]( 2.48 s)
    next_position_TCC16..................proved - complete   [shostak]( 0.13 s)
    next_position_TCC17..................proved - complete   [shostak]( 1.46 s)
    next_position_TCC18..................proved - complete   [shostak]( 0.11 s)
    next_position_TCC19..................proved - complete   [shostak]( 0.31 s)
    right_pos_subset.....................proved - complete   [shostak]( 1.56 s)
    next_position_commute................proved - complete   [shostak]( 2.25 s)
    next_position_is_position............proved - complete   [shostak]( 1.86 s)
    next_pos_length_and_last_TCC1........proved - complete   [shostak]( 0.08 s)
    next_pos_length_and_last_TCC2........proved - complete   [shostak]( 0.08 s)
    next_pos_length_and_last.............proved - complete   [shostak]( 3.00 s)
    next_pos_is_a_diff_pos...............proved - complete   [shostak]( 0.09 s)
    member_right_pos.....................proved - complete   [shostak](11.84 s)
    next_pos_member_right_pos............proved - complete   [shostak](10.86 s)
    equal_right_pos......................proved - complete   [shostak]( 3.92 s)
    subset_right_pos.....................proved - complete   [shostak](24.26 s)
    next_pos_to_the_right_TCC1...........proved - complete   [shostak]( 0.11 s)
    next_pos_to_the_right_TCC2...........proved - complete   [shostak]( 0.10 s)
    next_pos_to_the_right................proved - complete   [shostak]( 0.15 s)
    ext_link_remove_x_TCC1...............proved - complete   [shostak]( 0.51 s)
    ext_link_remove_x....................proved - complete   [shostak]( 0.19 s)
    vars_ext_link_s_subset...............proved - complete   [shostak]( 1.66 s)
    vars_ext_link_t_subset...............proved - complete   [shostak]( 1.02 s)
    union_vars_ext_link_subterm..........proved - complete   [shostak]( 0.32 s)
    termination_lemma_subterm_TCC1.......proved - complete   [shostak]( 0.11 s)
    termination_lemma_subterm_TCC2.......proved - complete   [shostak]( 0.10 s)
    termination_lemma_subterm............proved - complete   [shostak]( 0.86 s)
    subtermOF_next_position_TCC1.........proved - complete   [shostak]( 0.09 s)
    subtermOF_next_position_TCC2.........proved - complete   [shostak]( 0.09 s)
    subtermOF_next_position..............proved - complete   [shostak]( 0.23 s)
    np_o_fd_is_position_TCC1.............proved - complete   [shostak]( 0.09 s)
    np_o_fd_is_position..................proved - complete   [shostak]( 0.15 s)
    child_np_child_p.....................proved - complete   [shostak]( 2.49 s)
    next_pos_empty_equal_subterm_TCC1....proved - complete   [shostak]( 0.12 s)
    next_pos_empty_equal_subterm_TCC2....proved - complete   [shostak]( 0.12 s)
    next_pos_empty_equal_subterm.........proved - complete   [shostak]( 8.98 s)
    next_pos_equal_subterm_TCC1..........proved - complete   [shostak]( 0.12 s)
    next_pos_equal_subterm_TCC2..........proved - complete   [shostak]( 0.12 s)
    next_pos_equal_subterm...............proved - complete   [shostak]( 3.28 s)
    fd_equal_subterm.....................proved - complete   [shostak]( 2.54 s)
    child_p_o_fd_TCC1....................proved - complete   [shostak]( 0.09 s)
    child_p_o_fd_TCC2....................proved - complete   [shostak]( 0.09 s)
    child_p_o_fd_TCC3....................proved - complete   [shostak]( 0.13 s)
    child_p_o_fd_TCC4....................proved - complete   [shostak](-0.87 s)
    child_p_o_fd.........................proved - complete   [shostak]( 0.82 s)
    separation_lwc_pos...................proved - complete   [shostak]( 0.20 s)
    lwc_o_fd_empty_seq...................proved - complete   [shostak]( 0.31 s)
    lwc_p_o_fd...........................proved - complete   [shostak]( 2.72 s)
    np_p_o_fd_empty_unifiable_term_TCC1...proved - complete   [shostak]( 0.15 s)
    np_p_o_fd_empty_unifiable_term.......proved - complete   [shostak]( 1.36 s)
    np_p_o_fd_equal_subterm..............proved - complete   [shostak]( 0.78 s)
    robinson_unification_algorithm_aux_TCC1...proved - complete   [shostak]( 0.10 s)
    robinson_unification_algorithm_aux_TCC2...proved - complete   [shostak]( 0.09 s)
    robinson_unification_algorithm_aux_TCC3...proved - complete   [shostak]( 0.09 s)
    robinson_unification_algorithm_aux_TCC4...proved - complete   [shostak]( 0.09 s)
    robinson_unification_algorithm_aux_TCC5...proved - complete   [shostak]( 0.10 s)
    robinson_unification_algorithm_aux_TCC6...proved - complete   [shostak]( 0.08 s)
    robinson_unification_algorithm_aux_TCC7...proved - complete   [shostak]( 0.09 s)
    robinson_unification_algorithm_aux_TCC8...proved - complete   [shostak]( 0.12 s)
    robinson_unification_algorithm_aux_TCC9...proved - complete   [shostak]( 0.08 s)
    robinson_unification_algorithm_aux_TCC10...proved - complete   [shostak]( 0.16 s)
    robinson_unification_algorithm_aux_TCC11...proved - complete   [shostak]( 0.17 s)
    robinson_unification_algorithm_aux_TCC12...proved - complete   [shostak]( 0.16 s)
    robinson_unification_algorithm_aux_TCC13...proved - complete   [shostak]( 0.08 s)
    robinson_unification_algorithm_aux_TCC14...proved - complete   [shostak]( 0.54 s)
    robinson_unification_algorithm_EF_TCC1...proved - complete   [shostak]( 0.14 s)
    unifiable_implies_not_fail1..........proved - complete   [shostak]( 1.74 s)
    preserving_generality1...............proved - complete   [shostak]( 0.50 s)
    unifiable_preserves_unifiability1....proved - complete   [shostak]( 0.18 s)
    dom_ruaEF_subset_union_vars_aux......proved - complete   [shostak]( 1.59 s)
    dom_ruaEF_subset_union_vars..........proved - complete   [shostak]( 0.10 s)
    vran_ruaEF_subset_union_aux_TCC1.....proved - complete   [shostak]( 0.16 s)
    vran_ruaEF_subset_union_aux_TCC2.....proved - complete   [shostak]( 0.14 s)
    vran_ruaEF_subset_union_aux..........proved - complete   [shostak]( 0.77 s)
    dom_ran_ruaEF_disjoint...............proved - complete   [shostak]( 2.67 s)
    ruaEF_fails_iff_non_unifiable_aux_TCC1...proved - complete   [shostak]( 0.09 s)
    ruaEF_fails_iff_non_unifiable_aux_TCC2...proved - complete   [shostak]( 0.10 s)
    ruaEF_fails_iff_non_unifiable_aux....proved - complete   [shostak]( 1.92 s)
    ruaEF_gives_unifier_aux..............proved - complete   [shostak]( 2.57 s)
    ruaEF_gives_mg_subs_aux..............proved - complete   [shostak]( 2.59 s)
    ruaEF_fails_iff_non_unifiable........proved - complete   [shostak]( 0.22 s)
    ruaEF_gives_unifier..................proved - complete   [shostak]( 0.24 s)
    ruaEF_gives_mg_subs..................proved - complete   [shostak]( 0.16 s)
    completeness_ruaEF...................proved - complete   [shostak]( 0.10 s)
    Theory totals: 107 formulas, 107 attempted, 107 succeeded (118.37 s)

 Proof summary for theory robinsonunification
    IMP_unification_TCC1..................proved - complete   [shostak](0.01 s)
    xx_TCC1...............................proved - complete   [shostak](0.09 s)
    ff_TCC1...............................proved - complete   [shostak](0.08 s)
    fail_TCC1.............................proved - complete   [shostak](0.09 s)
    fail_TCC2.............................proved - complete   [shostak](0.22 s)
    first_diff_TCC1.......................proved - complete   [shostak](0.14 s)
    first_diff_TCC2.......................proved - complete   [shostak](0.14 s)
    first_diff_TCC3.......................proved - complete   [shostak](0.14 s)
    first_diff_TCC4.......................proved - complete   [shostak](0.74 s)
    first_diff_TCC5.......................proved - complete   [shostak](0.14 s)
    first_diff_TCC6.......................proved - complete   [shostak](0.13 s)
    first_diff_TCC7.......................proved - complete   [shostak](0.77 s)
    comutative_first_diff_TCC1............proved - complete   [shostak](0.09 s)
    comutative_first_diff.................proved - complete   [shostak](2.47 s)
    position_s_first_diff.................proved - complete   [shostak](0.67 s)
    position_t_first_diff.................proved - complete   [shostak](0.09 s)
    first_diff_has_diff_argument_TCC1.....proved - complete   [shostak](0.08 s)
    first_diff_has_diff_argument_TCC2.....proved - complete   [shostak](0.08 s)
    first_diff_has_diff_argument..........proved - complete   [shostak](0.88 s)
    first_diff_unifiable_vars.............proved - complete   [shostak](0.19 s)
    fd_equal_symbol_TCC1..................proved - complete   [shostak](0.10 s)
    fd_equal_symbol_TCC2..................proved - complete   [shostak](0.10 s)
    fd_equal_symbol.......................proved - complete   [shostak](4.26 s)
    link_of_frst_diff_TCC1................proved - complete   [shostak](0.10 s)
    link_of_frst_diff_TCC2................proved - complete   [shostak](0.18 s)
    link_of_frst_diff_TCC3................proved - complete   [shostak](0.55 s)
    link_of_frst_diff_TCC4................proved - complete   [shostak](0.18 s)
    dom_link_of_frst_diff_is..............proved - complete   [shostak](0.53 s)
    dom_ran_link_disjoint.................proved - complete   [shostak](0.34 s)
    link_remove_x.........................proved - complete   [shostak](0.17 s)
    link_of_frst_diff_s_is_subset_union...proved - complete   [shostak](1.46 s)
    comutative_link_fd....................proved - complete   [shostak](0.14 s)
    link_of_frst_diff_t_is_subset_union...proved - complete   [shostak](0.89 s)
    union_vars_ext_link...................proved - complete   [shostak](0.30 s)
    termination_lemma_TCC1................proved - complete   [shostak](0.12 s)
    termination_lemma_TCC2................proved - complete   [shostak](0.11 s)
    termination_lemma.....................proved - complete   [shostak](1.23 s)
    unifiable_implies_not_fail............proved - complete   [shostak](1.35 s)
    preserving_generality.................proved - complete   [shostak](0.31 s)
    unifiable_preserves_unifiability......proved - complete   [shostak](0.13 s)
    robinson_unification_algorithm_TCC1...proved - complete   [shostak](0.11 s)
    robinson_unification_algorithm_TCC2...proved - complete   [shostak](0.11 s)
    robinson_unification_algorithm_TCC3...proved - complete   [shostak](0.08 s)
    robinson_unification_algorithm_TCC4...proved - complete   [shostak](0.13 s)
    robinson_unification_algorithm_TCC5...proved - complete   [shostak](0.10 s)
    robinson_unification_algorithm_TCC6...proved - complete   [shostak](0.09 s)
    var_ext_term_exists_var_term..........proved - complete   [shostak](1.89 s)
    rob_uni_alg_dom_subset_union_vars.....proved - complete   [shostak](0.67 s)
    rob_uni_alg_vran_subset_union.........proved - complete   [shostak](0.48 s)
    rob_uni_alg_dom_ran_disjoint..........proved - complete   [shostak](1.17 s)
    robinson_unification_algorithm_fails_iff_non_unifiable...proved - complete   [shostak](0.63 s)
    robinson_unification_algorithm_gives_unifier...proved - complete   [shostak](0.39 s)
    robinson_unification_algorithm_gives_mg_subs...proved - complete   [shostak](0.70 s)
    completeness_robinson_unification_algorithm...proved - complete   [shostak](0.11 s)
    Theory totals: 54 formulas, 54 attempted, 54 succeeded (26.43 s)

 Proof summary for theory orthogonality
    IMP_critical_pairs_TCC1..............proved - complete   [shostak]( 0.01 s)
    ntCP?_TCC1...........................proved - complete   [shostak]( 0.07 s)
    ntCP_lemma_aux1_TCC1.................proved - complete   [shostak]( 0.06 s)
    ntCP_lemma_aux1......................proved - complete   [shostak]( 1.50 s)
    linear?_TCC1.........................proved - complete   [shostak]( 0.06 s)
    Orth_lemma_aux0_TCC1.................proved - complete   [shostak]( 0.05 s)
    Orth_lemma_aux0......................proved - complete   [shostak]( 0.10 s)
    equality_replaceTerm.................proved - complete   [shostak]( 0.07 s)
    Var_occurs_only_once_also_in_subterms_TCC1...proved - complete   [shostak]( 0.08 s)
    Var_occurs_only_once_also_in_subterms_TCC2...proved - complete   [shostak]( 0.07 s)
    Var_occurs_only_once_also_in_subterms...proved - complete   [shostak]( 2.59 s)
    SigmaP_equivalence_TCC1..............proved - complete   [shostak]( 0.07 s)
    SigmaP_equivalence_TCC2..............proved - complete   [shostak]( 0.07 s)
    SigmaP_equivalence...................proved - complete   [shostak]( 1.73 s)
    SigmaP_vs_replaceTerm_linearR_TCC1...proved - complete   [shostak]( 0.06 s)
    SigmaP_vs_replaceTerm_linearR_TCC2...proved - complete   [shostak]( 0.07 s)
    SigmaP_vs_replaceTerm_linearR_TCC3...proved - complete   [shostak]( 0.22 s)
    SigmaP_vs_replaceTerm_linearR........proved - complete   [shostak]( 3.77 s)
    Orth_lemma_aux.......................proved - complete   [shostak]( 3.36 s)
    Linear_and_Non_ambiguous_implies_triangle...proved - complete   [shostak]( 2.71 s)
    Triangle_implies_conflent............proved - complete   [shostak]( 0.43 s)
    Linear_and_Non_ambiguous_implies_confluent...proved - complete   [shostak]( 0.05 s)
    replace_par_pos_TCC1.................proved - complete   [shostak](-0.38 s)
    replace_par_pos_TCC2.................proved - complete   [shostak]( 0.64 s)
    replace_par_pos_TCC3.................proved - complete   [shostak]( 0.64 s)
    replace_par_pos_TCC4.................proved - complete   [shostak]( 0.32 s)
    replace_par_pos_TCC5.................proved - complete   [shostak]( 1.10 s)
    replace_par_pos_TCC6.................proved - complete   [shostak]( 0.05 s)
    sigma_rhs_TCC1.......................proved - complete   [shostak]( 0.81 s)
    subtermsOF_TCC1......................proved - complete   [shostak]( 0.07 s)
    parallel_reduction_fix?_TCC1.........proved - complete   [shostak]( 1.12 s)
    parallel_reduction_fix?_TCC2.........proved - complete   [shostak]( 1.10 s)
    parallel_reduction_fix?_TCC3.........proved - complete   [shostak]( 0.06 s)
    sub_pos_TCC1.........................proved - complete   [shostak]( 0.31 s)
    sub_pos_TCC2.........................proved - complete   [shostak]( 0.04 s)
    sub_pos_TCC3.........................proved - complete   [shostak]( 0.75 s)
    sub_pos_TCC4.........................proved - complete   [shostak]( 0.05 s)
    sub_pos_TCC5.........................proved - complete   [shostak]( 0.73 s)
    Pos_Over_TCC1........................proved - complete   [shostak]( 0.05 s)
    Pos_Over_TCC2........................proved - complete   [shostak]( 0.13 s)
    Pos_Over_TCC3........................proved - complete   [shostak]( 0.04 s)
    Pos_Over_TCC4........................proved - complete   [shostak]( 1.14 s)
    Pos_Under_TCC1.......................proved - complete   [shostak]( 0.31 s)
    Pos_Under_TCC2.......................proved - complete   [shostak]( 0.04 s)
    Pos_Under_TCC3.......................proved - complete   [shostak]( 0.12 s)
    Pos_Equal_TCC1.......................proved - complete   [shostak]( 0.04 s)
    Pos_Equal_TCC2.......................proved - complete   [shostak]( 0.05 s)
    Pos_Equal_TCC3.......................proved - complete   [shostak]( 0.05 s)
    Pos_Equal_TCC4.......................proved - complete   [shostak]( 0.05 s)
    comp_SPP_commute.....................proved - complete   [shostak]( 0.48 s)
    sub_pos_element......................proved - complete   [shostak]( 0.54 s)
    parallel_pos_are_dif.................proved - complete   [shostak]( 0.11 s)
    same_pos_in_Pos_Equal................proved - complete   [shostak]( 0.33 s)
    Pos_Over_is_sub_seq..................proved - complete   [shostak]( 0.24 s)
    Pos_Equal_is_sub_seq.................proved - complete   [shostak]( 0.20 s)
    sub_pos_is_sub_seq...................proved - complete   [shostak]( 0.20 s)
    Pos_Under_is_sub_seq.................proved - complete   [shostak]( 0.19 s)
    Pos_Over_is_PP.......................proved - complete   [shostak]( 0.42 s)
    Pos_Over_is_SPP_TCC1.................proved - complete   [shostak]( 0.64 s)
    Pos_Over_is_SPP_TCC2.................proved - complete   [shostak]( 0.64 s)
    Pos_Over_is_SPP......................proved - complete   [shostak]( 0.19 s)
    pos_up_in_Pos_Over...................proved - complete   [shostak]( 0.39 s)
    parallel_pos_in_Pos_Over.............proved - complete   [shostak]( 0.37 s)
    sub_pos_in_Pos_Under_aux.............proved - complete   [shostak]( 0.31 s)
    sub_pos_in_Pos_Under.................proved - complete   [shostak]( 0.29 s)
    sub_pos_is_under.....................proved - complete   [shostak]( 0.22 s)
    sub_pos_is_PP........................proved - complete   [shostak]( 0.35 s)
    sub_pos_is_SPP_TCC1..................proved - complete   [shostak]( 0.63 s)
    sub_pos_is_SPP.......................proved - complete   [shostak]( 0.18 s)
    Pos_Under_character..................proved - complete   [shostak]( 0.28 s)
    union_positions......................proved - complete   [shostak]( 0.29 s)
    sigma_rhs_rest_TCC1..................proved - complete   [shostak]( 0.95 s)
    sigma_rhs_rest.......................proved - complete   [shostak]( 1.74 s)
    sigma_rhs_o_TCC1.....................proved - complete   [shostak]( 1.01 s)
    sigma_rhs_o..........................proved - complete   [shostak]( 1.50 s)
    subtermsOF_rest_TCC1.................proved - complete   [shostak]( 0.06 s)
    subtermsOF_rest......................proved - complete   [shostak]( 0.50 s)
    parallel_reduction_inclusion.........proved - complete   [shostak]( 3.96 s)
    parallel_reduction_RTC...............proved - complete   [shostak]( 0.24 s)
    replace_par_pos_preservs_pos_TCC1....proved - complete   [shostak]( 0.08 s)
    replace_par_pos_preservs_pos.........proved - complete   [shostak]( 2.39 s)
    replace_par_pos_preservs_PP..........proved - complete   [shostak]( 1.95 s)
    replace_par_pos_preservs_PP_o_PP_TCC1...proved - complete   [shostak]( 0.28 s)
    replace_par_pos_preservs_PP_o_PP.....proved - complete   [shostak]( 3.67 s)
    replace_par_pos_equivalence_TCC1.....proved - complete   [shostak]( 0.63 s)
    replace_par_pos_equivalence_TCC2.....proved - complete   [shostak]( 0.63 s)
    replace_par_pos_equivalence_TCC3.....proved - complete   [shostak]( 0.65 s)
    replace_par_pos_equivalence_TCC4.....proved - complete   [shostak]( 0.25 s)
    replace_par_pos_equivalence_TCC5.....proved - complete   [shostak]( 1.09 s)
    replace_par_pos_equivalence_TCC6.....proved - complete   [shostak]( 4.73 s)
    replace_par_pos_equivalence_TCC7.....proved - complete   [shostak]( 1.37 s)
    replace_par_pos_equivalence..........proved - complete   [shostak]( 2.65 s)
    replace_par_pos_equivalence1_TCC1....proved - complete   [shostak]( 0.64 s)
    replace_par_pos_equivalence1_TCC2....proved - complete   [shostak]( 0.65 s)
    replace_par_pos_equivalence1_TCC3....proved - complete   [shostak]( 0.24 s)
    replace_par_pos_equivalence1_TCC4....proved - complete   [shostak]( 0.86 s)
    replace_par_pos_equivalence1.........proved - complete   [shostak]( 3.79 s)
    replace_par_pos_preservs_subterm_TCC1...proved - complete   [shostak]( 0.05 s)
    replace_par_pos_preservs_subterm_TCC2...proved - complete   [shostak]( 0.14 s)
    replace_par_pos_preservs_subterm.....proved - complete   [shostak]( 3.07 s)
    replace_par_pos_subterm_TCC1.........proved - complete   [shostak]( 0.05 s)
    replace_par_pos_subterm_TCC2.........proved - complete   [shostak]( 0.64 s)
    replace_par_pos_subterm..............proved - complete   [shostak]( 2.17 s)
    replace_par_pos_comp_TCC1............proved - complete   [shostak]( 0.68 s)
    replace_par_pos_comp_TCC2............proved - complete   [shostak]( 0.27 s)
    replace_par_pos_comp_TCC3............proved - complete   [shostak]( 1.47 s)
    replace_par_pos_comp.................proved - complete   [shostak]( 3.92 s)
    replace_par_pos_comp_commute_TCC1....proved - complete   [shostak]( 0.06 s)
    replace_par_pos_comp_commute_TCC2....proved - complete   [shostak]( 0.68 s)
    replace_par_pos_comp_commute.........proved - complete   [shostak]( 2.87 s)
    complement_pos_TCC1..................proved - complete   [shostak]( 0.05 s)
    complement_pos_TCC2..................proved - complete   [shostak]( 0.78 s)
    complement_pos_TCC3..................proved - complete   [shostak]( 0.04 s)
    complement_pos_TCC4..................proved - complete   [shostak]( 0.78 s)
    parallel_pos_same_prefix.............proved - complete   [shostak]( 0.26 s)
    complement_pos_character.............proved - complete   [shostak]( 0.40 s)
    complement_pos_is_PP.................proved - complete   [shostak]( 0.33 s)
    complement_pos_preservs_sub_pos_length1...proved - complete   [shostak]( 0.25 s)
    complement_pos_empty_TCC1............proved - complete   [shostak]( 0.06 s)
    complement_pos_empty.................proved - complete   [shostak]( 0.62 s)
    comp_preservs_parallel_pos...........proved - complete   [shostak]( 1.47 s)
    comp_preservs_parallel_pos2..........proved - complete   [shostak]( 0.98 s)
    comp_preservs_parallel_pos3..........proved - complete   [shostak]( 0.07 s)
    comp_pos_rest........................proved - complete   [shostak]( 0.83 s)
    comp_pos_preservs_length.............proved - complete   [shostak]( 0.07 s)
    comp_pos_character_TCC1..............proved - complete   [shostak]( 0.05 s)
    comp_pos_character...................proved - complete   [shostak]( 0.05 s)
    comp_pos_is_PP.......................proved - complete   [shostak]( 0.09 s)
    replace_replace_par_pos_TCC1.........proved - complete   [shostak]( 0.09 s)
    replace_replace_par_pos_TCC2.........proved - complete   [shostak]( 0.63 s)
    replace_replace_par_pos..............proved - complete   [shostak]( 2.39 s)
    complement_pos_preservs_sub_pos_length_TCC1...proved - complete   [shostak]( 0.04 s)
    complement_pos_preservs_sub_pos_length...proved - complete   [shostak]( 6.87 s)
    Pos_Over_character...................proved - complete   [shostak]( 0.43 s)
    Pos_Equal_character..................proved - complete   [shostak]( 0.29 s)
    Pos_Equal_is_PP......................proved - complete   [shostak]( 0.33 s)
    Pos_Over_and_Pos_Equal_is_PP.........proved - complete   [shostak]( 6.34 s)
    comp_pos_in_SP_preservs_SP_in_replace_TCC1...proved - complete   [shostak]( 0.63 s)
    comp_pos_in_SP_preservs_SP_in_replace_TCC2...proved - complete   [shostak]( 0.92 s)
    comp_pos_in_SP_preservs_SP_in_replace...proved - complete   [shostak]( 0.35 s)
    comp_pos_in_PP_preservs_PP_TCC1......proved - complete   [shostak]( 0.31 s)
    comp_pos_in_PP_preservs_PP...........proved - complete   [shostak]( 0.64 s)
    comp_pos_in_SPP_preservs_SPP_in_replace_TCC1...proved - complete   [shostak](-0.42 s)
    comp_pos_in_SPP_preservs_SPP_in_replace_TCC2...proved - complete   [shostak]( 0.93 s)
    comp_pos_in_SPP_preservs_SPP_in_replace...proved - complete   [shostak]( 0.06 s)
    comp_pos_in_SPP_preservs_SPP_in_replace_par_pos_TCC1...proved - complete   [shostak]( 0.63 s)
    comp_pos_in_SPP_preservs_SPP_in_replace_par_pos_TCC2...proved - complete   [shostak]( 0.63 s)
    comp_pos_in_SPP_preservs_SPP_in_replace_par_pos_TCC3...proved - complete   [shostak]( 1.21 s)
    comp_pos_in_SPP_preservs_SPP_in_replace_par_pos...proved - complete   [shostak]( 0.96 s)
    parallel_reduction_reflexive.........proved - complete   [shostak]( 0.16 s)
    non_ambiguous_implies_same_term......proved - complete   [shostak]( 0.31 s)
    parallel_reduction_context_aux2_TCC1...proved - complete   [shostak]( 0.63 s)
    parallel_reduction_context_aux2......proved - complete   [shostak]( 7.82 s)
    parallel_reduction_context...........proved - complete   [shostak]( 0.08 s)
    replace_par_pos_of_app_is_app........proved - complete   [shostak]( 1.96 s)
    replace_par_pos_preservs_f_TCC1......proved - complete   [shostak]( 0.06 s)
    replace_par_pos_preservs_f...........proved - complete   [shostak]( 1.96 s)
    parallel_reduction_closed_subs.......proved - complete   [shostak]( 2.63 s)
    parallel_reduction_result............proved - complete   [shostak]( 3.65 s)
    replace_par_pos_subterm2_TCC1........proved - complete   [shostak]( 0.06 s)
    replace_par_pos_subterm2_TCC2........proved - complete   [shostak]( 0.10 s)
    replace_par_pos_subterm2_TCC3........proved - complete   [shostak]( 0.09 s)
    replace_par_pos_subterm2_TCC4........proved - complete   [shostak]( 0.11 s)
    replace_par_pos_subterm2_TCC5........proved - complete   [shostak]( 0.05 s)
    replace_par_pos_subterm2.............proved - complete   [shostak](10.17 s)
    D_TCC1...............................proved - complete   [shostak]( 0.09 s)
    G_TCC1...............................proved - complete   [shostak]( 0.08 s)
    parallel_reduction_variables.........proved - complete   [shostak]( 3.77 s)
    Parallel_Moves_Lemma.................proved - complete   [shostak]( 0.83 s)
    replace_par_pos_dominance_TCC1.......proved - complete   [shostak]( 1.12 s)
    replace_par_pos_dominance_TCC2.......proved - complete   [shostak]( 1.28 s)
    replace_par_pos_dominance............proved - complete   [shostak]( 3.84 s)
    Pos_Over_and_Pos_Equal_dominance.....proved - complete   [shostak]( 0.57 s)
    divergence_in_Pos_Over_aux_TCC1......proved - complete   [shostak]( 0.07 s)
    divergence_in_Pos_Over_aux_TCC2......proved - complete   [shostak]( 0.18 s)
    divergence_in_Pos_Over_aux_TCC3......proved - complete   [shostak]( 0.12 s)
    divergence_in_Pos_Over_aux...........proved - complete   [shostak](11.87 s)
    divergence_in_Pos_Over_TCC1..........proved - complete   [shostak]( 0.12 s)
    divergence_in_Pos_Over_TCC2..........proved - complete   [shostak]( 0.14 s)
    divergence_in_Pos_Over_TCC3..........proved - complete   [shostak]( 0.19 s)
    divergence_in_Pos_Over...............proved - complete   [shostak]( 0.70 s)
    subterm_joinability_TCC1.............proved - complete   [shostak]( 0.59 s)
    subterm_joinability_TCC2.............proved - complete   [shostak]( 0.60 s)
    subterm_joinability..................proved - complete   [shostak]( 3.42 s)
    subterms_joinability_TCC1............proved - complete   [shostak](-1.04 s)
    subterms_joinability_TCC2............proved - complete   [shostak]( 0.09 s)
    subterms_joinability.................proved - complete   [shostak]( 0.97 s)
    parallel_reduction_has_DP............proved - complete   [shostak]( 1.36 s)
    Orthogonal_implies_confluent.........proved - complete   [shostak]( 0.09 s)
--> --------------------

--> maximum size reached

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

[ Verzeichnis aufwärts0.224unsichere Verbindung  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


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