19 lines
312 B
OpenEdge ABL
19 lines
312 B
OpenEdge ABL
|
include('Axioms/NUM-ROZEK.ax').
|
||
|
|
|
||
|
|
fof(c2, claim,
|
||
|
|
![X] : (successor(X) != "zero")
|
||
|
|
).
|
||
|
|
|
||
|
|
fof(c3, claim, "two" = sucessor(successor("zero"))).
|
||
|
|
|
||
|
|
fof(c4, claim,
|
||
|
|
![A, B]: (
|
||
|
|
(successor(successor(A)) = successor(B)) =>
|
||
|
|
(successor(A) = B)
|
||
|
|
)
|
||
|
|
).
|
||
|
|
|
||
|
|
fof(c5, claim,
|
||
|
|
"zero" = add("zero", "zero")
|
||
|
|
).
|