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
|
==========================================
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))
Bye.
|
