let k be Element of NAT ; :: thesis: for i being Instruction of SCM+FSA
for I being Instruction of SCM st i = I holds
IncAddr i,k = IncAddr I,k
let i be Instruction of SCM+FSA ; :: thesis: for I being Instruction of SCM st i = I holds
IncAddr i,k = IncAddr I,k
let I be Instruction of SCM ; :: thesis: ( i = I implies IncAddr i,k = IncAddr I,k )
assume A1: i = I ; :: thesis: IncAddr i,k = IncAddr I,k

per cases ( InsCode i in {6,7,8} or not InsCode i in {6,7,8} ) ;

suppose InsCode i in {6,7,8} ; :: thesis: IncAddr i,k = IncAddr I,k

then ex I being Instruction of SCM st
( I = i & IncAddr i,k = IncAddr I,k ) by Def3;
hence IncAddr i,k = IncAddr I,k by A1; :: thesis: verum

end;

suppose A2: not InsCode i in {6,7,8} ; :: thesis: IncAddr i,k = IncAddr I,k

then A3: ( InsCode I <> 6 & InsCode I <> 7 & InsCode I <> 8 ) by A1, ENUMSET1:def 1;
thus IncAddr i,k = i by A2, Def3
.= IncAddr I,k by A1, A3, RELOC:def 3 ; :: thesis: verum

end;

end;