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
|
==========================================
reduce in TEST : metaFrewrite(m, t, 1, 1) .
rewrites: 5
result ResultPair: {'f['f['i['s_['0.Zero]], 'i['s_['0.Zero]]], 'f['i['s_^3[
'0.Zero]], 'i['s_^2['0.Zero]]]], 'Foo}
==========================================
reduce in TEST : metaFrewrite(m, t, 2, 1) .
rewrites: 7
result ResultPair: {'f['f['i['s_['0.Zero]], 'i['0.Zero]], 'f['i['s_^3[
'0.Zero]], 'i['s_^2['0.Zero]]]], 'Foo}
==========================================
reduce in TEST : metaFrewrite(m, t, 3, 1) .
rewrites: 8
result ResultPair: {'f['i['s_['0.Zero]], 'f['i['s_^3['0.Zero]], 'i['s_^2[
'0.Zero]]]], 'Foo}
==========================================
reduce in TEST : metaFrewrite(m, t, 4, 1) .
rewrites: 10
result ResultPair: {'f['i['s_['0.Zero]], 'f['i['s_^2['0.Zero]], 'i['s_^2[
'0.Zero]]]], 'Foo}
==========================================
reduce in TEST : metaFrewrite(m, t, 5, 1) .
rewrites: 12
result ResultPair: {'f['i['s_['0.Zero]], 'f['i['s_^2['0.Zero]], 'i['s_[
'0.Zero]]]], 'Foo}
==========================================
reduce in TEST : metaFrewrite(m, t, 6, 1) .
rewrites: 14
result ResultPair: {'f['i['0.Zero], 'f['i['s_^2['0.Zero]], 'i['s_['0.Zero]]]],
'Foo}
==========================================
reduce in TEST : metaFrewrite(m, t, 7, 1) .
rewrites: 16
result ResultPair: {'f['i['0.Zero], 'f['i['s_['0.Zero]], 'i['s_['0.Zero]]]],
'Foo}
==========================================
reduce in TEST : metaFrewrite(m, t, 8, 1) .
rewrites: 18
result ResultPair: {'f['i['0.Zero], 'f['i['s_['0.Zero]], 'i['0.Zero]]], 'Foo}
==========================================
reduce in TEST : metaFrewrite(m, t, 9, 1) .
rewrites: 19
result ResultPair: {'f['i['0.Zero], 'i['s_['0.Zero]]], 'Foo}
==========================================
reduce in TEST : metaFrewrite(m, t, 10, 1) .
rewrites: 21
result ResultPair: {'f['i['0.Zero], 'i['0.Zero]], 'Foo}
==========================================
reduce in TEST : metaFrewrite(m, t, 11, 1) .
rewrites: 22
result ResultPair: {'i['0.Zero], 'Foo}
==========================================
reduce in TEST : metaFrewrite(m, t, unbounded, 1) .
rewrites: 22
result ResultPair: {'i['0.Zero], 'Foo}
==========================================
reduce in TEST : metaFrewrite(m, t, 0, 1) .
rewrites: 2
result [ResultPair?]: metaFrewrite(mod 'FAIR is
protecting 'INT .
sorts 'Foo .
none
op 'f : 'Foo 'Foo -> 'Foo [none] .
op 'i : 'Int -> 'Foo [none] .
none
none
rl 'f['X:Foo, 'i['0.Nat]] => 'X:Foo [none] .
rl 'i['M:NzInt] => 'i['_-_['M:NzInt, 's_['0.Nat]]] [none] .
endm, 'f['f['i['s_^2['0.Nat]], 'i['s_['0.Nat]]], 'f['i['s_^3['0.Nat]], 'i[
's_^2['0.Nat]]]], 0, 1)
==========================================
reduce in TEST : metaFrewrite(m, t, 1, 0) .
rewrites: 2
result [ResultPair?]: metaFrewrite(mod 'FAIR is
protecting 'INT .
sorts 'Foo .
none
op 'f : 'Foo 'Foo -> 'Foo [none] .
op 'i : 'Int -> 'Foo [none] .
none
none
rl 'f['X:Foo, 'i['0.Nat]] => 'X:Foo [none] .
rl 'i['M:NzInt] => 'i['_-_['M:NzInt, 's_['0.Nat]]] [none] .
endm, 'f['f['i['s_^2['0.Nat]], 'i['s_['0.Nat]]], 'f['i['s_^3['0.Nat]], 'i[
's_^2['0.Nat]]]], 1, 0)
Bye.
|
