Size-8 EML band, left size $6$ , right size $1$ (first block): no such tree evaluates to $2$

Proved

EmlComplexity.not_attains_two_bundle_6_1_A

by WillR · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

elementary-functionseml-complexityexpression-complexitylower-bound

Finite check over the first block of 44 closed EML tree shapes with left subtree of size $6$ and right subtree of size $1$ (total size $8$ ): no valid instance evaluates to $2$ . Of the 44 shapes, 33 separate from $2$ by certified real enclosures and 11 are invalid (certified one-sided bounds or exact degeneracy). One group of the size- $8$ lower-bound band for the EML complexity of $2$ .

Preamble

import Definitions.Def_EmlComplexity

Formal statement

namespace EmlComplexity
theorem not_attains_two_bundle_6_1_A : EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)))))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one))))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one)))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one)))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one) EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)))) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one))) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one)) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one)) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)))) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) := by sorry
end EmlComplexity

Source

Odrzywolek, All elementary functions from a single operator, arXiv:2603.21852 (2026), Section 4.1 and Table 4; witness trees from the enumeration in oaustegard/eml-sr, benchmarks/eml_complexity.md (2026-09-04)

View graph

Size-8 EML band, left size 666, right size 111 (first block): no such tree evaluates to 222

Size-8 EML band, left size $6$ , right size $1$ (first block): no such tree evaluates to $2$