(pred y : bb)

(pred y : bb * bb)

(pred y : bb * bb)(a, b)

4.18-4.20: *** Error:

expected further mixfix token: ["!","!=","*","+","-"]

5.7: *** Error: unexpected mixfix token: <

6.3: *** Error: unexpected mixfix token: #=

exists1(predy :: bb)

exists predy : bb . a

exists! a : v . x

exists! a : v . x

exists! a : v . x

forall a : v . x

a if b

def x

15.4: *** Error: unexpected mixfix token: #

16.2: *** Error: unexpected mixfix token: }

a /\ b /\ c

a \/ b \/ c

a => b

a <=> b

true

false

b in s

a =e= b

a = b

a => b => c => d

a if b if c if d

a <=> b

a /\ b if b \/ c if not c if def d

m div n = r <=> exists s : Nat . m = n * r + s /\ s < n

a => (b if c)

a if (b => c)

(a => b) if c

(a if b) => c