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
|
Maude> ==========================================
reduce in META-LEVEL : metaReduce(['BOOL], 'true.Bool) .
rewrites: 2
result ResultPair: {'true.Bool,'Bool}
==========================================
reduce in META-LEVEL : upTerm(1) .
rewrites: 1
result GroundTerm: 's_['0.Zero]
==========================================
reduce in META-LEVEL : upTerm(X:Nat + 21) .
rewrites: 1
result Term: '_+_['X:Nat,'s_^21['0.Zero]]
==========================================
reduce in META-LEVEL : downTerm('s_['0.Zero], 0) .
rewrites: 1
result NzNat: 1
==========================================
reduce in META-LEVEL : downTerm('_+_['X:Nat,'s_^21['0.Zero]], 0) .
rewrites: 1
result NzNat: X:Nat + 21
==========================================
reduce in META-LEVEL : upTerm(upTerm(X:Nat + 21)) .
rewrites: 2
result GroundTerm: '_`[_`][''_+_.Sort,'_`,_[''X:Nat.Variable,'_`[_`][
''s_^21.Sort,''0.Zero.Constant]]]
==========================================
reduce in META-LEVEL : upTerm(upTerm(upTerm(X:Nat + 21))) .
rewrites: 3
result GroundTerm: '_`[_`][''_`[_`].Qid,'_`,_['''_+_.Sort.Constant,'_`[_`][
''_`,_.Qid,'_`,_['''X:Nat.Variable.Constant,'_`[_`][''_`[_`].Qid,'_`,_[
'''s_^21.Sort.Constant,'''0.Zero.Constant.Constant]]]]]]
==========================================
reduce in META-LEVEL : downTerm(upTerm(X:Nat + 21), 0) .
rewrites: 2
result NzNat: X:Nat + 21
==========================================
reduce in META-LEVEL : downTerm(downTerm(upTerm(upTerm(X:Nat + 21)), X:Term),
0) .
rewrites: 4
result NzNat: X:Nat + 21
==========================================
reduce in META-LEVEL : downTerm(downTerm(downTerm(upTerm(upTerm(upTerm(X:Nat +
21))), X:Term), X:Term), 0) .
*********** equation
(built-in equation for symbol upTerm)
upTerm(X:Nat + 21)
--->
'_+_['X:Nat,'s_^21['0.Zero]]
*********** equation
(built-in equation for symbol upTerm)
upTerm('_+_['X:Nat,'s_^21['0.Zero]])
--->
'_`[_`][''_+_.Sort,'_`,_[''X:Nat.Variable,'_`[_`][''s_^21.Sort,
''0.Zero.Constant]]]
*********** equation
(built-in equation for symbol upTerm)
upTerm('_`[_`][''_+_.Sort,'_`,_[''X:Nat.Variable,'_`[_`][''s_^21.Sort,
''0.Zero.Constant]]])
--->
'_`[_`][''_`[_`].Qid,'_`,_['''_+_.Sort.Constant,'_`[_`][''_`,_.Qid,'_`,_[
'''X:Nat.Variable.Constant,'_`[_`][''_`[_`].Qid,'_`,_[
'''s_^21.Sort.Constant,'''0.Zero.Constant.Constant]]]]]]
*********** equation
(built-in equation for symbol downTerm)
downTerm('_`[_`][''_`[_`].Qid,'_`,_['''_+_.Sort.Constant,'_`[_`][''_`,_.Qid,
'_`,_['''X:Nat.Variable.Constant,'_`[_`][''_`[_`].Qid,'_`,_[
'''s_^21.Sort.Constant,'''0.Zero.Constant.Constant]]]]]], X:Term)
--->
'_`[_`][''_+_.Sort,'_`,_[''X:Nat.Variable,'_`[_`][''s_^21.Sort,
''0.Zero.Constant]]]
*********** equation
(built-in equation for symbol downTerm)
downTerm('_`[_`][''_+_.Sort,'_`,_[''X:Nat.Variable,'_`[_`][''s_^21.Sort,
''0.Zero.Constant]]], X:Term)
--->
'_+_['X:Nat,'s_^21['0.Zero]]
*********** equation
(built-in equation for symbol downTerm)
downTerm('_+_['X:Nat,'s_^21['0.Zero]], 0)
--->
X:Nat + 21
rewrites: 6
result NzNat: X:Nat + 21
==========================================
reduce in UP-DOWN-TEST : upTerm(f(a, f(b, c))) .
rewrites: 2
result GroundTerm: 'f['a.Foo,'f['b.Foo,'d.Foo]]
==========================================
reduce in UP-DOWN-TEST : upTerm(upTerm(f(a, f(b, c)))) .
rewrites: 3
result GroundTerm: '_`[_`][''f.Sort,'_`,_[''a.Foo.Constant,'_`[_`][''f.Sort,
'_`,_[''b.Foo.Constant,''d.Foo.Constant]]]]
==========================================
reduce in UP-DOWN-TEST : downTerm(upTerm(upTerm(f(a, f(b, c)))), X:Term) .
rewrites: 4
result GroundTerm: 'f['a.Foo,'f['b.Foo,'d.Foo]]
==========================================
reduce in UP-DOWN-TEST : downTerm(downTerm(upTerm(upTerm(f(a, f(b, c)))),
X:Term), a) .
rewrites: 5
result Foo: f(a, f(b, d))
==========================================
reduce in UP-DOWN-TEST : downTerm('f['a.Foo,'f['b.Foo,'c.Foo]], a) .
rewrites: 2
result Foo: f(a, f(b, d))
Maude> Bye.
|
