:: deftheorem Def1 defines Trivial-AMI EXTPRO_1:def 1 :
for N being with_zero set
for b₂ being strict AMI-Struct over N holds
( b₂ = Trivial-AMI N iff ( the carrier of b₂ = {0} & the ZeroF of b₂ = 0 & the InstructionsF of b₂ = {[0,{},{}]} & the Object-Kind of b₂ = 0 .--> 0 & the ValuesF of b₂ = N --> NAT & the Execution of b₂ = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) ) );