Given: ∀x[Even(x) => ∃y[x = 2*y]], ∀x[∃z[x = 2*z+1] => Odd(x)] and Even(n)
Prove: Odd(n+1)
NOTE: we will use + and * as usual rather than Plus(a,b) and Times(a,b)


1:  Even(n)                     __________________________________________________________________


2:  ∀x[Even(x) => ∃y[x = 2*y]]  __________________________________________________________________


4:  Even(n) => ∃y[n = 2*y]      __________________________________________________________________


5:  ∃y[n = 2*y]                 __________________________________________________________________


6:  n = 2*k                     __________________________________________________________________


7:  n+1 = n+1                   __________________________________________________________________


8:  n+1 = 2*k+1                 __________________________________________________________________


9:  ∃z[n+1 = 2*z+1]             __________________________________________________________________


10: ∀x[∃z[x = 2*z+1] => Odd(x)] __________________________________________________________________


11: ∃z[n+1 = 2*z+1] => Odd(n+1) __________________________________________________________________


12: Odd(n+1)                    __________________________________________________________________