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
|
Maude> ==========================================
reduce in TEST : metaXapply(m, 'f['a.Foo,'b.Foo], 'k, none, 0, 100, 0) .
rewrites: 3
result Result4Tuple: {'a.Foo,'Foo,
'X:Foo <- 'a.Foo ;
'Y:Foo <- 'b.Foo,[]}
==========================================
reduce in TEST : metaXapply(m, 'f['a.Foo,'b.Foo], 'k, none, 0, 100, 1) .
rewrites: 3
result Result4Tuple: {'b.Foo,'Foo,
'X:Foo <- 'b.Foo ;
'Y:Foo <- 'a.Foo,[]}
==========================================
reduce in TEST : metaXapply(m, 'f['a.Foo,'b.Foo], 'k, none, 0, 100, 2) .
rewrites: 3
result Result4Tuple: {'f['b.Foo,'c.Foo],'Foo,none,'f['b.Foo,[]]}
==========================================
reduce in TEST : metaXapply(m, 'f['a.Foo,'b.Foo], 'k, none, 0, 100, 3) .
rewrites: 2
result Result4Tuple?: (failure).Result4Tuple?
==========================================
reduce in TEST : metaXapply(m, 'f['a.Foo,'b.Foo], 'k, none, 0, unbounded, 0) .
rewrites: 3
result Result4Tuple: {'a.Foo,'Foo,
'X:Foo <- 'a.Foo ;
'Y:Foo <- 'b.Foo,[]}
==========================================
reduce in TEST : metaXapply(m, 'f['a.Foo,'b.Foo], 'k, none, 0, unbounded, 1) .
rewrites: 3
result Result4Tuple: {'b.Foo,'Foo,
'X:Foo <- 'b.Foo ;
'Y:Foo <- 'a.Foo,[]}
==========================================
reduce in TEST : metaXapply(m, 'f['a.Foo,'b.Foo], 'k, none, 0, unbounded, 2) .
rewrites: 3
result Result4Tuple: {'f['b.Foo,'c.Foo],'Foo,none,'f['b.Foo,[]]}
==========================================
reduce in TEST : metaXapply(m, 'f['a.Foo,'b.Foo], 'k, none, 0, unbounded, 3) .
rewrites: 2
result Result4Tuple?: (failure).Result4Tuple?
==========================================
reduce in TEST2 : metaXapply(m, 'g['f['a.Foo,'b.Foo],'a.Foo], 'k, none, 0, 100,
0) .
rewrites: 3
result Result4Tuple: {'g['c.Foo,'f['a.Foo,'b.Foo]],'Foo,none,'g['f['a.Foo,
'b.Foo],[]]}
==========================================
reduce in TEST2 : metaXapply(m, 'g['f['a.Foo,'b.Foo],'a.Foo], 'k, none, 0, 100,
1) .
rewrites: 3
result Result4Tuple: {'g['a.Foo,'a.Foo],'Foo,
'X:Foo <- 'a.Foo ;
'Y:Foo <- 'b.Foo,'g['a.Foo,[]]}
==========================================
reduce in TEST2 : metaXapply(m, 'g['f['a.Foo,'b.Foo],'a.Foo], 'k, none, 0, 100,
2) .
rewrites: 3
result Result4Tuple: {'g['a.Foo,'b.Foo],'Foo,
'X:Foo <- 'b.Foo ;
'Y:Foo <- 'a.Foo,'g['a.Foo,[]]}
==========================================
reduce in TEST2 : metaXapply(m, 'g['f['a.Foo,'b.Foo],'a.Foo], 'k, none, 0, 100,
3) .
rewrites: 3
result Result4Tuple: {'g['a.Foo,'f['b.Foo,'c.Foo]],'Foo,none,'g['a.Foo,'f[
'b.Foo,[]]]}
==========================================
reduce in TEST2 : metaXapply(m, 'g['f['a.Foo,'b.Foo],'a.Foo], 'k, none, 0, 100,
4) .
rewrites: 2
result Result4Tuple?: (failure).Result4Tuple?
==========================================
reduce in TEST3 : metaXapply(m, 'g['f['a.Foo,'b.Foo],'a.Foo], 'l, none, 0, 100,
0) .
rewrites: 3
result Result4Tuple: {'g['f['c.Foo,'c.Foo],'f['a.Foo,'b.Foo]],'Foo,none,'g['f[
'a.Foo,'b.Foo],[]]}
==========================================
reduce in TEST3 : metaXapply(m, 'g['f['a.Foo,'b.Foo],'a.Foo], 'l, none, 0, 100,
1) .
rewrites: 3
result Result4Tuple: {'g['a.Foo,'f['b.Foo,'c.Foo,'c.Foo]],'Foo,none,'g['a.Foo,
'f['b.Foo,[]]]}
==========================================
reduce in TEST3 : metaXapply(m, 'g['f['a.Foo,'b.Foo],'a.Foo], 'l, none, 0, 100,
0) .
rewrites: 3
result Result4Tuple: {'g['f['c.Foo,'c.Foo],'f['a.Foo,'b.Foo]],'Foo,none,'g['f[
'a.Foo,'b.Foo],[]]}
==========================================
reduce in TEST3 : metaXapply(m, 'g['f['a.Foo,'b.Foo],'a.Foo], 'l, none, 0, 100,
2) .
rewrites: 2
result Result4Tuple?: (failure).Result4Tuple?
==========================================
reduce in TEST3 : metaXapply(m, 'g['f['a.Foo,'b.Foo],'a.Foo], 'l, none, 0, 100,
0) .
rewrites: 3
result Result4Tuple: {'g['f['c.Foo,'c.Foo],'f['a.Foo,'b.Foo]],'Foo,none,'g['f[
'a.Foo,'b.Foo],[]]}
==========================================
reduce in ALL-ONE-STEP-REWRITES : findAllRews(m, 'f['a.Foo,'b.Foo], 'k) .
rewrites: 27
result TermSet: 'a.Foo | 'b.Foo | ('f['b.Foo,'c.Foo])
Maude> Bye.
|
