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 & STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions )
A1: ( [1,0 ] in {[1,0 ],[0 ,0 ]} & [0 ,0 ] in {[1,0 ],[0 ,0 ]} ) by TARSKI:def 2;
( the Instructions of (STC N) = {[0 ,0 ],[1,0 ]} & [1,0 ] <> [0 ,0 ] ) by AMISTD_1:def 11, ZFMISC_1:33;
then not the Instructions of (STC N) is trivial by A1, YELLOW_8:def 1;
hence ( 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 & STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions ) by Def1; :: thesis: verum