more precise symexec for nondet automata

- symexec handles or: demonic split in confgraphs
- triples are inferred from sets of confs that cover all nondet behavior
- moved [is_pure] from [Prover] to [Expression]
- added [mk_meet] to [Prover], but with dummy implementation