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