Prove:

(Proposition (conv of sum): l+) ,

under the assumptions:

(Definition (conv): l2:) ,

(Definition (sum of functions): ⊕:) ,

(Definition (product of functions): ⊕:) ,

(Proposition (distance of sum): |++|) ,

(Proposition (distance of product): |**|) ,

(Proposition (max): max:) ,

(Proposition (min): min:) .

For proving (), we replace the variables by arbitrary constants (, ) and we prove:

(1) .

For proving (), we assume:

(3) ,

(4) ,

and we prove:

(2) .

Using the definition (), we expand the goal () and the assumptions () and () into:

(5)

(6)

(7)

By the assumptions () and (), we can take appropriate constants (, ) such that:

(9)

(10)

For proving (), we have to find appropriate values such that:

(8) .

For proving (), we replace the universal variables by arbitrary constants (), we assume:

(11) ,

and we prove:

(12) .

For using the assumptions () and () we have to find appropriate values , , and we assume:

(13)

(14)

We prove first:

(15) .

For proving (), by (), it suffices to prove

(18) .

Using the substitution from step (), the goal () becomes:

(36) .

Pending proof of ().

Now we assume () and we continue with the proof of ().

From (), by the assumptions () and () we obtain:

(16)

(17)

By the assumptions () and (), we can take appropriate constants (, ) such that:

(20)

(21)

For proving (), we have to find appropriate values such that:

(19) .

For proving (), we replace the universal variables by arbitrary constants (), we assume:

(22) ,

and we prove:

(23) .

For using the assumptions () and () we have to find appropriate values , , and we assume:

(24)

(25)

We prove first:

(26) .

For proving (), by (), it suffices to prove

(29) .

Formula () is proved because it becomes an instance of () by taking: .

Now we assume () and we continue with the proof of ().

From (), by the assumptions () and () we obtain:

(27)

(28)

For proving (), by (), it suffices to prove

(30) .

Using the substitution from step (), the goal () becomes:

(32) .

Using (), the goal () is transformed into:

(35) .

Formula () is proved because it becomes an instance of () by taking: .

Additional Proof Generation Information

---

Converted by Mathematica      June 17, 2002