It is needed to prove an existing of such constant C that for any words $x$,$y$
$K(x,y) \le K(x) + K(y) + log(|x|+|y|) + C$
(K is Kolmogorov complexity)
I tried to prove it by using next true inequalities:
$K(x|l(x)) \le l(x) + c$
and
$K(x) \le K(x|l(x)) + 2log(l(x)) + c$
But theese inequalities are about Kolmogorov complexity for one word and I do not know how to expand them for a case of two words (like in inequality that I must prove). Could you help me please? Thank you in advance.
In fact a stronger statement can be proven:
Since $x$ and $y$ are given, two programs $P_x$ and $P_y$ exist with Kolmogorov complexity $K(x)$ and $K(y)$ to print $x$ and $y$ respectively. We can write another program $P$ without halting the Turing machine as following:
$$P_x \\ P_y$$
This program of length $K(x) + K(y) + C$ prints $x$ and $y$. Hence, in the worst case
$$K(x, y) = K(x) + K(y) + C$$
And in case if you can find a shorter program than $P$ after combining $x$ and $y$, its Kolmogorov complexity will be lesser than above mentioned result. Which means,
$$K(x, y) \le K(x) + K(y) + C$$
Let's fix optimal decompressor $D$. Let $p$, $q$ be the shortest programs to print $x$ and $y$ (in other words $D(p)=x, D(q)=y, K(x)=|p|, K(y)=|q|$).
Let $K(x)+K(y)=n$. Let $\tilde{s}$ be a word $s$ with possibly added zeroes before it, so $|\tilde{s}|=\log n$. Let $E$ also be a decompressor (probably not optimal). Let it work that way: it gets a string $\widetilde{|p|}pq$. It computes its length (it's $\log n+n$), then computes $n$ (for known $k$ there is only $n$ where $n+\log n =k$). Using $\log n$, decompressor can separate $\widetilde{|p|}$ from the input string and get length of $p$. Using $|p|$ decompressor separates $p$ from $pq$. Then decompressor calls $D$ on $p$ and $q$ and prints $x$ and $y$.
The decompressor $E$ is not optimal yet it can be used for description of all words. It means that $K(x,y)\leq|\widetilde{|p|}pq|+c$. So we can finish the proof: $$K(x,y)\leq|\widetilde{|p|}pq|+c\leq\log n + n + c=\log (K(x)+K(y))+K(x)+K(y)+c$$
