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