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, Th14; :: thesis: verum