Problem:
 a1() -> b1()
 a1() -> c1()
 b1() -> b2()
 c1() -> c2()
 a2() -> b2()
 a2() -> c2()
 b2() -> b3()
 c2() -> c3()
 a3() -> b3()
 a3() -> c3()
 b3() -> b4()
 c3() -> c4()
 a4() -> b4()
 a4() -> c4()
 b4() -> b5()
 c4() -> c5()
 a5() -> b5()
 a5() -> c5()
 b5() -> b6()
 c5() -> c6()
 a6() -> b6()
 a6() -> c6()
 b6() -> b7()
 c6() -> b7()
 b7() -> b1()
 b7() -> c1()

Proof:
 sorted: (order)
 0:a1() -> b1()
   a1() -> c1()
   b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
 1:b1() -> b2()
   c1() -> c2()
   a2() -> b2()
   a2() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
 2:b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   a3() -> b3()
   a3() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
 3:b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   a4() -> b4()
   a4() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
 4:b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   a5() -> b5()
   a5() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
 5:b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   a6() -> b6()
   a6() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
 -----
 sorts
   [1>7, 2>7, 3>7, 4>7, 5>7, 6>7]
 sort attachment (non-strict)
   a1 : 1
   b1 : 7
   c1 : 7
   b2 : 7
   c2 : 7
   a2 : 2
   b3 : 7
   c3 : 7
   a3 : 3
   b4 : 7
   c4 : 7
   a4 : 4
   b5 : 7
   c5 : 7
   a5 : 5
   b6 : 7
   c6 : 7
   a6 : 6
   b7 : 7
 -----
 0:a1() -> b1()
   a1() -> c1()
   b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
   Church Rosser Transformation Processor (star):
    
    strict:
     
    weak:
     
    critical peaks: 4
    b1() <-0|[]- a1() -1|[]-> c1()
    c1() <-1|[]- a1() -0|[]-> b1()
    b1() <-14|[]- b7() -15|[]-> c1()
    c1() <-15|[]- b7() -14|[]-> b1()
    Shift Processor lab=left (dd):
     
     strict:
      a1() -> b1()
      a1() -> c1()
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      b6() -> b7()
      c1() -> c2()
      c2() -> c3()
      c3() -> c4()
      c4() -> c5()
      c5() -> c6()
      c6() -> b7()
      a1() -> c1()
      a1() -> b1()
      c1() -> c2()
      c2() -> c3()
      c3() -> c4()
      c4() -> c5()
      c5() -> c6()
      c6() -> b7()
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      b6() -> b7()
      b7() -> b1()
      b7() -> c1()
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      b6() -> b7()
      c1() -> c2()
      c2() -> c3()
      c3() -> c4()
      c4() -> c5()
      c5() -> c6()
      c6() -> b7()
      b7() -> c1()
      b7() -> b1()
      c1() -> c2()
      c2() -> c3()
      c3() -> c4()
      c4() -> c5()
      c5() -> c6()
      c6() -> b7()
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      b6() -> b7()
     weak:
      a1() -> b1()
      a1() -> c1()
      b1() -> b2()
      c1() -> c2()
      b2() -> b3()
      c2() -> c3()
      b3() -> b4()
      c3() -> c4()
      b4() -> b5()
      c4() -> c5()
      b5() -> b6()
      c5() -> c6()
      b6() -> b7()
      c6() -> b7()
      b7() -> b1()
      b7() -> c1()
     Polynomial Interpretation Processor:
      dimension: 1
      interpretation:
       [b7] = 0,
       
       [c6] = 0,
       
       [b6] = 0,
       
       [c5] = 0,
       
       [b5] = 0,
       
       [c4] = 0,
       
       [b4] = 0,
       
       [c3] = 0,
       
       [b3] = 0,
       
       [c2] = 0,
       
       [b2] = 0,
       
       [c1] = 0,
       
       [b1] = 0,
       
       [a1] = 1
      orientation:
       a1() = 1 >= 0 = b1()
       
       a1() = 1 >= 0 = c1()
       
       b1() = 0 >= 0 = b2()
       
       b2() = 0 >= 0 = b3()
       
       b3() = 0 >= 0 = b4()
       
       b4() = 0 >= 0 = b5()
       
       b5() = 0 >= 0 = b6()
       
       b6() = 0 >= 0 = b7()
       
       c1() = 0 >= 0 = c2()
       
       c2() = 0 >= 0 = c3()
       
       c3() = 0 >= 0 = c4()
       
       c4() = 0 >= 0 = c5()
       
       c5() = 0 >= 0 = c6()
       
       c6() = 0 >= 0 = b7()
       
       a1() = 1 >= 0 = c1()
       
       a1() = 1 >= 0 = b1()
       
       c1() = 0 >= 0 = c2()
       
       c2() = 0 >= 0 = c3()
       
       c3() = 0 >= 0 = c4()
       
       c4() = 0 >= 0 = c5()
       
       c5() = 0 >= 0 = c6()
       
       c6() = 0 >= 0 = b7()
       
       b1() = 0 >= 0 = b2()
       
       b2() = 0 >= 0 = b3()
       
       b3() = 0 >= 0 = b4()
       
       b4() = 0 >= 0 = b5()
       
       b5() = 0 >= 0 = b6()
       
       b6() = 0 >= 0 = b7()
       
       b7() = 0 >= 0 = b1()
       
       b7() = 0 >= 0 = c1()
       
       b1() = 0 >= 0 = b2()
       
       b2() = 0 >= 0 = b3()
       
       b3() = 0 >= 0 = b4()
       
       b4() = 0 >= 0 = b5()
       
       b5() = 0 >= 0 = b6()
       
       b6() = 0 >= 0 = b7()
       
       c1() = 0 >= 0 = c2()
       
       c2() = 0 >= 0 = c3()
       
       c3() = 0 >= 0 = c4()
       
       c4() = 0 >= 0 = c5()
       
       c5() = 0 >= 0 = c6()
       
       c6() = 0 >= 0 = b7()
       
       b7() = 0 >= 0 = c1()
       
       b7() = 0 >= 0 = b1()
       
       c1() = 0 >= 0 = c2()
       
       c2() = 0 >= 0 = c3()
       
       c3() = 0 >= 0 = c4()
       
       c4() = 0 >= 0 = c5()
       
       c5() = 0 >= 0 = c6()
       
       c6() = 0 >= 0 = b7()
       
       b1() = 0 >= 0 = b2()
       
       b2() = 0 >= 0 = b3()
       
       b3() = 0 >= 0 = b4()
       
       b4() = 0 >= 0 = b5()
       
       b5() = 0 >= 0 = b6()
       
       b6() = 0 >= 0 = b7()
      problem:
       
       strict:
        b1() -> b2()
        b2() -> b3()
        b3() -> b4()
        b4() -> b5()
        b5() -> b6()
        b6() -> b7()
        c1() -> c2()
        c2() -> c3()
        c3() -> c4()
        c4() -> c5()
        c5() -> c6()
        c6() -> b7()
        c1() -> c2()
        c2() -> c3()
        c3() -> c4()
        c4() -> c5()
        c5() -> c6()
        c6() -> b7()
        b1() -> b2()
        b2() -> b3()
        b3() -> b4()
        b4() -> b5()
        b5() -> b6()
        b6() -> b7()
        b7() -> b1()
        b7() -> c1()
        b1() -> b2()
        b2() -> b3()
        b3() -> b4()
        b4() -> b5()
        b5() -> b6()
        b6() -> b7()
        c1() -> c2()
        c2() -> c3()
        c3() -> c4()
        c4() -> c5()
        c5() -> c6()
        c6() -> b7()
        b7() -> c1()
        b7() -> b1()
        c1() -> c2()
        c2() -> c3()
        c3() -> c4()
        c4() -> c5()
        c5() -> c6()
        c6() -> b7()
        b1() -> b2()
        b2() -> b3()
        b3() -> b4()
        b4() -> b5()
        b5() -> b6()
        b6() -> b7()
       weak:
        b1() -> b2()
        c1() -> c2()
        b2() -> b3()
        c2() -> c3()
        b3() -> b4()
        c3() -> c4()
        b4() -> b5()
        c4() -> c5()
        b5() -> b6()
        c5() -> c6()
        b6() -> b7()
        c6() -> b7()
        b7() -> b1()
        b7() -> c1()
      Shift Processor (ldh) lab=left (force):
       
       strict:
        
       weak:
        
       Rule Labeling Processor:
        
        strict:
         
        weak:
         
        rule labeling (right):
         a1() -> b1(): 0
         a1() -> c1(): 0
         b1() -> b2(): 0
         c1() -> c2(): 0
         b2() -> b3(): 0
         c2() -> c3(): 0
         b3() -> b4(): 0
         c3() -> c4(): 0
         b4() -> b5(): 0
         c4() -> c5(): 0
         b5() -> b6(): 0
         c5() -> c6(): 0
         b6() -> b7(): 16
         c6() -> b7(): 0
         b7() -> b1(): 5
         b7() -> c1(): 16
        Decreasing Processor:
         The following diagrams are decreasing:
         peak:
          b1() <-0|[1,0]- a1() -1|[1,0]-> c1()
         joins:
          b1() -2|[0,0]-> b2() -4|[0,0]-> b3() -6|[0,0]-> b4() -8|[0,0]-> 
           b5() -10|[0,0]-> b6() -12|[0,16]-> b7()
          c1() -3|[0,0]-> c2() -5|[0,0]-> c3() -7|[0,0]-> c4() -9|[0,0]-> 
           c5() -11|[0,0]-> c6() -13|[0,0]-> b7()
         peak:
          c1() <-1|[1,0]- a1() -0|[1,0]-> b1()
         joins:
          c1() -3|[0,0]-> c2() -5|[0,0]-> c3() -7|[0,0]-> c4() -9|[0,0]-> 
           c5() -11|[0,0]-> c6() -13|[0,0]-> b7()
          b1() -2|[0,0]-> b2() -4|[0,0]-> b3() -6|[0,0]-> b4() -8|[0,0]-> 
           b5() -10|[0,0]-> b6() -12|[0,16]-> b7()
         peak:
          b1() <-14|[1,5]- b7() -15|[1,16]-> c1()
         joins:
          b1() -2|[1,0]-> b2() -4|[1,0]-> b3() -6|[1,0]-> b4() -8|[1,0]-> 
           b5() -10|[1,0]-> b6() -12|[1,16]-> b7()
          c1() -3|[1,0]-> c2() -5|[1,0]-> c3() -7|[1,0]-> c4() -9|[1,0]-> 
           c5() -11|[1,0]-> c6() -13|[1,0]-> b7()
         peak:
          c1() <-15|[1,16]- b7() -14|[1,5]-> b1()
         joins:
          c1() -3|[1,0]-> c2() -5|[1,0]-> c3() -7|[1,0]-> c4() -9|[1,0]-> 
           c5() -11|[1,0]-> c6() -13|[1,0]-> b7()
          b1() -2|[1,0]-> b2() -4|[1,0]-> b3() -6|[1,0]-> b4() -8|[1,0]-> 
           b5() -10|[1,0]-> b6() -12|[1,16]-> b7()
         Qed
  
  
  1:b1() -> b2()
    c1() -> c2()
    a2() -> b2()
    a2() -> c2()
    b2() -> b3()
    c2() -> c3()
    b3() -> b4()
    c3() -> c4()
    b4() -> b5()
    c4() -> c5()
    b5() -> b6()
    c5() -> c6()
    b6() -> b7()
    c6() -> b7()
    b7() -> b1()
    b7() -> c1()
    Church Rosser Transformation Processor (star):
     
     strict:
      
     weak:
      
     critical peaks: 4
     b2() <-2|[]- a2() -3|[]-> c2()
     c2() <-3|[]- a2() -2|[]-> b2()
     b1() <-14|[]- b7() -15|[]-> c1()
     c1() <-15|[]- b7() -14|[]-> b1()
     Shift Processor lab=left (dd):
      
      strict:
       a2() -> b2()
       a2() -> c2()
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
       c2() -> c3()
       c3() -> c4()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       a2() -> c2()
       a2() -> b2()
       c2() -> c3()
       c3() -> c4()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
       b7() -> b1()
       b7() -> c1()
       b1() -> b2()
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
       c1() -> c2()
       c2() -> c3()
       c3() -> c4()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       b7() -> c1()
       b7() -> b1()
       c1() -> c2()
       c2() -> c3()
       c3() -> c4()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       b1() -> b2()
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
      weak:
       b1() -> b2()
       c1() -> c2()
       a2() -> b2()
       a2() -> c2()
       b2() -> b3()
       c2() -> c3()
       b3() -> b4()
       c3() -> c4()
       b4() -> b5()
       c4() -> c5()
       b5() -> b6()
       c5() -> c6()
       b6() -> b7()
       c6() -> b7()
       b7() -> b1()
       b7() -> c1()
      Polynomial Interpretation Processor:
       dimension: 1
       interpretation:
        [b7] = 0,
        
        [c6] = 0,
        
        [b6] = 0,
        
        [c5] = 0,
        
        [b5] = 0,
        
        [c4] = 0,
        
        [b4] = 0,
        
        [c3] = 0,
        
        [b3] = 0,
        
        [a2] = 1,
        
        [c2] = 0,
        
        [b2] = 0,
        
        [c1] = 0,
        
        [b1] = 0
       orientation:
        a2() = 1 >= 0 = b2()
        
        a2() = 1 >= 0 = c2()
        
        b2() = 0 >= 0 = b3()
        
        b3() = 0 >= 0 = b4()
        
        b4() = 0 >= 0 = b5()
        
        b5() = 0 >= 0 = b6()
        
        b6() = 0 >= 0 = b7()
        
        c2() = 0 >= 0 = c3()
        
        c3() = 0 >= 0 = c4()
        
        c4() = 0 >= 0 = c5()
        
        c5() = 0 >= 0 = c6()
        
        c6() = 0 >= 0 = b7()
        
        a2() = 1 >= 0 = c2()
        
        a2() = 1 >= 0 = b2()
        
        c2() = 0 >= 0 = c3()
        
        c3() = 0 >= 0 = c4()
        
        c4() = 0 >= 0 = c5()
        
        c5() = 0 >= 0 = c6()
        
        c6() = 0 >= 0 = b7()
        
        b2() = 0 >= 0 = b3()
        
        b3() = 0 >= 0 = b4()
        
        b4() = 0 >= 0 = b5()
        
        b5() = 0 >= 0 = b6()
        
        b6() = 0 >= 0 = b7()
        
        b7() = 0 >= 0 = b1()
        
        b7() = 0 >= 0 = c1()
        
        b1() = 0 >= 0 = b2()
        
        b2() = 0 >= 0 = b3()
        
        b3() = 0 >= 0 = b4()
        
        b4() = 0 >= 0 = b5()
        
        b5() = 0 >= 0 = b6()
        
        b6() = 0 >= 0 = b7()
        
        c1() = 0 >= 0 = c2()
        
        c2() = 0 >= 0 = c3()
        
        c3() = 0 >= 0 = c4()
        
        c4() = 0 >= 0 = c5()
        
        c5() = 0 >= 0 = c6()
        
        c6() = 0 >= 0 = b7()
        
        b7() = 0 >= 0 = c1()
        
        b7() = 0 >= 0 = b1()
        
        c1() = 0 >= 0 = c2()
        
        c2() = 0 >= 0 = c3()
        
        c3() = 0 >= 0 = c4()
        
        c4() = 0 >= 0 = c5()
        
        c5() = 0 >= 0 = c6()
        
        c6() = 0 >= 0 = b7()
        
        b1() = 0 >= 0 = b2()
        
        b2() = 0 >= 0 = b3()
        
        b3() = 0 >= 0 = b4()
        
        b4() = 0 >= 0 = b5()
        
        b5() = 0 >= 0 = b6()
        
        b6() = 0 >= 0 = b7()
       problem:
        
        strict:
         b2() -> b3()
         b3() -> b4()
         b4() -> b5()
         b5() -> b6()
         b6() -> b7()
         c2() -> c3()
         c3() -> c4()
         c4() -> c5()
         c5() -> c6()
         c6() -> b7()
         c2() -> c3()
         c3() -> c4()
         c4() -> c5()
         c5() -> c6()
         c6() -> b7()
         b2() -> b3()
         b3() -> b4()
         b4() -> b5()
         b5() -> b6()
         b6() -> b7()
         b7() -> b1()
         b7() -> c1()
         b1() -> b2()
         b2() -> b3()
         b3() -> b4()
         b4() -> b5()
         b5() -> b6()
         b6() -> b7()
         c1() -> c2()
         c2() -> c3()
         c3() -> c4()
         c4() -> c5()
         c5() -> c6()
         c6() -> b7()
         b7() -> c1()
         b7() -> b1()
         c1() -> c2()
         c2() -> c3()
         c3() -> c4()
         c4() -> c5()
         c5() -> c6()
         c6() -> b7()
         b1() -> b2()
         b2() -> b3()
         b3() -> b4()
         b4() -> b5()
         b5() -> b6()
         b6() -> b7()
        weak:
         b1() -> b2()
         c1() -> c2()
         b2() -> b3()
         c2() -> c3()
         b3() -> b4()
         c3() -> c4()
         b4() -> b5()
         c4() -> c5()
         b5() -> b6()
         c5() -> c6()
         b6() -> b7()
         c6() -> b7()
         b7() -> b1()
         b7() -> c1()
       Shift Processor (ldh) lab=left (force):
        
        strict:
         
        weak:
         
        Rule Labeling Processor:
         
         strict:
          
         weak:
          
         rule labeling (right):
          b1() -> b2(): 0
          c1() -> c2(): 0
          a2() -> b2(): 0
          a2() -> c2(): 0
          b2() -> b3(): 0
          c2() -> c3(): 7
          b3() -> b4(): 0
          c3() -> c4(): 0
          b4() -> b5(): 5
          c4() -> c5(): 0
          b5() -> b6(): 0
          c5() -> c6(): 0
          b6() -> b7(): 0
          c6() -> b7(): 0
          b7() -> b1(): 7
          b7() -> c1(): 5
         Decreasing Processor:
          The following diagrams are decreasing:
          peak:
           b2() <-2|[1,0]- a2() -3|[1,0]-> c2()
          joins:
           b2() -4|[0,0]-> b3() -6|[0,0]-> b4() -8|[0,5]-> b5() -10|[0,0]-> b6() -12|[0,0]-> b7()
           c2() -5|[0,7]-> c3() -7|[0,0]-> c4() -9|[0,0]-> c5() -11|[0,0]-> c6() -13|[0,0]-> b7()
          peak:
           c2() <-3|[1,0]- a2() -2|[1,0]-> b2()
          joins:
           c2() -5|[0,7]-> c3() -7|[0,0]-> c4() -9|[0,0]-> c5() -11|[0,0]-> c6() -13|[0,0]-> b7()
           b2() -4|[0,0]-> b3() -6|[0,0]-> b4() -8|[0,5]-> b5() -10|[0,0]-> b6() -12|[0,0]-> b7()
          peak:
           b1() <-14|[1,7]- b7() -15|[1,5]-> c1()
          joins:
           b1() -0|[1,0]-> b2() -4|[1,0]-> b3() -6|[1,0]-> b4() -8|[1,5]-> 
            b5() -10|[1,0]-> b6() -12|[1,0]-> b7()
           c1() -1|[1,0]-> c2() -5|[1,7]-> c3() -7|[1,0]-> c4() -9|[1,0]-> 
            c5() -11|[1,0]-> c6() -13|[1,0]-> b7()
          peak:
           c1() <-15|[1,5]- b7() -14|[1,7]-> b1()
          joins:
           c1() -1|[1,0]-> c2() -5|[1,7]-> c3() -7|[1,0]-> c4() -9|[1,0]-> 
            c5() -11|[1,0]-> c6() -13|[1,0]-> b7()
           b1() -0|[1,0]-> b2() -4|[1,0]-> b3() -6|[1,0]-> b4() -8|[1,5]-> 
            b5() -10|[1,0]-> b6() -12|[1,0]-> b7()
          Qed


2:b1() -> b2()
  c1() -> c2()
  b2() -> b3()
  c2() -> c3()
  a3() -> b3()
  a3() -> c3()
  b3() -> b4()
  c3() -> c4()
  b4() -> b5()
  c4() -> c5()
  b5() -> b6()
  c5() -> c6()
  b6() -> b7()
  c6() -> b7()
  b7() -> b1()
  b7() -> c1()
  Church Rosser Transformation Processor (star):
   
   strict:
    
   weak:
    
   critical peaks: 4
   b3() <-4|[]- a3() -5|[]-> c3()
   c3() <-5|[]- a3() -4|[]-> b3()
   b1() <-14|[]- b7() -15|[]-> c1()
   c1() <-15|[]- b7() -14|[]-> b1()
   Shift Processor lab=left (dd):
    
    strict:
     a3() -> b3()
     a3() -> c3()
     b3() -> b4()
     b4() -> b5()
     b5() -> b6()
     b6() -> b7()
     c3() -> c4()
     c4() -> c5()
     c5() -> c6()
     c6() -> b7()
     a3() -> c3()
     a3() -> b3()
     c3() -> c4()
     c4() -> c5()
     c5() -> c6()
     c6() -> b7()
     b3() -> b4()
     b4() -> b5()
     b5() -> b6()
     b6() -> b7()
     b7() -> b1()
     b7() -> c1()
     b1() -> b2()
     b2() -> b3()
     b3() -> b4()
     b4() -> b5()
     b5() -> b6()
     b6() -> b7()
     c1() -> c2()
     c2() -> c3()
     c3() -> c4()
     c4() -> c5()
     c5() -> c6()
     c6() -> b7()
     b7() -> c1()
     b7() -> b1()
     c1() -> c2()
     c2() -> c3()
     c3() -> c4()
     c4() -> c5()
     c5() -> c6()
     c6() -> b7()
     b1() -> b2()
     b2() -> b3()
     b3() -> b4()
     b4() -> b5()
     b5() -> b6()
     b6() -> b7()
    weak:
     b1() -> b2()
     c1() -> c2()
     b2() -> b3()
     c2() -> c3()
     a3() -> b3()
     a3() -> c3()
     b3() -> b4()
     c3() -> c4()
     b4() -> b5()
     c4() -> c5()
     b5() -> b6()
     c5() -> c6()
     b6() -> b7()
     c6() -> b7()
     b7() -> b1()
     b7() -> c1()
    Polynomial Interpretation Processor:
     dimension: 1
     interpretation:
      [b7] = 0,
      
      [c6] = 0,
      
      [b6] = 0,
      
      [c5] = 0,
      
      [b5] = 0,
      
      [c4] = 0,
      
      [b4] = 0,
      
      [a3] = 1,
      
      [c3] = 0,
      
      [b3] = 0,
      
      [c2] = 0,
      
      [b2] = 0,
      
      [c1] = 0,
      
      [b1] = 0
     orientation:
      a3() = 1 >= 0 = b3()
      
      a3() = 1 >= 0 = c3()
      
      b3() = 0 >= 0 = b4()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      b6() = 0 >= 0 = b7()
      
      c3() = 0 >= 0 = c4()
      
      c4() = 0 >= 0 = c5()
      
      c5() = 0 >= 0 = c6()
      
      c6() = 0 >= 0 = b7()
      
      a3() = 1 >= 0 = c3()
      
      a3() = 1 >= 0 = b3()
      
      c3() = 0 >= 0 = c4()
      
      c4() = 0 >= 0 = c5()
      
      c5() = 0 >= 0 = c6()
      
      c6() = 0 >= 0 = b7()
      
      b3() = 0 >= 0 = b4()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      b6() = 0 >= 0 = b7()
      
      b7() = 0 >= 0 = b1()
      
      b7() = 0 >= 0 = c1()
      
      b1() = 0 >= 0 = b2()
      
      b2() = 0 >= 0 = b3()
      
      b3() = 0 >= 0 = b4()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      b6() = 0 >= 0 = b7()
      
      c1() = 0 >= 0 = c2()
      
      c2() = 0 >= 0 = c3()
      
      c3() = 0 >= 0 = c4()
      
      c4() = 0 >= 0 = c5()
      
      c5() = 0 >= 0 = c6()
      
      c6() = 0 >= 0 = b7()
      
      b7() = 0 >= 0 = c1()
      
      b7() = 0 >= 0 = b1()
      
      c1() = 0 >= 0 = c2()
      
      c2() = 0 >= 0 = c3()
      
      c3() = 0 >= 0 = c4()
      
      c4() = 0 >= 0 = c5()
      
      c5() = 0 >= 0 = c6()
      
      c6() = 0 >= 0 = b7()
      
      b1() = 0 >= 0 = b2()
      
      b2() = 0 >= 0 = b3()
      
      b3() = 0 >= 0 = b4()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      b6() = 0 >= 0 = b7()
     problem:
      
      strict:
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
       c3() -> c4()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       c3() -> c4()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
       b7() -> b1()
       b7() -> c1()
       b1() -> b2()
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
       c1() -> c2()
       c2() -> c3()
       c3() -> c4()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       b7() -> c1()
       b7() -> b1()
       c1() -> c2()
       c2() -> c3()
       c3() -> c4()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       b1() -> b2()
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
      weak:
       b1() -> b2()
       c1() -> c2()
       b2() -> b3()
       c2() -> c3()
       b3() -> b4()
       c3() -> c4()
       b4() -> b5()
       c4() -> c5()
       b5() -> b6()
       c5() -> c6()
       b6() -> b7()
       c6() -> b7()
       b7() -> b1()
       b7() -> c1()
     Shift Processor (ldh) lab=left (force):
      
      strict:
       
      weak:
       
      Rule Labeling Processor:
       
       strict:
        
       weak:
        
       rule labeling (right):
        b1() -> b2(): 0
        c1() -> c2(): 5
        b2() -> b3(): 0
        c2() -> c3(): 0
        a3() -> b3(): 0
        a3() -> c3(): 0
        b3() -> b4(): 0
        c3() -> c4(): 0
        b4() -> b5(): 0
        c4() -> c5(): 0
        b5() -> b6(): 0
        c5() -> c6(): 0
        b6() -> b7(): 0
        c6() -> b7(): 0
        b7() -> b1(): 5
        b7() -> c1(): 0
       Decreasing Processor:
        The following diagrams are decreasing:
        peak:
         b3() <-4|[1,0]- a3() -5|[1,0]-> c3()
        joins:
         b3() -6|[0,0]-> b4() -8|[0,0]-> b5() -10|[0,0]-> b6() -12|[0,0]-> b7()
         c3() -7|[0,0]-> c4() -9|[0,0]-> c5() -11|[0,0]-> c6() -13|[0,0]-> b7()
        peak:
         c3() <-5|[1,0]- a3() -4|[1,0]-> b3()
        joins:
         c3() -7|[0,0]-> c4() -9|[0,0]-> c5() -11|[0,0]-> c6() -13|[0,0]-> b7()
         b3() -6|[0,0]-> b4() -8|[0,0]-> b5() -10|[0,0]-> b6() -12|[0,0]-> b7()
        peak:
         b1() <-14|[1,5]- b7() -15|[1,0]-> c1()
        joins:
         b1() -0|[1,0]-> b2() -2|[1,0]-> b3() -6|[1,0]-> b4() -8|[1,0]-> 
          b5() -10|[1,0]-> b6() -12|[1,0]-> b7()
         c1() -1|[1,5]-> c2() -3|[1,0]-> c3() -7|[1,0]-> c4() -9|[1,0]-> 
          c5() -11|[1,0]-> c6() -13|[1,0]-> b7()
        peak:
         c1() <-15|[1,0]- b7() -14|[1,5]-> b1()
        joins:
         c1() -1|[1,5]-> c2() -3|[1,0]-> c3() -7|[1,0]-> c4() -9|[1,0]-> 
          c5() -11|[1,0]-> c6() -13|[1,0]-> b7()
         b1() -0|[1,0]-> b2() -2|[1,0]-> b3() -6|[1,0]-> b4() -8|[1,0]-> 
          b5() -10|[1,0]-> b6() -12|[1,0]-> b7()
        Qed


3:b1() -> b2()
  c1() -> c2()
  b2() -> b3()
  c2() -> c3()
  b3() -> b4()
  c3() -> c4()
  a4() -> b4()
  a4() -> c4()
  b4() -> b5()
  c4() -> c5()
  b5() -> b6()
  c5() -> c6()
  b6() -> b7()
  c6() -> b7()
  b7() -> b1()
  b7() -> c1()
  Church Rosser Transformation Processor (star):
   
   strict:
    
   weak:
    
   critical peaks: 4
   b4() <-6|[]- a4() -7|[]-> c4()
   c4() <-7|[]- a4() -6|[]-> b4()
   b1() <-14|[]- b7() -15|[]-> c1()
   c1() <-15|[]- b7() -14|[]-> b1()
   Shift Processor lab=left (dd):
    
    strict:
     a4() -> b4()
     a4() -> c4()
     b4() -> b5()
     b5() -> b6()
     b6() -> b7()
     c4() -> c5()
     c5() -> c6()
     c6() -> b7()
     a4() -> c4()
     a4() -> b4()
     c4() -> c5()
     c5() -> c6()
     c6() -> b7()
     b4() -> b5()
     b5() -> b6()
     b6() -> b7()
     b7() -> b1()
     b7() -> c1()
     b1() -> b2()
     b2() -> b3()
     b3() -> b4()
     b4() -> b5()
     b5() -> b6()
     b6() -> b7()
     c1() -> c2()
     c2() -> c3()
     c3() -> c4()
     c4() -> c5()
     c5() -> c6()
     c6() -> b7()
     b7() -> c1()
     b7() -> b1()
     c1() -> c2()
     c2() -> c3()
     c3() -> c4()
     c4() -> c5()
     c5() -> c6()
     c6() -> b7()
     b1() -> b2()
     b2() -> b3()
     b3() -> b4()
     b4() -> b5()
     b5() -> b6()
     b6() -> b7()
    weak:
     b1() -> b2()
     c1() -> c2()
     b2() -> b3()
     c2() -> c3()
     b3() -> b4()
     c3() -> c4()
     a4() -> b4()
     a4() -> c4()
     b4() -> b5()
     c4() -> c5()
     b5() -> b6()
     c5() -> c6()
     b6() -> b7()
     c6() -> b7()
     b7() -> b1()
     b7() -> c1()
    Polynomial Interpretation Processor:
     dimension: 1
     interpretation:
      [b7] = 0,
      
      [c6] = 0,
      
      [b6] = 0,
      
      [c5] = 0,
      
      [b5] = 0,
      
      [a4] = 1,
      
      [c4] = 0,
      
      [b4] = 0,
      
      [c3] = 0,
      
      [b3] = 0,
      
      [c2] = 0,
      
      [b2] = 0,
      
      [c1] = 0,
      
      [b1] = 0
     orientation:
      a4() = 1 >= 0 = b4()
      
      a4() = 1 >= 0 = c4()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      b6() = 0 >= 0 = b7()
      
      c4() = 0 >= 0 = c5()
      
      c5() = 0 >= 0 = c6()
      
      c6() = 0 >= 0 = b7()
      
      a4() = 1 >= 0 = c4()
      
      a4() = 1 >= 0 = b4()
      
      c4() = 0 >= 0 = c5()
      
      c5() = 0 >= 0 = c6()
      
      c6() = 0 >= 0 = b7()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      b6() = 0 >= 0 = b7()
      
      b7() = 0 >= 0 = b1()
      
      b7() = 0 >= 0 = c1()
      
      b1() = 0 >= 0 = b2()
      
      b2() = 0 >= 0 = b3()
      
      b3() = 0 >= 0 = b4()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      b6() = 0 >= 0 = b7()
      
      c1() = 0 >= 0 = c2()
      
      c2() = 0 >= 0 = c3()
      
      c3() = 0 >= 0 = c4()
      
      c4() = 0 >= 0 = c5()
      
      c5() = 0 >= 0 = c6()
      
      c6() = 0 >= 0 = b7()
      
      b7() = 0 >= 0 = c1()
      
      b7() = 0 >= 0 = b1()
      
      c1() = 0 >= 0 = c2()
      
      c2() = 0 >= 0 = c3()
      
      c3() = 0 >= 0 = c4()
      
      c4() = 0 >= 0 = c5()
      
      c5() = 0 >= 0 = c6()
      
      c6() = 0 >= 0 = b7()
      
      b1() = 0 >= 0 = b2()
      
      b2() = 0 >= 0 = b3()
      
      b3() = 0 >= 0 = b4()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      b6() = 0 >= 0 = b7()
     problem:
      
      strict:
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
       b7() -> b1()
       b7() -> c1()
       b1() -> b2()
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
       c1() -> c2()
       c2() -> c3()
       c3() -> c4()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       b7() -> c1()
       b7() -> b1()
       c1() -> c2()
       c2() -> c3()
       c3() -> c4()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       b1() -> b2()
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
      weak:
       b1() -> b2()
       c1() -> c2()
       b2() -> b3()
       c2() -> c3()
       b3() -> b4()
       c3() -> c4()
       b4() -> b5()
       c4() -> c5()
       b5() -> b6()
       c5() -> c6()
       b6() -> b7()
       c6() -> b7()
       b7() -> b1()
       b7() -> c1()
     Shift Processor (ldh) lab=left (force):
      
      strict:
       
      weak:
       
      Rule Labeling Processor:
       
       strict:
        
       weak:
        
       rule labeling (right):
        b1() -> b2(): 0
        c1() -> c2(): 0
        b2() -> b3(): 0
        c2() -> c3(): 0
        b3() -> b4(): 0
        c3() -> c4(): 0
        a4() -> b4(): 0
        a4() -> c4(): 0
        b4() -> b5(): 0
        c4() -> c5(): 0
        b5() -> b6(): 0
        c5() -> c6(): 0
        b6() -> b7(): 16
        c6() -> b7(): 1
        b7() -> b1(): 1
        b7() -> c1(): 16
       Decreasing Processor:
        The following diagrams are decreasing:
        peak:
         b4() <-6|[1,0]- a4() -7|[1,0]-> c4()
        joins:
         b4() -8|[0,0]-> b5() -10|[0,0]-> b6() -12|[0,16]-> b7()
         c4() -9|[0,0]-> c5() -11|[0,0]-> c6() -13|[0,1]-> b7()
        peak:
         c4() <-7|[1,0]- a4() -6|[1,0]-> b4()
        joins:
         c4() -9|[0,0]-> c5() -11|[0,0]-> c6() -13|[0,1]-> b7()
         b4() -8|[0,0]-> b5() -10|[0,0]-> b6() -12|[0,16]-> b7()
        peak:
         b1() <-14|[1,1]- b7() -15|[1,16]-> c1()
        joins:
         b1() -0|[1,0]-> b2() -2|[1,0]-> b3() -4|[1,0]-> b4() -8|[1,0]-> 
          b5() -10|[1,0]-> b6() -12|[1,16]-> b7()
         c1() -1|[1,0]-> c2() -3|[1,0]-> c3() -5|[1,0]-> c4() -9|[1,0]-> 
          c5() -11|[1,0]-> c6() -13|[1,1]-> b7()
        peak:
         c1() <-15|[1,16]- b7() -14|[1,1]-> b1()
        joins:
         c1() -1|[1,0]-> c2() -3|[1,0]-> c3() -5|[1,0]-> c4() -9|[1,0]-> 
          c5() -11|[1,0]-> c6() -13|[1,1]-> b7()
         b1() -0|[1,0]-> b2() -2|[1,0]-> b3() -4|[1,0]-> b4() -8|[1,0]-> 
          b5() -10|[1,0]-> b6() -12|[1,16]-> b7()
        Qed


4:b1() -> b2()
  c1() -> c2()
  b2() -> b3()
  c2() -> c3()
  b3() -> b4()
  c3() -> c4()
  b4() -> b5()
  c4() -> c5()
  a5() -> b5()
  a5() -> c5()
  b5() -> b6()
  c5() -> c6()
  b6() -> b7()
  c6() -> b7()
  b7() -> b1()
  b7() -> c1()
  Church Rosser Transformation Processor (dup):
   
   strict:
    
   weak:
    b1() -> b2()
    c1() -> c2()
    b2() -> b3()
    c2() -> c3()
    b3() -> b4()
    c3() -> c4()
    b4() -> b5()
    c4() -> c5()
    a5() -> b5()
    a5() -> c5()
    b5() -> b6()
    c5() -> c6()
    b6() -> b7()
    c6() -> b7()
    b7() -> b1()
    b7() -> c1()
   critical peaks: 4
   b5() <-8|[]- a5() -9|[]-> c5()
   c5() <-9|[]- a5() -8|[]-> b5()
   b1() <-14|[]- b7() -15|[]-> c1()
   c1() <-15|[]- b7() -14|[]-> b1()
   Shift Processor (no label):
    
    strict:
     
    weak:
     
    Shift Processor lab=left (dd):
     
     strict:
      a5() -> b5()
      a5() -> c5()
      b5() -> b6()
      b6() -> b7()
      c5() -> c6()
      c6() -> b7()
      a5() -> c5()
      a5() -> b5()
      c5() -> c6()
      c6() -> b7()
      b5() -> b6()
      b6() -> b7()
      b7() -> b1()
      b7() -> c1()
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      b6() -> b7()
      c1() -> c2()
      c2() -> c3()
      c3() -> c4()
      c4() -> c5()
      c5() -> c6()
      c6() -> b7()
      b7() -> c1()
      b7() -> b1()
      c1() -> c2()
      c2() -> c3()
      c3() -> c4()
      c4() -> c5()
      c5() -> c6()
      c6() -> b7()
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      b6() -> b7()
     weak:
      b1() -> b2()
      c1() -> c2()
      b2() -> b3()
      c2() -> c3()
      b3() -> b4()
      c3() -> c4()
      b4() -> b5()
      c4() -> c5()
      a5() -> b5()
      a5() -> c5()
      b5() -> b6()
      c5() -> c6()
      b6() -> b7()
      c6() -> b7()
      b7() -> b1()
      b7() -> c1()
     Shift Processor (ldh) lab=left (force):
      
      strict:
       
      weak:
       
      Rule Labeling Processor:
       
       strict:
        
       weak:
        
       rule labeling (right):
        b1() -> b2(): 0
        c1() -> c2(): 0
        b2() -> b3(): 0
        c2() -> c3(): 0
        b3() -> b4(): 0
        c3() -> c4(): 0
        b4() -> b5(): 0
        c4() -> c5(): 0
        a5() -> b5(): 1
        a5() -> c5(): 1
        b5() -> b6(): 0
        c5() -> c6(): 0
        b6() -> b7(): 1
        c6() -> b7(): 1
        b7() -> b1(): 1
        b7() -> c1(): 3
       Decreasing Processor:
        The following diagrams are decreasing:
        peak:
         b5() <-8|[1,1]- a5() -9|[1,1]-> c5()
        joins:
         b5() -10|[1,0]-> b6() -12|[1,1]-> b7()
         c5() -11|[1,0]-> c6() -13|[1,1]-> b7()
        peak:
         c5() <-9|[1,1]- a5() -8|[1,1]-> b5()
        joins:
         c5() -11|[1,0]-> c6() -13|[1,1]-> b7()
         b5() -10|[1,0]-> b6() -12|[1,1]-> b7()
        peak:
         b1() <-14|[1,1]- b7() -15|[1,3]-> c1()
        joins:
         b1() -0|[1,0]-> b2() -2|[1,0]-> b3() -4|[1,0]-> b4() -6|[1,0]-> 
          b5() -10|[1,0]-> b6() -12|[1,1]-> b7()
         c1() -1|[1,0]-> c2() -3|[1,0]-> c3() -5|[1,0]-> c4() -7|[1,0]-> 
          c5() -11|[1,0]-> c6() -13|[1,1]-> b7()
        peak:
         c1() <-15|[1,3]- b7() -14|[1,1]-> b1()
        joins:
         c1() -1|[1,0]-> c2() -3|[1,0]-> c3() -5|[1,0]-> c4() -7|[1,0]-> 
          c5() -11|[1,0]-> c6() -13|[1,1]-> b7()
         b1() -0|[1,0]-> b2() -2|[1,0]-> b3() -4|[1,0]-> b4() -6|[1,0]-> 
          b5() -10|[1,0]-> b6() -12|[1,1]-> b7()
        Qed


5:b1() -> b2()
  c1() -> c2()
  b2() -> b3()
  c2() -> c3()
  b3() -> b4()
  c3() -> c4()
  b4() -> b5()
  c4() -> c5()
  b5() -> b6()
  c5() -> c6()
  a6() -> b6()
  a6() -> c6()
  b6() -> b7()
  c6() -> b7()
  b7() -> b1()
  b7() -> c1()
  Church Rosser Transformation Processor (dup):
   
   strict:
    
   weak:
    b1() -> b2()
    c1() -> c2()
    b2() -> b3()
    c2() -> c3()
    b3() -> b4()
    c3() -> c4()
    b4() -> b5()
    c4() -> c5()
    b5() -> b6()
    c5() -> c6()
    a6() -> b6()
    a6() -> c6()
    b6() -> b7()
    c6() -> b7()
    b7() -> b1()
    b7() -> c1()
   critical peaks: 4
   b6() <-10|[]- a6() -11|[]-> c6()
   c6() <-11|[]- a6() -10|[]-> b6()
   b1() <-14|[]- b7() -15|[]-> c1()
   c1() <-15|[]- b7() -14|[]-> b1()
   Shift Processor (no label):
    
    strict:
     
    weak:
     
    Shift Processor lab=left (dd):
     
     strict:
      a6() -> b6()
      a6() -> c6()
      b6() -> b7()
      c6() -> b7()
      a6() -> c6()
      a6() -> b6()
      c6() -> b7()
      b6() -> b7()
      b7() -> b1()
      b7() -> c1()
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      b6() -> b7()
      c1() -> c2()
      c2() -> c3()
      c3() -> c4()
      c4() -> c5()
      c5() -> c6()
      c6() -> b7()
      b7() -> c1()
      b7() -> b1()
      c1() -> c2()
      c2() -> c3()
      c3() -> c4()
      c4() -> c5()
      c5() -> c6()
      c6() -> b7()
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      b6() -> b7()
     weak:
      b1() -> b2()
      c1() -> c2()
      b2() -> b3()
      c2() -> c3()
      b3() -> b4()
      c3() -> c4()
      b4() -> b5()
      c4() -> c5()
      b5() -> b6()
      c5() -> c6()
      a6() -> b6()
      a6() -> c6()
      b6() -> b7()
      c6() -> b7()
      b7() -> b1()
      b7() -> c1()
     Shift Processor (ldh) lab=left (force):
      
      strict:
       
      weak:
       
      Rule Labeling Processor:
       
       strict:
        
       weak:
        
       rule labeling (right):
        b1() -> b2(): 0
        c1() -> c2(): 0
        b2() -> b3(): 0
        c2() -> c3(): 0
        b3() -> b4(): 0
        c3() -> c4(): 0
        b4() -> b5(): 0
        c4() -> c5(): 0
        b5() -> b6(): 0
        c5() -> c6(): 0
        a6() -> b6(): 1
        a6() -> c6(): 1
        b6() -> b7(): 0
        c6() -> b7(): 0
        b7() -> b1(): 1
        b7() -> c1(): 0
       Decreasing Processor:
        The following diagrams are decreasing:
        peak:
         b6() <-10|[1,1]- a6() -11|[1,1]-> c6()
        joins:
         b6() -12|[1,0]-> b7()
         c6() -13|[1,0]-> b7()
        peak:
         c6() <-11|[1,1]- a6() -10|[1,1]-> b6()
        joins:
         c6() -13|[1,0]-> b7()
         b6() -12|[1,0]-> b7()
        peak:
         b1() <-14|[1,1]- b7() -15|[1,0]-> c1()
        joins:
         b1() -0|[1,0]-> b2() -2|[1,0]-> b3() -4|[1,0]-> b4() -6|[1,0]-> 
          b5() -8|[1,0]-> b6() -12|[1,0]-> b7()
         c1() -1|[1,0]-> c2() -3|[1,0]-> c3() -5|[1,0]-> c4() -7|[1,0]-> 
          c5() -9|[1,0]-> c6() -13|[1,0]-> b7()
        peak:
         c1() <-15|[1,0]- b7() -14|[1,1]-> b1()
        joins:
         c1() -1|[1,0]-> c2() -3|[1,0]-> c3() -5|[1,0]-> c4() -7|[1,0]-> 
          c5() -9|[1,0]-> c6() -13|[1,0]-> b7()
         b1() -0|[1,0]-> b2() -2|[1,0]-> b3() -4|[1,0]-> b4() -6|[1,0]-> 
          b5() -8|[1,0]-> b6() -12|[1,0]-> b7()
        Qed