simp [sup_eq_max]
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ ({0, 1}.sup fun i => (![t, u] i).complexity) = max t.complexity u.complexity
no goals