| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/vect_analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 829 B |
|
Quelle compatibility.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 %% %%---------------------------------------------------------------------------- compatibility[variable: TYPE+, symbol: TYPE+, arity: [symbol -> nat]]: THEORY BEGIN IMPORTING replacement[variable,symbol, arity], finite_sets[(V)] as fsetvar, ars[term] r, s, t: VAR term R: VAR pred[[term, term]] x: VAR (V) n: VAR nat %%%% Defining the set of all function symbols whose arity is n %%%%%%%%%%%%%%%%% arity_eq(n): TYPE = {f: symbol | arity(f) = n} %%%% Defining, respectively, the concepts closed under operations, compatible %% %%%% with operations, and compatible with contexts %% close_op?(R): bool = FORALL ( n: nat, (f: arity_eq(n)), (st1, st2: fset.fs_len(n))): (FORALL (m: below[n]): R(st1(m), st2(m)) => R(app(f, st1), app(f, st2))) comp_op?(R): bool = FORALL (n: nat, i: below[n], (f: arity_eq(n)), (st1: fset.fs_len(n)), t): LET s = st1(i), st2 = replace(t, st1, i) IN R(s,t) => R(app(f,st1), app(f,st2)) comp_cont?(R): bool = FORALL (p: position), s: positionsOF(s)(p) => (FORALL r, t: R(r,t) => R(replaceTerm(s, r, p), replaceTerm(s, t, p))) %%%% Properties %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% comp_op_iff_comp_cont: LEMMA comp_op?(R) <=> comp_cont?(R) closure_comp_op: LEMMA comp_op?(R) => (comp_op?(TC(R)) & comp_op?(RTC(R)) & comp_op?(EC(R))) closure_comp_cont: LEMMA comp_cont?(R) => (comp_cont?(TC(R)) & comp_cont?(RTC(R)) & comp_cont?(EC(R))) END compatibility ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28