Suppose that the predicate P represents the property we care about. Then we need two properties: $P\ t \to \neg (t \leadsto 0)$ and $P\ t \to t \leadsto t' \to P\ t'$. Most likely, this property will need to be a logical relation (i.e., with respect to the type classifying the term). Some existing work has shown that ContainsVariant [.guard, .term, .var .openm, .var .term] t is a valid P, but it's too restrictive. It's useful to view P as a normalization property for a subset of $F_D$ syntax.
Suppose that the predicate$P\ t \to \neg (t \leadsto 0)$ and $P\ t \to t \leadsto t' \to P\ t'$ . Most likely, this property will need to be a logical relation (i.e., with respect to the type classifying the term). Some existing work has shown that $F_D$ syntax.
Prepresents the property we care about. Then we need two properties:ContainsVariant [.guard, .term, .var .openm, .var .term] tis a validP, but it's too restrictive. It's useful to viewPas a normalization property for a subset of