[STATEMENT]
lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bal t = (\<exists>n. full n t)
[PROOF STEP]
by (auto elim!: bal_imp_full full_imp_bal)