I bevis for riktigheten angitt en betegnelse som angir at et program produksjon påstander følger logisk fra input påstander og trinnene i behandlingen, og, i tillegg programmet avsluttes under alle input forhold.