|
|
|
|
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
]
|
|
|
|
|
|
