cl-banner

CSI-0.1


Problem:
 f(g(x,a(),b())) -> x
 g(f(h(c(),d())),x,y) -> h(k1(x),k2(y))
 k1(a()) -> c()
 k2(b()) -> d()
 f(h(k1(a()),k2(b()))) -> f(h(c(),d()))
 f(h(c(),k2(b()))) -> f(h(c(),d()))
 f(h(k1(a()),d())) -> f(h(c(),d()))

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   
  weak:
   
  critical peaks: 5
  f(h(k1(a()),k2(b()))) <-1|0[]- f(g(f(h(c(),d())),a(),b())) -0|[]-> f(h(c(),d()))
  f(h(c(),k2(b()))) <-2|0,0[]- f(h(k1(a()),k2(b()))) -4|[]-> f(h(c(),d()))
  f(h(c(),d())) <-2|0,0[]- f(h(k1(a()),d())) -6|[]-> f(h(c(),d()))
  f(h(k1(a()),d())) <-3|0,1[]- f(h(k1(a()),k2(b()))) -4|[]-> f(h(c(),d()))
  f(h(c(),d())) <-3|0,1[]- f(h(c(),k2(b()))) -5|[]-> f(h(c(),d()))
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed
Nach oben scrollen