:: deftheorem defines Result EXTPRO_1:def 13 :
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b₂ -valued non halt-free Function
for d being FinPartState of S st d is Autonomy of p holds
for b₅ being FinPartState of S holds
( b₅ = Result (p,d) iff for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
b₅ = (Result (P,s)) | (dom d) );