$`\newcommand{\Within}{\sqsubseteq}
\newcommand{\conc}{\mathop{\#} }
\newcommand{\dmid}{\mathrel{\|} }
\newcommand{\mrm}[1]{\mathrm{#1} }
%`$
$`\mrm{Ext}(\Sigma)`$ は拡張指標（派生指標）の全体。すると、
$`\quad \Gamma \in \mrm{Ext}(\Sigma) \iff \Gamma\setminus \Sigma \in \mrm{Frag}(\Sigma)`$
ここで、$`\mrm{Frag}(\Sigma)`$ は $`\Sigma`$ を接頭辞とする指標フラグメントの集合。
$`\Phi \in \mrm{Frag}(\Sigma), \sigma:\Sigma \to \Gamma`$ とする。ここで、$`\sigma`$ は指標射または拡張指標射（手続きの反対射）とする。フラグメント $`\Phi`$ に対して、$`\sigma`$ による置換ができる。それを次のように書く。
$`\quad \Phi[\Sigma := \sigma]`$
$`\sigma_*(\Phi) := \Phi[\Sigma := \sigma]`$ と置くと、
$`\quad \sigma_* : \mrm{Frag}[\Sigma] \to \mrm{Frag}[\Gamma]`$
$`\sigma_*`$ が指標射 $`\sigma`$ による前送り翻訳〈push forward translation〉を与える。
充足関係式は：
$`\quad \sigma^* N \models_\Sigma \Phi \iff N\models_\Gamma \sigma_* \Phi`$
書き換えれば：
$`(\sigma ; N) \models_\Sigma \Phi \iff N\models_\Gamma \Phi[\Sigma := \sigma]`$
さらに：
$`(\sigma ; N)\in_0 \mrm{Model}(\Sigma \conc \Phi) \iff
N \in_0 \mrm{Model}(\Gamma\conc \Phi[\Sigma := \sigma])
`$
上記を示せば充足関係式を証明できる。調べると、証明に関する知見も得られるかも。証明は、$`\mrm{Frag}(\Sigma)`$ または $`\mrm{Ext}(\Sigma)`$ の射として定式化する。
