(**)(**)
theory Scratch = Main: