Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle