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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
set show timing off .
set show advisories off .
fmod DECOMPOSE is
inc INITIAL-EQUALITY-PREDICATE .
sorts Nat String .
op 0 : -> Nat .
ops f g : Nat Nat -> Nat [ctor] .
ops h i : Nat Nat -> String [ctor] .
op c : Nat Nat -> Nat [ctor comm] .
ops b : Nat Nat -> Nat [assoc comm id: 0] .
op s : Nat -> Nat [iter ctor] .
vars W X Y Z : Nat .
vars A B C D : Nat .
endfm
red X .=. X .
red X .=. Y .
*** free
red f(X, Y) .=. f(Y, Z) .
red f(X, Y) .=. f(Y, X) .
red f(X, Y) .=. X .
red f(f(X, Y), Z) .=. f(X, Y) .
red f(X, Y) .=. g(W, Z) .
red h(X, Y) .=. h(W, Z) .
red h(X, Y) .=. h(Y, X) .
red h(X, Y) .=. i(W, Z) .
*** dissimilar collapse symbol
red f(X, Y) .=. b(W, Z) .
*** iter
red s^100(X) .=. s^40(X) .
red s^100(X) .=. s^40(Y) .
red s^10(X) .=. s^10(Y) .
*** commutative
red c(X, Y) .=. c(A, B) .
red c(X, Y) .=. c(A, X) .
red c(c(X, Y), Z) .=. c(X, Y) .
*** compound
red c(f(X, Y), g(W, Z)) .=. c(g(A, B), f(C, D)) .
red c(f(X, Y), g(W, Z)) .=. c(f(A, B), f(C, D)) .
fmod FOO is
inc INITIAL-EQUALITY-PREDICATE .
sort Foo .
ops a b c 1 : -> Foo .
op __ : Foo Foo -> Foo [assoc] .
op _+_ : Foo Foo -> Foo [assoc comm] .
op s : Foo Foo -> Foo [comm] .
op f : Foo Foo -> Foo [assoc comm id: 1] .
ops g h p : Foo -> Foo .
var A B C D E W X Y Z : Foo .
eq p(X) = g(h(X)) .
endfm
*** ctor declaration not needed for decomposition
red g(X) .=. g(Y) .
*** ground vs equationally-stable
red f(a, g(b), c) .=. h(X) .
*** canceling under commutative
red s(g(X), Z) .=. s(Y, g(X)) .
*** AC
red g(A) + g(B) + g(C) .=. g(A) + B + h(C) .
red g(A) + g(B) + g(C) .=. g(A) + B .
*** associative
red g(A) (B) X h(A) Y h(C) .=. h(A) g(D) g(E) Z X h(A) .
red g(A) X Y h(A) h(C) .=. g(D) g(E) g(D) X h(A) .
red g(A) g(B) X h(A) Y h(C) .=. g(D) g(E) Z X h(A) .
|
