knuth_bendix_egraph/math_converted9.rule at v4 · NeuralCoder3/knuth_bendix_egraph · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
Add(a, b) = Add(b, a)
Mul(a, b) = Mul(b, a)
Add(a, Add(b, c)) = Add(Add(a, b), c)
Mul(a, Mul(b, c)) = Mul(Mul(a, b), c)
Sub(a, b) = Add(a, Mul(MinusOne, b))
Div(a, b) = Mul(a, Pow(b, MinusOne))
Add(a, Zero) = a
Mul(a, Zero) = Zero
Mul(a, One) = a
a = Add(a, Zero)
a = Mul(a, One)
Sub(a, a) = Zero
Div(a, a) = If(Eq(a,Zero),Div(a,a),One)
Mul(a, Add(b, c)) = Add(Mul(a, b), Mul(a, c))
Add(Mul(a, b), Mul(a, c)) = Mul(a, Add(b, c))
Mul(Pow(a, b), Pow(a, c)) = Pow(a, Add(b, c))
Pow(x, Zero) = If(Eq(x,Zero),Pow(x, Zero),One)
Pow(x, One) = x
Pow(x, Two) = Mul(x, x)
Pow(x, MinusOne) = If(Eq(x,Zero),Pow(x, MinusOne),Div(One, x))
Mul(x, Div(One, x)) = If(Eq(x,Zero),Mul(x, Div(One, x)),One)
I(One, x) = x
I(Cos(x), x) = Sin(x)
I(Sin(x), x) = Mul(MinusOne, Cos(x))
I(Add(f, g), x) = Add(I(f, x), I(g, x))
I(Sub(f, g), x) = Sub(I(f, x), I(g, x))
If(True,y,z) = y
If(False,y,z) = z
Eq(x,x) = True
Eq(A,Zero) = False
Eq(Y,Zero) = False
Eq(B,Zero) = False
Eq(One,Zero) = False