SK言語で decもしくはeqが作れない

自然数とは何だろうか
それは"1を足す"という操作の回数とみなすことが出来る。
"1を足す"という操作を関数fで表した時 7 という数は
f(f(f(f(f(f(f(0))))))) と表される


自然数nを意味する項<n>を再帰的に定義する
xは任意の項である
・<0> f x ≡ x
・<n> f x ≡ f (<n-1> f x)

これにより
<7> f x ―*→ f(f(f(f(f(f(f(x))))))) となる

<0> f x = x ← K x (K x) ← SKK x ← K (SKK) f x
∴<0> = K(SKK)

<n> f x = f(<n-1> f x) ← K f x (<n-1> f x) ← S(Kf)(<n-1>f)x
← (KSf)(Kf)(<n-1>f)x ← S(KS)K f (<n-1>f) x
← S(S(KS)K))<n-1> f x
∴<n> = S(S(KS)K))<n-1>

また <succ> <n> = <n+1> となる <succ>は
<succ> = S(S(KS)K) により定義出来る




では 次のように定義される <dec> はどうやって定義出来るのだろうか？
・<dec> <0> = <0>
・<dec> <n+1> = <n>


次のように定義される <eq> はどうやって定義出来るのだろうか？
・<eq> <0> <0> = <true>
・<eq> <n+1> <0> = <false>
・<eq> <0> <m+1> = <false>
・<eq> <n+1> <m+1> = <eq> <n> <m>