| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/TRS/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle replace_positions.pvs Sprache: PVS |
|||||||||
|
%%-------------------** 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.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28