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 p being FinPartState of S
for l being Element of NAT 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 N; :: thesis: for s being State of S
for p being FinPartState of S
for l being Element of NAT 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 Element of NAT st p c= s & p halts_at l holds
s halts_at l
let p be FinPartState of S; :: thesis: for l being Element of NAT st p c= s & p halts_at l holds
s halts_at l
let l be Element of NAT ; :: 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