cl-banner

CSI-0.1


Problem:
 f(f(x,y),z) -> f(x,f(y,z))
 f(1(),x) -> x

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

   interpretation:
    [1] = 2,

    [f](x0, x1) = x0 + x1 + 1
   orientation:
    f(f(x,y),z) = x + y + z + 2 >= x + y + z + 2 = f(x,f(y,z))

    f(1(),x) = x + 3 >= x = x
   problem:
    f(f(x,y),z) -> f(x,f(y,z))
   Matrix Interpretation Processor: dim=1

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

    Qed

Nach oben scrollen