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 s . (IC (Comput (ProgramPart s),s,k)) = halt S holds
Result s = 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 s . (IC (Comput (ProgramPart s),s,k)) = halt S holds
Result s = Comput (ProgramPart s),s,k
let s be State of S; :: thesis: for k being Element of NAT st s . (IC (Comput (ProgramPart s),s,k)) = halt S holds
Result s = Comput (ProgramPart s),s,k
let k be Element of NAT ; :: thesis: ( s . (IC (Comput (ProgramPart s),s,k)) = halt S implies Result s = Comput (ProgramPart s),s,k )
IC (Comput (ProgramPart s),s,k) in NAT ;
then X: IC (Comput (ProgramPart s),s,k) in dom (ProgramPart s) by LmU;
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;
assume s . (IC (Comput (ProgramPart s),s,k)) = halt S ; :: thesis: Result s = Comput (ProgramPart s),s,k
then A1: CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt S by Th54, Y;
then (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = halt S by LmX;
then ProgramPart s halts_on s by Def20, X;
hence Result s = Comput (ProgramPart s),s,k by A1, Def22; :: thesis: verum