let N be with_zero set ; for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for i being Element of the InstructionsF of T holds (il. (T,0)) .--> i is lower
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; for i being Element of the InstructionsF of T holds (il. (T,0)) .--> i is lower
let i be Element of the InstructionsF of T; (il. (T,0)) .--> i is lower
set F = (il. (T,0)) .--> i;
let l be Element of NAT ; AMI_WSTD:def 10 ( l in dom ((il. (T,0)) .--> i) implies for m being Element of NAT st m <= l,T holds
m in dom ((il. (T,0)) .--> i) )
assume A1:
l in dom ((il. (T,0)) .--> i)
; for m being Element of NAT st m <= l,T holds
m in dom ((il. (T,0)) .--> i)
let m be Element of NAT ; ( m <= l,T implies m in dom ((il. (T,0)) .--> i) )
assume A2:
m <= l,T
; m in dom ((il. (T,0)) .--> i)
consider k being Nat such that
A3:
m = il. (T,k)
by Th6;
A4:
l = il. (T,0)
by A1, TARSKI:def 1;
then
( 0 <= k & k <= 0 )
by A2, A3, Th8;
hence
m in dom ((il. (T,0)) .--> i)
by A1, A4, A3, XXREAL_0:1; verum