cl-banner

CSI-0.1


Problem:
 f(x) -> x
 f(x) -> f(f(x))

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   f(0)(x) -> f(0)(f(0)(x))
   f(0)(x) -> x
  critical peaks: 2
  x <-0|[]- f(x) -1|[]-> f(f(x))
  f(f(x)) <-1|[]- f(x) -0|[]-> x
  Shift Processor lab=left (dd):
   
   strict:
    f(x) -> x
    f(x) -> f(f(x))
    f(f(x)) -> f(x)
    f(x) -> x
    f(x) -> f(f(x))
    f(x) -> x
    f(f(x)) -> f(x)
    f(x) -> x
   weak:
    f(x) -> x
    f(x) -> f(f(x))
   Shift Processor (ldh) lab=left (force):
    
    strict:
     
    weak:
     
    Rule Labeling Processor:
     
     strict:
      
     weak:
      
     rule labeling (right):
      f(x) -> x: 0
      f(x) -> f(f(x)): 2
     Decreasing Processor:
      The following diagrams are decreasing:
      peak:
       x <-0|[1,0]- f(x) -1|[1,2]-> f(f(x))
      joins:
       
       f(f(x)) -0|[1,0]-> f(x) -0|[1,0]-> x
      peak:
       f(f(x)) <-1|[1,2]- f(x) -0|[1,0]-> x
      joins:
       f(f(x)) -0|[1,0]-> f(x) -0|[1,0]-> x
       
      Qed
Nach oben scrollen