take STC N ; :: thesis: ( STC N is halting & STC N is realistic & STC N is steady-programmed & STC N is with_explicit_jumps & STC N is without_implicit_jumps & STC N is IC-good & STC N is Exec-preserving )
thus ( STC N is halting & STC N is realistic & STC N is steady-programmed & STC N is with_explicit_jumps & STC N is without_implicit_jumps & STC N is IC-good & STC N is Exec-preserving ) ; :: thesis: verum