cl-banner

CSI-0.1


Problem:
 F(x,y) -> c(A())
 G(x) -> x
 h(x) -> c(x)

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