let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed parahalting MacroInstruction of SCM+FSA st WithVariantWhile>0 a,I,s,p holds
while>0 (a,I) is_halting_on s,p
let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being really-closed parahalting MacroInstruction of SCM+FSA st WithVariantWhile>0 a,I,s,p holds
while>0 (a,I) is_halting_on s,p
let a be read-write Int-Location; :: thesis: for I being really-closed parahalting MacroInstruction of SCM+FSA st WithVariantWhile>0 a,I,s,p holds
while>0 (a,I) is_halting_on s,p
let I be really-closed parahalting MacroInstruction of SCM+FSA ; :: thesis: ( WithVariantWhile>0 a,I,s,p implies while>0 (a,I) is_halting_on s,p )
assume A1: WithVariantWhile>0 a,I,s,p ; :: thesis: while>0 (a,I) is_halting_on s,p
ProperBodyWhile>0 a,I,s,p by SCMFSA7B:19;
hence while>0 (a,I) is_halting_on s,p by A1, Th27; :: thesis: verum