|
%%-------------------** 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
%%
%%----------------------------------------------------------------------------
rewrite_rules[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 substitution[variable,symbol, arity]
l, r: VAR term
rho: VAR Ren
%%%% Defining rewriting rules in agreement with Baader and Terese %%%%%%%%%%%%
rewrite_rule?(l,r): bool = (NOT vars?(l)) & subset?(Vars(r), Vars(l))
rewrite_rule: TYPE = (rewrite_rule?)
ren_rewrite: LEMMA rewrite_rule?(l,r) => rewrite_rule?(ext(rho)(l),ext(rho)(r))
%%%% A subset of rewrite rules %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
E: VAR set[rewrite_rule]
e: VAR rewrite_rule
lhs(e): term = e`1
rhs(e): term = e`2
END rewrite_rules
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
