== (letrec formula_rank f = case f:
x
0;
p (formula_rank(p)+1);p
q (formula_rank(p)+formula_rank(q)+1);p
q (formula_rank(p)+formula_rank(q)+1);p
q (formula_rank(p)+formula_rank(q)+1); ) | def | formula_rank | == (letrec formula_rank f = case f:x 0;p (formula_rank(p)+1);pq (formula_rank(p)+formula_rank(q)+1);pq (formula_rank(p)+formula_rank(q)+1);pq (formula_rank(p)+formula_rank(q)+1); ) |