cl-banner

CSI-0.1


Problem:
 or(true(),true()) -> true()
 or(x,y) -> or(y,x)

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   
  weak:
   
  critical peaks: 2
  true() <-0|[]- or(true(),true()) -1|[]-> or(true(),true())
  or(true(),true()) <-1|[]- or(true(),true()) -0|[]-> true()
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed

Nach oben scrollen