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 Def7;
hence InsCode (AddTo (a,b)) = 2 ; :: thesis: verum