knuth_bendix_egraph/math_converted7.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
35
36
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)
D(x, x) = One
D(x, Add(a, b)) = Add(D(x, a), D(x, b))
D(x, Mul(a, b)) = Add(Mul(a, D(x, b)), Mul(b, D(x, a)))
D(x, Sin(x)) = Cos(x)
D(x, Cos(x)) = Mul(MinusOne, Sin(x))
D(x, Ln(x)) = If(Eq(x,Zero),D(x, Ln(x)),Div(One, x))
D(x, Pow(f, g)) = If(Eq(f,zero),D(x, Pow(f, g)),If(Eq(g,zero),D(x, Pow(f, g)),Mul(Pow(f, g), Add(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(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))
I(Mul(a, b), x) = Sub(Mul(a, I(b, x)), I(Mul(D(x, a), I(b, x)), x))

If(Eq(x,x),y,z) = y