Initialized (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))) is halting by Lm6, SCM_HALT:76;
hence Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))))) is InitHalting good Program of SCM+FSA by SCM_HALT:def 2; :: thesis: verum