We prove [Graphics:submitted.nbgr114.gif] by natural deduction.

For proving [Graphics:submitted.nbgr115.gif] we prove, for arbitrary but fixed values,

[Graphics:submitted.nbgr116.gif] [Graphics:submitted.nbgr117.gif].

We prove [Graphics:submitted.nbgr118.gif] by the deduction rule.

We assume

[Graphics:submitted.nbgr119.gif] [Graphics:submitted.nbgr120.gif]

and show

[Graphics:submitted.nbgr121.gif] [Graphics:submitted.nbgr122.gif].

From [Graphics:submitted.nbgr123.gif] and [Graphics:submitted.nbgr124.gif] we obtain by modus ponens

[Graphics:submitted.nbgr125.gif] [Graphics:submitted.nbgr126.gif].

From [Graphics:submitted.nbgr127.gif] and [Graphics:submitted.nbgr128.gif] we obtain by modus ponens

[Graphics:submitted.nbgr129.gif] [Graphics:submitted.nbgr130.gif].

From [Graphics:submitted.nbgr131.gif] by specialization we obtain

[Graphics:submitted.nbgr132.gif] [Graphics:submitted.nbgr133.gif].

For proving [Graphics:submitted.nbgr134.gif], by [Graphics:submitted.nbgr135.gif], it suffices to prove

[Graphics:submitted.nbgr136.gif] [Graphics:submitted.nbgr137.gif].

For proving [Graphics:submitted.nbgr259.gif] we prove, for arbitrary but fixed values,