⁴Since executes@state₀ and returns@state₀ are contradictory, the inner conditional formula can be reduced to its second branch; here the formula is not yet sufficiently simplified by the RISC ProgramExplorer.