$ simple.0/0 D x x C x y C y y C y x $ simple.0/1 D x y C x (_. x) C y z C y x $ simple.0/2 D a (x. x b) (x. x c) C a (x. b b) @ C a @ c C a (x. x x) a C a (a a a) (a c c) $ simple.0/3 D x (y. x y y) C x (y. x y x) $ simple.0/4 D x a a a a C x b a a a C x a b a a C x a a b a C x a a a b $ simple.0/5 # Controesempio ad usare un conto dei lambda che non considera le permutazioni D x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b C x a a a a (_. a) b b b C x a a a a (_. _. _. _. x. y. x y) $ simple.0/6 # bug in eat that was erasing terms in convergent that then diverged D x y z C x @ @ C z (y @ (y @)) $ simple.0/7 # bug in no_leading_lambdas where x in j-th position D v0 (v1 v2) (x. y. v0 v3 v4 v2) C v5 (v6 (x. v6) v7 v8 (x. v9) (x. v9 (v10 v10))) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y))) (v9 (x. v11) (v4 v8) (x. y. z. v12) (v4 v6 (x. v7 v11) v12) (x. x v8)) (v0 v3 v4 v9 (v7 v11) (v0 v3 v4 v2) v10) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y)) (v9 (x. v11) (v4 v8)))