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_{1} being set holds

( not a := k c= b_{1} or b_{1} 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

let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 10 :: thesis: for b

( not a := k c= b

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