** 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)$