cl-banner

CSI-0.1


Problem:
 h(f(),a(),a()) -> h(g(),a(),a())
 h(g(),a(),a()) -> h(f(),a(),a())
 a() -> a'()
 h(x,a'(),y) -> h(x,y,y)
 g() -> f()
 f() -> g()

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   h(2)(y) -> h(1)(y)
   h(2)(y) -> h(2)(y)
  weak:
   h(0)(x) -> h(0)(x)
  critical peaks: 6
  h(f(),a'(),a()) <-2|1[]- h(f(),a(),a()) -0|[]-> h(g(),a(),a())
  h(f(),a(),a'()) <-2|2[]- h(f(),a(),a()) -0|[]-> h(g(),a(),a())
  h(g(),a'(),a()) <-2|1[]- h(g(),a(),a()) -1|[]-> h(f(),a(),a())
  h(g(),a(),a'()) <-2|2[]- h(g(),a(),a()) -1|[]-> h(f(),a(),a())
  h(f(),a(),a()) <-4|0[]- h(g(),a(),a()) -1|[]-> h(f(),a(),a())
  h(g(),a(),a()) <-5|0[]- h(f(),a(),a()) -0|[]-> h(g(),a(),a())
  Matrix Interpretation Processor: dim=1, lab=right
   
   interpretation:
    [h(1)](x0) = 2x0,
    
    [h(2)](x0) = 2x0 + 1,
    
    [h(0)](x0) = x0
   orientation:
    h(2)(y) = 2y + 1 >= 2y = h(1)(y)
    
    h(2)(y) = 2y + 1 >= 2y + 1 = h(2)(y)
    
    h(0)(x) = x >= x = h(0)(x)
   problem:
    
    strict:
     h(2)(y) -> h(2)(y)
    weak:
     h(0)(x) -> h(0)(x)
   Shift Processor (**) lab=left:
    
    strict:
     
    weak:
     
    Shift Processor lab=left (dd):
     
     strict:
      h(f(),a(),a()) -> h(f(),a'(),a())
      h(f(),a(),a()) -> h(g(),a(),a())
      h(f(),a'(),a()) -> h(f(),a(),a())
      h(g(),a(),a()) -> h(f(),a(),a())
      h(f(),a'(),a()) -> h(g(),a'(),a())
      h(g(),a(),a()) -> h(g(),a'(),a())
      h(f(),a(),a()) -> h(f(),a(),a'())
      h(f(),a(),a()) -> h(g(),a(),a())
      h(f(),a(),a'()) -> h(g(),a(),a'())
      h(g(),a(),a()) -> h(g(),a(),a'())
      h(g(),a(),a()) -> h(g(),a'(),a())
      h(g(),a(),a()) -> h(f(),a(),a())
      h(g(),a'(),a()) -> h(g(),a(),a())
      h(f(),a(),a()) -> h(g(),a(),a())
      h(g(),a'(),a()) -> h(f(),a'(),a())
      h(f(),a(),a()) -> h(f(),a'(),a())
      h(g(),a(),a()) -> h(g(),a(),a'())
      h(g(),a(),a()) -> h(f(),a(),a())
      h(g(),a(),a'()) -> h(f(),a(),a'())
      h(f(),a(),a()) -> h(f(),a(),a'())
      h(g(),a(),a()) -> h(f(),a(),a())
      h(g(),a(),a()) -> h(f(),a(),a())
      h(f(),a(),a()) -> h(g(),a(),a())
      h(f(),a(),a()) -> h(g(),a(),a())
     weak:
      h(f(),a(),a()) -> h(g(),a(),a())
      h(g(),a(),a()) -> h(f(),a(),a())
      a() -> a'()
      h(x,a'(),y) -> h(x,y,y)
      g() -> f()
      f() -> g()
     Shift Processor (ldh) lab=left (force):
      
      strict:
       
      weak:
       
      Decreasing Processor:
       The following diagrams are decreasing:
       peak:
        h(f(),a'(),a()) <-2|1[1,0]- h(f(),a(),a()) -0|[1,0]-> h(g(),a(),a())
       joins:
        h(f(),a'(),a()) -3|[1,0]-> h(f(),a(),a())
        h(g(),a(),a()) -1|[1,0]-> h(f(),a(),a())
       peak:
        h(f(),a(),a'()) <-2|2[1,1]- h(f(),a(),a()) -0|[1,0]-> h(g(),a(),a())
       joins:
        h(f(),a(),a'()) -5|0[1,0]-> h(g(),a(),a'())
        h(g(),a(),a()) -2|2[1,1]-> h(g(),a(),a'())
       peak:
        h(g(),a'(),a()) <-2|1[1,0]- h(g(),a(),a()) -1|[1,0]-> h(f(),a(),a())
       joins:
        h(g(),a'(),a()) -3|[1,0]-> h(g(),a(),a())
        h(f(),a(),a()) -0|[1,0]-> h(g(),a(),a())
       peak:
        h(g(),a(),a'()) <-2|2[1,1]- h(g(),a(),a()) -1|[1,0]-> h(f(),a(),a())
       joins:
        h(g(),a(),a'()) -4|0[1,0]-> h(f(),a(),a'())
        h(f(),a(),a()) -2|2[1,1]-> h(f(),a(),a'())
       peak:
        h(f(),a(),a()) <-4|0[1,0]- h(g(),a(),a()) -1|[1,0]-> h(f(),a(),a())
       joins:
        
        
       peak:
        h(g(),a(),a()) <-5|0[1,0]- h(f(),a(),a()) -0|[1,0]-> h(g(),a(),a())
       joins:
        
        
       Qed
Nach oben scrollen