My next attempt :) Below, "PA" means Peano Arithmetic.

def A(): Enumerate proofs (in PA) by length if found a proof that "A()==a implies U()==u, and A()!=a implies U()<=u" then return a def U(): Enumerate proofs in PA+Consistent(PA) by length up to a very large N if found a proof that "A()==1" then return (A()==1 ? 5 : 0) if(A()==2) return 10 return 0

Proposition: A() returns 1 (if PA is consistent).
Proof:
Let X = "there exist a!=1 and u, such that: A()==a => U()==u and A()!=a => U()<=u".
Let S = "there exists u, such that: A()==1 => U()==u and A()!=1 => U()<u".
Let T = "A()==1".
Let ProvableU(P) = the provability formula of U (PA+Consistent(PA), with proofs of length < N).
Let ProvableA(P) = the provability formula of A (PA).
Let "U⊦ P" mean P is a theorem of U's proof system.
Then:

1. U⊦ ProvableU(T) => S // by inspection of U 2. U⊦ S => ~X // by definitions of X and S 3. U⊦ ProvableU(T) => ~X // from the previous two 4. U⊦ ~X => ~ProvableA(X) // by the axiom Consistent(PA) 5. U⊦ ProvableA(ProvableU(T) => S) // by A's inspection of U 6. U⊦ ProvableA(ProvableU(T)) => ProvableA(S) // from the previous 7. U⊦ ProvableU(T) => ProvableA(ProvableU(T))
// because PA is sufficient to model provability in any formal system 8. U⊦ ProvableU(T) => ProvableA(S) and ~ProvableA(X) // from 3, 4, 6, and 7 9. U⊦ ProvableA(S) and ~ProvableA(X) => T // by inspection of A 10. U⊦ ProvableU(T) => T // from the previous two 11. U⊦ T // by Loeb's theorem

QED