# Formal description of Coq’s termination checker

Coq’s built-in termination checker accepts some rather intricate recursion patterns with functional values in data types, as shown by this example

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.

Fixpoint n_sum_all_values (n:nat)(t:Z_inf_branch_tree){struct t} : Z :=
(match t with
| Z_inf_leaf ⇒ 0
| Z_inf_node v f ⇒ v + sum_f n (fun x:nat ⇒ n_sum_all_values n (f x)) end ).


(taken from from Chapter 7.3.5.2 here https://www.labri.fr/perso/casteran/CoqArt/coqartF.pdf).

I am looking for a formal description of the termination checker at work here, in order to reimplement it in a different system? Is it written down somewhere accessible?