** latex pngs
:PROPERTIES:
:DATE:     2009-11-20
:END:
$x \mapsto y$

*** Theorem
:PROPERTIES:
:DATE:     2009-11-20
:END:
$|consts(t)| \leq sizes(t)$

- by induction on the structure of t
- base cases are $t \in [true, false, 0]$:
- $|consts(t)| = |[t]| = 1 = size(t)$
- inductive size
- $t \in [succ(t_1), pred(t_1), iszero(t_1)]$:
- $|consts(t)| = |consts(t_1)| = |[t]| \leq size(t_1) < size(t)$
- $t = if\, t_1 \, then \, t_2 \, else t_3$
- $|consts(t)| = |consts(t_1) \cup consts(t_1) \cup consts(t_1)|$
- $\leq |consts(t_1)| + |consts(t_1)| + |consts(t_1)|$
- $\leq size(t_1) + size(t_1) + size(t_1)$
- $< size(t)$