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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
set show timing off .
set show advisories off .
mod COUNTER-TEST is
inc COUNTER .
sort List .
subsort Nat < List .
op __ : List List -> List [assoc id: nil] .
op nil : -> List .
op f : Nat -> List .
var N : Nat .
eq f(s N) = counter f(N) .
eq f(0) = nil .
endm
rew counter .
rew f(11) .
rew f(11) .
set clear rules off .
rew f(11) .
set clear rules on .
rew f(11) .
mod COUNTER-TEST2 is
inc COUNTER .
inc RANDOM .
sort List .
subsort Nat < List .
op __ : List List -> List [assoc id: nil] .
op nil : -> List .
op f : Nat -> List .
var N : Nat .
eq f(s N) = random(counter) f(N) .
eq f(0) = nil .
endm
rew random(counter) .
rew f(11) .
rew f(100) .
mod FOO is
sort Foo .
ops a b c d e : -> Foo .
rl a => b .
rl a => c .
rl a => d .
rl a => e .
endm
rew a .
rew a .
set clear rules off .
rew a .
rew a .
rew a .
rew a .
set clear rules on .
rew a .
mod COUNTER-TEST3 is
inc COUNTER .
sort List .
subsort Nat < List .
op __ : List List -> List [assoc id: nil] .
op nil : -> List .
op f : Nat -> List .
var N : Nat .
eq f(s N) = counter f(N) .
eq f(0) = nil .
endm
debug rew f(4) .
step .
step .
step .
step .
step .
step .
step .
rew counter .
resume .
debug frew f(4) .
step .
step .
step .
step .
step .
step .
step .
rew counter .
resume .
rew [4] f(8) .
cont .
mod COUNTER-TEST4 is
inc COUNTER .
inc COUNTER * (op counter to counter2) .
sort List .
subsort Nat < List .
op __ : List List -> List [assoc id: nil] .
op nil : -> List .
op f : Nat -> List .
var N : Nat .
eq f(s N) = counter (counter2 f(N)) .
eq f(0) = nil .
endm
rew f(4) .
search f(4) =>* L:List .
red in META-LEVEL : metaRewrite(['COUNTER-TEST4], '__['counter.Nat,
'counter.Nat], 2) .
|
