let k, loc be Nat; :: thesis: for a being Data-Location holds IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)
let a be Data-Location; :: thesis: IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)
A1: InsCode (IncAddr ((a =0_goto loc),k)) = InsCode (a =0_goto loc) by COMPOS_0:def 9
.= 7
.= InsCode (a =0_goto (loc + k)) ;
A2: AddressPart (IncAddr ((a =0_goto loc),k)) = AddressPart (a =0_goto loc) by COMPOS_0:def 9
.= <*a*>
.= AddressPart (a =0_goto (loc + k)) ;
A3: 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 A4: dom (JumpPart (IncAddr ((a =0_goto loc),k))) = dom (JumpPart (a =0_goto (loc + k))) by A1, COMPOS_0:def 5; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in proj1 (JumpPart (IncAddr ((a =0_goto loc),k))) or (JumpPart (IncAddr ((a =0_goto loc),k))) . b1 = (JumpPart (a =0_goto (loc + k))) . b1 )
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 A5: 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 A6: x = 1 by A5, A4, TARSKI:def 1;
thus (JumpPart (IncAddr ((a =0_goto loc),k))) . x = k + ((JumpPart (a =0_goto loc)) . x) by A3, A5, VALUED_1:def 2
.= loc + k by A6, FINSEQ_1:40
.= (JumpPart (a =0_goto (loc + k))) . x by A6, FINSEQ_1:40 ; :: thesis: verum
end;
hence IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k) by A1, A2, COMPOS_0:1; :: thesis: verum