DEFINITION next_plus()
TYPE =
       G→nat→nat→nat
BODY =
FIXnext_plus{
         next_plus:G→nat→nat→nat
         :=λg:G.λn:nat.λi:nat.<λn1:nat.nat> CASE i OF O⇒n | S i0⇒next g (next_plus g n i0)
         }