Peanote

there exists a { for all b { S(b) != a } }

a = b -> b = a

a = b and b = c -> a = c

a = b and b is N -> a is N

a is N -> S(a) is N

S(a) = S(b) -> a = b

S(a) != 0

O is K and (a is K -> S(a) is K) -> b is K

define: +

a + 0 = a

a + S(b) = S(a + b)

define: *

a * 0 = 0

a * S(b) = a + a * b

define: |

n | a := there exists b in N { n * b = a }

define: is prime

a is prime := for all n in N { n | a -> n = 1 or n = a }

TODO 何か簡単な定理を証明する

TODO パースする

TODO 自動で証明を validate する

TODO 定数・関数・定理を定義できるようにする

TODO 定数・関数・定理を利用・適用できるようにする