let m, n be Element of NAT ; :: thesis: for i being Instruction of SCM+FSA holds IncAddr (IncAddr i,m),n = IncAddr i,(m + n)
let i be Instruction of SCM+FSA ; :: thesis: IncAddr (IncAddr i,m),n = IncAddr i,(m + n)

per cases ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or not InsCode i in {6,7,8} ) by ENUMSET1:def 1;

suppose InsCode i = 6 ; :: thesis: IncAddr (IncAddr i,m),n = IncAddr i,(m + n)

then consider l being Element of NAT such that
A1: i = goto l by SCMFSA_2:59;
IncAddr i,m = goto (l + m) by A1, Th14;
hence IncAddr (IncAddr i,m),n = goto ((l + m) + n) by Th14
.= goto (l + (m + n))
.= IncAddr i,(m + n) by A1, Th14 ;
:: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: IncAddr (IncAddr i,m),n = IncAddr i,(m + n)

then consider l being Element of NAT , a being Int-Location such that
A2: i = a =0_goto l by SCMFSA_2:60;
IncAddr i,m = a =0_goto (l + m) by A2, Th15;
hence IncAddr (IncAddr i,m),n = a =0_goto ((l + m) + n) by Th15
.= a =0_goto (l + (m + n))
.= IncAddr i,(m + n) by A2, Th15 ;
:: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: IncAddr (IncAddr i,m),n = IncAddr i,(m + n)

then consider l being Element of NAT , a being Int-Location such that
A3: i = a >0_goto l by SCMFSA_2:61;
IncAddr i,m = a >0_goto (l + m) by A3, Th16;
hence IncAddr (IncAddr i,m),n = a >0_goto ((l + m) + n) by Th16
.= a >0_goto (l + (m + n))
.= IncAddr i,(m + n) by A3, Th16 ;
:: thesis: verum

end;

suppose A4: not InsCode i in {6,7,8} ; :: thesis: IncAddr (IncAddr i,m),n = IncAddr i,(m + n)

then not InsCode (IncAddr i,m) in {6,7,8} by Th22;
then IncAddr (IncAddr i,m),n = IncAddr i,m by Def3
.= i by A4, Def3
.= IncAddr i,(m + n) by A4, Def3 ;
hence IncAddr (IncAddr i,m),n = IncAddr i,(m + n) ; :: thesis: verum

end;

end;