How to construct proof for $\forall x,n.x\leq n \wedge n\geq 0 \wedge x \geq 0 \wedge n< L \wedge x< L \implies F_2(x,n)\geq0$

Question

I have following axioms

$F_1$ and $F_2$ are function representing integer values of a 2-dimensinal matrix$(L\times L)$.

$b$ is natural number function

$n,x,L \in N$(represent natural numbers )

$b(0)=0$

$\forall n.n\geq 0 \wedge n< L\wedge F_1(n,n)<0 \implies b(n+1)=b(n)$

$\forall n.n\geq 0 \wedge n< L \wedge F_1(n,n)\geq0 \implies b(n+1)=b(n)+1$

$\forall n.n\geq 0 \wedge n< L \wedge F_1(n,n)\geq0 \implies F_2(b(n),n)=F_1(n,n)$

Need to prove the following

$\forall x,n.x\leq n \wedge n\geq 0 \wedge x \geq 0 \wedge n< L \wedge x< L \implies F_2(x,n)\geq0$

Can anyone suggest how to construct the proof for above?

Answer 1

As it stands, you can't prove it. If you can show that $F_1(n,n) \ge 0$ then you can show (if you have induction) that $F_2(n,n)\ge 0$, but that still doesnot give you $F_2(x,n)$, and there is nothing that forces $F_1(n,n) \ge 0$. Indeed, if $F_1(n,n)<0$, then you can't show that $F_2(x,n)\ge 0$ either.