let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for I being Element of the Instructions of S holds IncAddr I,0 = I
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N; :: thesis: for I being Element of the Instructions of S holds IncAddr I,0 = I
let I be Element of the Instructions of S; :: thesis: IncAddr I,0 = I
A1: InsCode (IncAddr I,0 ) = InsCode I by Def14;
A2: dom (AddressPart I) = dom (AddressPart (IncAddr I,0 )) by Def14;
for k being Nat st k in dom (AddressPart I) holds
(AddressPart (IncAddr I,0 )) . k = (AddressPart I) . k

proof

let k be Nat; :: thesis: ( k in dom (AddressPart I) implies (AddressPart (IncAddr I,0 )) . k = (AddressPart I) . k )
assume A3: k in dom (AddressPart I) ; :: thesis: (AddressPart (IncAddr I,0 )) . k = (AddressPart I) . k

per cases ( (product" (AddressParts (InsCode I))) . k = NAT or (product" (AddressParts (InsCode I))) . k <> NAT ) ;

suppose (product" (AddressParts (InsCode I))) . k = NAT ; :: thesis: (AddressPart (IncAddr I,0 )) . k = (AddressPart I) . k

then ex f being Instruction-Location of S st
( f = (AddressPart I) . k & (AddressPart (IncAddr I,0 )) . k = il. S,(0 + (locnum f)) ) by A3, Def14;
hence (AddressPart (IncAddr I,0 )) . k = (AddressPart I) . k by AMISTD_1:def 13; :: thesis: verum

end;

suppose (product" (AddressParts (InsCode I))) . k <> NAT ; :: thesis: (AddressPart (IncAddr I,0 )) . k = (AddressPart I) . k

hence (AddressPart (IncAddr I,0 )) . k = (AddressPart I) . k by A3, Def14; :: thesis: verum

end;

end;

end;

hence IncAddr I,0 = I by A1, Th16, A2, FINSEQ_1:17; :: thesis: verum