|
%%-------------------** 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
%%
%%----------------------------------------------------------------------------
replace_positions[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]
s, t, t1, t2: VAR term
sig, delta, alpha: VAR Sub
x: VAR (V)
f: VAR symbol
args: VAR finite_sequence[term]
%%%% Definition: replacing all subterms of s occurring in a sequence of %%%%%%%
%%%% parallel positions by t. %%%%%%%
replace_pos(s, t, (fssp:SPP(s)) ): RECURSIVE term =
IF length(fssp) = 0
THEN
s
ELSE
replace_pos(replaceTerm(s, t, fssp(0)), t, rest(fssp))
ENDIF
MEASURE length(fssp)
%%%% Properties %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% compatibility with substitution
replace_pos_is_stable: LEMMA
FORALL t, s, (fss: SPP(s)), sig:
ext(sig)(replace_pos(s, t, fss)) = replace_pos(ext(sig)(s),ext(sig)(t),fss)
% Preserves first replaced position
preserv_first_position: LEMMA
FORALL t, s, (fss: SPP(s)), (q: positions?(s)):
(FORALL (i: below[length(fss)]): parallel(fss(i),q))
=>
positionsOF(replace_pos(s, t, add_first(q, fss)))(q)
% Preserves all parallel positions
preserv_all_parallel_positions: LEMMA
FORALL t, s, (fss: SPP(s)), (q: positions?(s)):
(FORALL (i: below[length(fss)]): parallel(fss(i),q))
=>
positionsOF(replace_pos(s, t, fss))(q)
% Preserves all replaced positions
preserv_all_replaced_positions: LEMMA
FORALL t, s, (fssp: SPP(s)), (i: below[fssp`length]):
positionsOF(replace_pos(s, t, fssp))(fssp(i))
% preserves unchanged subterms
preserv_unchanged_subterms: LEMMA
FORALL t, s, (fss: SPP(s)), (q: positions?(s)):
(FORALL (i: below[length(fss)]): parallel(fss(i),q))
=>
subtermOF(replace_pos(s, t, fss), q) = subtermOF(s, q)
replace_pos_subterm_to_term: LEMMA
FORALL t, s, (fss: SPP(s)):
(FORALL (i: below[length(fss)]): subtermOF(s, fss(i)) = t)
IMPLIES replace_pos(s, t, fss) = s
replace_pos_to_term : LEMMA replace_pos(s, x, set2seq(Pos_var(s, x))) = s
CP_lemma_aux2a: LEMMA
FORALL t, s, (fss: SPP(s)), (q: positions?(s)):
(FORALL (i: below[length(fss)]): parallel(fss(i),q))
=>
replace_pos(s, t, add_last(fss,q)) = replaceTerm(replace_pos(s, t, fss), t, q)
CP_lemma_aux2a1: LEMMA
FORALL t, s, (fss: SPP(s)), (q: positions?(s)):
(FORALL (i: below[length(fss)]): parallel(fss(i),q))
=>
replace_pos(s, t, add_first(q, fss)) = replaceTerm(replace_pos(s, t, fss), t, q)
CP_lemma_aux2a2: LEMMA
FORALL t, s, (fss: SPP(s)), (i: below[length(fss)]):
replace_pos(s, t, fss) =
replaceTerm(replace_pos(s, t, delete(fss,i)), t, fss(i))
CP_lemma_aux2a3: LEMMA
FORALL t, s, (fss1, fss2: SPP(s)):
equivalent(fss1, fss2)
=>
replace_pos(s, t, fss1) = replace_pos(s, t, fss2)
END replace_positions
¤ Dauer der Verarbeitung: 0.16 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.
|
