### CSI-0.1

``````Problem:
-(+(x,-(x))) -> 0()
+(x,-(x)) -> 0()
-(+(0(),0())) -> 0()
+(0(),0()) -> 0()
-(0()) -> 0()

Proof:
Church Rosser Transformation Processor (kb):
-(+(x,-(x))) -> 0()
+(x,-(x)) -> 0()
-(+(0(),0())) -> 0()
+(0(),0()) -> 0()
-(0()) -> 0()
critical peaks: joinable
Matrix Interpretation Processor: dim=3

interpretation:
[0]
[0] = [0]
[0],

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

[1 0 0]
[-](x0) = [0 0 0]x0
[0 0 0]
orientation:
[2 0 0]    [1]    [0]
-(+(x,-(x))) = [0 0 0]x + [0] >= [0] = 0()
[0 0 0]    [0]    [0]

[2 0 0]    [1]    [0]
+(x,-(x)) = [0 0 0]x + [0] >= [0] = 0()
[0 0 0]    [0]    [0]

[1]    [0]
-(+(0(),0())) = [0] >= [0] = 0()
[0]    [0]

[1]    [0]
+(0(),0()) = [0] >= [0] = 0()
[0]    [0]

[0]    [0]
-(0()) = [0] >= [0] = 0()
[0]    [0]
problem:
-(0()) -> 0()
Matrix Interpretation Processor: dim=3

interpretation:
[0]
[0] = [0]
[0],

[1 0 0]     [1]
[-](x0) = [0 0 0]x0 + [0]
[0 0 0]     [0]
orientation:
[1]    [0]
-(0()) = [0] >= [0] = 0()
[0]    [0]
problem:

Qed
``````
Nach oben scrollen