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
for s being State of S st (IC S),loc --> l,h c= s holds
CurInstr s = halt S
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
for s being State of S st (IC S),loc --> l,h c= s holds
CurInstr s = halt S
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
for s being State of S st (IC S),loc --> l,h c= s holds
CurInstr s = halt S
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
for s being State of S st (IC S),loc --> l,h c= s holds
CurInstr s = halt S
let l be Element of ObjectKind (IC S); :: thesis: ( l = loc implies for h being Element of ObjectKind loc st h = halt S holds
for s being State of S st (IC S),loc --> l,h c= s holds
CurInstr s = halt S )
assume A1: l = loc ; :: thesis: for h being Element of ObjectKind loc st h = halt S holds
for s being State of S st (IC S),loc --> l,h c= s holds
CurInstr s = halt S
let h be Element of ObjectKind loc; :: thesis: ( h = halt S implies for s being State of S st (IC S),loc --> l,h c= s holds
CurInstr s = halt S )
assume A2: h = halt S ; :: thesis: for s being State of S st (IC S),loc --> l,h c= s holds
CurInstr s = halt S
let s be State of S; :: thesis: ( (IC S),loc --> l,h c= s implies CurInstr s = halt S )
assume A3: (IC S),loc --> l,h c= s ; :: thesis: CurInstr s = halt S
loc in IL by Def4;
then A4: IC S <> loc by Def21;
dom ((IC S),loc --> l,h) = {(IC S),loc} by FUNCT_4:65;
then A5: ( IC S in dom ((IC S),loc --> l,h) & loc in dom ((IC S),loc --> l,h) ) by TARSKI:def 2;
then A6: ((IC S),loc --> l,h) . (IC S) in dom ((IC S),loc --> l,h) by A1, A4, FUNCT_4:66;
thus CurInstr s = s . (((IC S),loc --> l,h) . (IC S)) by A3, A5, GRFUNC_1:8
.= ((IC S),loc --> l,h) . (((IC S),loc --> l,h) . (IC S)) by A3, A6, GRFUNC_1:8
.= ((IC S),loc --> l,h) . loc by A1, A4, FUNCT_4:66
.= halt S by A2, FUNCT_4:66 ; :: thesis: verum