let A be preIfWhileAlgebra; :: thesis: for I being Element of A st I in ElementaryInstructions A holds
I is absolutely-terminating
let I be Element of A; :: thesis: ( I in ElementaryInstructions A implies I is absolutely-terminating )
assume A1: I in ElementaryInstructions A ; :: thesis: I is absolutely-terminating
let S be non empty set ; :: according to AOFA_000:def 36 :: thesis: for s being Element of S
for T being Subset of S
for f being ExecutionFunction of A,S,T holds [s,I] in TerminatingPrograms (A,S,T,f)
thus for s being Element of S
for T being Subset of S
for f being ExecutionFunction of A,S,T holds [s,I] in TerminatingPrograms (A,S,T,f) by A1, Th94; :: thesis: verum