cl-banner

CSI-0.1


Problem:
 F(x,C(x)) -> A()
 F(x,x) -> B()
 a() -> g(C(a()))
 g(x) -> x

Proof:
 Nonconfluence Processor:
  terms: B() *<- F(a(),C(a())) ->* A()
  Qed
Nach oben scrollen