let P, Q be FinPartState of SCM+FSA ; :: thesis: for k being Element of NAT st P c= Q holds
ProgramPart (Relocated P,k) c= ProgramPart (Relocated Q,k)
let k be Element of NAT ; :: thesis: ( P c= Q implies ProgramPart (Relocated P,k) c= ProgramPart (Relocated Q,k) )
set rP = Relocated P,k;
set rQ = Relocated Q,k;
A1: dom (ProgramPart (Relocated P,k)) = dom (Reloc (ProgramPart P),k) by AMISTD_2:69
.= { (m + k) where m is Element of NAT : m in dom (ProgramPart P) } by AMISTD_2:70 ;
A2: dom (Shift (ProgramPart P),k) = { (m + k) where m is Element of NAT : m in dom (ProgramPart P) } by VALUED_1:def 12;
A3: dom (Shift (ProgramPart Q),k) = { (m + k) where m is Element of NAT : m in dom (ProgramPart Q) } by VALUED_1:def 12;
assume P c= Q ; :: thesis: ProgramPart (Relocated P,k) c= ProgramPart (Relocated Q,k)
then A4: ProgramPart P c= ProgramPart Q by RELAT_1:105;
then A5: Shift (ProgramPart P),k c= Shift (ProgramPart Q),k by VALUED_1:21;
A6: dom (ProgramPart P) c= dom (ProgramPart Q) by A4, GRFUNC_1:8;

A7: now

let x be set ; :: thesis: ( x in dom (ProgramPart (Relocated P,k)) implies (ProgramPart (Relocated P,k)) . x = (ProgramPart (Relocated Q,k)) . x )
assume x in dom (ProgramPart (Relocated P,k)) ; :: thesis: (ProgramPart (Relocated P,k)) . x = (ProgramPart (Relocated Q,k)) . x
then consider m1 being Element of NAT such that
A8: x = m1 + k and
A9: m1 in dom (ProgramPart P) by A1;
A10: m1 + k in dom (Shift (ProgramPart Q),k) by A6, A3, A9;
A11: m1 + k in dom (Shift (ProgramPart P),k) by A2, A9;
then A12: (Shift (ProgramPart P),k) /. (m1 + k) = (Shift (ProgramPart P),k) . (m1 + k) by PARTFUN1:def 8
.= (Shift (ProgramPart Q),k) . (m1 + k) by A5, A11, GRFUNC_1:8
.= (Shift (ProgramPart Q),k) /. (m1 + k) by A10, PARTFUN1:def 8 ;
thus (ProgramPart (Relocated P,k)) . x = (Reloc (ProgramPart P),k) . (m1 + k) by A8, AMISTD_2:69
.= IncAddr ((Shift (ProgramPart Q),k) /. (m1 + k)),k by A11, A12, AMISTD_2:def 15
.= (Reloc (ProgramPart Q),k) . (m1 + k) by A10, AMISTD_2:def 15
.= (ProgramPart (Relocated Q,k)) . x by A8, AMISTD_2:69 ; :: thesis: verum

end;

A13: ProgramPart (Relocated Q,k) = Reloc (ProgramPart Q),k by AMISTD_2:69;
A14: ProgramPart (Relocated P,k) = Reloc (ProgramPart P),k by AMISTD_2:69;
A15: dom (Shift (ProgramPart P),k) c= dom (Shift (ProgramPart Q),k) by A5, GRFUNC_1:8;

now

let x be set ; :: thesis: ( x in dom (ProgramPart (Relocated P,k)) implies x in dom (ProgramPart (Relocated Q,k)) )
assume x in dom (ProgramPart (Relocated P,k)) ; :: thesis: x in dom (ProgramPart (Relocated Q,k))
then x in dom (Shift (ProgramPart P),k) by A14, AMISTD_2:def 15;
then x in dom (Shift (ProgramPart Q),k) by A15;
hence x in dom (ProgramPart (Relocated Q,k)) by A13, AMISTD_2:def 15; :: thesis: verum

end;

then dom (ProgramPart (Relocated P,k)) c= dom (ProgramPart (Relocated Q,k)) by TARSKI:def 3;
hence ProgramPart (Relocated P,k) c= ProgramPart (Relocated Q,k) by A7, GRFUNC_1:8; :: thesis: verum