:: deftheorem Def1 defines with_non_trivial_Instructions AMISTD_4:def 1 :
for A being COM-Struct holds
( A is with_non_trivial_Instructions iff not the InstructionsF of A is trivial );