theorem Th12: :: SCMFSA_M:12

(Initialize ((intloc 0) .--> 1)) . (intloc 0) = 1