ntimm@cs.up.ac.za2018-08-082018-08-082018-08-012018-08-01Nils Timm and Stefan Gruner, Three-Valued Bounded Model Checking with Cause-Guided Abstraction Refinement: PROOFS. Technical Report TR-SSFM-01-08-2018, Research Group for System Specifications and Formal Methods, Department of Computer Science, University of Pretoria, 2018.http://hdl.handle.net/2263/66136In 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.enCopyright: the authors.Model Checking, Bounded Model Checking, Theorem, ProofTechnical Report