theorem :: AOFA_000:103

for S being non empty set
for T being Subset of S
for A being free ECIW-strict preIfWhileAlgebra
for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] holds
for s being Element of S
for I being Element of A st [s,I] in TerminatingPrograms (A,S,T,f1) holds
f1 . (s,I) = f2 . (s,I) by Lm3;