let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for g being FinPartState of S
for k being Element of NAT st IC S in dom g holds
Start-At ((IC g) + k),S c= Relocated g,k
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N; :: thesis: for g being FinPartState of S
for k being Element of NAT st IC S in dom g holds
Start-At ((IC g) + k),S c= Relocated g,k
let g be FinPartState of S; :: thesis: for k being Element of NAT st IC S in dom g holds
Start-At ((IC g) + k),S c= Relocated g,k
let k be Element of NAT ; :: thesis: ( IC S in dom g implies Start-At ((IC g) + k),S c= Relocated g,k )
assume Z: IC S in dom g ; :: thesis: Start-At ((IC g) + k),S c= Relocated g,k
A1: Start-At ((IC g) + k),S = {[(IC S),((IC g) + k)]} by FUNCT_4:87;
A2: IC (Relocated g,k) = (IC g) + k by Z, Th73;
A3: IC S in dom (Relocated g,k) by Th72;
A4: [(IC S),((IC g) + k)] in Relocated g,k by A3, A2, FUNCT_1:def 4;
thus Start-At ((IC g) + k),S c= Relocated g,k :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Start-At ((IC g) + k),S or x in Relocated g,k )
assume x in Start-At ((IC g) + k),S ; :: thesis: x in Relocated g,k
hence x in Relocated g,k by A1, A4, TARSKI:def 1; :: thesis: verum

end;