Rot et al. present various operations on languages by using the mathematical theory approach in order to prove the similarity of two languages. Four operations are used for the proof of soundness on their technique, called bisimulation-up-to: relation, union, function, and equation.

In their approach, bisimulation-up-to is used to establish a theorem prover. The soundness of their theorem prover is established by using the axioms of Kleene algebra. That is, they first establish the definition of deterministic automata by using a relation operation. They then establish the theorem of coinduction for any two states of deterministic automata.

Based on their approach, the mathematical results for the proof of soundness on their technique are discussed. The results show that bisimulation-up-to can be used as a tool for a theorem prover.