567 by (induct n) (simp_all add: rec_iter_def)

   567 by (induct n) (simp_all add: rec_iter_def)

   568 

   568 

   569 

   569 

   570 section {* Bounded Maximisation *}

   570 section {* Bounded Maximisation *}

   571 

   571 

   572 fun BMax_rec where

   573 fun BMax_rec where

   573   "BMax_rec R 0 = 0"

   574   "BMax_rec R 0 = 0"

   574 | "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)"

   575 | "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)"

   575 

   576 

   576 definition 

   577 definition