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

[Graphics:submitted.nbgr170.gif] [Graphics:submitted.nbgr171.gif].

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

We assume

[Graphics:submitted.nbgr173.gif] [Graphics:submitted.nbgr174.gif]

and show

[Graphics:submitted.nbgr175.gif] [Graphics:submitted.nbgr176.gif].

From [Graphics:submitted.nbgr177.gif] and [Graphics:submitted.nbgr178.gif] we obtain by modus ponens

[Graphics:submitted.nbgr179.gif] [Graphics:submitted.nbgr180.gif].

From [Graphics:submitted.nbgr181.gif] and [Graphics:submitted.nbgr182.gif] we obtain by modus ponens

[Graphics:submitted.nbgr183.gif] [Graphics:submitted.nbgr184.gif].

From [Graphics:submitted.nbgr185.gif] and [Graphics:submitted.nbgr186.gif] we obtain by modus ponens

[Graphics:submitted.nbgr187.gif] [Graphics:submitted.nbgr188.gif].

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

[Graphics:submitted.nbgr190.gif] [Graphics:submitted.nbgr191.gif].

Formula [Graphics:submitted.nbgr192.gif] is simplified to

[Graphics:submitted.nbgr193.gif] [Graphics:submitted.nbgr194.gif].

For proving [Graphics:submitted.nbgr195.gif], by [Graphics:submitted.nbgr196.gif], it suffices to prove

[Graphics:submitted.nbgr197.gif] [Graphics:submitted.nbgr198.gif].

For proving [Graphics:submitted.nbgr254.gif], by [Graphics:submitted.nbgr255.gif], it suffices to prove