cl-banner

CSI-0.1


Problem:
 H(F(x,y)) -> F(H(R(x)),y)
 F(x,K(y,z)) -> G(P(y),Q(z,x))
 H(Q(x,y)) -> Q(x,H(R(y)))
 Q(x,H(R(y))) -> H(Q(x,y))
 H(G(x,y)) -> G(x,H(y))

Proof:
 Church Rosser Transformation Processor (star):

  strict:

  weak:
   H(0)(G(0)(x)) -> G(0)(x)
   H(0)(G(1)(y)) -> G(1)(H(0)(y))
   Q(0)(x) -> H(0)(Q(0)(x))
   Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y))
   H(0)(Q(0)(x)) -> Q(0)(x)
   H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y)))
   F(0)(x) -> G(1)(Q(1)(x))
   F(1)(K(0)(y)) -> G(0)(P(0)(y))
   F(1)(K(1)(z)) -> G(1)(Q(0)(z))
   H(0)(F(0)(x)) -> F(0)(H(0)(R(0)(x)))
   H(0)(F(1)(y)) -> F(1)(y)
  critical peaks: 2
  H(G(P(x125),Q(x126,x))) <-1|0[]- H(F(x,K(x125,x126))) -0|[]-> F(H(R(x)),K(x125,x126))
  H(H(Q(x,x128))) <-3|0[]- H(Q(x,H(R(x128)))) -2|[]-> Q(x,H(R(H(R(x128)))))
  Matrix Interpretation Processor: dim=1, lab=right

   interpretation:
    [K(1)](x0) = x0,

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

    [K(0)](x0) = 2x0 + 3,

    [F(1)](x0) = x0,

    [F(0)](x0) = 2x0,

    [R(0)](x0) = x0,

    [Q(1)](x0) = 2x0,

    [Q(0)](x0) = x0,

    [G(1)](x0) = x0,

    [G(0)](x0) = 2x0,

    [H(0)](x0) = x0
   orientation:
    H(0)(G(0)(x)) = 2x >= 2x = G(0)(x)

    H(0)(G(1)(y)) = y >= y = G(1)(H(0)(y))

    Q(0)(x) = x >= x = H(0)(Q(0)(x))

    Q(1)(H(0)(R(0)(y))) = 2y >= 2y = H(0)(Q(1)(y))

    H(0)(Q(0)(x)) = x >= x = Q(0)(x)

    H(0)(Q(1)(y)) = 2y >= 2y = Q(1)(H(0)(R(0)(y)))

    F(0)(x) = 2x >= 2x = G(1)(Q(1)(x))

    F(1)(K(0)(y)) = 2y + 3 >= 2y + 2 = G(0)(P(0)(y))

    F(1)(K(1)(z)) = z >= z = G(1)(Q(0)(z))

    H(0)(F(0)(x)) = 2x >= 2x = F(0)(H(0)(R(0)(x)))

    H(0)(F(1)(y)) = y >= y = F(1)(y)
   problem:

    strict:

    weak:
     H(0)(G(0)(x)) -> G(0)(x)
     H(0)(G(1)(y)) -> G(1)(H(0)(y))
     Q(0)(x) -> H(0)(Q(0)(x))
     Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y))
     H(0)(Q(0)(x)) -> Q(0)(x)
     H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y)))
     F(0)(x) -> G(1)(Q(1)(x))
     F(1)(K(1)(z)) -> G(1)(Q(0)(z))
     H(0)(F(0)(x)) -> F(0)(H(0)(R(0)(x)))
     H(0)(F(1)(y)) -> F(1)(y)
   Matrix Interpretation Processor: dim=1, lab=right

    interpretation:
     [K(1)](x0) = x0 + 1,

     [F(1)](x0) = x0 + 1,

     [F(0)](x0) = x0 + 3,

     [R(0)](x0) = x0,

     [Q(1)](x0) = x0,

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

     [G(1)](x0) = x0,

     [G(0)](x0) = 2x0 + 1,

     [H(0)](x0) = x0
    orientation:
     H(0)(G(0)(x)) = 2x + 1 >= 2x + 1 = G(0)(x)

     H(0)(G(1)(y)) = y >= y = G(1)(H(0)(y))

     Q(0)(x) = x + 1 >= x + 1 = H(0)(Q(0)(x))

     Q(1)(H(0)(R(0)(y))) = y >= y = H(0)(Q(1)(y))

     H(0)(Q(0)(x)) = x + 1 >= x + 1 = Q(0)(x)

     H(0)(Q(1)(y)) = y >= y = Q(1)(H(0)(R(0)(y)))

     F(0)(x) = x + 3 >= x = G(1)(Q(1)(x))

     F(1)(K(1)(z)) = z + 2 >= z + 1 = G(1)(Q(0)(z))

     H(0)(F(0)(x)) = x + 3 >= x + 3 = F(0)(H(0)(R(0)(x)))

     H(0)(F(1)(y)) = y + 1 >= y + 1 = F(1)(y)
    problem:

     strict:

     weak:
      H(0)(G(0)(x)) -> G(0)(x)
      H(0)(G(1)(y)) -> G(1)(H(0)(y))
      Q(0)(x) -> H(0)(Q(0)(x))
      Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y))
      H(0)(Q(0)(x)) -> Q(0)(x)
      H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y)))
      H(0)(F(0)(x)) -> F(0)(H(0)(R(0)(x)))
      H(0)(F(1)(y)) -> F(1)(y)
    Matrix Interpretation Processor: dim=2, lab=right

     interpretation:
                   [1 0]     [2]
      [F(1)](x0) = [0 0]x0 + [0],

                   [1 0]  
      [F(0)](x0) = [1 1]x0,

                   [1 1]  
      [R(0)](x0) = [0 0]x0,

                   [2 2]  
      [Q(1)](x0) = [0 0]x0,

                   [2 0]  
      [Q(0)](x0) = [0 0]x0,


      [G(1)](x0) = x0,

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

                   [1 2]  
      [H(0)](x0) = [0 2]x0
     orientation:
                      [3 2]    [2]    [1 0]    [0]          
      H(0)(G(0)(x)) = [2 2]x + [2] >= [1 1]x + [1] = G(0)(x)

                      [1 2]     [1 2]                 
      H(0)(G(1)(y)) = [0 2]y >= [0 2]y = G(1)(H(0)(y))

                [2 0]     [2 0]                 
      Q(0)(x) = [0 0]x >= [0 0]x = H(0)(Q(0)(x))

                            [2 2]     [2 2]                 
      Q(1)(H(0)(R(0)(y))) = [0 0]y >= [0 0]y = H(0)(Q(1)(y))

                      [2 0]     [2 0]           
      H(0)(Q(0)(x)) = [0 0]x >= [0 0]x = Q(0)(x)

                      [2 2]     [2 2]                       
      H(0)(Q(1)(y)) = [0 0]y >= [0 0]y = Q(1)(H(0)(R(0)(y)))

                      [3 2]     [1 1]                       
      H(0)(F(0)(x)) = [2 2]x >= [1 1]x = F(0)(H(0)(R(0)(x)))

                      [1 0]    [2]    [1 0]    [2]          
      H(0)(F(1)(y)) = [0 0]y + [0] >= [0 0]y + [0] = F(1)(y)
     problem:

      strict:

      weak:
       H(0)(G(1)(y)) -> G(1)(H(0)(y))
       Q(0)(x) -> H(0)(Q(0)(x))
       Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y))
       H(0)(Q(0)(x)) -> Q(0)(x)
       H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y)))
       H(0)(F(0)(x)) -> F(0)(H(0)(R(0)(x)))
       H(0)(F(1)(y)) -> F(1)(y)
     Matrix Interpretation Processor: dim=2, lab=right

      interpretation:
                    [1 0]  
       [F(1)](x0) = [0 0]x0,


       [F(0)](x0) = x0,

                    [1 1]  
       [R(0)](x0) = [0 0]x0,

                    [2 2]  
       [Q(1)](x0) = [0 0]x0,

                    [1 0]  
       [Q(0)](x0) = [0 0]x0,

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

                    [1 2]  
       [H(0)](x0) = [0 1]x0
      orientation:
                       [1 2]    [2]    [1 2]    [0]                
       H(0)(G(1)(y)) = [0 1]y + [1] >= [0 1]y + [1] = G(1)(H(0)(y))

                 [1 0]     [1 0]                 
       Q(0)(x) = [0 0]x >= [0 0]x = H(0)(Q(0)(x))

                             [2 2]     [2 2]                 
       Q(1)(H(0)(R(0)(y))) = [0 0]y >= [0 0]y = H(0)(Q(1)(y))

                       [1 0]     [1 0]           
       H(0)(Q(0)(x)) = [0 0]x >= [0 0]x = Q(0)(x)

                       [2 2]     [2 2]                       
       H(0)(Q(1)(y)) = [0 0]y >= [0 0]y = Q(1)(H(0)(R(0)(y)))

                       [1 2]     [1 1]                       
       H(0)(F(0)(x)) = [0 1]x >= [0 0]x = F(0)(H(0)(R(0)(x)))

                       [1 0]     [1 0]           
       H(0)(F(1)(y)) = [0 0]y >= [0 0]y = F(1)(y)
      problem:

       strict:

       weak:
        Q(0)(x) -> H(0)(Q(0)(x))
        Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y))
        H(0)(Q(0)(x)) -> Q(0)(x)
        H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y)))
        H(0)(F(0)(x)) -> F(0)(H(0)(R(0)(x)))
        H(0)(F(1)(y)) -> F(1)(y)
      Matrix Interpretation Processor: dim=2, lab=right

       interpretation:
                     [2 0]     [0]
        [F(1)](x0) = [1 0]x0 + [1],

                     [1 2]  
        [F(0)](x0) = [1 1]x0,

                     [2 0]  
        [R(0)](x0) = [0 0]x0,

                     [1 0]  
        [Q(1)](x0) = [1 0]x0,

                     [1 0]     [2]
        [Q(0)](x0) = [0 0]x0 + [0],

                     [1 1]  
        [H(0)](x0) = [0 2]x0
       orientation:
                  [1 0]    [2]    [1 0]    [2]                
        Q(0)(x) = [0 0]x + [0] >= [0 0]x + [0] = H(0)(Q(0)(x))

                              [2 0]     [2 0]                 
        Q(1)(H(0)(R(0)(y))) = [2 0]y >= [2 0]y = H(0)(Q(1)(y))

                        [1 0]    [2]    [1 0]    [2]          
        H(0)(Q(0)(x)) = [0 0]x + [0] >= [0 0]x + [0] = Q(0)(x)

                        [2 0]     [2 0]                       
        H(0)(Q(1)(y)) = [2 0]y >= [2 0]y = Q(1)(H(0)(R(0)(y)))

                        [2 3]     [2 0]                       
        H(0)(F(0)(x)) = [2 2]x >= [2 0]x = F(0)(H(0)(R(0)(x)))

                        [3 0]    [1]    [2 0]    [0]          
        H(0)(F(1)(y)) = [2 0]y + [2] >= [1 0]y + [1] = F(1)(y)
       problem:

        strict:

        weak:
         Q(0)(x) -> H(0)(Q(0)(x))
         Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y))
         H(0)(Q(0)(x)) -> Q(0)(x)
         H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y)))
         H(0)(F(0)(x)) -> F(0)(H(0)(R(0)(x)))
       Matrix Interpretation Processor: dim=2, lab=right

        interpretation:
                      [1 0]     [0]
         [F(0)](x0) = [1 0]x0 + [1],

                      [1 0]  
         [R(0)](x0) = [0 0]x0,

                      [1 0]  
         [Q(1)](x0) = [0 0]x0,

                      [2 0]  
         [Q(0)](x0) = [0 0]x0,

                      [1 1]  
         [H(0)](x0) = [0 1]x0
        orientation:
                   [2 0]     [2 0]                 
         Q(0)(x) = [0 0]x >= [0 0]x = H(0)(Q(0)(x))

                               [1 0]     [1 0]                 
         Q(1)(H(0)(R(0)(y))) = [0 0]y >= [0 0]y = H(0)(Q(1)(y))

                         [2 0]     [2 0]           
         H(0)(Q(0)(x)) = [0 0]x >= [0 0]x = Q(0)(x)

                         [1 0]     [1 0]                       
         H(0)(Q(1)(y)) = [0 0]y >= [0 0]y = Q(1)(H(0)(R(0)(y)))

                         [2 0]    [1]    [1 0]    [0]                      
         H(0)(F(0)(x)) = [1 0]x + [1] >= [1 0]x + [1] = F(0)(H(0)(R(0)(x)))
        problem:

         strict:

         weak:
          Q(0)(x) -> H(0)(Q(0)(x))
          Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y))
          H(0)(Q(0)(x)) -> Q(0)(x)
          H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y)))
        Shift Processor lab=left (dd):

         strict:
          H(F(x,K(x125,x126))) -> H(G(P(x125),Q(x126,x)))
          H(F(x,K(x125,x126))) -> F(H(R(x)),K(x125,x126))
          H(G(P(x125),Q(x126,x))) -> G(P(x125),H(Q(x126,x)))
          F(H(R(x)),K(x125,x126)) -> G(P(x125),Q(x126,H(R(x))))
          G(P(x125),Q(x126,H(R(x)))) -> G(P(x125),H(Q(x126,x)))
          H(G(P(x125),Q(x126,x))) -> G(P(x125),H(Q(x126,x)))
          G(P(x125),H(Q(x126,x))) -> G(P(x125),Q(x126,H(R(x))))
          F(H(R(x)),K(x125,x126)) -> G(P(x125),Q(x126,H(R(x))))
          H(Q(x,H(R(x128)))) -> H(H(Q(x,x128)))
          H(Q(x,H(R(x128)))) -> Q(x,H(R(H(R(x128)))))
          H(H(Q(x,x128))) -> H(Q(x,H(R(x128))))
          Q(x,H(R(H(R(x128))))) -> H(Q(x,H(R(x128))))
         weak:
          H(F(x,y)) -> F(H(R(x)),y)
          F(x,K(y,z)) -> G(P(y),Q(z,x))
          H(Q(x,y)) -> Q(x,H(R(y)))
          Q(x,H(R(y))) -> H(Q(x,y))
          H(G(x,y)) -> G(x,H(y))
         Matrix Interpretation Processor: dim=1

          interpretation:
           [G](x0, x1) = 7x0 + 2x1,

           [Q](x0, x1) = x0 + 2x1,

           [P](x0) = x0,

           [K](x0, x1) = 7x0 + 3x1 + 6,

           [R](x0) = x0,

           [H](x0) = x0,

           [F](x0, x1) = 4x0 + x1 + 3
          orientation:
           H(F(x,K(x125,x126))) = 4x + 7x125 + 3x126 + 9 >= 4x + 7x125 + 2x126 = H(G(P(x125),Q(x126,x)))

           H(F(x,K(x125,x126))) = 4x + 7x125 + 3x126 + 9 >= 4x + 7x125 + 3x126 + 9 = F(H(R(x)),K(x125,x126))

           H(G(P(x125),Q(x126,x))) = 4x + 7x125 + 2x126 >= 4x + 7x125 + 2x126 = G(P(x125),H(Q(x126,x)))

           F(H(R(x)),K(x125,x126)) = 4x + 7x125 + 3x126 + 9 >= 4x + 7x125 + 2x126 = G(P(x125),Q(x126,H(R(x))))

           G(P(x125),Q(x126,H(R(x)))) = 4x + 7x125 + 2x126 >= 4x + 7x125 + 2x126 = G(P(x125),H(Q(x126,x)))

           H(G(P(x125),Q(x126,x))) = 4x + 7x125 + 2x126 >= 4x + 7x125 + 2x126 = G(P(x125),H(Q(x126,x)))

           G(P(x125),H(Q(x126,x))) = 4x + 7x125 + 2x126 >= 4x + 7x125 + 2x126 = G(P(x125),Q(x126,H(R(x))))

           F(H(R(x)),K(x125,x126)) = 4x + 7x125 + 3x126 + 9 >= 4x + 7x125 + 2x126 = G(P(x125),Q(x126,H(R(x))))

           H(Q(x,H(R(x128)))) = x + 2x128 >= x + 2x128 = H(H(Q(x,x128)))

           H(Q(x,H(R(x128)))) = x + 2x128 >= x + 2x128 = Q(x,H(R(H(R(x128)))))

           H(H(Q(x,x128))) = x + 2x128 >= x + 2x128 = H(Q(x,H(R(x128))))

           Q(x,H(R(H(R(x128))))) = x + 2x128 >= x + 2x128 = H(Q(x,H(R(x128))))

           H(F(x,y)) = 4x + y + 3 >= 4x + y + 3 = F(H(R(x)),y)

           F(x,K(y,z)) = 4x + 7y + 3z + 9 >= 4x + 7y + 2z = G(P(y),Q(z,x))

           H(Q(x,y)) = x + 2y >= x + 2y = Q(x,H(R(y)))

           Q(x,H(R(y))) = x + 2y >= x + 2y = H(Q(x,y))

           H(G(x,y)) = 7x + 2y >= 7x + 2y = G(x,H(y))
          problem:

           strict:
            H(F(x,K(x125,x126))) -> F(H(R(x)),K(x125,x126))
            H(G(P(x125),Q(x126,x))) -> G(P(x125),H(Q(x126,x)))
            G(P(x125),Q(x126,H(R(x)))) -> G(P(x125),H(Q(x126,x)))
            H(G(P(x125),Q(x126,x))) -> G(P(x125),H(Q(x126,x)))
            G(P(x125),H(Q(x126,x))) -> G(P(x125),Q(x126,H(R(x))))
            H(Q(x,H(R(x128)))) -> H(H(Q(x,x128)))
            H(Q(x,H(R(x128)))) -> Q(x,H(R(H(R(x128)))))
            H(H(Q(x,x128))) -> H(Q(x,H(R(x128))))
            Q(x,H(R(H(R(x128))))) -> H(Q(x,H(R(x128))))
           weak:
            H(F(x,y)) -> F(H(R(x)),y)
            H(Q(x,y)) -> Q(x,H(R(y)))
            Q(x,H(R(y))) -> H(Q(x,y))
            H(G(x,y)) -> G(x,H(y))
          Matrix Interpretation Processor: dim=2

           interpretation:
                          [2 1]          [0]
            [G](x0, x1) = [0 1]x0 + x1 + [1],

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


            [P](x0) = x0,

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

                      [1 0]  
            [R](x0) = [0 0]x0,

                      [1 2]  
            [H](x0) = [0 2]x0,

                          [2 0]     [2 2]     [2]
            [F](x0, x1) = [0 1]x0 + [0 0]x1 + [0]
           orientation:
                                   [2 2]    [2 0]       [2 0]       [2]    [2 0]    [2 0]       [2 0]       [2]                          
            H(F(x,K(x125,x126))) = [0 2]x + [0 0]x125 + [0 0]x126 + [0] >= [0 0]x + [0 0]x125 + [0 0]x126 + [0] = F(H(R(x)),K(x125,x126))

                                      [2 0]    [2 3]       [1 0]       [2]    [2 0]    [2 1]       [1 0]       [0]                          
            H(G(P(x125),Q(x126,x))) = [0 0]x + [0 2]x125 + [0 0]x126 + [2] >= [0 0]x + [0 1]x125 + [0 0]x126 + [1] = G(P(x125),H(Q(x126,x)))

                                         [2 0]    [2 1]       [1 0]       [0]    [2 0]    [2 1]       [1 0]       [0]                          
            G(P(x125),Q(x126,H(R(x)))) = [0 0]x + [0 1]x125 + [0 0]x126 + [1] >= [0 0]x + [0 1]x125 + [0 0]x126 + [1] = G(P(x125),H(Q(x126,x)))

                                      [2 0]    [2 3]       [1 0]       [2]    [2 0]    [2 1]       [1 0]       [0]                          
            H(G(P(x125),Q(x126,x))) = [0 0]x + [0 2]x125 + [0 0]x126 + [2] >= [0 0]x + [0 1]x125 + [0 0]x126 + [1] = G(P(x125),H(Q(x126,x)))

                                      [2 0]    [2 1]       [1 0]       [0]    [2 0]    [2 1]       [1 0]       [0]                             
            G(P(x125),H(Q(x126,x))) = [0 0]x + [0 1]x125 + [0 0]x126 + [1] >= [0 0]x + [0 1]x125 + [0 0]x126 + [1] = G(P(x125),Q(x126,H(R(x))))

                                 [1 0]    [2 0]        [1 0]    [2 0]                      
            H(Q(x,H(R(x128)))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(H(Q(x,x128)))

                                 [1 0]    [2 0]        [1 0]    [2 0]                            
            H(Q(x,H(R(x128)))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = Q(x,H(R(H(R(x128)))))

                              [1 0]    [2 0]        [1 0]    [2 0]                         
            H(H(Q(x,x128))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(Q(x,H(R(x128))))

                                    [1 0]    [2 0]        [1 0]    [2 0]                         
            Q(x,H(R(H(R(x128))))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(Q(x,H(R(x128))))

                        [2 2]    [2 2]    [2]    [2 0]    [2 2]    [2]               
            H(F(x,y)) = [0 2]x + [0 0]y + [0] >= [0 0]x + [0 0]y + [0] = F(H(R(x)),y)

                        [1 0]    [2 0]     [1 0]    [2 0]                
            H(Q(x,y)) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = Q(x,H(R(y)))

                           [1 0]    [2 0]     [1 0]    [2 0]             
            Q(x,H(R(y))) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = H(Q(x,y))

                        [2 3]    [1 2]    [2]    [2 1]    [1 2]    [0]            
            H(G(x,y)) = [0 2]x + [0 2]y + [2] >= [0 1]x + [0 2]y + [1] = G(x,H(y))
           problem:

            strict:
             H(F(x,K(x125,x126))) -> F(H(R(x)),K(x125,x126))
             G(P(x125),Q(x126,H(R(x)))) -> G(P(x125),H(Q(x126,x)))
             G(P(x125),H(Q(x126,x))) -> G(P(x125),Q(x126,H(R(x))))
             H(Q(x,H(R(x128)))) -> H(H(Q(x,x128)))
             H(Q(x,H(R(x128)))) -> Q(x,H(R(H(R(x128)))))
             H(H(Q(x,x128))) -> H(Q(x,H(R(x128))))
             Q(x,H(R(H(R(x128))))) -> H(Q(x,H(R(x128))))
            weak:
             H(F(x,y)) -> F(H(R(x)),y)
             H(Q(x,y)) -> Q(x,H(R(y)))
             Q(x,H(R(y))) -> H(Q(x,y))
           Matrix Interpretation Processor: dim=2

            interpretation:
                           [1 0]     [1 0]  
             [G](x0, x1) = [0 0]x0 + [1 0]x1,

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

                       [2 0]  
             [P](x0) = [0 0]x0,

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

                       [1 2]  
             [R](x0) = [0 0]x0,

                       [1 2]  
             [H](x0) = [0 3]x0,

                           [1 2]     [2 0]  
             [F](x0, x1) = [0 0]x0 + [0 1]x1
            orientation:
                                    [1 2]    [2 2]       [2 0]       [2]    [1 2]    [2 2]       [2 0]       [0]                          
             H(F(x,K(x125,x126))) = [0 0]x + [0 0]x125 + [0 0]x126 + [3] >= [0 0]x + [0 0]x125 + [0 0]x126 + [1] = F(H(R(x)),K(x125,x126))

                                          [1 2]    [2 0]       [2 0]        [1 2]    [2 0]       [2 0]                              
             G(P(x125),Q(x126,H(R(x)))) = [1 2]x + [0 0]x125 + [2 0]x126 >= [1 2]x + [0 0]x125 + [2 0]x126 = G(P(x125),H(Q(x126,x)))

                                       [1 2]    [2 0]       [2 0]        [1 2]    [2 0]       [2 0]                                 
             G(P(x125),H(Q(x126,x))) = [1 2]x + [0 0]x125 + [2 0]x126 >= [1 2]x + [0 0]x125 + [2 0]x126 = G(P(x125),Q(x126,H(R(x))))

                                  [2 0]    [1 2]        [2 0]    [1 2]                      
             H(Q(x,H(R(x128)))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(H(Q(x,x128)))

                                  [2 0]    [1 2]        [2 0]    [1 2]                            
             H(Q(x,H(R(x128)))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = Q(x,H(R(H(R(x128)))))

                               [2 0]    [1 2]        [2 0]    [1 2]                         
             H(H(Q(x,x128))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(Q(x,H(R(x128))))

                                     [2 0]    [1 2]        [2 0]    [1 2]                         
             Q(x,H(R(H(R(x128))))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(Q(x,H(R(x128))))

                         [1 2]    [2 2]     [1 2]    [2 0]                
             H(F(x,y)) = [0 0]x + [0 3]y >= [0 0]x + [0 1]y = F(H(R(x)),y)

                         [2 0]    [1 2]     [2 0]    [1 2]                
             H(Q(x,y)) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = Q(x,H(R(y)))

                            [2 0]    [1 2]     [2 0]    [1 2]             
             Q(x,H(R(y))) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = H(Q(x,y))
            problem:

             strict:
              G(P(x125),Q(x126,H(R(x)))) -> G(P(x125),H(Q(x126,x)))
              G(P(x125),H(Q(x126,x))) -> G(P(x125),Q(x126,H(R(x))))
              H(Q(x,H(R(x128)))) -> H(H(Q(x,x128)))
              H(Q(x,H(R(x128)))) -> Q(x,H(R(H(R(x128)))))
              H(H(Q(x,x128))) -> H(Q(x,H(R(x128))))
              Q(x,H(R(H(R(x128))))) -> H(Q(x,H(R(x128))))
             weak:
              H(F(x,y)) -> F(H(R(x)),y)
              H(Q(x,y)) -> Q(x,H(R(y)))
              Q(x,H(R(y))) -> H(Q(x,y))
            Matrix Interpretation Processor: dim=2

             interpretation:
                            [2 0]     [1 0]  
              [G](x0, x1) = [0 0]x0 + [1 0]x1,

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

                        [2 0]  
              [P](x0) = [0 0]x0,

                        [1 1]  
              [R](x0) = [0 0]x0,

                        [1 2]  
              [H](x0) = [0 2]x0,

                            [1 1]     [1 0]     [0]
              [F](x0, x1) = [0 0]x0 + [0 0]x1 + [1]
             orientation:
                                           [2 2]    [4 0]       [1 0]        [2 2]    [4 0]       [1 0]                              
              G(P(x125),Q(x126,H(R(x)))) = [2 2]x + [0 0]x125 + [1 0]x126 >= [2 2]x + [0 0]x125 + [1 0]x126 = G(P(x125),H(Q(x126,x)))

                                        [2 2]    [4 0]       [1 0]        [2 2]    [4 0]       [1 0]                                 
              G(P(x125),H(Q(x126,x))) = [2 2]x + [0 0]x125 + [1 0]x126 >= [2 2]x + [0 0]x125 + [1 0]x126 = G(P(x125),Q(x126,H(R(x))))

                                   [1 0]    [2 2]        [1 0]    [2 2]                      
              H(Q(x,H(R(x128)))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(H(Q(x,x128)))

                                   [1 0]    [2 2]        [1 0]    [2 2]                            
              H(Q(x,H(R(x128)))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = Q(x,H(R(H(R(x128)))))

                                [1 0]    [2 2]        [1 0]    [2 2]                         
              H(H(Q(x,x128))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(Q(x,H(R(x128))))

                                      [1 0]    [2 2]        [1 0]    [2 2]                         
              Q(x,H(R(H(R(x128))))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(Q(x,H(R(x128))))

                          [1 1]    [1 0]    [2]    [1 1]    [1 0]    [0]               
              H(F(x,y)) = [0 0]x + [0 0]y + [2] >= [0 0]x + [0 0]y + [1] = F(H(R(x)),y)

                          [1 0]    [2 2]     [1 0]    [2 2]                
              H(Q(x,y)) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = Q(x,H(R(y)))

                             [1 0]    [2 2]     [1 0]    [2 2]             
              Q(x,H(R(y))) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = H(Q(x,y))
             problem:

              strict:
               G(P(x125),Q(x126,H(R(x)))) -> G(P(x125),H(Q(x126,x)))
               G(P(x125),H(Q(x126,x))) -> G(P(x125),Q(x126,H(R(x))))
               H(Q(x,H(R(x128)))) -> H(H(Q(x,x128)))
               H(Q(x,H(R(x128)))) -> Q(x,H(R(H(R(x128)))))
               H(H(Q(x,x128))) -> H(Q(x,H(R(x128))))
               Q(x,H(R(H(R(x128))))) -> H(Q(x,H(R(x128))))
              weak:
               H(Q(x,y)) -> Q(x,H(R(y)))
               Q(x,H(R(y))) -> H(Q(x,y))
             Shift Processor (ldh) lab=left (force):

              strict:

              weak:

              Decreasing Processor:
               The following diagrams are decreasing:
               peak:
                H(G(P(x125),Q(x126,x))) <-1|0[1,0,0,0,0,0,0]- H(F(x,K(x125,x126))) -0|
                                                              [1,0,0,0,0,0,0]-> 
                                                              F(H(R(x)),K(x125,x126))
               joins:
                H(G(P(x125),Q(x126,x))) -4|[0,0,0,0,0,0,0]-> G(P(x125),H(Q(x126,x)))
                F(H(R(x)),K(x125,x126)) -1|[0,0,0,0,0,0,0]-> G(P(x125),Q(x126,H(R(x)))) -3|
                                                             1[0,0,0,0,0,0,0]-> 
                                                             G(P(x125),H(Q(x126,x)))
               peak:
                H(H(Q(x,x128))) <-3|0[1,0,0,0,0,0,0]- H(Q(x,H(R(x128)))) -2|
                                                      [1,0,0,0,0,0,0]-> 
                                                      Q(x,H(R(H(R(x128)))))
               joins:
                H(H(Q(x,x128))) -2|0[1,0,0,0,0,0,0]-> H(Q(x,H(R(x128))))
                Q(x,H(R(H(R(x128))))) -3|[1,0,0,0,0,0,0]-> H(Q(x,H(R(x128))))
               Qed
Nach oben scrollen