# Finding 0 in an infinitely branching tree

We use the type of infinitely branching tree defined as:

Inductive Z_inf_branch_tree : Set :=
Z_inf_leaf : Z_inf_branch_tree
| Z_inf_node : Z->(nat->Z_inf_branch_tree)->Z_inf_branch_tree.

We say that a value *v* is accessible by indices lower than *n* in a
tree *t* if the tree the tree has the form *Z_inf_node v' f*
and *v=v'*, or if it is
(recursively) accessible by indices lower than *n* in one of the
tree *f p* for *p <= n*.
Write a function that computes whether the value 0 is accessible by
indices lower than a natural number in an infinitely branching tree.

## Solution

Look at this file

Going home

Pierre Castéran