take STC N ; :: thesis: ( STC N is standard & STC N is regular & STC N is J/A-independent & STC N is homogeneous & STC N is halting & STC N is with_explicit_jumps )
thus ( STC N is standard & STC N is regular & STC N is J/A-independent & STC N is homogeneous & STC N is halting & STC N is with_explicit_jumps ) ; :: thesis: verum