Σ⊢=

Σ = { 0 1 2 3 4 5 6 7 8 9 + = }
≺ : 0 ≺ 1 ≺ 2 ≺ 3 ≺ 4 ≺ 5 ≺ 6 ≺ 7 ≺ 8 ≺ 9 ≺ + ≺ =
N ::= 0 | [1-9][0-9]*
T ::= N | T + N
E ::= T = T
⊨ E  ⟺  ⟦T₁⟧ = ⟦T₂⟧
ℓ ≤ 6   ·   𝕂 = { E ∈ Σ* | ⊨ E }   ·   ⇅ (ℓ, ≺)

𝕂× = { a×b=c | a, b ∈ {0 1 2 3}, ⊨ }

Σ𝔾 = { 0 1 2 3 n + × ( ) = ∀ : }
≺ : 0 ≺ 1 ≺ 2 ≺ 3 ≺ n ≺ + ≺ × ≺ ( ≺ ) ≺ =
P ::= 0 | 1 | 2 | 3 | n | ( P + P ) | ( P × P )
G ::= ∀n: P = P
⊨ ∀n: P₁=P₂  ⟺  ∀k ∈ ℕ: ⟦P₁⟧(k) = ⟦P₂⟧(k)
𝔾 = { ∀n: P₀=P | ⊨, P ≉ P₀, |P| ≤ 9 }   ·   ∀P ∈ [P₀]: P₀ ≼ P

使う記号は 0〜9 と + と = の 12 個です。数の書き方は「0 単独」か「先頭が 0 でない数字の並び」、項は数を + でつないだもの、式は項 = 項 です。⊨ は「両辺の値が等しい」ことを表し、𝕂 は長さ 6 以下でこれを満たす式すべてです。並べ方は長さが短い順、同じ長さの中では上の記号順 ≺ による辞書順です。短い項目ほど少ない記号で出来ているので、前の項目を読めば後の項目が読めるように並びます。

𝕂× は掛け算の実例 16 個です（0〜3 同士の積）。𝔾 で使う × と n は ⊢ の後半で導入します。P は 0〜3 と n から + と × と括弧で作る式、∀n: P₁=P₂ は「どんな n でも両辺の値が等しい」ことです。≉ は「足し算・掛け算の順番の入れ替え、+0・×1・×0 の消去、定数の計算だけでは一致しない」こと、[P₀] は P₀ と同じ多項式になる式の集まり、P₀ ≼ P は P₀ が P より短い（同じ長さなら記号順で前）ことで、P₀ はその集まりで最も短い式です。

既知の区画です。ミニ・バベル篩（STEP 2219）が全 3,257,436 文字列から検出した正しい等式 300 個と同じ集合で、このページでも読み込み時に一つずつ計算し直しています。

機器が生成したものを受け入れる区画です。予想生成器の結果から、分配法則を使わないと一致が分からない恒等式だけを取り出しました。g001〜g129 は 7 節点以下の式 26,055 個（STEP 2400〜2404）から、g130〜g1064 は 9 節点以下の式 726,055 個（STEP 2416）から加えたものです。番号は一度公開したら変えないので、K=9 で増えた項目は末尾に足しています。同じ多項式になる式の組 364 個を帯にまとめ、帯の見出しに最も短い式を置き、他の式を一つずつ結んでいます。帯を開くと項目が見えます。すべて厳密判定（多項式の展開）で確かめた「検証済」で、このページでも読み込み時に展開し直して確認しています。各辺は 9 節点以内の式に限ります。例えば (1+n)×(1+n) は g065 で (1+(n×(2+n))) と結ばれ、展開した形 (1+((2×n)+(n×n))) も g190 で同じ式と結ばれています。一方、(1+n)×((1+n)×(1+n)) は 11 節点になるため現れません。