84   "apply_assn f ANil = (0 :: nat)"

    84   "apply_assn f ANil = (0 :: nat)"

    85 | "apply_assn f (ACons x t as) = max (f t) (apply_assn f as)"

    85 | "apply_assn f (ACons x t as) = max (f t) (apply_assn f as)"

    86 apply(case_tac x)

    86 apply(case_tac x)

    87 apply(case_tac b rule: trm_assn.exhaust(2))

    87 apply(case_tac b rule: trm_assn.exhaust(2))

    88 apply(simp_all)

    88 apply(simp_all)

    90 done

    89 done

    91 

    90 

    92 termination by lexicographic_order

    91 termination by lexicographic_order

    93 

    92 

    94 lemma [eqvt]:

    93 lemma [eqvt]:

   143   "apply_assn2 f ANil = ANil"

   142   "apply_assn2 f ANil = ANil"

   144 | "apply_assn2 f (ACons x t as) = ACons x (f t) (apply_assn2 f as)"

   143 | "apply_assn2 f (ACons x t as) = ACons x (f t) (apply_assn2 f as)"

   145   apply(case_tac x)

   144   apply(case_tac x)

   146   apply(case_tac b rule: trm_assn.exhaust(2))

   145   apply(case_tac b rule: trm_assn.exhaust(2))

   147   apply(simp_all)

   146   apply(simp_all)

   149   done

   147   done

   150 

   148 

   151 termination by lexicographic_order

   149 termination by lexicographic_order

   152 

   150 

   153 lemma [eqvt]:

   151 lemma [eqvt]: