trace 1
1からxまでの合計が _ある式 で表せる ?

1からxまでの合計が F[x] で表せる とは、
F[x] が演算子 (e e e e) 個以下の計算式 で、
F[x] への 1 の適用後が F[1] で、F[1] = 1 で、
F[x] への n の適用後が F[n] で、F[x] への (n - 1) の適用後が F[n-1] で、F[n] = (F[n-1] + n) っていう意味。

F[x] が演算子 Nz 個以下の計算式 とは、
Nz が、(e ez ... 1) で、F[x] が演算子 (ez ... 1) 個以下の計算式 か、
F[x] が演算子 Nz 個の計算式 っていう意味。

F[x] が演算子 Nz 個の計算式 とは、
Nz が、() で、F[x] が、x か、
Nz が、() で、F[x] が、1 か、
Nz が、(e ez ... 1) で、(ez ... 1) = Na + Nb で、
A が演算子 Na 個の計算式 で、
B が演算子 Nb 個の計算式 で、
Op が演算子 で、(A Op B) が冗長 でなく、F[x] が、(A Op B) っていう意味。

Op が演算子 とは、
Op が、+ か、
Op が、- か、
Op が、* か、
Op が、/ っていう意味。

Z が冗長 とは、
Z が、(A * 1) か、
Z が、(1 * A) か、
Z が、(A / 1) か、
Z が、(A / A) か、
Z が、(A - A) っていう意味。

Nz = Na + Nb とは、
Nz が、(e ez ... 1) で、Na が、(e ea ... 1) で、(ez ... 1) = (ea ... 1) + Nb か、
Nz が、Nb で、Na が、() っていう意味。

F[x] への P の適用後が Z とは、
F[x] が、x で、Z が、P か、
F[x] が、(G[x] Op H[x]) で、G[x] への P の適用後が A で、H[x] への P の適用後が B で、Z が、(A Op B) か、
F[x] が、x でなく、F[x] が、(G[x] Op H[x]) でなく、Z が、F[x] っていう意味。

A = B とは、
A が、(AC / C) で、B の C 倍が BC で、AC = BC か、
B が、(BC / C) で、A の C 倍が AC で、AC = BC か、
A も B も除算式以外 で、A の展開後が As で、As の簡素化後が Z で、B の展開後が Bs で、Bs の簡素化後が Z っていう意味。

P の C 倍が Z とは、
P が、(A + B) で、A の C 倍が AC で、B の C 倍が BC で、Z が、(AC + BC) か、
P が、(A - B) で、A の C 倍が AC で、B の C 倍が BC で、Z が、(AC - BC) か、
P が、(A / C) で、Z が、A か、
P が加減算式 でなく、Z が、(P * C) っていう意味。

P の展開後が Z とは、
P が、(A * 1) で、A の展開後が Z か、
P が、(1 * B) で、B の展開後が Z か、
P が、(A + B) で、A の展開後が As で、B の展開後が Bs で、Z が、(As + Bs) か、
P が、(A - B) で、A の展開後が As で、B の展開後が Bs で、Z が、(As - Bs) か、
P が、((A1 + A2) * B) で、B が、1 でなく、(A1 * B) の展開後が C1 で、(A2 * B) の展開後が C2 で、Z が、(C1 + C2) か、
P が、((A1 - A2) * B) で、B が、1 でなく、(A1 * B) の展開後が C1 で、(A2 * B) の展開後が C2 で、Z が、(C1 - C2) か、
P が、(A * (B1 + B2)) で、A が1か加減算式 でなく、(A * B1) の展開後が C1 で、(A * B2) の展開後が C2 で、Z が、(C1 + C2) か、
P が、(A * (B1 - B2)) で、A が1か加減算式 でなく、(A * B1) の展開後が C1 で、(A * B2) の展開後が C2 で、Z が、(C1 - C2) か、
P が、(A * B) で、A が1か加減算式 でなく、B が1か加減算式 でなく、A の展開後が As で、B の展開後が Bs で、Z が、(As * Bs) か、
P が、(A Op B) でなく、Z が、P っていう意味。

P の簡素化後が Z とは、
P が、(A + (B + C)) で、((A + B) + C) の簡素化後が Z か、
P が、(A + (B - C)) で、((A + B) - C) の簡素化後が Z か、
P が、(A - (B + C)) で、((A - B) - C) の簡素化後が Z か、
P が、(A - (B - C)) で、((A - B) + C) の簡素化後が Z か、
P が、(A + B) で、B が加減算式 でなく、A の簡素化後が As で、(As + B) の打消し後が Z か、
P が、(A - B) で、B が加減算式 でなく、A の簡素化後が As で、(As - B) の打消し後が Z か、
P が加減算式 でなく、Z が、P っていう意味。

(P + C) の打消し後が Z とは、
P が、(A - C) で、Z が、A か、
P が、(A - B) で、B が、C でなく、(A + C) の打消し後が AC で、Z が、(AC - B) か、
P が、(A + B) で、(A + C) の打消し後が AC で、Z が、(AC + B) か、
P が加減算式 でなく、Z が、(P + C) っていう意味。

(P - C) の打消し後が Z とは、
P が、(A + C) で、Z が、A か、
P が、(C + B) で、Z が、B か、
P が、(A + B) で、A が、C でなく、B が、C でなく、(A - C) の打消し後が AC で、Z が、(AC + B) か、
P が、(A - B) で、(A - C) の打消し後が AC で、Z が、(AC - B) か、
P が加減算式 でなく、Z が、(P - C) っていう意味。

A が1か加減算式 とは、
A が、1 か、
A が加減算式 っていう意味。

P が加減算式 とは、
P が、(A + B) か、
P が、(A - B) っていう意味。

A も B も除算式以外 とは、
A が、(A1 / A2) でなく、B が、(B1 / B2) でないっていう意味。
