# Is it a valid number theory expression?

A number theory expression contains:

There exists at least one non-negative integer (written as E, existential quantifier)
All non-negative integers (written as A, universal quantifier)
* (multiplication)
= (equality)
>, < (comparison operators)
&(and), |(or), !(not)
(, ) (for grouping)
variable names(all lowercase letters and numbers, not necessary one char long)


However, it has some more limitations:

• Arithmetic expressions should be syntactically valid. Here we only treat + as addition, not positive, so + and * should be surrounded by two number expressions
• brackets should be well paired
• < = > should be surrounded by two number expressions
• & | ! are fed with logical expressions
• E and A are fed with a variable and an expression
• For E and A, there should be a reasonable affected range. (*)

For (*): We write Ax Ey y>x & y=x, Ax Ey y>x & Ey y=x as well as Ax Ey y>x & Ax Ey y=x, which mean Ax (Ey ((y>x) & (y=x))), Ax ((Ey (y>x)) & (Ey (y=x))) and (Ax (Ey (y>x))) & (Ax (Ey (y=x))); however we don't write Ax Ey Ax x=y or Ax Ey x<y & Ex x>y. That means there should be some way to add brackets, so everywhere any variable is at most defined for once, and anywhere that use the variable has it defined.

## Input

You'll be given an expression with these chars (invalid chars won't appear), only split when necessary (two variable names together), split after each quantifier variable, or each symbols are separated. No invalid symbol.

## Output

Check whether it's a valid number theory expression. Either true/false or multi/one are allowed.

## True samples (each symbol separated)

E a E b a < b
E b A x b < x & A x b > x
E b A x b < x & b > x
A b b + b < ( b + b ) * b | E x x < b
E x E y y < x & E x2 y = x2
E 1 A x x * 1 = x & E 2 2 * 2 = 2 + 2 & 2 > 1 & E x x + 1 = x * x * 2
E x E y y = y & y + y * y = y


## False samples

E a E b a + b < c
E a E b b * ( a > a ) + b
A a A b ( a = b ) = b
A x A y A z A y x < z
E x E y y < x & E x y = x
E E x x = x
E x ( x < x
E x = x


## Undefined behavior samples

E C C = C
AA x x = x
Ex = x


Shortest code in bytes win

Symbol definition: It's a resexpr

numexpr({s},∅) = s
numexpr(a∪b,c∪d) = numexpr(a,c) + numexpr(b,d)
numexpr(a∪b,c∪d) = numexpr(a,c) * numexpr(b,d)
numexpr(a,c) = ( numexpr(a,c) )
boolexpr(a∪b,c∪d) = numexpr(a,c) = numexpr(b,d)
boolexpr(a∪b,c∪d) = numexpr(a,c) < numexpr(b,d)
boolexpr(a∪b,c∪d) = numexpr(a,c) > numexpr(b,d)
boolexpr(a∪b,c∪d) = boolexpr(a,c) & boolexpr(b,d)
boolexpr(a∪b,c∪d) = boolexpr(a,c) | boolexpr(b,d)
boolexpr(a,c) = ! boolexpr(a,c)
boolexpr(a,c) = ( boolexpr(a,c) )
boolexpr(a-{s},c∪{s}) = E s boolexpr(a,c) if s∉c
boolexpr(a-{s},c∪{s}) = A s boolexpr(a,c) if s∉c
resexpr = boolexpr(∅,a)
a,b,c,d mean sets, s mean non-empty strings containing a-z0-9


## Notes

• You don't need to check whether the expression is true, as it's usually impossible
• What does the symbol definition block mean in the challenge context? – Nit Apr 7 '18 at 10:14
• @Nit It's like a BNF but with infinite expressions, so I write it in this kind of view. Different expressions can lead to same elementnumexpr(a,c), meaning "or" in BNF – l4m2 Apr 7 '18 at 10:44
• Sandbox undeleted – l4m2 Apr 7 '18 at 10:47
• @orlp I think that parsing and the expression being ambiguous is actually the main part of the challenge. – user202729 Apr 7 '18 at 10:56
• Holy moly I'm blind... The challenge is about syntax verification, not seeing whether the expression is true... Never mind... – orlp Apr 7 '18 at 12:08