symbol	type	comment
+	+
−	-
3y	3y	at least one factor must be constant
y ⋅ 3	y*3
(3 + 4)(x + 5)	(3+4)(x+5)
|2x − 5|	|2x-5|
x + 1 6	(x+1)/6	only in ℝ mode
2 3 4	2 3/4
x div 3	y div 3	not in ℝ mode
x mod 3	x mod 3

The set of available symbols depends on the mode. ℤ Presburger has also band, bor, bxor, bnot (bitwise operators), lpow2, hpow2 (lowest and highest 1-bit), and pow2 (is power of 2).

symbol	type
<	<
≤	<=
=	=
≠	!=
≥	>=
>	>

symbol	type	comment
∧	/\
∨	\/
¬	!
F	FF
T	TT
U	UU	not in ℤ mode
→	-->
↔	<->
&&	&&	short-circuit and, not in ℤ mode
||	||	short-circuit or

symbol	type	comment
⇒	==>
⇐	<==
⇔	<=>	unifies U and F
≡	===	does not unify U and F

A global assumption (i.e., axiom) may be added to the front, e.g.: assume x > 3 \/ x = y;.

A subproof is started with subproof and ended with subend. The first formula at the same level can be referred to with original. At the beginning of a subproof original refers to the previous level.

The ℤ Presburger mode has also define P(x,y) === ...;

symbol	type
∀ x:	AA x:
∀ x; 0 ≤ x < y:	AA x; 0 <= x < y:
∃ x:	EE x:
∃ x; x + 2 ≠ z:	EE x; x+2 != z:

Between ; and :, not all operators are available.