Abstract:
In this Technical Report we provide the proof to Theorem 1 which appears in our forthcoming article "Three-Valued Bounded Model Checking with Cause-Guided Abstraction Refinement", to appear in the journal: Science of Computer Programming. Due to shortage of page-space the proof cannot be printed in the journal article itself. In the forthcoming journal article, wherein Theorem 1 will appear, a literature reference will point the readers to this Technical Report for the proof.
