2.4 2項記号の操作

word+(\({\tt x}\)\({\tt y}\),\({\tt z}\)→\({\tt y}\)\({\tt x}\),\({\tt z}\)) … \(\leftrightarrow\)
lower … \(A \stackrel{\leftrightarrow}{\mathbin{{\sf p}}} B\) ≃ \(B \mathbin{{\sf p}} A\)
word+(\({\tt x}\)\({\tt x}\),\({\tt y}\)→\({\tt x}\),\({\tt y}\)) … \(\prime\prime\)
lower … \(\stackrel{\prime\prime}{\mathbin{{\sf p}}} A\) ≃ \(A \mathbin{{\sf p}} A\)

2.5 2項記号の関数化

word+(\({\tt x}\)\({\tt x}\),\({\tt y}\)→[s,\({\tt x}\)][s,\({\tt x}\)],\({\tt y}\)) … \(\star\)
lower … \([\mathbin{{\sf f}}] \stackrel{\star}{\mathbin{{\sf a}}} [\mathbin{{\sf g}}]\) ≃ \(\forall x ( ( \mathbin{{\sf f}} x ) \mathbin{{\sf a}} ( \mathbin{{\sf g}} x ) )\)
word+(\({\tt x}\)\({\tt x}\),\({\tt y}\)→[ss,\({\tt x}\)][ss,\({\tt x}\)],\({\tt y}\)) … \(\star\!\star\)
lower … \([\mathbin{{\sf f}}] \stackrel{\star\!\star}{\mathbin{{\sf a}}} [\mathbin{{\sf g}}]\) ≃ \(\forall x , y ( ( x \mathbin{{\sf f}} y ) \mathbin{{\sf a}} ( x \mathbin{{\sf g}} y ) )\)
{*_}
{*_*_}