\(S = \{(x,y,z) : x^2 + 4yz = p\}\) の上の対合 \(f\)（不動点は \((1,1,k)\) だけ）と \(g(x,y,z) = (x,z,y)\)、\(S\) が有限であること。20 で使う。

1 三つ組

数字の計算：\(4 = 2 \cdot 2\)。
L44 … \(4 = 2 \cdot 2\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
素数 \(p = 4k + 1\) は奇数で、平方数ではない。
Lpo … \(p = 4 \cdot k + 1 , k \in \mathbb{M} \Longrightarrow \neg 2 \mid p\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，L44
Lns … \(p \in \mathbb{P} , x \in \mathbb{M} \Longrightarrow \neg x \cdot x = p\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
計算の道具：和の平方・2 倍・4 倍。
Lsq … \(a , b \in \mathbb{M} \Longrightarrow ( a + b ) \cdot ( a + b ) = ( a \cdot a + 2 \cdot ( a \cdot b ) ) + b \cdot b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
L4m … \(a \in \mathbb{M} \Longrightarrow 4 \cdot a = 2 \cdot ( 2 \cdot a )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，L44
場合 A（\(y = (x + z) + w\)）の等式：\((x + 2z)^2 + 4zw = x^2 + 4yz\)。
IA … \(x , z , w \in \mathbb{M} \Longrightarrow ( x + 2 \cdot z ) \cdot ( x + 2 \cdot z ) + 4 \cdot ( z \cdot w ) = x \cdot x + 4 \cdot ( ( ( x + z ) + w ) \cdot z )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
場合 C（\(x = 2y + b\)）の等式：\(b^2 + 4(y + b + z)y = x^2 + 4yz\)。
IC … \(y , b , z \in \mathbb{M} \Longrightarrow b \cdot b + 4 \cdot ( ( ( y + b ) + z ) \cdot y ) = ( 2 \cdot y + b ) \cdot ( 2 \cdot y + b ) + 4 \cdot ( y \cdot z )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
場合 B（\(2y = x + a\)・\(x + z = y + c\)）の等式：\(a^2 + 4yc = x^2 + 4yz\)。
Ib1 … \(x , y , z , a , c \in \mathbb{M} , 2 \cdot y = x + a , x + z = y + c \Longrightarrow x + 2 \cdot z = a + 2 \cdot c\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Ib3 … \(x , z , a \in \mathbb{M} \Longrightarrow ( x + a ) \cdot ( x + 2 \cdot z ) = ( x \cdot x + 2 \cdot ( x \cdot z ) ) + ( x \cdot a + 2 \cdot ( a \cdot z ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Ib4 … \(x , a , c \in \mathbb{M} \Longrightarrow ( x + a ) \cdot ( a + 2 \cdot c ) = ( a \cdot a + 2 \cdot ( a \cdot c ) ) + ( x \cdot a + 2 \cdot ( x \cdot c ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Ib6 … \(y , z , x , a \in \mathbb{M} , 2 \cdot y = x + a \Longrightarrow 4 \cdot ( y \cdot z ) = 2 \cdot ( x \cdot z ) + 2 \cdot ( a \cdot z )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，L4m
IB … \(x , y , z , a , c \in \mathbb{M} , 2 \cdot y = x + a , x + z = y + c \Longrightarrow a \cdot a + 4 \cdot ( y \cdot c ) = x \cdot x + 4 \cdot ( y \cdot z )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Ib1 ，Ib3 ，Ib4 ，Ib6
等号の場合：\(y = x + z\) なら \(p = (x + 2z)^2\)（IA で \(w = 0\)）、\(x = 2y\) なら \(p\) は偶数（IC で \(b = 0\)）。
Lex1 … \(x , y , z \in \mathbb{M} , y = x + z , x \cdot x + 4 \cdot ( y \cdot z ) = p \Longrightarrow ( x + 2 \cdot z ) \cdot ( x + 2 \cdot z ) = p\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，IA
Lex2 … \(x , y , z \in \mathbb{M} , x = 2 \cdot y , x \cdot x + 4 \cdot ( y \cdot z ) = p \Longrightarrow 2 \mid p\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，L4m ，IC

2 三つ組の分類

等号は起こらない（\(y = x + z\)・\(x = 2y\)）。
Lcl1 … \(x , y , z , w \in \mathbb{M} , p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} , x \cdot x + 4 \cdot ( y \cdot z ) = p , y = ( x + z ) + w \Longrightarrow \neg w = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Lns ，Lex1
Lcl2 … \(x , y , z , c \in \mathbb{M} , p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} , x \cdot x + 4 \cdot ( y \cdot z ) = p , x + z = y + c \Longrightarrow \neg c = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Lns ，Lex1
Lcl3 … \(x , y , z , b \in \mathbb{M} , p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} , x \cdot x + 4 \cdot ( y \cdot z ) = p , x = 2 \cdot y + b \Longrightarrow \neg b = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Lpo ，Lex2
Lcl4 … \(x , y , z , a \in \mathbb{M} , p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} , x \cdot x + 4 \cdot ( y \cdot z ) = p , 2 \cdot y = x + a \Longrightarrow \neg a = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Lpo ，Lex2
分類：\(S\) の元 \((x,y,z)\) は場合 A・B・C のちょうど1つに入る（網羅）。
Lcls … \(x , y , z \in \mathbb{M} , x \in \mathbb{N} , y \in \mathbb{N} , z \in \mathbb{N} , p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} , x \cdot x + 4 \cdot ( y \cdot z ) = p \Longrightarrow \exists w \in \mathbb{N} . y = ( x + z ) + w \mathbin{\rm o\!r} \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . 2 \cdot y = x + a , x + z = y + c \mathbin{\rm o\!r} \exists b \in \mathbb{N} . x = 2 \cdot y + b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Lcl1 ，Lcl2 ，Lcl3 ，Lcl4
排他性：場合 A・B・C は同時には起こらない。
LxAB … \(x , z , w , c , y \in \mathbb{M} , w \in \mathbb{N} , y = ( x + z ) + w , x + z = y + c \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
LxAC … \(x , z , w , b , y \in \mathbb{M} , x \in \mathbb{N} , y = ( x + z ) + w , x = 2 \cdot y + b \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
LxBC … \(x , y , a , b \in \mathbb{M} , a \in \mathbb{N} , 2 \cdot y = x + a , x = 2 \cdot y + b \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄

3 集合 S

\(S\) は \(x^2 + 4yz = p\) を満たす正の整数の三つ組 \((x,y,z)\)（入れ子の対 \(\langle x, \langle y, z\rangle\rangle\)）の集合。
LmS … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) \Longrightarrow ( x \in \mathbb{N} , y \in \mathbb{N} , z \in \mathbb{N} , x \cdot x + 4 \cdot ( y \cdot z ) = p \Longleftrightarrow \langle x , \langle y , z \rangle \rangle \in S )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
\(S\) の元から1歩進んだ三つ組も \(S\) に入る（閉）：場合 A・B・C の各場合に IA・IB・IC。
Lnp … \(x \in \mathbb{N} , u \in \mathbb{M} \Longrightarrow x + u \in \mathbb{N}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Lnp
LF1A … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , x , z , w \in \mathbb{M} , x \in \mathbb{N} , z \in \mathbb{N} , w \in \mathbb{N} , \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle \in S \Longrightarrow \langle x + 2 \cdot z , \langle z , w \rangle \rangle \in S\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，IA ，LmS ，Lnp
LF1B … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , x , y , z , a , c \in \mathbb{M} , x \in \mathbb{N} , y \in \mathbb{N} , z \in \mathbb{N} , a \in \mathbb{N} , c \in \mathbb{N} , 2 \cdot y = x + a , x + z = y + c , \langle x , \langle y , z \rangle \rangle \in S \Longrightarrow \langle a , \langle y , c \rangle \rangle \in S\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，IB ，LmS
LF1C … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , y , b , z \in \mathbb{M} , y \in \mathbb{N} , b \in \mathbb{N} , z \in \mathbb{N} , \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle \in S \Longrightarrow \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle \in S\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，IC ，LmS ，Lnp
\(S\) 上の関係 \(F\)（写像 \(f\) のグラフ）：場合 A・B・C それぞれで \(f\) を与える。
LF1 … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( \langle s , t \rangle \in F \Longleftrightarrow s \in S , ( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) ) , p \in \mathbb{P} , s \in S , \langle s , t \rangle \in F \Longrightarrow t \in S\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LF1A ，LF1B ，LF1C
全域：\(S\) の各元に \(F\) の相手がある（分類 Lcls の各場合）。
LF2 … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( \langle s , t \rangle \in F \Longleftrightarrow s \in S , ( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) ) , p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} , s \in S \Longrightarrow \exists t \, \langle s , t \rangle \in F\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Lcls ，Lnp
関数：\(F\) は \(S\) の各元に高々1つの相手（場合は排他的・各場合の相手は一意）。
LF3p … \(( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) , ( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , u = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , u = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , u = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) \Longrightarrow t = u\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LxAB ，LxAC ，LxBC
LF3 … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( \langle s , t \rangle \in F \Longleftrightarrow s \in S , ( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) ) , p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} , \langle s , t \rangle \in F , \langle s , u \rangle \in F \Longrightarrow t = u\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LF3p
対称：場合 A の相手から場合 C で戻る・場合 B は自分に戻る。
LBq … \(x , y , z , a , c \in \mathbb{M} , 2 \cdot y = x + a , x + z = y + c \Longrightarrow a + c = y + z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
LF4C2 … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( s \in S , \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \Longrightarrow \langle s , t \rangle \in F ) , p \in \mathbb{P} , y , b , z \in \mathbb{M} , y \in \mathbb{N} , b \in \mathbb{N} , z \in \mathbb{N} , s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle , s \in S \Longrightarrow \langle t , s \rangle \in F\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LF1C ，Lnp
LF4A2 … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( s \in S , \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle \Longrightarrow \langle s , t \rangle \in F ) , p \in \mathbb{P} , x , z , w \in \mathbb{M} , x \in \mathbb{N} , z \in \mathbb{N} , w \in \mathbb{N} , s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle , s \in S \Longrightarrow \langle t , s \rangle \in F\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LF1A ，Lnp
LF4B2 … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( s \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \Longrightarrow \langle s , t \rangle \in F ) , p \in \mathbb{P} , x , y , z , a , c \in \mathbb{M} , x \in \mathbb{N} , y \in \mathbb{N} , z \in \mathbb{N} , a \in \mathbb{N} , c \in \mathbb{N} , 2 \cdot y = x + a , x + z = y + c , s = \langle x , \langle y , z \rangle \rangle , t = \langle a , \langle y , c \rangle \rangle , s \in S \Longrightarrow \langle t , s \rangle \in F\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LF1B ，LBq ，Lnp
LF4 … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( \langle s , t \rangle \in F \Longleftrightarrow s \in S , ( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) ) , p \in \mathbb{P} , \langle s , t \rangle \in F \Longrightarrow \langle t , s \rangle \in F\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LF4C2 ，LF4A2 ，LF4B2

4 不動点

\(f\) の不動点は場合 B だけで、\(x = y\)・\(p = x(x + 4z)\) から \(x = 1\)・\(z = k\)。
Fx1 … \(x , z , w \in \mathbb{M} , z \in \mathbb{N} , \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Fx2 … \(y , b , z \in \mathbb{M} , y \in \mathbb{N} , \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Fx3 … \(x , y , z , a , c \in \mathbb{M} , \langle x , \langle y , z \rangle \rangle = \langle a , \langle y , c \rangle \rangle , 2 \cdot y = x + a \Longrightarrow y = x , a = x , c = z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lpd0 … \(p \in \mathbb{P} , f \in \mathbb{M} , f \mid p \Longrightarrow f = 1 \mathbin{\rm o\!r} f = p\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Fx4 … \(x \in \mathbb{N} , x , z \in \mathbb{M} , p \in \mathbb{P} , x \cdot x + 4 \cdot ( x \cdot z ) = p \Longrightarrow x = 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Lpd0
Fx5 … \(z , k \in \mathbb{M} , 1 \cdot 1 + 4 \cdot ( 1 \cdot z ) = 4 \cdot k + 1 \Longrightarrow z = k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，L4m
場合 B で \(s = f(s)\) なら \(s = (1, 1, k)\)（Fx3・Fx4・Fx5）。
Fx6 … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} , x , y , z , a , c \in \mathbb{M} , x \in \mathbb{N} , y \in \mathbb{N} , z \in \mathbb{N} , s = \langle x , \langle y , z \rangle \rangle , s = \langle a , \langle y , c \rangle \rangle , 2 \cdot y = x + a , s \in S \Longrightarrow s = \langle 1 , \langle 1 , k \rangle \rangle\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LmS ，Fx3 ，Fx4 ，Fx5
不動点：\(\langle s, s\rangle \in F\) なら \(s = (1, 1, k)\)。
LFixI … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( \langle s , t \rangle \in F \Longleftrightarrow s \in S , ( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) ) , p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} , \langle s , s \rangle \in F \Longrightarrow s = \langle 1 , \langle 1 , k \rangle \rangle\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Fx1 ，Fx2 ，Fx6
逆に \((1, 1, k)\) は \(S\) に入り、\(F\) の不動点。
LFixR … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( \langle s , t \rangle \in F \Longleftrightarrow s \in S , ( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) ) , p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} \Longrightarrow \langle 1 , \langle 1 , k \rangle \rangle \in S , \langle \langle 1 , \langle 1 , k \rangle \rangle , \langle 1 , \langle 1 , k \rangle \rangle \rangle \in F\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LmS

5 対合 g（y と z の入れ替え）

\(g(x, y, z) = (x, z, y)\)：\(S\) を \(S\) に写す対合で、不動点は \(y = z\)。
LG1 … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( \langle s , t \rangle \in G \Longleftrightarrow s \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , t = \langle x , \langle z , y \rangle \rangle ) , s \in S , \langle s , t \rangle \in G \Longrightarrow t \in S\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LmS
LG2 … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( \langle s , t \rangle \in G \Longleftrightarrow s \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , t = \langle x , \langle z , y \rangle \rangle ) , s \in S \Longrightarrow \exists t \, \langle s , t \rangle \in G\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
LG3 … \(\forall s , t \, ( \langle s , t \rangle \in G \Longleftrightarrow s \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , t = \langle x , \langle z , y \rangle \rangle ) , \langle s , t \rangle \in G , \langle s , u \rangle \in G \Longrightarrow t = u\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
LG4 … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( \langle s , t \rangle \in G \Longleftrightarrow s \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , t = \langle x , \langle z , y \rangle \rangle ) , \langle s , t \rangle \in G \Longrightarrow \langle t , s \rangle \in G\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LmS
LG5 … \(\forall s , t \, ( \langle s , t \rangle \in G \Longleftrightarrow s \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , t = \langle x , \langle z , y \rangle \rangle ) , \langle s , s \rangle \in G \Longrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . s = \langle x , \langle y , y \rangle \rangle\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄

6 S は有限

\(x^2 + 4yz = p\) の正の整数解は \(x, y, z \le p\)。
Lsl … \(a \in \mathbb{N} , b \in \mathbb{N} \Longrightarrow a \le a \cdot b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
LbX … \(x , y , z \in \mathbb{M} , x \in \mathbb{N} , x \cdot x + 4 \cdot ( y \cdot z ) = p \Longrightarrow x \le p\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Lsl
LbY … \(x , y , z \in \mathbb{M} , y \in \mathbb{N} , z \in \mathbb{N} , x \cdot x + 4 \cdot ( y \cdot z ) = p \Longrightarrow y \le p , z \le p\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Lsl ，L4m
3つ組の全体 \((0..p)^3\) は \((p+1)^3\) 個。
Lcn … \(p \in \mathbb{M} \Longrightarrow ( 0 \mathinner{\ldotp\ldotp} p ) \times ( ( 0 \mathinner{\ldotp\ldotp} p ) \times ( 0 \mathinner{\ldotp\ldotp} p ) ) \stackrel{\#}= ( p + 1 ) \cdot ( ( p + 1 ) \cdot ( p + 1 ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
\(S\) は \((0..p)^3\) の部分集合なので有限。
LSsub … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , p \in \mathbb{M} \Longrightarrow S \subset ( 0 \mathinner{\ldotp\ldotp} p ) \times ( ( 0 \mathinner{\ldotp\ldotp} p ) \times ( 0 \mathinner{\ldotp\ldotp} p ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LmS ，LbX ，LbY
LSfin … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , p \in \mathbb{M} \Longrightarrow \exists k \in \mathbb{M} . S \stackrel{\#}= k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Lcn ，LSsub