packagetype _plain
packagetype _code
primitive !return val -> void
primitive !plus val val -> val
primitive !minus val val -> val
primitive !jump lab -> void
primitive !modulo val val -> val
package main _plain
	typename K_number = int32
	typename K_phrase_number____nothing = function /main/K_number -> void
	package (K_phrase_number____nothing) MyRoutine _code
		local (/main/K_number) x
		local (/main/K_number) y
		code
			inv !return
				val x
			inv !return
				inv !plus
					val x
					val y
			inv !return
				inv !minus
					val x
					val y
			inv !jump
				lab .useful
			.useful
			inv !return
				inv !modulo
					val x
					val y