Order-Sorted Equality Enrichments Modulo Axioms
Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications with initial algebra semantics beyond the pale of theorem proving tools based, f...
- Autores:
-
Gutiérrez, Raúl
Meseguer, José
Rocha, Camilo
- Tipo de recurso:
- Part of book
- Fecha de publicación:
- 2012
- Institución:
- Escuela Colombiana de Ingeniería Julio Garavito
- Repositorio:
- Repositorio Institucional ECI
- Idioma:
- eng
- OAI Identifier:
- oai:repositorio.escuelaing.edu.co:001/1859
- Acceso en línea:
- https://repositorio.escuelaing.edu.co/handle/001/1859
- Palabra clave:
- Teoría Ecuacional
Obligación de prueba
Transformación de la teoría
Especificación algebraica
Álgebra Inicial
Equational Theory
Proof Obligation
Theory Transformation
Algebraic Specification
Initial Algebra
- Rights
- closedAccess
- License
- http://purl.org/coar/access_right/c_14cb
| id |
ESCUELAIG2_9a7ffa1ac003bc18d6edfa8dd529c4ef |
|---|---|
| oai_identifier_str |
oai:repositorio.escuelaing.edu.co:001/1859 |
| network_acronym_str |
ESCUELAIG2 |
| network_name_str |
Repositorio Institucional ECI |
| repository_id_str |
|
| dc.title.eng.fl_str_mv |
Order-Sorted Equality Enrichments Modulo Axioms |
| title |
Order-Sorted Equality Enrichments Modulo Axioms |
| spellingShingle |
Order-Sorted Equality Enrichments Modulo Axioms Teoría Ecuacional Obligación de prueba Transformación de la teoría Especificación algebraica Álgebra Inicial Equational Theory Proof Obligation Theory Transformation Algebraic Specification Initial Algebra |
| title_short |
Order-Sorted Equality Enrichments Modulo Axioms |
| title_full |
Order-Sorted Equality Enrichments Modulo Axioms |
| title_fullStr |
Order-Sorted Equality Enrichments Modulo Axioms |
| title_full_unstemmed |
Order-Sorted Equality Enrichments Modulo Axioms |
| title_sort |
Order-Sorted Equality Enrichments Modulo Axioms |
| dc.creator.fl_str_mv |
Gutiérrez, Raúl Meseguer, José Rocha, Camilo |
| dc.contributor.author.none.fl_str_mv |
Gutiérrez, Raúl Meseguer, José Rocha, Camilo |
| dc.contributor.researchgroup.spa.fl_str_mv |
Informática |
| dc.subject.armarc.spa.fl_str_mv |
Teoría Ecuacional Obligación de prueba Transformación de la teoría Especificación algebraica Álgebra Inicial |
| topic |
Teoría Ecuacional Obligación de prueba Transformación de la teoría Especificación algebraica Álgebra Inicial Equational Theory Proof Obligation Theory Transformation Algebraic Specification Initial Algebra |
| dc.subject.proposal.eng.fl_str_mv |
Equational Theory Proof Obligation Theory Transformation Algebraic Specification Initial Algebra |
| description |
Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications with initial algebra semantics beyond the pale of theorem proving tools based, for example, on explicit or inductionless induction techniques, and of other formal tools for checking key properties such as confluence, termination, and sufficient completeness. Such specifications would instead be amenable to formal analysis if an equationally-defined equality predicate enriching the algebraic data types were to be added to them. Furthermore, having an equationally-defined equality predicate is very useful in its own right, particularly in inductive theorem proving. Is it possible to effectively define a theory transformation E↦E≃ that extends an algebraic specification E to a specification E≃ having an equationally-defined equality predicate? This paper answers this question in the affirmative for a broad class of order-sorted conditional specifications E that are sort-decreasing, ground confluent, and operationally terminating modulo axioms B and have a subsignature of constructors. The axioms B can consist of associativity, or commutativity, or associativity-commutativity axioms, so that the constructors are free modulo B. We prove that the transformation E↦E≃ preserves all the just-mentioned properties of E . The transformation has been automated in Maude using reflection and is used in several Maude formal tools. |
| publishDate |
2012 |
| dc.date.issued.none.fl_str_mv |
2012 |
| dc.date.accessioned.none.fl_str_mv |
2021-11-27T16:01:46Z |
| dc.date.available.none.fl_str_mv |
2021-11-27T16:01:46Z |
| dc.type.spa.fl_str_mv |
Capítulo - Parte de Libro |
| dc.type.coar.fl_str_mv |
http://purl.org/coar/resource_type/c_2df8fbb1 |
| dc.type.coarversion.fl_str_mv |
http://purl.org/coar/version/c_970fb48d4fbd8a85 |
| dc.type.version.spa.fl_str_mv |
info:eu-repo/semantics/publishedVersion |
| dc.type.coar.spa.fl_str_mv |
http://purl.org/coar/resource_type/c_3248 |
| dc.type.content.spa.fl_str_mv |
Text |
| dc.type.driver.spa.fl_str_mv |
info:eu-repo/semantics/bookPart |
| dc.type.redcol.spa.fl_str_mv |
http://purl.org/redcol/resource_type/ART |
| format |
http://purl.org/coar/resource_type/c_3248 |
| status_str |
publishedVersion |
| dc.identifier.isbn.none.fl_str_mv |
9783642340055 |
| dc.identifier.uri.none.fl_str_mv |
https://repositorio.escuelaing.edu.co/handle/001/1859 |
| identifier_str_mv |
9783642340055 |
| url |
https://repositorio.escuelaing.edu.co/handle/001/1859 |
| dc.language.iso.spa.fl_str_mv |
eng |
| language |
eng |
| dc.relation.ispartofseries.none.fl_str_mv |
Lecture Notes in Computer Science book series (LNCS);7571 |
| dc.relation.indexed.spa.fl_str_mv |
N/A |
| dc.relation.ispartofbook.eng.fl_str_mv |
Rewriting Logic and Its Applications |
| dc.relation.references.spa.fl_str_mv |
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998) Bergstra, J., Tucker, J.: Characterization of Computable Data Types by Means of a Finite Equational Specification Method. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 81, pp. 76–90. Springer, Heidelberg (1980) Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007) Durán, F., Lucas, S., Marché, C., Meseguer, J., Urbain, X.: Proving Operational Termination of Membership Equational Programs. Higher Order Symbolic Computation 21(1-2), 59–88 (2008) Durán, F., Lucas, S., Meseguer, J.: Termination Modulo Combinations of Equational Theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 246–262. Springer, Heidelberg (2009) Durán, F., Meseguer, J.: On the Church-Rosser and Coherence Properties of Conditional Order-Sorted Rewrite Theories. Journal of Logic and Algebraic Programming (2011) (to appear) Goguen, J., Meseguer, J.: Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theoretical Computer Science 105, 217–273 (1992) Goguen, J.A.: How to Prove Algebraic Inductive Hypotheses Without Induction. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol. 87, pp. 356–373. Springer, Heidelberg (1980) Gutiérrez, R., Meseguer, J., Rocha, C.: Order-Sorted Equality Enrichments Modulo Axioms (Extended Version). Tech. rep., University of Illinois at Urbana-Champaing (December 2011), http://hdl.handle.net/2142/28597 Hendrix, J.: Decision Procedures for Equationally Based Reasoning. Ph.D. thesis, Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL, USA (2008) Hendrix, J., Clavel, M., Meseguer, J.: A Sufficient Completeness Reasoning Tool for Partial Specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005) Lucas, S., Marché, C., Meseguer, J.: Operational Termination of Conditional Term Rewriting Systems. Information Processing Letters 95(4), 446–453 (2005) Meseguer, J.: Membership Algebra as a Logical Framework for Equational Specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998) Meseguer, J., Goguen, J.A.: Initially, Induction and Computability. Algebraic Methods in Semantics (1986) Musser, D.R.: On Proving Inductive Properties of Abstract Data Types. In: Proc. of the 7th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1980, pp. 154–162. ACM Press (1980) Masaki, N., Kokichi, F.: On Equality Predicates in Algebraic Specification Languages. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 381–395. Springer, Heidelberg (2007) Rocha, C., Meseguer, J.: Theorem Proving Modulo Based on Boolean Equational Procedures. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS/AKA 2008. LNCS, vol. 4988, pp. 337–351. Springer, Heidelberg (2008) Rocha, C., Meseguer, J.: Proving Safety Properties of Rewrite Theories. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 314–328. Springer, Heidelberg (2011) |
| dc.rights.coar.fl_str_mv |
http://purl.org/coar/access_right/c_14cb |
| dc.rights.accessrights.spa.fl_str_mv |
info:eu-repo/semantics/closedAccess |
| eu_rights_str_mv |
closedAccess |
| rights_invalid_str_mv |
http://purl.org/coar/access_right/c_14cb |
| dc.format.extent.spa.fl_str_mv |
20 páginas. |
| dc.format.mimetype.spa.fl_str_mv |
application/pdf |
| dc.publisher.spa.fl_str_mv |
Springer |
| dc.publisher.place.spa.fl_str_mv |
Berlin. |
| institution |
Escuela Colombiana de Ingeniería Julio Garavito |
| bitstream.url.fl_str_mv |
https://repositorio.escuelaing.edu.co/bitstream/001/1859/3/Order-Sorted%20Equality%20Enrichments%20Modulo%20Axioms.png https://repositorio.escuelaing.edu.co/bitstream/001/1859/4/Order-Sorted%20Equality%20Enrichments%20Modulo%20Axioms.png.jpg https://repositorio.escuelaing.edu.co/bitstream/001/1859/1/Order-Sorted%20Equality%20Enrichments%20Modulo%20Axioms.png https://repositorio.escuelaing.edu.co/bitstream/001/1859/2/license.txt |
| bitstream.checksum.fl_str_mv |
d1d133d6370fc776634dd28eb905b678 b3cfb2d465b6323eedfaa1eb3a39827d b28fadbd3a62d439751fefaa4b41c7a0 5a7ca94c2e5326ee169f979d71d0f06e |
| bitstream.checksumAlgorithm.fl_str_mv |
MD5 MD5 MD5 MD5 |
| repository.name.fl_str_mv |
Repositorio Escuela Colombiana de Ingeniería Julio Garavito |
| repository.mail.fl_str_mv |
repositorio.eci@escuelaing.edu.co |
| _version_ |
1814355626217701376 |
| spelling |
Gutiérrez, Raúlc48f602a579aed48a42a3d36547c54cc600Meseguer, José6da02984a567cfba226ed9b8bf7c47c0600Rocha, Camilo649eba80a4c919beefa7d19955bc2950600Informática2021-11-27T16:01:46Z2021-11-27T16:01:46Z20129783642340055https://repositorio.escuelaing.edu.co/handle/001/1859Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications with initial algebra semantics beyond the pale of theorem proving tools based, for example, on explicit or inductionless induction techniques, and of other formal tools for checking key properties such as confluence, termination, and sufficient completeness. Such specifications would instead be amenable to formal analysis if an equationally-defined equality predicate enriching the algebraic data types were to be added to them. Furthermore, having an equationally-defined equality predicate is very useful in its own right, particularly in inductive theorem proving. Is it possible to effectively define a theory transformation E↦E≃ that extends an algebraic specification E to a specification E≃ having an equationally-defined equality predicate? This paper answers this question in the affirmative for a broad class of order-sorted conditional specifications E that are sort-decreasing, ground confluent, and operationally terminating modulo axioms B and have a subsignature of constructors. The axioms B can consist of associativity, or commutativity, or associativity-commutativity axioms, so that the constructors are free modulo B. We prove that the transformation E↦E≃ preserves all the just-mentioned properties of E . The transformation has been automated in Maude using reflection and is used in several Maude formal tools.Los predicados de igualdad y desigualdad incorporados basados en la comparación de formas canónicas en especificaciones algebraicas se usan con frecuencia porque son prácticos y eficientes. Sin embargo, su uso sitúa las especificaciones algebraicas con semántica inicial del álgebra más allá de las herramientas de prueba de teoremas basadas, por ejemplo, en técnicas de inducción explícitas o sin inducción, y de otras herramientas formales para verificar propiedades clave como la confluencia, la terminación y la completitud suficiente. En cambio, tales especificaciones serían susceptibles de análisis formal si se les agregara un predicado de igualdad definido ecuacionalmente que enriqueciera los tipos de datos algebraicos. Además, tener un predicado de igualdad definido ecuacionalmente es muy útil por derecho propio, particularmente en la demostración inductiva de teoremas. ¿Es posible definir efectivamente una transformación teórica E↦E≃ que extienda una especificación algebraica E a una especificación E≃ que tenga un predicado de igualdad definido ecuacionalmente? Este artículo responde afirmativamente a esta pregunta para una amplia clase de especificaciones E condicionales clasificadas por orden que son de orden decreciente, confluentes en el suelo y que terminan operacionalmente los axiomas del módulo B y tienen una subfirma de constructores. Los axiomas B pueden consistir en axiomas de asociatividad, de conmutatividad o de asociatividad-conmutatividad, de modo que los constructores sean módulo B libre. Probamos que la transformación E↦E≃ conserva todas las propiedades de E recién mencionadas. La transformación se ha automatizado en Maude mediante reflexión y se utiliza en varias herramientas formales de Maude.20 páginas.application/pdfengSpringerBerlin.Lecture Notes in Computer Science book series (LNCS);7571N/ARewriting Logic and Its ApplicationsBaader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)Bergstra, J., Tucker, J.: Characterization of Computable Data Types by Means of a Finite Equational Specification Method. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 81, pp. 76–90. Springer, Heidelberg (1980)Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)Durán, F., Lucas, S., Marché, C., Meseguer, J., Urbain, X.: Proving Operational Termination of Membership Equational Programs. Higher Order Symbolic Computation 21(1-2), 59–88 (2008)Durán, F., Lucas, S., Meseguer, J.: Termination Modulo Combinations of Equational Theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 246–262. Springer, Heidelberg (2009)Durán, F., Meseguer, J.: On the Church-Rosser and Coherence Properties of Conditional Order-Sorted Rewrite Theories. Journal of Logic and Algebraic Programming (2011) (to appear)Goguen, J., Meseguer, J.: Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theoretical Computer Science 105, 217–273 (1992)Goguen, J.A.: How to Prove Algebraic Inductive Hypotheses Without Induction. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol. 87, pp. 356–373. Springer, Heidelberg (1980)Gutiérrez, R., Meseguer, J., Rocha, C.: Order-Sorted Equality Enrichments Modulo Axioms (Extended Version). Tech. rep., University of Illinois at Urbana-Champaing (December 2011), http://hdl.handle.net/2142/28597Hendrix, J.: Decision Procedures for Equationally Based Reasoning. Ph.D. thesis, Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL, USA (2008)Hendrix, J., Clavel, M., Meseguer, J.: A Sufficient Completeness Reasoning Tool for Partial Specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005)Lucas, S., Marché, C., Meseguer, J.: Operational Termination of Conditional Term Rewriting Systems. Information Processing Letters 95(4), 446–453 (2005)Meseguer, J.: Membership Algebra as a Logical Framework for Equational Specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)Meseguer, J., Goguen, J.A.: Initially, Induction and Computability. Algebraic Methods in Semantics (1986)Musser, D.R.: On Proving Inductive Properties of Abstract Data Types. In: Proc. of the 7th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1980, pp. 154–162. ACM Press (1980)Masaki, N., Kokichi, F.: On Equality Predicates in Algebraic Specification Languages. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 381–395. Springer, Heidelberg (2007)Rocha, C., Meseguer, J.: Theorem Proving Modulo Based on Boolean Equational Procedures. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS/AKA 2008. LNCS, vol. 4988, pp. 337–351. Springer, Heidelberg (2008)Rocha, C., Meseguer, J.: Proving Safety Properties of Rewrite Theories. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 314–328. Springer, Heidelberg (2011)Order-Sorted Equality Enrichments Modulo AxiomsCapítulo - Parte de Libroinfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_3248http://purl.org/coar/resource_type/c_2df8fbb1Textinfo:eu-repo/semantics/bookParthttp://purl.org/redcol/resource_type/ARThttp://purl.org/coar/version/c_970fb48d4fbd8a85info:eu-repo/semantics/closedAccesshttp://purl.org/coar/access_right/c_14cbTeoría EcuacionalObligación de pruebaTransformación de la teoríaEspecificación algebraicaÁlgebra InicialEquational TheoryProof ObligationTheory TransformationAlgebraic SpecificationInitial AlgebraTHUMBNAILOrder-Sorted Equality Enrichments Modulo Axioms.pngOrder-Sorted Equality Enrichments Modulo Axioms.pngimage/png125067https://repositorio.escuelaing.edu.co/bitstream/001/1859/3/Order-Sorted%20Equality%20Enrichments%20Modulo%20Axioms.pngd1d133d6370fc776634dd28eb905b678MD53open accessOrder-Sorted Equality Enrichments Modulo Axioms.png.jpgOrder-Sorted Equality Enrichments Modulo Axioms.png.jpgGenerated Thumbnailimage/jpeg4164https://repositorio.escuelaing.edu.co/bitstream/001/1859/4/Order-Sorted%20Equality%20Enrichments%20Modulo%20Axioms.png.jpgb3cfb2d465b6323eedfaa1eb3a39827dMD54open accessORIGINALOrder-Sorted Equality Enrichments Modulo Axioms.pngOrder-Sorted Equality Enrichments Modulo Axioms.pngimage/png29134https://repositorio.escuelaing.edu.co/bitstream/001/1859/1/Order-Sorted%20Equality%20Enrichments%20Modulo%20Axioms.pngb28fadbd3a62d439751fefaa4b41c7a0MD51open accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1859/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open access001/1859oai:repositorio.escuelaing.edu.co:001/18592022-12-13 03:01:46.895open accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK |