等差数列の和：初項 \(a\)・公差 \(d\) で \(2s(n+1) = (n+1)(2a+nd)\)。
自然数の公理と加法・乗法は common/word_basis のもの。
\(s(n)\) を初項 \(a\)、公差 \(d\) の等差数列の最初の \(n\) 項の和とします。
補題 Ari では \(s\) を \(s(0) = 0\) と漸化式を満たす関数として仮定します（\(a\)・\(d\) は可換半環 \(S\) の元）。そのような \(s\) が在ることは、最後の定理で再帰定理（REC）から示します。
\(s(1) = a\)、\(s(2) = a + (a + d)\) です。主定理は最初の \(n+1\) 項の和 \(s(n+1)\)（最後の項は \(a + nd\)）について、割り算を使わず \(2s(n+1) = (n+1)(2a + nd)\) の形で述べます。
証明は \(n\) についての帰納法（INDC）です。\(n = 0\) では両辺とも \(2a\)。\(n\) から \(n+1\) へは、漸化式と帰納法の仮定から
\(2s(n+2) = 2s(n+1) + 2(a + (n+1)d) = (n+1)(2a + nd) + 2(a + (n+1)d)\) で、分配・結合・交換法則により \(= (n+2)(2a + (n+1)d)\) です。

1 準備

加法・乗法の可換半環 \(S\) の元 \(a, d\) について。最初の項：\(2(a + 0d) = (0+1)(2a + 0d)\)。
次の項へ：\(2u = (m+1)(2a + md)\) ならば \(2(u + (a + (m+1)d)) = (m+2)(2a + (m+1)d)\)。

2 主定理

Ari … \(\begin{cases} ( S , [+] , [\cdot] ) \text{csemiring} \\ a , d \in S \\ s ( 0 ) = 0 \\ \forall i \in \mathbb{M} . s ( ( i + 1 ) ) = s ( i ) + ( a + i \cdot d ) \end{cases} , n \in \mathbb{M} \Longrightarrow 2 \cdot s ( ( n + 1 ) ) = ( ( n + 1 ) ) \cdot ( 2 \cdot a + n \cdot d )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄

3 和の関数の存在

上の定理は \(s\) を仮定していました。再帰定理（REC）で、漸化式を満たす写像 \(s\) が実際に在ることを示し、定理を無条件にします（\(\langle \langle n, x\rangle, x + (a + nd)\rangle\) の集合を \(G\) とする）。
\(( S , [+] , [\cdot] ) \text{csemiring} , a , d \in S \Longrightarrow \exists s \in ( \mathbb{M} \to S ) . ( s ( 0 ) = 0 , \forall i \in \mathbb{M} . s ( ( i + 1 ) ) = s ( i ) + ( a + i \cdot d ) , \forall n \in \mathbb{M} . 2 \cdot s ( ( n + 1 ) ) = ( ( n + 1 ) ) \cdot ( 2 \cdot a + n \cdot d ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，1.. ，2.. ，ap. ，=_.