Index Introduction Obligatory Cartoon Alternate Talk Titles Overview Executable Formal Models (EFM) Project DEFTYPE #. (Read Time Form Evaluation) #. Dual Mode Solution DEFABBREV DEFABBREV : THE DEFABBREV : THE Solution(s) DEFABBREV : IF DEFABBREV : IF -vs- MY-IF DEFABBREV : IF, The JEM1 Solution DEFABBREV : IF, An ACL2 Solution Modular Arithmetic Modular Arithmetic : Background Modular Arithmetic : Solutions Conclusion