let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for k being Element of NAT st ProgramPart s halts_on s holds
( Result s = Comput (ProgramPart s),s,k iff s halts_at IC (Comput (ProgramPart s),s,k) )
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of N; :: thesis: for s being State of S
for k being Element of NAT st ProgramPart s halts_on s holds
( Result s = Comput (ProgramPart s),s,k iff s halts_at IC (Comput (ProgramPart s),s,k) )
let s be State of S; :: thesis: for k being Element of NAT st ProgramPart s halts_on s holds
( Result s = Comput (ProgramPart s),s,k iff s halts_at IC (Comput (ProgramPart s),s,k) )
let k be Element of NAT ; :: thesis: ( ProgramPart s halts_on s implies ( Result s = Comput (ProgramPart s),s,k iff s halts_at IC (Comput (ProgramPart s),s,k) ) )
assume A1: ProgramPart s halts_on s ; :: thesis: ( Result s = Comput (ProgramPart s),s,k iff s halts_at IC (Comput (ProgramPart s),s,k) )
Y: (ProgramPart (Comput (ProgramPart s),s,k)) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by BWL1;

hereby :: thesis: ( s halts_at IC (Comput (ProgramPart s),s,k) implies Result s = Comput (ProgramPart s),s,k )

assume Result s = Comput (ProgramPart s),s,k ; :: thesis: s halts_at IC (Comput (ProgramPart s),s,k)
then ex i being Element of NAT st
( Comput (ProgramPart s),s,k = Comput (ProgramPart s),s,i & CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt S ) by A1, Def22;
then s . (IC (Comput (ProgramPart s),s,k)) = halt S by Th54, Y;
hence s halts_at IC (Comput (ProgramPart s),s,k) by Def42; :: thesis: verum

end;

assume s . (IC (Comput (ProgramPart s),s,k)) = halt S ; :: according to AMI_1:def 42 :: thesis: Result s = Comput (ProgramPart s),s,k
then CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt S by Th54, Y;
hence Result s = Comput (ProgramPart s),s,k by A1, Def22; :: thesis: verum