for N being with_zero set
for s being State of (Trivial-AMI N)
for i being Instruction of (Trivial-AMI N) holds Exec (i,s) = s