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 definite realistic AMI-Struct of IL,N
for loc being Instruction-Location of S
for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is halting
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of IL,N
for loc being Instruction-Location of S
for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is halting
let S be non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of IL,N; :: thesis: for loc being Instruction-Location of S
for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is halting
let loc be Instruction-Location of S; :: thesis: for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is halting
let l be Element of ObjectKind (IC S); :: thesis: ( l = loc implies for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is halting )
assume A1: l = loc ; :: thesis: for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is halting
let h be Element of ObjectKind loc; :: thesis: ( h = halt S implies (IC S),loc --> l,h is halting )
assume A2: h = halt S ; :: thesis: (IC S),loc --> l,h is halting
thus (IC S),loc --> l,h is halting :: thesis: verum

proof

let s be State of S; :: according to AMI_1:def 26 :: thesis: ( (IC S),loc --> l,h c= s implies s is halting )
assume A3: (IC S),loc --> l,h c= s ; :: thesis: s is halting
take 0 ; :: according to AMI_1:def 20 :: thesis: CurInstr (Computation s,0 ) = halt S
thus CurInstr (Computation s,0 ) = CurInstr s by Tx0
.= halt S by A1, A2, A3, Th64 ; :: thesis: verum

end;