Go backward to Example: Type Correctness Go up to Top Go forward to General Invariance Proofs

Proof

• Prove T and [A]_{<x, y>} => T'
  • T and A₁ => T'
  • T and A₂ => T'
  • T and (<x, y >' = <x, y >) => T'
• Prove T and A₁ => T'
  • T' <=> ((x in Nat) and (y in Nat))'
    <=>(x' in Nat) and (y' in Nat)
  • T and A₁ => x' in Nat T and A₁ => y' in Nat
• Prove T and A₁ => x' in Nat
  • T and A₁
    => (x in Nat) and (x' = x+1)
    => x' in Nat

Proofs "mechanically" guided by the structure of formulas.