### CSI-0.1

``````Problem:
*(e(),x) -> x
*(-(x),x) -> e()
*(*(x,y),z) -> *(x,*(y,z))
*(-(x),*(x,y)) -> y
*(x,e()) -> x
-(e()) -> e()
-(-(x)) -> x
*(x,-(x)) -> e()
*(x,*(-(x),y)) -> y
-(*(x,y)) -> *(-(y),-(x))

Proof:
Church Rosser Transformation Processor (kb):
*(e(),x) -> x
*(-(x),x) -> e()
*(*(x,y),z) -> *(x,*(y,z))
*(-(x),*(x,y)) -> y
*(x,e()) -> x
-(e()) -> e()
-(-(x)) -> x
*(x,-(x)) -> e()
*(x,*(-(x),y)) -> y
-(*(x,y)) -> *(-(y),-(x))
critical peaks: joinable
Matrix Interpretation Processor: dim=1

interpretation:
[-](x0) = 2x0 + 3,

[*](x0, x1) = x0 + x1 + 3,

[e] = 6
orientation:
*(e(),x) = x + 9 >= x = x

*(-(x),x) = 3x + 6 >= 6 = e()

*(*(x,y),z) = x + y + z + 6 >= x + y + z + 6 = *(x,*(y,z))

*(-(x),*(x,y)) = 3x + y + 9 >= y = y

*(x,e()) = x + 9 >= x = x

-(e()) = 15 >= 6 = e()

-(-(x)) = 4x + 9 >= x = x

*(x,-(x)) = 3x + 6 >= 6 = e()

*(x,*(-(x),y)) = 3x + y + 9 >= y = y

-(*(x,y)) = 2x + 2y + 9 >= 2x + 2y + 9 = *(-(y),-(x))
problem:
*(-(x),x) -> e()
*(*(x,y),z) -> *(x,*(y,z))
*(x,-(x)) -> e()
-(*(x,y)) -> *(-(y),-(x))
Matrix Interpretation Processor: dim=1

interpretation:
[-](x0) = 6x0,

[*](x0, x1) = x0 + x1 + 4,

[e] = 4
orientation:
*(-(x),x) = 7x + 4 >= 4 = e()

*(*(x,y),z) = x + y + z + 8 >= x + y + z + 8 = *(x,*(y,z))

*(x,-(x)) = 7x + 4 >= 4 = e()

-(*(x,y)) = 6x + 6y + 24 >= 6x + 6y + 4 = *(-(y),-(x))
problem:
*(-(x),x) -> e()
*(*(x,y),z) -> *(x,*(y,z))
*(x,-(x)) -> e()
Matrix Interpretation Processor: dim=1

interpretation:
[-](x0) = 4x0 + 1,

[*](x0, x1) = 4x0 + x1,

[e] = 1
orientation:
*(-(x),x) = 17x + 4 >= 1 = e()

*(*(x,y),z) = 16x + 4y + z >= 4x + 4y + z = *(x,*(y,z))

*(x,-(x)) = 8x + 1 >= 1 = e()
problem:
*(*(x,y),z) -> *(x,*(y,z))
*(x,-(x)) -> e()
Matrix Interpretation Processor: dim=1

interpretation:
[-](x0) = x0,

[*](x0, x1) = x0 + x1 + 1,

[e] = 0
orientation:
*(*(x,y),z) = x + y + z + 2 >= x + y + z + 2 = *(x,*(y,z))

*(x,-(x)) = 2x + 1 >= 0 = e()
problem:
*(*(x,y),z) -> *(x,*(y,z))
Matrix Interpretation Processor: dim=1

interpretation:
[*](x0, x1) = 2x0 + x1 + 1
orientation:
*(*(x,y),z) = 4x + 2y + z + 3 >= 2x + 2y + z + 2 = *(x,*(y,z))
problem:

Qed

``````
Nach oben scrollen