cl-banner

CSI-0.1


Problem:
 h(f(),a(),a()) -> h(g(),a(),a())
 h(g(),a(),a()) -> h(f(),a(),a())
 a() -> a'()
 h(x,a'(),y) -> h(x,y,y)
 h(x,y,a'()) -> h(x,y,y)

Proof:
 Nonconfluence Processor:
  terms: h(f(),a'(),a'()) *<- h(f(),a(),a()) ->* h(g(),a'(),a'())
  Qed
Nach oben scrollen