(pred y : bb)

(pred y : bb * bb)

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

*** Error 4.20, expected further mixfix token: [":","!=","/=","<","<="]

*** Error 5.7, unexpected mixfix token: <

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

*** Error 7.10, unexpected mixfix token: predy

*** Error 7.1, unexpected mixfix token: exists1

exists predy:bb . a

exists! a:v . x

exists! a:v . x

exists! a:v . x

forall a:v . x

b => a

def x

*** Error 15.4, unexpected mixfix token: #

*** Error 16.2, unexpected mixfix token: }

*** Error 16.3, not a formula: {} when [] else {}

a /\ b /\ c

a \/ b \/ c

a => b

a <=> b

true

false

b in s

a =e= b

a = b

a => b => c => d

d => c => b => a

a <=> b

def d => not c => b \/ c => a /\ b

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