knuth_bendix_egraph/math_converted5.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
34
Mul(a, b) = Mul(b, a)
Mul(a, b) = Mul(b, a)
Mul(a, Mul(b, c)) = Mul(Mul(a, b), c)
Mul(a, Mul(b, c)) = Mul(Mul(a, b), c)
Sub(a, b) = Mul(a, Mul(-One, b))
Div(a, b) = Mul(a, Pow(b, -One))
Mul(a, Zero) = a
Mul(a, Zero) = Zero
Mul(a, One) = a
a = Mul(a, Zero)
a = Mul(a, One)
Sub(a, a) = Zero
Div(a, a) = One
Mul(a, Mul(b, c)) = Mul(Mul(a, b), Mul(a, c))
Mul(Mul(a, b), Mul(a, c)) = Mul(a, Mul(b, c))
Mul(Pow(a, b), Pow(a, c)) = Pow(a, Mul(b, c))
Pow(x, Zero) = One
Pow(x, One) = x
Pow(x, Two) = Mul(x, x)
Pow(x, -One) = Div(One, x)
Mul(x, Div(One, x)) = One
D(x, x) = One
D(x, Mul(a, b)) = Mul(D(x, a), D(x, b))
D(x, Mul(a, b)) = Mul(Mul(a, D(x, b)), Mul(b, D(x, a)))
D(x, Sin(x)) = Cos(x)
D(x, Cos(x)) = Mul(-One, Sin(x))
D(x, Ln(x)) = Div(One, x)
D(x, Pow(f, g)) = Mul(Pow(f, g), Mul(Mul(D(x, f), Div(g, f)), Mul(D(x, g), Ln(f))))
I(One, x) = x
I(Cos(x), x) = Sin(x)
I(Sin(x), x) = Mul(-One, Cos(x))
I(Mul(f, g), x) = Mul(I(f, x), I(g, x))
I(Sub(f, g), x) = Sub(I(f, x), I(g, x))
I(Mul(a, b), x) = Sub(Mul(a, I(b, x)), I(Mul(D(x, a), I(b, x)), x))