let i be Instruction of SCM+FSA; :: thesis: for k being Element of NAT holds UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))
let k be Element of NAT ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))
A1: InsCode i <= 12 by SCMFSA_2:16;

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, NAT_1:36;

suppose InsCode i = 0 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then i = halt SCM+FSA by SCMFSA_2:95;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_1:11; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then ex a, b being Int-Location st i = a := b by SCMFSA_2:30;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_1:11; :: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then ex a, b being Int-Location st i = AddTo (a,b) by SCMFSA_2:31;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_1:11; :: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then ex a, b being Int-Location st i = SubFrom (a,b) by SCMFSA_2:32;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_1:11; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then ex a, b being Int-Location st i = MultBy (a,b) by SCMFSA_2:33;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_1:11; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then ex a, b being Int-Location st i = Divide (a,b) by SCMFSA_2:34;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_1:11; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then consider l being Element of NAT such that
A4: i = goto l by SCMFSA_2:35;
IncAddr (i,k) = goto (l + k) by A4, SCMFSA_4:1;
hence UsedInt*Loc (IncAddr (i,k)) = {} by Th36
.= UsedInt*Loc i by A4, Th36 ;
:: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then consider l being Element of NAT , a being Int-Location such that
A5: i = a =0_goto l by SCMFSA_2:36;
IncAddr (i,k) = a =0_goto (l + k) by A5, SCMFSA_4:2;
hence UsedInt*Loc (IncAddr (i,k)) = {} by Th36
.= UsedInt*Loc i by A5, Th36 ;
:: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then consider l being Element of NAT , a being Int-Location such that
A6: i = a >0_goto l by SCMFSA_2:37;
IncAddr (i,k) = a >0_goto (l + k) by A6, SCMFSA_4:3;
hence UsedInt*Loc (IncAddr (i,k)) = {} by Th36
.= UsedInt*Loc i by A6, Th36 ;
:: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then ex a, b being Int-Location ex f being FinSeq-Location st i = b := (f,a) by SCMFSA_2:38;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_1:11; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b by SCMFSA_2:39;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_1:11; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then ex a being Int-Location ex f being FinSeq-Location st i = a :=len f by SCMFSA_2:40;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_1:11; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

then ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a by SCMFSA_2:41;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_1:11; :: thesis: verum

end;

end;