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 p being FinPartState of S
for l being Instruction-Location of S st p c= s & p halts_at l holds
s 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 p being FinPartState of S
for l being Instruction-Location of S st p c= s & p halts_at l holds
s 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 p being FinPartState of S
for l being Instruction-Location of S st p c= s & p halts_at l holds
s halts_at l
let s be State of S; :: thesis: for p being FinPartState of S
for l being Instruction-Location of S st p c= s & p halts_at l holds
s halts_at l
let p be FinPartState of S; :: thesis: for l being Instruction-Location of S st p c= s & p halts_at l holds
s halts_at l
let l be Instruction-Location of S; :: thesis: ( p c= s & p halts_at l implies s halts_at l )
assume A1: p c= s ; :: thesis: ( not p halts_at l or s halts_at l )
assume ( l in dom p & p . l = halt S ) ; :: according to AMI_1:def 45 :: thesis: s halts_at l
hence s . l = halt S by A1, GRFUNC_1:8; :: according to AMI_1:def 42 :: thesis: verum