| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/TRS/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 4 kB |
|
Quelle replacement.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 %% %%---------------------------------------------------------------------------- replacement[variable: TYPE+, symbol: TYPE+, arity: [symbol -> nat]]: THEORY BEGIN IMPORTING subterm[variable,symbol, arity] p, q, p1, p2, q1: VAR position s, r, t: VAR term i: VAR posnat fs: VAR finseq[term] x, y: VAR (V) %%%% Definition: replacing the subterm of s at position p by t %%%%%%%%%%%%%%% replaceTerm(s: term, t: term, (p: positions?(s))): RECURSIVE term = (IF length(p) = 0 THEN t ELSE LET st = args(s), i = first(p), q = rest(p), rst = replace(replaceTerm(st(i-1), t, q), st,i-1) IN app(f(s), rst) ENDIF) MEASURE length(p) %%%% Properties %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% replace_preserv_pos: LEMMA positionsOF(s)(p) => positionsOF(replaceTerm(s, t, p))(p) replace_compose_pos: LEMMA positionsOF(t)(q) & positionsOF(s)(p) => positionsOF(replaceTerm(s, t, p))(p o q) replace_preserv_parallel_pos: LEMMA positionsOF(s)(q) & positionsOF(s)(p) & parallel(p, q) => positionsOF(replaceTerm(s, t, p))(q) preserv_unchanged_pos: LEMMA positionsOF(s)(p) & positionsOF(replaceTerm(s, t, p))(q) & parallel(p, q) => positionsOF(s)(q) subterm_of_replace: LEMMA positionsOF(s)(p) => subtermOF(replaceTerm(s, t, p),p) = t replace_subterm_of_term: LEMMA positionsOF(s)(p) => replaceTerm(s, subtermOF(s, p), p) = s replace_embedding: LEMMA positionsOF(s)(p) & positionsOF(t)(q) => subtermOF(replaceTerm(s, t, p),p o q) = subtermOF(t, q) replace_associativity: LEMMA positionsOF(s)(p) & positionsOF(t)(q) => replaceTerm(replaceTerm(s,t,p),r,p o q) = replaceTerm(s,replaceTerm(t,r,q),p) replace_distributivity: LEMMA positionsOF(s)(p o q) => subtermOF(replaceTerm(s,t,p o q), p) = replaceTerm(subtermOF(s, p), t, q) replace_dominance: LEMMA positionsOF(s)(p o q) => replaceTerm(replaceTerm(s,t,p o q),r,p) = replaceTerm(s,r,p) replace_persistence: LEMMA positionsOF(s)(p) & positionsOF(s)(q) & parallel(p,q) => subtermOF(replaceTerm(s, t, p), q) = subtermOF(s,q) replace_commutativity: LEMMA positionsOF(s)(p) & positionsOF(s)(q) & parallel(p,q) => replaceTerm(replaceTerm(s,t,p),r,q) = replaceTerm(replaceTerm(s,r,q),t,p) pos_replaces_is_subset: LEMMA FORALL t, x, (p: positions?(t)): subset?(positionsOF(replaceTerm(t, x, p)), positionsOF(t)) pos_occ_var_replace: LEMMA FORALL t, y, x, (p: positions?(t)): Pos_var(t, x)(p) & y /= x => Pos_var(replaceTerm(t, y, p), x) = remove(p, Pos_var(t, x)) pos_occ_var_replace_as_diff: LEMMA FORALL t, y, x, (p: positions?(t)): Pos_var(t, x)(p) & y /= x => Pos_var(replaceTerm(t, y, p), x) = difference(Pos_var(t, x), singleton(p)) END replacement ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28