I think some of the commenters were confused by the notation $\Gamma \vdash A \downarrow B$, which I have only seen written as $\Gamma [ A ] \vdash B$ or $\Gamma \vdash A > B$. The latter is closest to the notation you were using. 

First, you're missing at least one necessary rule, and arguably you're missing three; I would write the full system of focused (a.k.a. uniform) proofs as follows:

$${A \in \Gamma \quad \Gamma \vdash A > P \over \Gamma \vdash P}{\it focus}
\qquad
{{} \over \Gamma \vdash P > P}{\it init}$$

$${\Gamma, A \vdash B \over \Gamma \vdash A \supset B}{{\supset}R}
\qquad
{\Gamma \vdash A \qquad \Gamma \vdash B > P \over \Gamma \vdash A \supset B > P}{{\supset}L}$$

$${\Gamma \vdash A(\alpha) \over \Gamma \vdash \forall x.A(x)}{{\forall}R^\alpha}
\qquad
{\Gamma \vdash A(t) > P \over \Gamma \vdash \forall x. A (x) > P}{{\forall}L}$$

... where $A$ and $B$ represent arbitrary propositions and $P$ represents an atomic proposition.

Assuming this fits with your understanding, then the proof you describe is simple: it is provable simply by case analysis and the observation that the rule $\it focus$ is the only rule that is applicable. Without the $\it focus$ rule, the caculus as you describe it cannot possibly be complete with respect to minimal first-order logic.

The original reference for what I think you're trying to do here is:

Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. *Uniform proofs as a foundation for logic programming*. Annals of Pure and Applied Logic, 51:125-157, 1991