## § Decreasing Metric for Mutual Recursive Functions

```
mutual
def bar (fooN : Nat) (barN : Nat) : Nat :=
match barN with
| 0 => foo fooN
| n'+ 1 => bar fooN n'
termination_by (fooN, barN + 1) -- when dropping from bar to foo, give yourself an extra point.
decreasing_by
. simp_wf; apply Prod.Lex.right; omega
. simp_wf; apply Prod.Lex.right; omega
def foo (fooN : Nat) : Nat :=
match fooN with
| 0 => 42
| fooN' + 1 => bar fooN' fooN
termination_by (fooN, 0)
decreasing_by
· simp_wf; apply Prod.Lex.left; omega
end
```

- This took me a while to figure out
- Actually, what we are saying is that
`fooN`

terminates by `(fooN, bot)`

, `barN`

terminates by `(fooN, barN)`

with the condition that `bot < _`

. - In general, I guess this is how we want the termination criteria to be.
- I should read the Isabelle docs on how they prove termination.