Optimization
optimize :: BAE -> BAE
optimize (Plus l r) = if (optimize l)==(Nat 0) then (optimize r) else (Plus (optimize l) (optimize r))
optimize (And l r) = if (optimize l)=(Boolean True) then (optimize r) else (And (optimize l) (optimize r))
optimize simply looks for places to 'compress' execution during runtime. For example optimize (Plus l r) looks if the left subtree is just 0 and returns the right subtree if so.