A1: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 10 :: thesis: for b₁ being set holds
( not a := k c= b₁ or b₁ halts_on s )
A2: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not a := k c= P or P halts_on s )
assume A3: a := k c= P ; :: thesis: P halts_on s
IC s = IC (Start-At (0,SCM+FSA)) by A2, A1, GRFUNC_1:2
.= 0 ;
hence P halts_on s by Lm1, A3; :: thesis: verum