let k, loc be Nat; :: thesis: for a being Int-Location holds IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k)
let a be Int-Location; :: thesis: IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k)
A1: a >0_goto loc = [8,<*loc*>,<*a*>] by SCMFSA10:8;
A2: a >0_goto (loc + k) = [8,<*(loc + k)*>,<*a*>] by SCMFSA10:8;
A3: InsCode (IncAddr ((a >0_goto loc),k)) = InsCode (a >0_goto loc) by COMPOS_0:def 9
.= 8 by A1
.= InsCode (a >0_goto (loc + k)) by A2 ;
A4: AddressPart (IncAddr ((a >0_goto loc),k)) = AddressPart (a >0_goto loc) by COMPOS_0:def 9
.= <*a*> by A1
.= AddressPart (a >0_goto (loc + k)) by A2 ;
A5: JumpPart (IncAddr ((a >0_goto loc),k)) = k + (JumpPart (a >0_goto loc)) by COMPOS_0:def 9;
JumpPart (IncAddr ((a >0_goto loc),k)) = JumpPart (a >0_goto (loc + k))

proof

thus A6: dom (JumpPart (IncAddr ((a >0_goto loc),k))) = dom (JumpPart (a >0_goto (loc + k))) by A3, COMPOS_0:def 5; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in proj1 (JumpPart (IncAddr ((a >0_goto loc),k))) or (JumpPart (IncAddr ((a >0_goto loc),k))) . b₁ = (JumpPart (a >0_goto (loc + k))) . b₁ )
A7: JumpPart (a >0_goto loc) = <*loc*> by A1;
A8: JumpPart (a >0_goto (loc + k)) = <*(loc + k)*> by A2;
let x be object ; :: thesis: ( not x in proj1 (JumpPart (IncAddr ((a >0_goto loc),k))) or (JumpPart (IncAddr ((a >0_goto loc),k))) . x = (JumpPart (a >0_goto (loc + k))) . x )
assume A9: x in dom (JumpPart (IncAddr ((a >0_goto loc),k))) ; :: thesis: (JumpPart (IncAddr ((a >0_goto loc),k))) . x = (JumpPart (a >0_goto (loc + k))) . x
dom <*(loc + k)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A10: x = 1 by A9, A6, A8, TARSKI:def 1;
thus (JumpPart (IncAddr ((a >0_goto loc),k))) . x = k + ((JumpPart (a >0_goto loc)) . x) by A5, A9, VALUED_1:def 2
.= loc + k by A7, A10
.= (JumpPart (a >0_goto (loc + k))) . x by A8, A10 ; :: thesis: verum

end;

hence IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k) by A3, A4, COMPOS_0:1; :: thesis: verum