let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for p being FinPartState of S
for l being Element of NAT st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: for p being FinPartState of S
for l being Element of NAT st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l
let p be FinPartState of S; :: thesis: for l being Element of NAT st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l
let l be Element of NAT ; :: thesis: ( p starts_at l implies for s being State of S st p c= s holds
s starts_at l )
assume that
A1: IC S in dom p and
A2: IC p = l ; :: according to AMI_1:def 44 :: thesis: for s being State of S st p c= s holds
s starts_at l
let s be State of S; :: thesis: ( p c= s implies s starts_at l )
assume p c= s ; :: thesis: s starts_at l
hence IC s = p . (IC S) by A1, GRFUNC_1:8
.= l by A1, A2, Def43 ;
:: according to AMI_1:def 41 :: thesis: verum