Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	set-basic	f	set → nat
. + .	nat-basic	f	nat × nat → nat
. ++ .	set-basic	f	set × elem → set
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. ∈ .	set-basic	p	elem × set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	set-basic	p	set × set
∅	set-basic	c	set
a	elem	v	elem
b	elem	v	elem
c	elem	v	elem
elem	elem	s
m	nat-basic	v	nat
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
s	set-basic	v	set
s0	set-basic	v	set
s1	set-basic	v	set
s2	set-basic	v	set
set	set-basic	s