Go backward to Example: Type CorrectnessGo up to TopGo forward to General Invariance Proofs |

- Prove
*T**and*[`A`]_{<x, y>}*=>**T'**T**and*`A`_{1}*=>**T'**T**and*`A`_{2}*=>**T'**T**and*(<*x*,*y*>' = <*x*,*y*>)*=>**T'*

- Prove
*T**and*`A`_{1}*=>**T'**T'**<=>*((*x*in**Nat**)*and*(*y*in**Nat**))'*<=>*(*x'*in**Nat**)*and*(*y'*in**Nat**)*T**and*`A`_{1}*=>**x'*in**Nat***T**and*`A`_{1}*=>**y'*in**Nat**

- Prove
*T**and*`A`_{1}*=>**x'*in**Nat***T**and*`A`_{1}*=>*(*x*in**Nat**)*and*(*x'*=*x+1*)*=>**x'*in**Nat**

*Proofs "mechanically" guided by the structure of formulas.*

Author: Wolfgang Schreiner

Last Modification: May 14, 1998