cl-banner

CSI-0.1


Problem:
 nats() -> :(0(),inc(nats()))
 inc(:(x,y)) -> :(s(x),inc(y))
 hd(:(x,y)) -> x
 tl(:(x,y)) -> y
 inc(tl(nats())) -> tl(inc(nats()))

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   tl(0)(:(1)(y)) -> y
   hd(0)(:(0)(x)) -> x
   inc(0)(:(0)(x)) -> :(0)(s(0)(x))
   inc(0)(:(1)(y)) -> :(1)(inc(0)(y))
  critical peaks: 1
  inc(tl(:(0(),inc(nats())))) <-0|0,0[]- inc(tl(nats())) -4|[]-> tl(inc(nats()))
  Matrix Interpretation Processor: dim=1, lab=right
   
   interpretation:
    [s(0)](x0) = 2x0 + 2,
    
    [inc(0)](x0) = 2x0 + 2,
    
    [:(0)](x0) = x0,
    
    [hd(0)](x0) = 2x0 + 1,
    
    [:(1)](x0) = x0,
    
    [tl(0)](x0) = 2x0
   orientation:
    tl(0)(:(1)(y)) = 2y >= y = y
    
    hd(0)(:(0)(x)) = 2x + 1 >= x = x
    
    inc(0)(:(0)(x)) = 2x + 2 >= 2x + 2 = :(0)(s(0)(x))
    
    inc(0)(:(1)(y)) = 2y + 2 >= 2y + 2 = :(1)(inc(0)(y))
   problem:
    
    strict:
     
    weak:
     tl(0)(:(1)(y)) -> y
     inc(0)(:(0)(x)) -> :(0)(s(0)(x))
     inc(0)(:(1)(y)) -> :(1)(inc(0)(y))
   Matrix Interpretation Processor: dim=1, lab=right
    
    interpretation:
     [s(0)](x0) = x0,
     
     [inc(0)](x0) = x0,
     
     [:(0)](x0) = 2x0,
     
     [:(1)](x0) = 2x0,
     
     [tl(0)](x0) = x0 + 1
    orientation:
     tl(0)(:(1)(y)) = 2y + 1 >= y = y
     
     inc(0)(:(0)(x)) = 2x >= 2x = :(0)(s(0)(x))
     
     inc(0)(:(1)(y)) = 2y >= 2y = :(1)(inc(0)(y))
    problem:
     
     strict:
      
     weak:
      inc(0)(:(0)(x)) -> :(0)(s(0)(x))
      inc(0)(:(1)(y)) -> :(1)(inc(0)(y))
    Matrix Interpretation Processor: dim=1, lab=right
     
     interpretation:
      [s(0)](x0) = 2x0 + 1,
      
      [inc(0)](x0) = 2x0 + 1,
      
      [:(0)](x0) = x0,
      
      [:(1)](x0) = x0 + 1
     orientation:
      inc(0)(:(0)(x)) = 2x + 1 >= 2x + 1 = :(0)(s(0)(x))
      
      inc(0)(:(1)(y)) = 2y + 3 >= 2y + 2 = :(1)(inc(0)(y))
     problem:
      
      strict:
       
      weak:
       inc(0)(:(0)(x)) -> :(0)(s(0)(x))
     Matrix Interpretation Processor: dim=1, lab=right
      
      interpretation:
       [s(0)](x0) = 2x0,
       
       [inc(0)](x0) = 2x0 + 1,
       
       [:(0)](x0) = x0
      orientation:
       inc(0)(:(0)(x)) = 2x + 1 >= 2x = :(0)(s(0)(x))
      problem:
       
       strict:
        
       weak:
        
      Shift Processor lab=left (dd):
       
       strict:
        inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
        inc(tl(nats())) -> tl(inc(nats()))
        inc(tl(:(0(),inc(nats())))) -> inc(inc(nats()))
        tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
        tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
        tl(:(s(0()),inc(inc(nats())))) -> inc(inc(nats()))
       weak:
        nats() -> :(0(),inc(nats()))
        inc(:(x,y)) -> :(s(x),inc(y))
        hd(:(x,y)) -> x
        tl(:(x,y)) -> y
        inc(tl(nats())) -> tl(inc(nats()))
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [tl](x0) = 4x0,
         
         [hd](x0) = x0 + 5,
         
         [s](x0) = 2x0,
         
         [:](x0, x1) = 2x0 + 2x1,
         
         [inc](x0) = 4x0,
         
         [0] = 0,
         
         [nats] = 0
        orientation:
         inc(tl(nats())) = 0 >= 0 = inc(tl(:(0(),inc(nats()))))
         
         inc(tl(nats())) = 0 >= 0 = tl(inc(nats()))
         
         inc(tl(:(0(),inc(nats())))) = 0 >= 0 = inc(inc(nats()))
         
         tl(inc(nats())) = 0 >= 0 = tl(inc(:(0(),inc(nats()))))
         
         tl(inc(:(0(),inc(nats())))) = 0 >= 0 = tl(:(s(0()),inc(inc(nats()))))
         
         tl(:(s(0()),inc(inc(nats())))) = 0 >= 0 = inc(inc(nats()))
         
         nats() = 0 >= 0 = :(0(),inc(nats()))
         
         inc(:(x,y)) = 8x + 8y >= 4x + 8y = :(s(x),inc(y))
         
         hd(:(x,y)) = 2x + 2y + 5 >= x = x
         
         tl(:(x,y)) = 8x + 8y >= y = y
        problem:
         
         strict:
          inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
          inc(tl(nats())) -> tl(inc(nats()))
          inc(tl(:(0(),inc(nats())))) -> inc(inc(nats()))
          tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
          tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
          tl(:(s(0()),inc(inc(nats())))) -> inc(inc(nats()))
         weak:
          nats() -> :(0(),inc(nats()))
          inc(:(x,y)) -> :(s(x),inc(y))
          tl(:(x,y)) -> y
          inc(tl(nats())) -> tl(inc(nats()))
        Matrix Interpretation Processor: dim=1
         
         interpretation:
          [tl](x0) = x0 + 2,
          
          [s](x0) = x0,
          
          [:](x0, x1) = 4x0 + 2x1,
          
          [inc](x0) = x0,
          
          [0] = 0,
          
          [nats] = 0
         orientation:
          inc(tl(nats())) = 2 >= 2 = inc(tl(:(0(),inc(nats()))))
          
          inc(tl(nats())) = 2 >= 2 = tl(inc(nats()))
          
          inc(tl(:(0(),inc(nats())))) = 2 >= 0 = inc(inc(nats()))
          
          tl(inc(nats())) = 2 >= 2 = tl(inc(:(0(),inc(nats()))))
          
          tl(inc(:(0(),inc(nats())))) = 2 >= 2 = tl(:(s(0()),inc(inc(nats()))))
          
          tl(:(s(0()),inc(inc(nats())))) = 2 >= 0 = inc(inc(nats()))
          
          nats() = 0 >= 0 = :(0(),inc(nats()))
          
          inc(:(x,y)) = 4x + 2y >= 4x + 2y = :(s(x),inc(y))
          
          tl(:(x,y)) = 4x + 2y + 2 >= y = y
         problem:
          
          strict:
           inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
           inc(tl(nats())) -> tl(inc(nats()))
           tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
           tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
          weak:
           nats() -> :(0(),inc(nats()))
           inc(:(x,y)) -> :(s(x),inc(y))
           inc(tl(nats())) -> tl(inc(nats()))
         Matrix Interpretation Processor: dim=1
          
          interpretation:
           [tl](x0) = x0 + 3,
           
           [s](x0) = 4x0,
           
           [:](x0, x1) = 2x0 + 2x1,
           
           [inc](x0) = 4x0,
           
           [0] = 0,
           
           [nats] = 0
          orientation:
           inc(tl(nats())) = 12 >= 12 = inc(tl(:(0(),inc(nats()))))
           
           inc(tl(nats())) = 12 >= 3 = tl(inc(nats()))
           
           tl(inc(nats())) = 3 >= 3 = tl(inc(:(0(),inc(nats()))))
           
           tl(inc(:(0(),inc(nats())))) = 3 >= 3 = tl(:(s(0()),inc(inc(nats()))))
           
           nats() = 0 >= 0 = :(0(),inc(nats()))
           
           inc(:(x,y)) = 8x + 8y >= 8x + 8y = :(s(x),inc(y))
          problem:
           
           strict:
            inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
            tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
            tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
           weak:
            nats() -> :(0(),inc(nats()))
            inc(:(x,y)) -> :(s(x),inc(y))
          Bounds Processor:
           bound: 1
           enrichment: match-rt
           automaton:
            final states: {7}
            transitions:
             s1(15) -> 51*
             s1(7) -> 15*
             s1(51) -> 15*
             inc0(7) -> 7*
             tl0(7) -> 7*
             nats0() -> 7*
             :0(7,7) -> 7*
             00() -> 7*
             s0(7) -> 7*
             inc1(50) -> 14*
             inc1(17) -> 14,7
             inc1(7) -> 14*
             inc1(14) -> 50*
             inc1(16) -> 46*
             inc1(13) -> 14*
             tl1(46) -> 7*
             tl1(16) -> 17*
             :1(51,50) -> 50,7,14,46
             :1(15,14) -> 50,14,13,7,16
             01() -> 15*
             nats1() -> 13*
           problem:
            
            strict:
             tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
             tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
            weak:
             nats() -> :(0(),inc(nats()))
             inc(:(x,y)) -> :(s(x),inc(y))
           Bounds Processor:
            bound: 1
            enrichment: match-rt
            automaton:
             final states: {7}
             transitions:
              s1(15) -> 33*
              s1(7) -> 15*
              s1(33) -> 15*
              inc0(7) -> 7*
              tl0(7) -> 7*
              nats0() -> 7*
              :0(7,7) -> 7*
              00() -> 7*
              s0(7) -> 7*
              inc1(32) -> 14*
              inc1(7) -> 14*
              inc1(14) -> 32*
              inc1(16) -> 17*
              inc1(13) -> 14*
              tl1(17) -> 7*
              :1(33,32) -> 32,7,14,17
              :1(15,14) -> 32,14,13,7,16
              01() -> 15*
              nats1() -> 13*
            problem:
             
             strict:
              tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
             weak:
              nats() -> :(0(),inc(nats()))
              inc(:(x,y)) -> :(s(x),inc(y))
            Bounds Processor:
             bound: 1
             enrichment: match-rt
             automaton:
              final states: {7}
              transitions:
               s1(17) -> 18*
               s1(7) -> 17*
               s1(18) -> 17*
               inc0(7) -> 7*
               tl0(7) -> 7*
               nats0() -> 7*
               :0(7,7) -> 7*
               00() -> 7*
               s0(7) -> 7*
               inc1(15) -> 16*
               inc1(7) -> 15*
               inc1(14) -> 15*
               inc1(16) -> 15*
               tl1(19) -> 7*
               :1(17,15) -> 16,15,14,7
               :1(18,16) -> 16,15,7,19
               01() -> 17*
               nats1() -> 14*
             problem:
              
              strict:
               
              weak:
               nats() -> :(0(),inc(nats()))
               inc(:(x,y)) -> :(s(x),inc(y))
             Shift Processor (ldh) lab=left (force):
              
              strict:
               
              weak:
               
              Rule Labeling Processor:
               
               strict:
                
               weak:
                
               rule labeling (right):
                nats() -> :(0(),inc(nats())): 1
                inc(:(x,y)) -> :(s(x),inc(y)): 0
                hd(:(x,y)) -> x: 0
                tl(:(x,y)) -> y: 0
                inc(tl(nats())) -> tl(inc(nats())): 0
               Decreasing Processor:
                The following diagrams are decreasing:
                peak:
                 inc(tl(:(0(),inc(nats())))) <-0|0,0[1,2,0,1,0,1]- inc(tl(nats())) -4|
                                                                   [1,0,0,0,0,0]-> 
                                                                   tl(inc(nats()))
                joins:
                 inc(tl(:(0(),inc(nats())))) -3|0[1,2,0,1,0,0]-> inc(inc(nats()))
                 tl(inc(nats())) -0|0,0[0,4,0,1,0,1]-> tl(inc(:(0(),inc(nats())))) -1|
                                                       0[0,0,0,0,0,0]-> 
                  tl(:(s(0()),inc(inc(nats())))) -3|[0,0,0,0,0,0]-> inc(inc(nats()))
                Qed

Nach oben scrollen