|
%%-------------------** Term Rewriting System (TRS) **------------------------
%%
%% Authors : Andre Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% and
%%
%% Mauricio Ayala Rincon
%% Universidade de Brasília - Brasil
%%
%% Last Modified On: September 29, 2009
%%
%%----------------------------------------------------------------------------
reduction[variable: TYPE+, symbol: TYPE+, arity: [symbol -> nat]]: THEORY
BEGIN
ASSUMING
IMPORTING variables_term[variable,symbol, arity],
sets_aux@countability[term],
sets_aux@countable_props[term]
var_countable: ASSUMPTION is_countably_infinite(V)
ENDASSUMING
IMPORTING rewrite_rules[variable,symbol, arity]
s, t, t1, t2: VAR term
sigma, sg1, sg2: VAR Sub
x: VAR (V)
R: VAR pred[[term, term]]
E: VAR set[rewrite_rule]
e: VAR rewrite_rule
%%%% Defining, respectively, the concepts Reduction relation and closed under %%
%%%% substitutions,Close under substitution %%
reduction?(E)(s,t): bool =
EXISTS ( (e | member(e, E)), sigma, (p: positions?(s))):
subtermOF(s, p) = ext(sigma)(lhs(e)) &
t = replaceTerm(s, ext(sigma)(rhs(e)), p)
close_subs?(R): bool = FORALL s, t, sigma: R(s,t) =>
R(ext(sigma)(s),ext(sigma)(t))
%%%% Properties %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
closure_close_subs: LEMMA close_subs?(R) =>
(close_subs?(TC(R)) & close_subs?(RTC(R)) & close_subs?(EC(R)))
reduction_is_subs_op: LEMMA close_subs?(reduction?(E)) & comp_op?(reduction?(E))
lhs_reduces_to_rhs: LEMMA
FORALL (E, (e | member(e, E))): reduction?(E)(lhs(e), rhs(e))
END reduction
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
