let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for F being NAT -defined non empty lower FinPartState of holds il. T,0 in dom F
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for F being NAT -defined non empty lower FinPartState of holds il. T,0 in dom F
let F be NAT -defined non empty lower FinPartState of ; :: thesis: il. T,0 in dom F
consider l being set such that
A1: l in dom F by XBOOLE_0:def 1;
A2: dom F c= NAT by RELAT_1:def 18;
then reconsider l = l as Instruction-Location of T by A1, AMI_1:def 4;
consider f being IL-Function of NAT ,T such that
A3: f is bijective and
A4: for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) and
A5: il. T,0 = f . 0 by Def12;
rng f = NAT by A3, FUNCT_2:def 3;
then consider x being set such that
A6: x in dom f and
A7: l = f . x by A1, A2, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A6;
0 <= x by NAT_1:2;
then f . 0 <= f . x by A4;
hence il. T,0 in dom F by A1, A5, A7, Def20; :: thesis: verum