let a, b be Int-Location ; :: thesis: InsCode (AddTo a,b) = 2
ex A, B being Data-Location st
( a = A & b = B & AddTo a,b = AddTo A,B ) by Def12;
hence InsCode (AddTo a,b) = 2 by RECDEF_2:def 1; :: thesis: verum