我想自动在 latex 文件中添加文本顶部标记（每个页面）。我的 MWE 是：
\documentclass{book}
\usepackage{amsmath}
\usepackage{everypage}
\makeatletter
\renewcommand*{\sc@ep@init}{%
\let\sc@op@saved\@outputpage
\def\@outputpage{%
XXX\sc@op@preamble
YYY\sc@op@saved
\sc@op@postamble}}
\makeatother
\begin{document}
\chapter{Article title here}
\section{Introduction}
Separation logic is a well-known with aaa pointers stemming from BI logic. Such programs have specific errors to be detected and separation logic is used as an assertion language for Hoare-like proof systems that are dedicated to verify programs manipulating heaps. Any procedure mechanizing the proof search requires subroutines that check the satisfiability or the validity of formulae (more precisely entailment) from the assertion language. That is why, characterizing the computational complexity of separation logic and its fragments and designing optimal decision procedures remain essential tasks. Separation logic contains a structural separating connective and its adjoint (the separating implication, also known as the magic wand).
The main concern of the paper is to study a non-trivial fragment of first-order separation logic with one record field as far as expressive power, decidability and complexity are concerned. Herein, the models of separation logic are pairsmade of a variable valuation (store) and a partial function with finite domain (heap), also known as memory states.
Separation logic is a well-known logic for analysing programs with pointers stemming from BI logic. Such programs have specific errors to be detected and separation logic is used as an assertion language for Hoare-like proof systems that are dedicated to verify programs manipulating heaps. Any procedure mechanizing the proof search requires subroutines that check the satisfiability or the validity of formul{\ae} (more precisely entailment) from the assertion language. That is why, characterizing the computational complexity of separation logic and its fragments and designing optimal decision procedures remain essential tasks. Separation logic contains a structural separating connective and its adjoint (the separating implication, also known as the magic wand). Concise and modular proofs can be derived using these connectives, since they can express properties such as non-aliasing.
The main concern of the paper is to study a non-trivial fragment of first-order separation logic with one record field as far as expressive power, decidability and complexity are concerned. Herein, the models of separation logic are pairs made of a variable valuation (store) and a partial function with finite domain (heap), also known as memory states.
Separation logic is a well-known logic for analysing programs with pointers stemming from BI logic. Such programs have specific errors to be detected and separation logic is used as an assertion language for iability or the validity of formul{\ae} (more precisely entailment) from the assertion language. That is why, characterizing the computational complexity of separation logic and its fragments and designing optimal decision procedures remain essential tasks. Separation logic contains a structural separating connective and its adjoint (the separating implication, also known as the magic wand). Concise and modular proofs can be derived using these connectives, since they can express properties such as non-aliasing.
The main concern of the paper is to study a non-trivial fragment of first-order separation logic with one record field as far as expressive power, decidability and complexity are concerned. Herein, the models of separation logic are pairs made of a variable valuation (store) and a partial function with finite domain (heap), also known as memory states. Separation logic is a well-known logic for analysing programs with pointers stemming from BI logic. Such programs have specific errors to be detected and separation logic is used as an assertion language for Hoare-like proof systems that are dedicated to verify programs manipulating heaps. Any procedure mechanizing the proof search requires subroutines that check the satisfiability or the validity of formul{\ae} (more precisely entailment) from the assertion language. That is why, characterizing the computational complexity of separation logic and its fragments and designing optimal decision procedures remain essential tasks. Separation logic contains a structural separating connective and its adjoint (the separating implication, also known as the magic wand). Concise and modular proofs can be derived using these connectives, since they can express properties such asnon-aliasing.
The main concern of the paper is to study a non-trivial fragment of first-order separation logic with one record field as far as expressive power, decidability and complexity are concerned. Herein, the models of separation logic are pairs made of a variable valuation (store) and a partial function with finite domain (heap), also known as memory states.
Separation logic is a well-known logic for analysing programs with pointers stemming from BI logic. Such programs have specific errors to be detected and separation logic is used as an assertion language for Hoare-like proof systems that are dedicated to verify programs manipulating heaps. Any procedure mechanizing the proof search requires subroutines that check the satisfiability or the validity of formul{\ae} (more precisely entailment) from the assertion lan,,,,,,guage. asdfasdfThat is why, characterizing the computational complexity of separation logic and its fragments and designing optimal decision procedures remain essential tasks. Separation logic contains a structural separating connective and its adjoint (the separating implication, also known as the magic wand). Concise and modular proofs can be derived using these connectives, since they can express properties such as non-aliasing. The main concern of the paper is to study a non-trivial fragment of first-order separation logic with one record fieldas far as expressive power, decidability and complexity are concerned. Herein, the models of separation logic are pairs made of a variable valuation (store) and a partial function with finite domain (heap), also known as memory states.
Separation logic is a well-known logic for analysing programs with pointers stemming from BI logic. Such programs have specific errors to be detected and separation logic is used as an assertion language for Hoare-like proof systems that are dedicated to verify programs manipulating heaps. Any procedure mechanizing the proof search requires subroutines that check the satisfiability or the validity of formul{\ae} (more precisely entailment) from the assertion language. That is why, characterizing the computational complexity of separation logic and its fragments and designing optimal decision procedures remain essential tasks. Separation logic contains a structural separating connective and its adjoint (the separating implication, also known as the magic wand). Concise and modular proofs can be derived using these connectives, since they can express properties such as non-aliasing.
\end{document}
因此，我想在 LaTeX 文件中的每个页面中添加一些标记文本，如 {%startpage}。如何实现这一点...