let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for s being State of S
for l being Instruction-Location of S
for k being Element of NAT holds
( s halts_at l iff Computation s,k halts_at l )
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for s being State of S
for l being Instruction-Location of S
for k being Element of NAT holds
( s halts_at l iff Computation s,k halts_at l )
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of IL,N; :: thesis: for s being State of S
for l being Instruction-Location of S
for k being Element of NAT holds
( s halts_at l iff Computation s,k halts_at l )
let s be State of S; :: thesis: for l being Instruction-Location of S
for k being Element of NAT holds
( s halts_at l iff Computation s,k halts_at l )
let l be Instruction-Location of S; :: thesis: for k being Element of NAT holds
( s halts_at l iff Computation s,k halts_at l )
let k be Element of NAT ; :: thesis: ( s halts_at l iff Computation s,k halts_at l )

hereby :: thesis: ( Computation s,k halts_at l implies s halts_at l )

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

end;

assume (Computation 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