let a, b be Int-Location; :: thesis: a := b = [1,{},<*a,b*>]
ex A, B being Data-Location st
( a = A & b = B & a := b = A := B ) by SCMFSA_2:def 8;
hence a := b = [1,{},<*a,b*>] ; :: thesis: verum