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
|
==========================================
reduce in META-TEST : metaVariantMatch(['XOR], upTerm(cst1 + X:XOR) <=? upTerm(
cst2 + Y:XOR), empty, '#, none, 0) .
rewrites: 7
result Assignment:
'X:XOR <- '_+_['cst1.Elem, 'cst2.Elem, 'Y:XOR]
==========================================
reduce in META-TEST : metaVariantMatch(['XOR], upTerm(cst1 + X:XOR) <=? upTerm(
cst2 + Y:XOR), empty, '#, none, 1) .
rewrites: 4
result Substitution?: (noMatch).Substitution?
==========================================
reduce in META-TEST : metaVariantMatch(['XOR], upTerm(X:XOR + Y:XOR) <=?
upTerm(cst1 + cst2), empty, '#, none, 0) .
rewrites: 14
result Substitution:
'X:XOR <- 'cst1.Elem ;
'Y:XOR <- 'cst2.Elem
==========================================
reduce in META-TEST : metaVariantMatch(['XOR], upTerm(X:XOR + Y:XOR) <=?
upTerm(cst1 + cst2), empty, '#, none, 1) .
rewrites: 4
result Substitution:
'X:XOR <- 'cst2.Elem ;
'Y:XOR <- 'cst1.Elem
==========================================
reduce in META-TEST : metaVariantMatch(['XOR], upTerm(X:XOR + Y:XOR) <=?
upTerm(cst1 + cst2), empty, '#, none, 2) .
rewrites: 4
result Substitution:
'X:XOR <- '0.XOR ;
'Y:XOR <- '_+_['cst1.Elem, 'cst2.Elem]
==========================================
reduce in META-TEST : metaVariantMatch(['XOR], upTerm(X:XOR + Y:XOR) <=?
upTerm(cst1 + cst2), empty, '#, none, 3) .
rewrites: 4
result Substitution:
'X:XOR <- '_+_['cst1.Elem, 'cst2.Elem] ;
'Y:XOR <- '0.XOR
==========================================
reduce in META-TEST : metaVariantMatch(['XOR], upTerm(X:XOR + Y:XOR) <=?
upTerm(cst1 + cst2), empty, '#, none, 4) .
rewrites: 4
result Substitution:
'X:XOR <- '_+_['cst1.Elem, '#1:XOR] ;
'Y:XOR <- '_+_['cst2.Elem, '#1:XOR]
==========================================
reduce in META-TEST : metaVariantMatch(['XOR], upTerm(X:XOR + Y:XOR) <=?
upTerm(cst1 + cst2), empty, '#, none, 5) .
rewrites: 4
result Substitution:
'X:XOR <- '_+_['cst2.Elem, '#1:XOR] ;
'Y:XOR <- '_+_['cst1.Elem, '#1:XOR]
==========================================
reduce in META-TEST : metaVariantMatch(['XOR], upTerm(X:XOR + Y:XOR) <=?
upTerm(cst1 + cst2), empty, '#, none, 6) .
rewrites: 4
result Substitution:
'X:XOR <- '_+_['cst1.Elem, 'cst2.Elem, '#1:XOR] ;
'Y:XOR <- '#1:XOR
==========================================
reduce in META-TEST : metaVariantMatch(['XOR], upTerm(X:XOR + Y:XOR) <=?
upTerm(cst1 + cst2), empty, '#, none, 7) .
rewrites: 4
result Substitution:
'X:XOR <- '#1:XOR ;
'Y:XOR <- '_+_['cst1.Elem, 'cst2.Elem, '#1:XOR]
==========================================
reduce in META-TEST : metaVariantMatch(['XOR], upTerm(X:XOR + Y:XOR) <=?
upTerm(cst1 + cst2), empty, '#, none, 8) .
rewrites: 4
result Substitution?: (noMatch).Substitution?
Bye.
|
