theorem Th12: :: SCMFSA_M:12
(Initialize ((intloc 0) .--> 1)) . (intloc 0) = 1