### CSI-0.1

``````Problem:
Ap(Ap(Ap(S(),x),y),z) -> Ap(Ap(x,z),Ap(y,z))
Ap(Ap(K(),x),y) -> x
Ap(I(),x) -> x
B(true(),x,y) -> x
B(false(),x,y) -> y
B(z,x,x) -> x

Proof:
sorted: (order)
0:B(true(),x,y) -> x
B(false(),x,y) -> y
B(z,x,x) -> x
1:Ap(Ap(Ap(S(),x),y),z) -> Ap(Ap(x,z),Ap(y,z))
Ap(Ap(K(),x),y) -> x
Ap(I(),x) -> x
-----
sorts
[1>2, 2>3, 2>4, 5>6, 5>7, 5>8]
sort attachment (strict)
Ap : 5 x 5 -> 5
S : 8
K : 7
I : 6
B : 2 x 1 x 1 -> 1
true : 4
false : 3
-----
0:B(true(),x,y) -> x
B(false(),x,y) -> y
B(z,x,x) -> x
Church Rosser Transformation Processor (kb):
B(true(),x,y) -> x
B(false(),x,y) -> y
B(z,x,x) -> x
critical peaks: joinable
Matrix Interpretation Processor: dim=1

interpretation:
[false] = 0,

[B](x0, x1, x2) = x0 + x1 + x2 + 3,

[true] = 0
orientation:
B(true(),x,y) = x + y + 3 >= x = x

B(false(),x,y) = x + y + 3 >= y = y

B(z,x,x) = 2x + z + 3 >= x = x
problem:

Qed

1:Ap(Ap(Ap(S(),x),y),z) -> Ap(Ap(x,z),Ap(y,z))
Ap(Ap(K(),x),y) -> x
Ap(I(),x) -> x
Church Rosser Transformation Processor:

strict:

weak:

critical peaks: 0
Qed

``````
Nach oben scrollen