Jancar's formal system for deciding bisimulation of first-order grammars and its non-soundness

Géraud Sénizergues

We construct an example of proof within the main formal system from arXiv:1010.4760v3, which is intended to capture the bisimulation equivalence for non-deterministic first-order g…