30 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"

    31   by (simp add: permute_pure)

    32 

    33 nominal_primrec

    34     height_trm :: "trm \<Rightarrow> nat"

    35 and height_bp :: "bp \<Rightarrow> nat"

    36 where

    37   "height_trm (Var x) = 1"

    38 | "height_trm (App l r) = max (height_trm l) (height_trm r)"

    39 | "height_trm (Lam v b) = 1 + (height_trm b)"

    40 | "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)"

    41 | "height_bp (Bp v t) = height_trm t"

    42   apply (simp only: eqvt_def height_trm_height_bp_graph_def)

    43   apply (rule, perm_simp, rule, rule TrueI)

    44   apply auto

    45   apply (case_tac x)

    46   apply (case_tac a rule: let_rec.exhaust(1))

    47   apply auto

    48   apply (case_tac b rule: let_rec.exhaust(2))

    49   apply blast

    50   apply (erule Abs_set_fcb)

    51   apply (simp_all add: pure_fresh)

    52   apply (simp add: eqvt_at_def)

    53   apply (simp add: Abs_eq_iff2)

    54   apply (simp add: alphas)

    55   apply clarify

    56   apply (rule trans)

    57   apply(rule_tac p="p" in supp_perm_eq[symmetric])

    58   apply (simp add: pure_supp fresh_star_def)

    59   apply (simp only: eqvts)

    60   apply (simp add: eqvt_at_def)

    61   done

    62 

    63 termination by lexicographic_order