let A be preIfWhileAlgebra; :: thesis: for I being Element of A
for S being non empty set
for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T st I in ElementaryInstructions A holds
[s,I] in TerminatingPrograms A,S,T,f
let I be Element of A; :: thesis: for S being non empty set
for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T st I in ElementaryInstructions A holds
[s,I] in TerminatingPrograms A,S,T,f
let S be non empty set ; :: thesis: for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T st I in ElementaryInstructions A holds
[s,I] in TerminatingPrograms A,S,T,f
let T be Subset of S; :: thesis: for s being Element of S
for f being ExecutionFunction of A,S,T st I in ElementaryInstructions A holds
[s,I] in TerminatingPrograms A,S,T,f
let s be Element of S; :: thesis: for f being ExecutionFunction of A,S,T st I in ElementaryInstructions A holds
[s,I] in TerminatingPrograms A,S,T,f
let f be ExecutionFunction of A,S,T; :: thesis: ( I in ElementaryInstructions A implies [s,I] in TerminatingPrograms A,S,T,f )
assume I in ElementaryInstructions A ; :: thesis: [s,I] in TerminatingPrograms A,S,T,f
then ( [s,I] in [:S,(ElementaryInstructions A):] & [:S,(ElementaryInstructions A):] c= TerminatingPrograms A,S,T,f ) by Def35, ZFMISC_1:106;
hence [s,I] in TerminatingPrograms A,S,T,f ; :: thesis: verum