Brae J. Webb, Ian J. Hayes, Mark Utting: Verifying Term Graph Optimizations using Isabelle/HOL. CPP 2023: 320-333