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
|
==========================================
irredundant unify in U-TEST : X =? f(Z, Y) /\ Z =? f(X, Y) /\ f(X, Y) =? f(A,
B) .
Unifier 1
X --> f(#1:Foo, #2:Foo)
Z --> f(#1:Foo, #2:Foo)
Y --> 1
A --> #1:Foo
B --> #2:Foo
==========================================
irredundant unify in U-TEST : f(X, Y) =? a /\ Z =? f(X, Y) /\ X =? f(Z, Y) .
Unifier 1
X --> a
Y --> 1
Z --> a
==========================================
irredundant unify in U-TEST : X =? f(f(f(X, Y), X), Y) .
Unifier 1
X --> 1
Y --> 1
==========================================
irredundant unify in U-TEST : X =? f(f(f(X, X), Z), Y) .
Unifier 1
X --> 1
Z --> 1
Y --> 1
==========================================
irredundant unify in U-TEST : X =? f(f(X, Y), f(Y, X)) .
Unifier 1
X --> 1
Y --> 1
==========================================
irredundant unify in U-TEST : X =? f(f(f(f(Y, X), Y), X), Z) .
Unifier 1
X --> 1
Y --> 1
Z --> 1
==========================================
irredundant unify in CU-TEST : X =? f(Z, Y) /\ Z =? f(X, Y) /\ f(X, Y) =? f(A,
B) .
Unifier 1
X --> f(#1:Foo, #2:Foo)
Z --> f(#1:Foo, #2:Foo)
Y --> 1
A --> #1:Foo
B --> #2:Foo
==========================================
irredundant unify in CU-TEST : f(X, Y) =? a /\ Z =? f(X, Y) /\ X =? f(Z, Y) .
Unifier 1
X --> a
Y --> 1
Z --> a
==========================================
irredundant unify in CU-TEST : X =? f(f(f(X, Y), X), Y) .
Unifier 1
X --> 1
Y --> 1
==========================================
irredundant unify in CU-TEST : X =? f(f(f(X, X), Z), Y) .
Unifier 1
X --> 1
Y --> 1
Z --> 1
==========================================
irredundant unify in CU-TEST : X =? f(f(f(f(Y, X), Y), X), Z) .
Unifier 1
X --> 1
Z --> 1
Y --> 1
Bye.
|
