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 l, k being Element of NAT holds
( s halts_at l iff Comput (ProgramPart s),s,k halts_at l )
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 l, k being Element of NAT holds
( s halts_at l iff Comput (ProgramPart s),s,k halts_at l )
let s be State of S; :: thesis: for l, k being Element of NAT holds
( s halts_at l iff Comput (ProgramPart s),s,k halts_at l )
let l, k be Element of NAT ; :: thesis: ( s halts_at l iff Comput (ProgramPart s),s,k halts_at l )

hereby :: thesis: ( Comput (ProgramPart s),s,k halts_at l implies s halts_at l )

assume s halts_at l ; :: thesis: Comput (ProgramPart s),s,k halts_at l
then s . l = halt S by Def42;
then (Comput (ProgramPart s),s,k) . l = halt S by Th54;
hence Comput (ProgramPart s),s,k halts_at l by Def42; :: thesis: verum

end;

assume (Comput (ProgramPart s),s,k) . l = halt S ; :: according to AMI_1:def 42 :: thesis: s halts_at l
hence s . l = halt S by Th54; :: according to AMI_1:def 42 :: thesis: verum