let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for F being FinPartState of S
for k being natural number st k > 0 holds
not il. S,0 in dom (Shift F,k)
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for F being FinPartState of S
for k being natural number st k > 0 holds
not il. S,0 in dom (Shift F,k)
let F be FinPartState of S; :: thesis: for k being natural number st k > 0 holds
not il. S,0 in dom (Shift F,k)
let k be natural number ; :: thesis: ( k > 0 implies not il. S,0 in dom (Shift F,k) )
assume that
A1: k > 0 and
A2: il. S,0 in dom (Shift F,k) ; :: thesis: contradiction
dom (Shift F,k) = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom F } by Def16;
then ex m being Element of NAT st
( il. S,0 = il. S,(m + k) & il. S,m in dom F ) by A2;
hence contradiction by A1, AMISTD_1:25; :: thesis: verum