let k, m be natural number ; :: thesis: for S being standard-ins homogeneous regular J/A-independent COM-Struct
for I being Instruction of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))
let S be standard-ins homogeneous regular J/A-independent COM-Struct ; :: thesis: for I being Instruction of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))
let I be Instruction of S; :: thesis: IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))
A1: InsCode (IncAddr ((IncAddr (I,k)),m)) = InsCode (IncAddr (I,k)) by Def38
.= InsCode I by Def38
.= InsCode (IncAddr (I,(k + m))) by Def38 ;
A2: AddressPart (IncAddr ((IncAddr (I,k)),m)) = AddressPart (IncAddr (I,k)) by Def38
.= AddressPart I by Def38
.= AddressPart (IncAddr (I,(k + m))) by Def38 ;
A3: JumpPart (IncAddr ((IncAddr (I,k)),m)) = m + (JumpPart (IncAddr (I,k))) by Def38;
A4: JumpPart (IncAddr (I,k)) = k + (JumpPart I) by Def38;
A5: JumpPart (IncAddr (I,(k + m))) = (k + m) + (JumpPart I) by Def38;
then A6: dom (JumpPart (IncAddr (I,(k + m)))) = dom (JumpPart I) by VALUED_1:def 2
.= dom (JumpPart (IncAddr (I,k))) by A4, VALUED_1:def 2
.= dom (JumpPart (IncAddr ((IncAddr (I,k)),m))) by A3, VALUED_1:def 2 ;
for n being set st n in dom (JumpPart (IncAddr ((IncAddr (I,k)),m))) holds
(JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = (JumpPart (IncAddr (I,(k + m)))) . n

proof

let n be set ; :: thesis: ( n in dom (JumpPart (IncAddr ((IncAddr (I,k)),m))) implies (JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = (JumpPart (IncAddr (I,(k + m)))) . n )
assume A7: n in dom (JumpPart (IncAddr ((IncAddr (I,k)),m))) ; :: thesis: (JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = (JumpPart (IncAddr (I,(k + m)))) . n
then A8: n in dom (JumpPart (IncAddr (I,k))) by A3, VALUED_1:def 2;
then A9: n in dom (JumpPart I) by A4, VALUED_1:def 2;
A10: (JumpPart (IncAddr (I,k))) . n = k + ((JumpPart I) . n) by A4, A8, VALUED_1:def 2;
A11: (JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = m + ((JumpPart (IncAddr (I,k))) . n) by A7, A3, VALUED_1:def 2;
n in dom (JumpPart (IncAddr (I,(k + m)))) by A5, A9, VALUED_1:def 2;
then (JumpPart (IncAddr (I,(k + m)))) . n = (k + m) + ((JumpPart I) . n) by A5, VALUED_1:def 2;
hence (JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = (JumpPart (IncAddr (I,(k + m)))) . n by A11, A10; :: thesis: verum

end;

then JumpPart (IncAddr ((IncAddr (I,k)),m)) = JumpPart (IncAddr (I,(k + m))) by A6, FUNCT_1:2;
hence IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m)) by A1, A2, Th7; :: thesis: verum