Agda developement of my BSc thesis "Formally verified derivation of an executable and terminating CEK machine from call-by-value λp̂-calculus"