:: deftheorem Def7 defines STC AMISTD_1:def 7 :
for N being with_zero set
for b₂ being strict AMI-Struct over N holds
( b₂ = STC N iff ( the carrier of b₂ = {0} & IC = 0 & the InstructionsF of b₂ = {[0,0,0],[1,0,0]} & the Object-Kind of b₂ = 0 .--> 0 & the ValuesF of b₂ = N --> NAT & ex f being Function of (product (the_Values_of b₂)),(product (the_Values_of b₂)) st
( ( for s being Element of product (the_Values_of b₂) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of b₂ = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b₂)))) ) ) );