[STATEMENT]
lemma combine_finite_tree :
  assumes "finite_tree t1"
  and     "finite_tree t2"
shows "finite_tree (combine t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (combine t1 t2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite_tree t1
finite_tree t2

goal (1 subgoal):
 1. finite_tree (combine t1 t2)
[PROOF STEP]
unfolding finite_tree_iff combine_set
[PROOF STATE]
proof (prove)
using this:
finite (Prefix_Tree.set t1)
finite (Prefix_Tree.set t2)

goal (1 subgoal):
 1. finite (Prefix_Tree.set t1 \<union> Prefix_Tree.set t2)
[PROOF STEP]
by blast