:: deftheorem Def2 defines ExecTree AMISTD_3:def 2 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for M being non empty preProgram of S
for b₄ being DecoratedTree of NAT holds
( b₄ = ExecTree M iff ( b₄ . {} = FirstLoc M & ( for t being Element of dom b₄ holds
( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (b₄ . t)),(b₄ . t))) } & ( for m being Nat st m in card (NIC ((M /. (b₄ . t)),(b₄ . t))) holds
b₄ . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b₄ . t)),(b₄ . t))),S)) . m ) ) ) ) );