let i be Instruction of SCM+FSA ; :: thesis: for k being Element of NAT holds UsedIntLoc i = UsedIntLoc (IncAddr i,k)
let k be Element of NAT ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)
A1: InsCode i <= 11 + 1 by SCMFSA_2:35;
A2: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
A3: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;

per cases ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A1, A2, A3, NAT_1:8, NAT_1:33;

suppose InsCode i = 0 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then i = halt SCM+FSA by SCMFSA_2:122;
hence UsedIntLoc i = UsedIntLoc (IncAddr i,k) by SCMFSA_4:8; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then consider a, b being Int-Location such that
A4: i = a := b by SCMFSA_2:54;
thus UsedIntLoc i = UsedIntLoc (IncAddr i,k) by A4, SCMFSA_4:9; :: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then consider a, b being Int-Location such that
A5: i = AddTo a,b by SCMFSA_2:55;
thus UsedIntLoc i = UsedIntLoc (IncAddr i,k) by A5, SCMFSA_4:10; :: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then consider a, b being Int-Location such that
A6: i = SubFrom a,b by SCMFSA_2:56;
thus UsedIntLoc i = UsedIntLoc (IncAddr i,k) by A6, SCMFSA_4:11; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then consider a, b being Int-Location such that
A7: i = MultBy a,b by SCMFSA_2:57;
thus UsedIntLoc i = UsedIntLoc (IncAddr i,k) by A7, SCMFSA_4:12; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then consider a, b being Int-Location such that
A8: i = Divide a,b by SCMFSA_2:58;
thus UsedIntLoc i = UsedIntLoc (IncAddr i,k) by A8, SCMFSA_4:13; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then consider l being Instruction-Location of SCM+FSA such that
A9: i = goto l by SCMFSA_2:59;
IncAddr i,k = goto (l + k) by A9, SCMFSA_4:14;
hence UsedIntLoc (IncAddr i,k) = {} by Th19
.= UsedIntLoc i by A9, Th19 ;
:: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then consider l being Instruction-Location of SCM+FSA , a being Int-Location such that
A10: i = a =0_goto l by SCMFSA_2:60;
IncAddr i,k = a =0_goto (l + k) by A10, SCMFSA_4:15;
hence UsedIntLoc (IncAddr i,k) = {a} by Th20
.= UsedIntLoc i by A10, Th20 ;
:: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then consider l being Instruction-Location of SCM+FSA , a being Int-Location such that
A11: i = a >0_goto l by SCMFSA_2:61;
IncAddr i,k = a >0_goto (l + k) by A11, SCMFSA_4:16;
hence UsedIntLoc (IncAddr i,k) = {a} by Th20
.= UsedIntLoc i by A11, Th20 ;
:: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then consider a, b being Int-Location , f being FinSeq-Location such that
A12: i = b := f,a by SCMFSA_2:62;
thus UsedIntLoc i = UsedIntLoc (IncAddr i,k) by A12, SCMFSA_4:17; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then consider a, b being Int-Location , f being FinSeq-Location such that
A13: i = f,a := b by SCMFSA_2:63;
thus UsedIntLoc i = UsedIntLoc (IncAddr i,k) by A13, SCMFSA_4:18; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then consider a being Int-Location , f being FinSeq-Location such that
A14: i = a :=len f by SCMFSA_2:64;
thus UsedIntLoc i = UsedIntLoc (IncAddr i,k) by A14, SCMFSA_4:19; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr i,k)

then consider a being Int-Location , f being FinSeq-Location such that
A15: i = f :=<0,...,0> a by SCMFSA_2:65;
thus UsedIntLoc i = UsedIntLoc (IncAddr i,k) by A15, SCMFSA_4:20; :: thesis: verum

end;

end;