$`\require{color} % 緑色
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\Providing}{\Keyword{Providing } }%
\newcommand{\When}{\Keyword{When } }%
\newcommand{\And}{\Keyword{And } }%
\newcommand{\Holds}{\Keyword{Holds } }%
\newcommand{\HoldsUp}{\Keyword{Holds Up! } }%
\newcommand{\DoesHold}{\Keyword{Does Hold? } }%
\newcommand{\BecauseOf}{\Keyword{Because Of } }%
\newcommand{\Fact }{\Keyword{Fact } }%
\newcommand{\Judgement }{\Keyword{Judgement } }%
\newcommand{\Question }{\Keyword{Question } }%
\newcommand{\DeclFunction }{\Keyword{Decl Function } }%
\newcommand{\DefFunction }{\Keyword{Def Function } }%
\newcommand{\Given}{\Keyword{Given } }%
\newcommand{\Returns}{\Keyword{Returns } }%
\newcommand{\ReturnsInto}{\Keyword{Returns Into! } }%
\newcommand{\Body}{\Keyword{Body } }%
\newcommand{\DoesReturn}{\Keyword{Does Return? } }%
\newcommand{\AskOnFunction}{\Keyword{AskOnFunction } }%
`$
事実：
$`\Providing x : {\bf R}\\
\And y : {\bf R}\\
\:\\
\Fact \text{sumPositive}\\
\When 0 \le x\\
\When 0 \le y\\
\HoldsUp 0 \le x + y
`$
関数版：
$`\Providing x : {\bf R}\\
\And y : {\bf R}\\
\:\\
\DeclFunction \text{sumPositive}\\
\Given 0 \le x\\
\Given 0 \le y\\
\ReturnsInto 0 \le x + y
`$
判断：
$`\Providing x : {\bf R}\\
\And y : {\bf R}\\
\:\\
\Judgement \text{sumPositive}\\
\When 0 \le x\\
\When 0 \le y\\
\Holds 0 \le x + y\\
\BecauseOf \cdots
`$
関数版：
$`\Providing x : {\bf R}\\
\And y : {\bf R}\\
\:\\
\DefFunction \text{sumPositive}\\
\Given 0 \le x\\
\Given 0 \le y\\
\Returns 0 \le x + y\\
\Body \cdots
`$
質問：
$`\Providing x : {\bf R}\\
\And y : {\bf R}\\
\:\\
\Question \text{sumPositive}\\
\When 0 \le x\\
\When 0 \le y\\
\DoesHold 0 \le x + y
`$
関数版：
$`\Providing x : {\bf R}\\
\And y : {\bf R}\\
\:\\
\AskOnFunction \text{sumPositive}\\
\Given 0 \le x\\
\Given 0 \le y\\
\DoesReturn 0 \le x + y
`$
同義語：
- judgement = theorem = lemma
- axiom は judgement の特殊な場合。self evident な判断〈定理〉が公理。
- because of と from と proof と body は同義語。
- question と problem と query は同義語。
