Spracherkennung für: .dep vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
/top,trs,variables_term,term,critical_pairs,critical_pairs_aux,rewrite_rules,substitution,compatibility,replacement,subterm,positions,IUnion_extra,ars,results_commutation,noetherian,ars_terminology,relations_closure,modulo_equivalence,confluence_commute,results_confluence,results_normal_form,newman_yokouchi,extending_rename,replace_positions,reduction,unification,robinsonunificationEF,robinsonunification,orthogonality,mem_test
structures/set2seq,sort_array,permutations,min_array_def,min_seq,sort_seq,seq2set,max_array_def,below_arrays,seqs,sort_seq_lems,seq_extras,max_seq,permutations_seq,sort_array_def
sets_aux/card_comp_set_props,countable_props,countability,infinite_nat_def,card_comp_set
orders/relations_extra,lattices,bounded_orders,minmax_orders,bounded_integers,chain_chain,set_antisymmetric,ordered_subset,monotone_sequences,relation_iterate,skolemization,integer_enumerations,zorn,total_lattices,non_empty_bounded_sets,well_foundedness,upper_semilattices,bounded_sets,chain,indexed_sets_extra,set_dichotomous,lower_semilattices,subset_chain,closure_ops
finite_sets/func_composition,finite_sets_minmax,finite_sets_inductions,finite_sets_card_eq,finite_sets_below
top:trs,robinsonunificationEF,orthogonality
trs:variables_term,sets_aux@countability,sets_aux@countable_props,critical_pairs
variables_term:term
term:
critical_pairs:variables_term,sets_aux@countability,sets_aux@countable_props,critical_pairs_aux,reduction,unification
critical_pairs_aux:variables_term,sets_aux@countability,sets_aux@countable_props,rewrite_rules,replace_positions
rewrite_rules:variables_term,sets_aux@countability,sets_aux@countable_props,substitution
substitution:compatibility,sets_aux@countability,sets_aux@countable_props,extending_rename
compatibility:replacement,ars
replacement:subterm
subterm:positions,IUnion_extra,sets_aux@infinite_nat_def
positions:IUnion_extra,variables_term,structures@seq_extras
IUnion_extra:
ars:results_commutation,modulo_equivalence,confluence_commute,results_normal_form,newman_yokouchi
results_commutation:noetherian
noetherian:ars_terminology,orders@well_foundedness
ars_terminology:relations_closure
relations_closure:orders@closure_ops
modulo_equivalence:noetherian
confluence_commute:noetherian,results_confluence
results_confluence:ars_terminology
results_normal_form:results_confluence,noetherian
newman_yokouchi:results_confluence,noetherian
extending_rename:
replace_positions:variables_term,sets_aux@countability,sets_aux@countable_props,substitution
reduction:variables_term,sets_aux@countability,sets_aux@countable_props,rewrite_rules
unification:variables_term,sets_aux@countability,sets_aux@countable_props,substitution
robinsonunificationEF:variables_term,sets_aux@countability,sets_aux@countable_props,robinsonunification
robinsonunification:variables_term,sets_aux@countability,sets_aux@countable_props,unification
orthogonality:variables_term,sets_aux@countability,sets_aux@countable_props,critical_pairs,mem_test
mem_test:structures@seq_extras,structures@seq2set
