take STC N ; :: thesis: ( STC N is halting & STC N is realistic & STC N is steady-programmed & STC N is programmable & 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 )
STC N is with_non_trivial_Instructions

proof

A1: the Instructions of (STC N) = {[0 ,0 ],[1,0 ]} by AMISTD_1:def 11;
A2: [1,0 ] <> [0 ,0 ] by ZFMISC_1:33;
( [1,0 ] in {[1,0 ],[0 ,0 ]} & [0 ,0 ] in {[1,0 ],[0 ,0 ]} ) by TARSKI:def 2;
hence not the Instructions of (STC N) is trivial by A1, A2, YELLOW_8:def 1; :: according to AMI_7:def 1 :: thesis: verum

end;

hence ( STC N is halting & STC N is realistic & STC N is steady-programmed & STC N is programmable & 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 ) ; :: thesis: verum