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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
==========================================
erewrite in VARIANT-UNIFY-TEST : <> < me : User | problem:('_+_['X:XOR,
'c1.Elem] =? '_+_['Y:XOR, 'c2.Elem], empty) > createInterpreter(
interpreterManager, me, none) .
rewrites: 52
result Configuration: <> < me : User | soln: 9, result(gotVariantUnifier(me,
interpreter(0), 6,
'X:XOR <- '_+_['c2.Elem, '@1:XOR] ;
'Y:XOR <- '_+_['c1.Elem, '@1:XOR], '@), gotVariantUnifier(me, interpreter(0),
0,
'X:XOR <- 'c2.Elem ;
'Y:XOR <- 'c1.Elem, '@), gotVariantUnifier(me, interpreter(0), 18,
'X:XOR <- '_+_['c1.Elem, 'c2.Elem, '%1:XOR] ;
'Y:XOR <- '%1:XOR, '%), gotVariantUnifier(me, interpreter(0), 0,
'X:XOR <- '%1:XOR ;
'Y:XOR <- '_+_['c1.Elem, 'c2.Elem, '%1:XOR], '%), gotVariantUnifier(me,
interpreter(0), 0,
'X:XOR <- '0.XOR ;
'Y:XOR <- '_+_['c1.Elem, 'c2.Elem], '@), gotVariantUnifier(me, interpreter(
0), 0,
'X:XOR <- 'c1.Elem ;
'Y:XOR <- 'c2.Elem, '@), gotVariantUnifier(me, interpreter(0), 0,
'X:XOR <- '_+_['c1.Elem, 'c2.Elem] ;
'Y:XOR <- '0.XOR, '@), gotVariantUnifier(me, interpreter(0), 0,
'X:XOR <- '_+_['c1.Elem, '@1:XOR] ;
'Y:XOR <- '_+_['c2.Elem, '@1:XOR], '@)), problem:('_+_['X:XOR, 'c1.Elem] =?
'_+_['Y:XOR, 'c2.Elem], empty) > noSuchResult(me, interpreter(0), 0, true)
==========================================
variant unify in XOR : X + c1 =? Y + c2 .
Unifier 1
rewrites: 6
X --> c2 + %1:XOR
Y --> c1 + %1:XOR
Unifier 2
rewrites: 6
X --> c2
Y --> c1
Unifier 3
rewrites: 24
X --> c1 + c2 + #1:XOR
Y --> #1:XOR
Unifier 4
rewrites: 24
X --> #1:XOR
Y --> c1 + c2 + #1:XOR
Unifier 5
rewrites: 24
X --> 0
Y --> c1 + c2
Unifier 6
rewrites: 24
X --> c1
Y --> c2
Unifier 7
rewrites: 24
X --> c1 + c2
Y --> 0
Unifier 8
rewrites: 24
X --> c1 + %1:XOR
Y --> c2 + %1:XOR
No more unifiers.
rewrites: 24
==========================================
erewrite in VARIANT-UNIFY-TEST : <> < me : User | problem:('_+_['X:XOR,
'c1.Elem] =? '_+_['Y:XOR, 'c2.Elem], '_+_['X:XOR, 'c1.Elem]) >
createInterpreter(interpreterManager, me, none) .
rewrites: 16
result Configuration: <> < me : User | soln: 4, result(gotVariantUnifier(me,
interpreter(0), 3,
'X:XOR <- '_+_['c2.Elem, '@1:XOR] ;
'Y:XOR <- '_+_['c1.Elem, '@1:XOR], '@), gotVariantUnifier(me, interpreter(0),
0,
'X:XOR <- 'c2.Elem ;
'Y:XOR <- 'c1.Elem, '@), gotVariantUnifier(me, interpreter(0), 0,
'X:XOR <- '%1:XOR ;
'Y:XOR <- '_+_['c1.Elem, 'c2.Elem, '%1:XOR], '%)), problem:('_+_['X:XOR,
'c1.Elem] =? '_+_['Y:XOR, 'c2.Elem], '_+_['X:XOR, 'c1.Elem]) >
noSuchResult(me, interpreter(0), 0, true)
==========================================
variant unify in XOR : X + c1 =? Y + c2 such that X + c1 irreducible .
Unifier 1
rewrites: 3
X --> c2 + %1:XOR
Y --> c1 + %1:XOR
Unifier 2
rewrites: 3
X --> c2
Y --> c1
Unifier 3
rewrites: 3
X --> #1:XOR
Y --> c1 + c2 + #1:XOR
No more unifiers.
rewrites: 3
==========================================
erewrite in DISJOINT-VARIANT-UNIFY-TEST : <> < me : User | problem:('_+_[
'X:XOR, 'c1.Elem] =? '_+_['Y:XOR, 'c2.Elem], empty) > createInterpreter(
interpreterManager, me, none) .
rewrites: 52
result Configuration: <> < me : User | soln: 9, result(
gotDisjointVariantUnifier(me, interpreter(0), 6,
'X:XOR <- '_+_['c2.Elem, '@1:XOR],
'Y:XOR <- '_+_['c1.Elem, '@1:XOR], '@), gotDisjointVariantUnifier(me,
interpreter(0), 0,
'X:XOR <- 'c2.Elem,
'Y:XOR <- 'c1.Elem, '@), gotDisjointVariantUnifier(me, interpreter(0), 18,
'X:XOR <- '_+_['c1.Elem, 'c2.Elem, '%1:XOR],
'Y:XOR <- '%1:XOR, '%), gotDisjointVariantUnifier(me, interpreter(0), 0,
'X:XOR <- '%1:XOR,
'Y:XOR <- '_+_['c1.Elem, 'c2.Elem, '%1:XOR], '%), gotDisjointVariantUnifier(
me, interpreter(0), 0,
'X:XOR <- '0.XOR,
'Y:XOR <- '_+_['c1.Elem, 'c2.Elem], '@), gotDisjointVariantUnifier(me,
interpreter(0), 0,
'X:XOR <- 'c1.Elem,
'Y:XOR <- 'c2.Elem, '@), gotDisjointVariantUnifier(me, interpreter(0), 0,
'X:XOR <- '_+_['c1.Elem, 'c2.Elem],
'Y:XOR <- '0.XOR, '@), gotDisjointVariantUnifier(me, interpreter(0), 0,
'X:XOR <- '_+_['c1.Elem, '@1:XOR],
'Y:XOR <- '_+_['c2.Elem, '@1:XOR], '@)), problem:('_+_['X:XOR, 'c1.Elem] =?
'_+_['Y:XOR, 'c2.Elem], empty) > noSuchResult(me, interpreter(0), 0, true)
==========================================
erewrite in DISJOINT-VARIANT-UNIFY-TEST : <> < me : User | problem:('_+_[
'X:XOR, 'c1.Elem] =? '_+_['Y:XOR, 'c2.Elem], '_+_['X:XOR, 'c1.Elem]) >
createInterpreter(interpreterManager, me, none) .
rewrites: 16
result Configuration: <> < me : User | soln: 4, result(
gotDisjointVariantUnifier(me, interpreter(0), 3,
'X:XOR <- '_+_['c2.Elem, '@1:XOR],
'Y:XOR <- '_+_['c1.Elem, '@1:XOR], '@), gotDisjointVariantUnifier(me,
interpreter(0), 0,
'X:XOR <- 'c2.Elem,
'Y:XOR <- 'c1.Elem, '@), gotDisjointVariantUnifier(me, interpreter(0), 0,
'X:XOR <- '%1:XOR,
'Y:XOR <- '_+_['c1.Elem, 'c2.Elem, '%1:XOR], '%)), problem:('_+_['X:XOR,
'c1.Elem] =? '_+_['Y:XOR, 'c2.Elem], '_+_['X:XOR, 'c1.Elem]) >
noSuchResult(me, interpreter(0), 0, true)
Bye.
|
