3 begin

     3 begin

     4 

     4 

     5 text {* 

     5 text {* 

     6   The following two auxiliary lemmas are used to reason about @{term Max}.

     6   The following two auxiliary lemmas are used to reason about @{term Max}.

     7 *}

     7 *}