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

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

[Graphics:submitted.nbgr53.gif] [Graphics:submitted.nbgr54.gif].

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

We assume

[Graphics:submitted.nbgr56.gif] [Graphics:submitted.nbgr57.gif]

and show

[Graphics:submitted.nbgr58.gif] [Graphics:submitted.nbgr59.gif].

From [Graphics:submitted.nbgr60.gif] and [Graphics:submitted.nbgr61.gif] we obtain by modus ponens

[Graphics:submitted.nbgr62.gif] [Graphics:submitted.nbgr63.gif].

From [Graphics:submitted.nbgr64.gif] and [Graphics:submitted.nbgr65.gif] we obtain by modus ponens

[Graphics:submitted.nbgr66.gif] [Graphics:submitted.nbgr67.gif].

For proving [Graphics:submitted.nbgr68.gif], by [Graphics:submitted.nbgr69.gif], it suffices to prove

[Graphics:submitted.nbgr70.gif] [Graphics:submitted.nbgr71.gif].

We prove the individual conjunctive parts of [Graphics:submitted.nbgr95.gif]: