tokens: This is indeed the semantics of termination used in several proof assistants ; in particular , in the Prototype Verification Systems ( PVS ) such ranking functions should be provided by the specifier , as part of each recursive definition , and the decreasingness requirements are implemented through the so - called termination Type Correctness Conditions ( termination TCCs , for short ) .