cl-banner

CSI-0.1


Problem:
 F(x,y) -> c(y)
 G(x) -> x
 f(x) -> g(x)
 g(x) -> c(x)

Proof:
 sorted: (order)
 0:F(x,y) -> c(y)
 1:G(x) -> x
 2:f(x) -> g(x)
   g(x) -> c(x)
 -----
 sorts
   [1>5, 1>10, 2>9, 3>4, 4>5, 5>6, 6>7, 6>11, 7>8]
 sort attachment (non-strict)
   F : 10 x 11 -> 1
   c : 6 -> 5
   G : 9 -> 2
   f : 8 -> 3
   g : 7 -> 4
 -----
 0:F(x,y) -> c(y)
   Church Rosser Transformation Processor:
    
    strict:
     
    weak:
     
    critical peaks: 0
    Qed
 
 
 1:G(x) -> x
   Church Rosser Transformation Processor:
    
    strict:
     
    weak:
     
    critical peaks: 0
    Qed
 
 
 2:f(x) -> g(x)
   g(x) -> c(x)
   Church Rosser Transformation Processor:
    
    strict:
     
    weak:
     
    critical peaks: 0
    Qed
 
Nach oben scrollen