mutualdef 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; omegadef foo (fooN : Nat) : Nat :=  match fooN with  | 0 => 42  | fooN' + 1 => bar fooN' fooNtermination_by (fooN, 0)decreasing_by  · simp_wf; apply Prod.Lex.left; omegaend

• 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.